isabelle: src/HOL/ex/Hebrew.thy@180f1b3508ed (annotated)

40967 5eb59b62e7de avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle; wenzelm parents: 39246 diff changeset	1	(* Author: Makarius
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	2
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	3	Example theory involving Unicode characters (UTF-8 encoding) -- both
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	4	formal and informal ones.
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	5	*)
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	6
17506 f20e5c8433a4 tuned; wenzelm parents: 17414 diff changeset	7	header {* A Hebrew theory *}
f20e5c8433a4 tuned; wenzelm parents: 17414 diff changeset	8
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	9	theory Hebrew
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	10	imports Main
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	11	begin
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	12
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	13	text {* The Hebrew Alef-Bet (א-ב). *}
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	14
58249 180f1b3508ed use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries blanchet parents: 40967 diff changeset	15	datatype_new alef_bet =
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	16	Alef ("א")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	17	\| Bet ("ב")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	18	\| Gimel ("ג")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	19	\| Dalet ("ד")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	20	\| He ("ה")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	21	\| Vav ("ו")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	22	\| Zayin ("ז")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	23	\| Het ("ח")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	24	\| Tet ("ט")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	25	\| Yod ("י")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	26	\| Kaf ("כ")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	27	\| Lamed ("ל")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	28	\| Mem ("מ")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	29	\| Nun ("נ")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	30	\| Samekh ("ס")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	31	\| Ayin ("ע")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	32	\| Pe ("פ")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	33	\| Tsadi ("צ")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	34	\| Qof ("ק")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	35	\| Resh ("ר")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	36	\| Shin ("ש")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	37	\| Tav ("ת")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	38
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	39	thm alef_bet.induct
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	40
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	41
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	42	text {* Interpreting Hebrew letters as numbers. *}
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	43
39246 9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	44	primrec mispar :: "alef_bet => nat" where
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	45	"mispar א = 1"
39246 9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	46	\| "mispar ב = 2"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	47	\| "mispar ג = 3"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	48	\| "mispar ד = 4"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	49	\| "mispar ה = 5"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	50	\| "mispar ו = 6"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	51	\| "mispar ז = 7"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	52	\| "mispar ח = 8"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	53	\| "mispar ט = 9"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	54	\| "mispar י = 10"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	55	\| "mispar כ = 20"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	56	\| "mispar ל = 30"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	57	\| "mispar מ = 40"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	58	\| "mispar נ = 50"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	59	\| "mispar ס = 60"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	60	\| "mispar ע = 70"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	61	\| "mispar פ = 80"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	62	\| "mispar צ = 90"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	63	\| "mispar ק = 100"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	64	\| "mispar ר = 200"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	65	\| "mispar ש = 300"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	66	\| "mispar ת = 400"
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	67
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	68	thm mispar.simps
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	69
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	70	lemma "mispar ק + mispar ל + mispar ה = 135"
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	71	by simp
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	72
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	73	end

author	blanchet
	Tue, 09 Sep 2014 20:51:36 +0200
changeset 58249	180f1b3508ed
parent 40967	5eb59b62e7de
child 58310	91ea607a34d8
permissions	-rw-r--r--