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