isabelle: src/HOL/ex/Hebrew.thy@c3658c18b7bc (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
59031 4c3bb56b8ce7 misc tuning and modernization; wenzelm parents: 58889 diff changeset	7	section \<open>A Hebrew theory\<close>
17506 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
59031 4c3bb56b8ce7 misc tuning and modernization; wenzelm parents: 58889 diff changeset	13	text \<open>The Hebrew Alef-Bet (א-ב).\<close>
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	14
58310 91ea607a34d8 updated news blanchet parents: 58249 diff changeset	15	datatype 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
59031 4c3bb56b8ce7 misc tuning and modernization; wenzelm parents: 58889 diff changeset	42	text \<open>Interpreting Hebrew letters as numbers.\<close>
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	43
59031 4c3bb56b8ce7 misc tuning and modernization; wenzelm parents: 58889 diff changeset	44	primrec mispar :: "alef_bet => nat"
4c3bb56b8ce7 misc tuning and modernization; wenzelm parents: 58889 diff changeset	45	where
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	46	"mispar א = 1"
39246 9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	47	\| "mispar ב = 2"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	48	\| "mispar ג = 3"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	49	\| "mispar ד = 4"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	50	\| "mispar ה = 5"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	51	\| "mispar ו = 6"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	52	\| "mispar ז = 7"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	53	\| "mispar ח = 8"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	54	\| "mispar ט = 9"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	55	\| "mispar י = 10"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	56	\| "mispar כ = 20"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	57	\| "mispar ל = 30"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	58	\| "mispar מ = 40"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	59	\| "mispar נ = 50"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	60	\| "mispar ס = 60"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	61	\| "mispar ע = 70"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	62	\| "mispar פ = 80"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	63	\| "mispar צ = 90"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	64	\| "mispar ק = 100"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	65	\| "mispar ר = 200"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	66	\| "mispar ש = 300"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	67	\| "mispar ת = 400"
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	68
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	69	thm mispar.simps
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	70
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	71	lemma "mispar ק + mispar ל + mispar ה = 135"
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	72	by simp
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	73
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	74	end

author	haftmann
	Tue, 13 Oct 2015 09:21:15 +0200
changeset 61424	c3658c18b7bc
parent 59031	4c3bb56b8ce7
child 62809	4b8f08de2792
permissions	-rw-r--r--