isabelle: src/HOL/ex/Hebrew.thy@db37cae970a6 (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
62809 4b8f08de2792 explicit warning about bidi uncertainty in Unicode; wenzelm parents: 59031 diff changeset	13	text \<open>
62812 ce22e5c3d4ce more robust display of bidirectional Unicode text: enforce left-to-right; wenzelm parents: 62809 diff changeset	14	\<^bold>\<open>Warning:\<close> Bidirectional Unicode text may confuse display in browsers, editors, etc.!
62809 4b8f08de2792 explicit warning about bidi uncertainty in Unicode; wenzelm parents: 59031 diff changeset	15	\<close>
4b8f08de2792 explicit warning about bidi uncertainty in Unicode; wenzelm parents: 59031 diff changeset	16
4b8f08de2792 explicit warning about bidi uncertainty in Unicode; wenzelm parents: 59031 diff changeset	17	subsection \<open>The Hebrew Alef-Bet (א-ב).\<close>
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	18
58310 91ea607a34d8 updated news blanchet parents: 58249 diff changeset	19	datatype alef_bet =
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	20	Alef ("א")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	21	\| Bet ("ב")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	22	\| Gimel ("ג")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	23	\| Dalet ("ד")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	24	\| He ("ה")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	25	\| Vav ("ו")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	26	\| Zayin ("ז")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	27	\| Het ("ח")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	28	\| Tet ("ט")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	29	\| Yod ("י")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	30	\| Kaf ("כ")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	31	\| Lamed ("ל")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	32	\| Mem ("מ")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	33	\| Nun ("נ")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	34	\| Samekh ("ס")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	35	\| Ayin ("ע")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	36	\| Pe ("פ")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	37	\| Tsadi ("צ")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	38	\| Qof ("ק")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	39	\| Resh ("ר")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	40	\| Shin ("ש")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	41	\| Tav ("ת")
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	42
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	43	thm alef_bet.induct
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	44
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	45
62809 4b8f08de2792 explicit warning about bidi uncertainty in Unicode; wenzelm parents: 59031 diff changeset	46	subsection \<open>Interpreting Hebrew letters as numbers.\<close>
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	47
62809 4b8f08de2792 explicit warning about bidi uncertainty in Unicode; wenzelm parents: 59031 diff changeset	48	primrec mispar :: "alef_bet \<Rightarrow> nat"
59031 4c3bb56b8ce7 misc tuning and modernization; wenzelm parents: 58889 diff changeset	49	where
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	50	"mispar א = 1"
39246 9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	51	\| "mispar ב = 2"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	52	\| "mispar ג = 3"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	53	\| "mispar ד = 4"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	54	\| "mispar ה = 5"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	55	\| "mispar ו = 6"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	56	\| "mispar ז = 7"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	57	\| "mispar ח = 8"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	58	\| "mispar ט = 9"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	59	\| "mispar י = 10"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	60	\| "mispar כ = 20"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	61	\| "mispar ל = 30"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	62	\| "mispar מ = 40"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	63	\| "mispar נ = 50"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	64	\| "mispar ס = 60"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	65	\| "mispar ע = 70"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	66	\| "mispar פ = 80"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	67	\| "mispar צ = 90"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	68	\| "mispar ק = 100"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	69	\| "mispar ר = 200"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	70	\| "mispar ש = 300"
9e58f0499f57 modernized primrec haftmann parents: 24312 diff changeset	71	\| "mispar ת = 400"
17414 c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	72
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	73	thm mispar.simps
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	74
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	75	lemma "mispar ק + mispar ל + mispar ה = 135"
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	76	by simp
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	77
c9e9d2a2fc72 The Hebrew Alef-Bet -- Unicode example; wenzelm parents: diff changeset	78	end

author	wenzelm
	Thu, 26 Oct 2023 22:10:22 +0200
changeset 78851	db37cae970a6
parent 62812	ce22e5c3d4ce
child 80914	d97fdabd9e2b
permissions	-rw-r--r--