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