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