src/HOL/ex/Hebrew.thy
author haftmann
Wed Sep 08 19:21:46 2010 +0200 (2010-09-08)
changeset 39246 9e58f0499f57
parent 24312 bb5ec06f7c7a
child 40967 5eb59b62e7de
permissions -rw-r--r--
modernized primrec
     1 (* -*- coding: utf-8 -*- :encoding=utf-8:  
     2     Author:     Makarius
     3 
     4 Example theory involving Unicode characters (UTF-8 encoding) -- both
     5 formal and informal ones.
     6 *)
     7 
     8 header {* A Hebrew theory *}
     9 
    10 theory Hebrew
    11 imports Main
    12 begin
    13 
    14 text {* The Hebrew Alef-Bet (א-ב). *}
    15 
    16 datatype alef_bet =
    17     Alef    ("א")
    18   | Bet     ("ב")
    19   | Gimel   ("ג")
    20   | Dalet   ("ד")
    21   | He      ("ה")
    22   | Vav     ("ו")
    23   | Zayin   ("ז")
    24   | Het     ("ח")
    25   | Tet     ("ט")
    26   | Yod     ("י")
    27   | Kaf     ("כ")
    28   | Lamed   ("ל")
    29   | Mem     ("מ")
    30   | Nun     ("נ")
    31   | Samekh  ("ס")
    32   | Ayin    ("ע")
    33   | Pe      ("פ")
    34   | Tsadi   ("צ")
    35   | Qof     ("ק")
    36   | Resh    ("ר")
    37   | Shin    ("ש")
    38   | Tav     ("ת")
    39 
    40 thm alef_bet.induct
    41 
    42 
    43 text {* Interpreting Hebrew letters as numbers. *}
    44 
    45 primrec mispar :: "alef_bet => nat" 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