src/HOL/ex/Hebrew.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 59031 4c3bb56b8ce7
child 62809 4b8f08de2792
permissions -rw-r--r--
prefer symbols;
wenzelm@40967
     1
(*  Author:     Makarius
wenzelm@17414
     2
wenzelm@17414
     3
Example theory involving Unicode characters (UTF-8 encoding) -- both
wenzelm@17414
     4
formal and informal ones.
wenzelm@17414
     5
*)
wenzelm@17414
     6
wenzelm@59031
     7
section \<open>A Hebrew theory\<close>
wenzelm@17506
     8
wenzelm@17414
     9
theory Hebrew
wenzelm@17414
    10
imports Main
wenzelm@17414
    11
begin
wenzelm@17414
    12
wenzelm@59031
    13
text \<open>The Hebrew Alef-Bet (א-ב).\<close>
wenzelm@17414
    14
blanchet@58310
    15
datatype alef_bet =
wenzelm@17414
    16
    Alef    ("א")
wenzelm@17414
    17
  | Bet     ("ב")
wenzelm@17414
    18
  | Gimel   ("ג")
wenzelm@17414
    19
  | Dalet   ("ד")
wenzelm@17414
    20
  | He      ("ה")
wenzelm@17414
    21
  | Vav     ("ו")
wenzelm@17414
    22
  | Zayin   ("ז")
wenzelm@17414
    23
  | Het     ("ח")
wenzelm@17414
    24
  | Tet     ("ט")
wenzelm@17414
    25
  | Yod     ("י")
wenzelm@17414
    26
  | Kaf     ("כ")
wenzelm@17414
    27
  | Lamed   ("ל")
wenzelm@17414
    28
  | Mem     ("מ")
wenzelm@17414
    29
  | Nun     ("נ")
wenzelm@17414
    30
  | Samekh  ("ס")
wenzelm@17414
    31
  | Ayin    ("ע")
wenzelm@17414
    32
  | Pe      ("פ")
wenzelm@17414
    33
  | Tsadi   ("צ")
wenzelm@17414
    34
  | Qof     ("ק")
wenzelm@17414
    35
  | Resh    ("ר")
wenzelm@17414
    36
  | Shin    ("ש")
wenzelm@17414
    37
  | Tav     ("ת")
wenzelm@17414
    38
wenzelm@17414
    39
thm alef_bet.induct
wenzelm@17414
    40
wenzelm@17414
    41
wenzelm@59031
    42
text \<open>Interpreting Hebrew letters as numbers.\<close>
wenzelm@17414
    43
wenzelm@59031
    44
primrec mispar :: "alef_bet => nat"
wenzelm@59031
    45
where
wenzelm@17414
    46
  "mispar א = 1"
haftmann@39246
    47
| "mispar ב = 2"
haftmann@39246
    48
| "mispar ג = 3"
haftmann@39246
    49
| "mispar ד = 4"
haftmann@39246
    50
| "mispar ה = 5"
haftmann@39246
    51
| "mispar ו = 6"
haftmann@39246
    52
| "mispar ז = 7"
haftmann@39246
    53
| "mispar ח = 8"
haftmann@39246
    54
| "mispar ט = 9"
haftmann@39246
    55
| "mispar י = 10"
haftmann@39246
    56
| "mispar כ = 20"
haftmann@39246
    57
| "mispar ל = 30"
haftmann@39246
    58
| "mispar מ = 40"
haftmann@39246
    59
| "mispar נ = 50"
haftmann@39246
    60
| "mispar ס = 60"
haftmann@39246
    61
| "mispar ע = 70"
haftmann@39246
    62
| "mispar פ = 80"
haftmann@39246
    63
| "mispar צ = 90"
haftmann@39246
    64
| "mispar ק = 100"
haftmann@39246
    65
| "mispar ר = 200"
haftmann@39246
    66
| "mispar ש = 300"
haftmann@39246
    67
| "mispar ת = 400"
wenzelm@17414
    68
wenzelm@17414
    69
thm mispar.simps
wenzelm@17414
    70
wenzelm@17414
    71
lemma "mispar ק + mispar ל + mispar ה = 135"
wenzelm@17414
    72
  by simp
wenzelm@17414
    73
wenzelm@17414
    74
end