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;
     1 (*  Author:     Makarius
     2 
     3 Example theory involving Unicode characters (UTF-8 encoding) -- both
     4 formal and informal ones.
     5 *)
     6 
     7 section \<open>A Hebrew theory\<close>
     8 
     9 theory Hebrew
    10 imports Main
    11 begin
    12 
    13 text \<open>The Hebrew Alef-Bet (א-ב).\<close>
    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 \<open>Interpreting Hebrew letters as numbers.\<close>
    43 
    44 primrec mispar :: "alef_bet => nat"
    45 where
    46   "mispar א = 1"
    47 | "mispar ב = 2"
    48 | "mispar ג = 3"
    49 | "mispar ד = 4"
    50 | "mispar ה = 5"
    51 | "mispar ו = 6"
    52 | "mispar ז = 7"
    53 | "mispar ח = 8"
    54 | "mispar ט = 9"
    55 | "mispar י = 10"
    56 | "mispar כ = 20"
    57 | "mispar ל = 30"
    58 | "mispar מ = 40"
    59 | "mispar נ = 50"
    60 | "mispar ס = 60"
    61 | "mispar ע = 70"
    62 | "mispar פ = 80"
    63 | "mispar צ = 90"
    64 | "mispar ק = 100"
    65 | "mispar ר = 200"
    66 | "mispar ש = 300"
    67 | "mispar ת = 400"
    68 
    69 thm mispar.simps
    70 
    71 lemma "mispar ק + mispar ל + mispar ה = 135"
    72   by simp
    73 
    74 end