blob: 0305091b32974022014874f81d5467a3a6c77bb6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
(* -*- coding: utf-8 -*- *)
(*
Example theory involving unicode characters (utf-8 encoding) -- both
formal and informal ones.
*)
theory Unicode
imports Main
begin
text {* The Hebrew Alef-Bet (א-ב). *}
datatype alef_bet =
Alef ("א")
| Bet ("ב")
| Gimel ("ג")
| Dalet ("ד")
| He ("ה")
| Vav ("ו")
| Zayin ("ז")
| Het ("ח")
| Tet ("ט")
| Yod ("י")
| Kaf ("כ")
| Lamed ("ל")
| Mem ("מ")
| Nun ("נ")
| Samekh ("ס")
| Ayin ("ע")
| Pe ("פ")
| Tsadi ("צ")
| Qof ("ק")
| Resh ("ר")
| Shin ("ש")
| Tav ("ת")
thm alef_bet.induct
text {* Interpreting Hebrew letters as numbers. *}
consts
mispar :: "alef_bet => nat"
primrec
"mispar א = 1"
"mispar ב = 2"
"mispar ג = 3"
"mispar ד = 4"
"mispar ה = 5"
"mispar ו = 6"
"mispar ז = 7"
"mispar ח = 8"
"mispar ט = 9"
"mispar י = 10"
"mispar כ = 20"
"mispar ל = 30"
"mispar מ = 40"
"mispar נ = 50"
"mispar ס = 60"
"mispar ע = 70"
"mispar פ = 80"
"mispar צ = 90"
"mispar ק = 100"
"mispar ר = 200"
"mispar ש = 300"
"mispar ת = 400"
thm mispar.simps
lemma "mispar ק + mispar ל + mispar ה = 135"
by simp
end
|
