src/HOL/ex/Hebrew.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 62812 ce22e5c3d4ce
permissions -rw-r--r--
bundle lifting_syntax;
     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>
    14   \<^bold>\<open>Warning:\<close> Bidirectional Unicode text may confuse display in browsers, editors, etc.!
    15 \<close>
    16 
    17 subsection \<open>The Hebrew Alef-Bet (א-ב).\<close>
    18 
    19 datatype alef_bet =
    20     Alef    ("א")
    21   | Bet     ("ב")
    22   | Gimel   ("ג")
    23   | Dalet   ("ד")
    24   | He      ("ה")
    25   | Vav     ("ו")
    26   | Zayin   ("ז")
    27   | Het     ("ח")
    28   | Tet     ("ט")
    29   | Yod     ("י")
    30   | Kaf     ("כ")
    31   | Lamed   ("ל")
    32   | Mem     ("מ")
    33   | Nun     ("נ")
    34   | Samekh  ("ס")
    35   | Ayin    ("ע")
    36   | Pe      ("פ")
    37   | Tsadi   ("צ")
    38   | Qof     ("ק")
    39   | Resh    ("ר")
    40   | Shin    ("ש")
    41   | Tav     ("ת")
    42 
    43 thm alef_bet.induct
    44 
    45 
    46 subsection \<open>Interpreting Hebrew letters as numbers.\<close>
    47 
    48 primrec mispar :: "alef_bet \<Rightarrow> nat"
    49 where
    50   "mispar א = 1"
    51 | "mispar ב = 2"
    52 | "mispar ג = 3"
    53 | "mispar ד = 4"
    54 | "mispar ה = 5"
    55 | "mispar ו = 6"
    56 | "mispar ז = 7"
    57 | "mispar ח = 8"
    58 | "mispar ט = 9"
    59 | "mispar י = 10"
    60 | "mispar כ = 20"
    61 | "mispar ל = 30"
    62 | "mispar מ = 40"
    63 | "mispar נ = 50"
    64 | "mispar ס = 60"
    65 | "mispar ע = 70"
    66 | "mispar פ = 80"
    67 | "mispar צ = 90"
    68 | "mispar ק = 100"
    69 | "mispar ר = 200"
    70 | "mispar ש = 300"
    71 | "mispar ת = 400"
    72 
    73 thm mispar.simps
    74 
    75 lemma "mispar ק + mispar ל + mispar ה = 135"
    76   by simp
    77 
    78 end