equal
deleted
inserted
replaced
1 (* -*- coding: utf-8 -*- :encoding=utf-8: |
1 (* -*- coding: utf-8 -*- :encoding=utf-8: |
2 ID: $Id$ |
|
3 Author: Makarius |
2 Author: Makarius |
4 |
3 |
5 Example theory involving Unicode characters (UTF-8 encoding) -- both |
4 Example theory involving Unicode characters (UTF-8 encoding) -- both |
6 formal and informal ones. |
5 formal and informal ones. |
7 *) |
6 *) |
41 thm alef_bet.induct |
40 thm alef_bet.induct |
42 |
41 |
43 |
42 |
44 text {* Interpreting Hebrew letters as numbers. *} |
43 text {* Interpreting Hebrew letters as numbers. *} |
45 |
44 |
46 consts |
45 primrec mispar :: "alef_bet => nat" where |
47 mispar :: "alef_bet => nat" |
|
48 primrec |
|
49 "mispar א = 1" |
46 "mispar א = 1" |
50 "mispar ב = 2" |
47 | "mispar ב = 2" |
51 "mispar ג = 3" |
48 | "mispar ג = 3" |
52 "mispar ד = 4" |
49 | "mispar ד = 4" |
53 "mispar ה = 5" |
50 | "mispar ה = 5" |
54 "mispar ו = 6" |
51 | "mispar ו = 6" |
55 "mispar ז = 7" |
52 | "mispar ז = 7" |
56 "mispar ח = 8" |
53 | "mispar ח = 8" |
57 "mispar ט = 9" |
54 | "mispar ט = 9" |
58 "mispar י = 10" |
55 | "mispar י = 10" |
59 "mispar כ = 20" |
56 | "mispar כ = 20" |
60 "mispar ל = 30" |
57 | "mispar ל = 30" |
61 "mispar מ = 40" |
58 | "mispar מ = 40" |
62 "mispar נ = 50" |
59 | "mispar נ = 50" |
63 "mispar ס = 60" |
60 | "mispar ס = 60" |
64 "mispar ע = 70" |
61 | "mispar ע = 70" |
65 "mispar פ = 80" |
62 | "mispar פ = 80" |
66 "mispar צ = 90" |
63 | "mispar צ = 90" |
67 "mispar ק = 100" |
64 | "mispar ק = 100" |
68 "mispar ר = 200" |
65 | "mispar ר = 200" |
69 "mispar ש = 300" |
66 | "mispar ש = 300" |
70 "mispar ת = 400" |
67 | "mispar ת = 400" |
71 |
68 |
72 thm mispar.simps |
69 thm mispar.simps |
73 |
70 |
74 lemma "mispar ק + mispar ל + mispar ה = 135" |
71 lemma "mispar ק + mispar ל + mispar ה = 135" |
75 by simp |
72 by simp |