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