src/HOL/ex/Hebrew.thy
author krauss
Tue, 28 Sep 2010 09:54:07 +0200
changeset 39754 150f831ce4a3
parent 39246 9e58f0499f57
child 40967 5eb59b62e7de
permissions -rw-r--r--
no longer declare .psimps rules as [simp]. This regularly caused confusion (e.g., they show up in simp traces when the regular simp rules are disabled). In the few places where the rules are used, explicitly mentioning them actually clarifies the proof text.

(* -*- coding: utf-8 -*- :encoding=utf-8:  
    Author:     Makarius

Example theory involving Unicode characters (UTF-8 encoding) -- both
formal and informal ones.
*)

header {* A Hebrew theory *}

theory Hebrew
imports Main
begin

text {* The Hebrew Alef-Bet (א-ב). *}

datatype alef_bet =
    Alef    ("א")
  | Bet     ("ב")
  | Gimel   ("ג")
  | Dalet   ("ד")
  | He      ("ה")
  | Vav     ("ו")
  | Zayin   ("ז")
  | Het     ("ח")
  | Tet     ("ט")
  | Yod     ("י")
  | Kaf     ("כ")
  | Lamed   ("ל")
  | Mem     ("מ")
  | Nun     ("נ")
  | Samekh  ("ס")
  | Ayin    ("ע")
  | Pe      ("פ")
  | Tsadi   ("צ")
  | Qof     ("ק")
  | Resh    ("ר")
  | Shin    ("ש")
  | Tav     ("ת")

thm alef_bet.induct


text {* Interpreting Hebrew letters as numbers. *}

primrec mispar :: "alef_bet => nat" where
  "mispar א = 1"
| "mispar ב = 2"
| "mispar ג = 3"
| "mispar ד = 4"
| "mispar ה = 5"
| "mispar ו = 6"
| "mispar ז = 7"
| "mispar ח = 8"
| "mispar ט = 9"
| "mispar י = 10"
| "mispar כ = 20"
| "mispar ל = 30"
| "mispar מ = 40"
| "mispar נ = 50"
| "mispar ס = 60"
| "mispar ע = 70"
| "mispar פ = 80"
| "mispar צ = 90"
| "mispar ק = 100"
| "mispar ר = 200"
| "mispar ש = 300"
| "mispar ת = 400"

thm mispar.simps

lemma "mispar ק + mispar ל + mispar ה = 135"
  by simp

end