The Hebrew Alef-Bet -- Unicode example;
authorwenzelm
Thu Sep 15 17:17:02 2005 +0200 (2005-09-15)
changeset 17414c9e9d2a2fc72
parent 17413 89ccb3799428
child 17415 ec859c451f59
The Hebrew Alef-Bet -- Unicode example;
src/HOL/ex/Hebrew.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Hebrew.thy	Thu Sep 15 17:17:02 2005 +0200
     1.3 @@ -0,0 +1,75 @@
     1.4 +(* -*- coding: utf-8 -*-  
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Example theory involving Unicode characters (UTF-8 encoding) -- both
     1.9 +formal and informal ones.
    1.10 +*)
    1.11 +
    1.12 +theory Hebrew
    1.13 +imports Main
    1.14 +begin
    1.15 +
    1.16 +text {* The Hebrew Alef-Bet (א-ב). *}
    1.17 +
    1.18 +datatype alef_bet =
    1.19 +    Alef    ("א")
    1.20 +  | Bet     ("ב")
    1.21 +  | Gimel   ("ג")
    1.22 +  | Dalet   ("ד")
    1.23 +  | He      ("ה")
    1.24 +  | Vav     ("ו")
    1.25 +  | Zayin   ("ז")
    1.26 +  | Het     ("ח")
    1.27 +  | Tet     ("ט")
    1.28 +  | Yod     ("י")
    1.29 +  | Kaf     ("כ")
    1.30 +  | Lamed   ("ל")
    1.31 +  | Mem     ("מ")
    1.32 +  | Nun     ("נ")
    1.33 +  | Samekh  ("ס")
    1.34 +  | Ayin    ("ע")
    1.35 +  | Pe      ("פ")
    1.36 +  | Tsadi   ("צ")
    1.37 +  | Qof     ("ק")
    1.38 +  | Resh    ("ר")
    1.39 +  | Shin    ("ש")
    1.40 +  | Tav     ("ת")
    1.41 +
    1.42 +thm alef_bet.induct
    1.43 +
    1.44 +
    1.45 +text {* Interpreting Hebrew letters as numbers. *}
    1.46 +
    1.47 +consts
    1.48 +  mispar :: "alef_bet => nat"
    1.49 +primrec
    1.50 +  "mispar א = 1"
    1.51 +  "mispar ב = 2"
    1.52 +  "mispar ג = 3"
    1.53 +  "mispar ד = 4"
    1.54 +  "mispar ה = 5"
    1.55 +  "mispar ו = 6"
    1.56 +  "mispar ז = 7"
    1.57 +  "mispar ח = 8"
    1.58 +  "mispar ט = 9"
    1.59 +  "mispar י = 10"
    1.60 +  "mispar כ = 20"
    1.61 +  "mispar ל = 30"
    1.62 +  "mispar מ = 40"
    1.63 +  "mispar נ = 50"
    1.64 +  "mispar ס = 60"
    1.65 +  "mispar ע = 70"
    1.66 +  "mispar פ = 80"
    1.67 +  "mispar צ = 90"
    1.68 +  "mispar ק = 100"
    1.69 +  "mispar ר = 200"
    1.70 +  "mispar ש = 300"
    1.71 +  "mispar ת = 400"
    1.72 +
    1.73 +thm mispar.simps
    1.74 +
    1.75 +lemma "mispar ק + mispar ל + mispar ה = 135"
    1.76 +  by simp
    1.77 +
    1.78 +end