1.1 --- a/CONTRIBUTORS Sat Feb 28 20:29:20 2009 +0100
1.2 +++ b/CONTRIBUTORS Sat Feb 28 21:34:33 2009 +0100
1.3 @@ -7,6 +7,9 @@
1.4 Contributions to this Isabelle version
1.5 --------------------------------------
1.6
1.7 +* February 2009: Filip Maric, Univ. of Belgrade
1.8 + A Serbian theory.
1.9 +
1.10 * February 2009: Jasmin Christian Blanchette, TUM
1.11 Misc cleanup of HOL/refute.
1.12
1.13 @@ -52,7 +55,7 @@
1.14 HOLCF library improvements.
1.15
1.16 * 2007/2008: Stefan Berghofer, TUM
1.17 - HOL-Nominal package improvements.
1.18 + HOL-Nominal package improvements.
1.19
1.20 * March 2008: Markus Reiter, TUM
1.21 HOL/Library/RBT: red-black trees.
2.1 --- a/src/HOL/IsaMakefile Sat Feb 28 20:29:20 2009 +0100
2.2 +++ b/src/HOL/IsaMakefile Sat Feb 28 21:34:33 2009 +0100
2.3 @@ -811,34 +811,31 @@
2.4 HOL-ex: HOL $(LOG)/HOL-ex.gz
2.5
2.6 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
2.7 - Library/Primes.thy \
2.8 - ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy ex/BT.thy \
2.9 - ex/BinEx.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \
2.10 - ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy \
2.11 - ex/Groebner_Examples.thy ex/Quickcheck_Generators.thy \
2.12 - ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \
2.13 - ex/CodegenSML_Test.thy ex/Formal_Power_Series_Examples.thy \
2.14 - ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy \
2.15 - ex/Hex_Bin_Examples.thy ex/Commutative_Ring_Complete.thy \
2.16 - ex/ExecutableContent.thy ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy \
2.17 - ex/Binary.thy ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \
2.18 + Library/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
2.19 + ex/ApproximationEx.thy ex/Arith_Examples.thy \
2.20 + ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \
2.21 + ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \
2.22 + ex/CodegenSML_Test.thy ex/Codegenerator.thy \
2.23 + ex/Codegenerator_Pretty.thy ex/Coherent.thy \
2.24 + ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy \
2.25 + ex/Dense_Linear_Order_Ex.thy ex/Efficient_Nat_examples.thy \
2.26 + ex/Eval_Examples.thy ex/ExecutableContent.thy \
2.27 + ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy \
2.28 + ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
2.29 + ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
2.30 + ex/Hilbert_Classical.thy ex/ImperativeQuicksort.thy \
2.31 ex/Induction_Scheme.thy ex/InductiveInvariant.thy \
2.32 ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \
2.33 - ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
2.34 - ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
2.35 + ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \
2.36 + ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
2.37 ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
2.38 - ex/Quickcheck_Examples.thy \
2.39 - ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
2.40 + ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML \
2.41 + ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
2.42 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
2.43 - ex/Subarray.thy ex/Sublist.thy \
2.44 - ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy \
2.45 - ex/Unification.thy ex/document/root.bib \
2.46 - ex/document/root.tex ex/Meson_Test.thy ex/set.thy \
2.47 - ex/svc_funcs.ML ex/svc_test.thy \
2.48 - ex/ImperativeQuicksort.thy \
2.49 - ex/Arithmetic_Series_Complex.thy ex/HarmonicSeries.thy \
2.50 - ex/Sqrt.thy ex/Sqrt_Script.thy \
2.51 - ex/ApproximationEx.thy
2.52 + ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Subarray.thy \
2.53 + ex/Sublist.thy ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy \
2.54 + ex/Termination.thy ex/Unification.thy ex/document/root.bib \
2.55 + ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
2.56 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
2.57
2.58
3.1 --- a/src/HOL/ex/ROOT.ML Sat Feb 28 20:29:20 2009 +0100
3.2 +++ b/src/HOL/ex/ROOT.ML Sat Feb 28 21:34:33 2009 +0100
3.3 @@ -93,4 +93,5 @@
3.4 use_thy "Sudoku"
3.5 else ();
3.6
3.7 -HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"];
3.8 +HTML.with_charset "utf-8" (no_document use_thys)
3.9 + ["Hebrew", "Chinese", "Serbian"];
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/ex/Serbian.thy Sat Feb 28 21:34:33 2009 +0100
4.3 @@ -0,0 +1,217 @@
4.4 +(* -*- coding: utf-8 -*- :encoding=utf-8:
4.5 + Author: Filip Maric
4.6 +
4.7 +Example theory involving Unicode characters (UTF-8 encoding) --
4.8 +Conversion between Serbian cyrillic and latin letters (српска ћирилица и латиница)
4.9 +*)
4.10 +
4.11 +header {* A Serbian theory *}
4.12 +
4.13 +theory Serbian
4.14 +imports Main
4.15 +begin
4.16 +
4.17 +text{* Serbian cyrillic letters *}
4.18 +datatype azbuka =
4.19 + azbA ("А")
4.20 +| azbB ("Б")
4.21 +| azbV ("В")
4.22 +| azbG ("Г")
4.23 +| azbD ("Д")
4.24 +| azbDj ("Ђ")
4.25 +| azbE ("Е")
4.26 +| azbZv ("Ж")
4.27 +| azbZ ("З")
4.28 +| azbI ("И")
4.29 +| azbJ ("Ј")
4.30 +| azbK ("К")
4.31 +| azbL ("Л")
4.32 +| azbLj ("Љ")
4.33 +| azbM ("М")
4.34 +| azbN ("Н")
4.35 +| azbNj ("Њ")
4.36 +| azbO ("О")
4.37 +| azbP ("П")
4.38 +| azbR ("Р")
4.39 +| azbS ("С")
4.40 +| azbT ("Т")
4.41 +| azbC' ("Ћ")
4.42 +| azbU ("У")
4.43 +| azbF ("Ф")
4.44 +| azbH ("Х")
4.45 +| azbC ("Ц")
4.46 +| azbCv ("Ч")
4.47 +| azbDzv ("Џ")
4.48 +| azbSv ("Ш")
4.49 +| azbSpc
4.50 +
4.51 +thm azbuka.induct
4.52 +
4.53 +text{* Serbian latin letters *}
4.54 +datatype abeceda =
4.55 + abcA ("A")
4.56 +| abcB ("B")
4.57 +| abcC ("C")
4.58 +| abcCv ("Č")
4.59 +| abcC' ("Ć")
4.60 +| abcD ("D")
4.61 +| abcE ("E")
4.62 +| abcF ("F")
4.63 +| abcG ("G")
4.64 +| abcH ("H")
4.65 +| abcI ("I")
4.66 +| abcJ ("J")
4.67 +| abcK ("K")
4.68 +| abcL ("L")
4.69 +| abcM ("M")
4.70 +| abcN ("N")
4.71 +| abcO ("O")
4.72 +| abcP ("P")
4.73 +| abcR ("R")
4.74 +| abcS ("S")
4.75 +| abcSv ("Š")
4.76 +| abcT ("T")
4.77 +| abcU ("U")
4.78 +| abcV ("V")
4.79 +| abcZ ("Z")
4.80 +| abcvZ ("Ž")
4.81 +| abcSpc
4.82 +
4.83 +thm abeceda.induct
4.84 +
4.85 +
4.86 +text{* Conversion from cyrillic to latin -
4.87 + this conversion is valid in all cases *}
4.88 +primrec azb2abc_aux :: "azbuka \<Rightarrow> abeceda list"
4.89 +where
4.90 + "azb2abc_aux А = [A]"
4.91 +| "azb2abc_aux Б = [B]"
4.92 +| "azb2abc_aux В = [V]"
4.93 +| "azb2abc_aux Г = [G]"
4.94 +| "azb2abc_aux Д = [D]"
4.95 +| "azb2abc_aux Ђ = [D, J]"
4.96 +| "azb2abc_aux Е = [E]"
4.97 +| "azb2abc_aux Ж = [Ž]"
4.98 +| "azb2abc_aux З = [Z]"
4.99 +| "azb2abc_aux И = [I]"
4.100 +| "azb2abc_aux Ј = [J]"
4.101 +| "azb2abc_aux К = [K]"
4.102 +| "azb2abc_aux Л = [L]"
4.103 +| "azb2abc_aux Љ = [L, J]"
4.104 +| "azb2abc_aux М = [M]"
4.105 +| "azb2abc_aux Н = [N]"
4.106 +| "azb2abc_aux Њ = [N, J]"
4.107 +| "azb2abc_aux О = [O]"
4.108 +| "azb2abc_aux П = [P]"
4.109 +| "azb2abc_aux Р = [R]"
4.110 +| "azb2abc_aux С = [S]"
4.111 +| "azb2abc_aux Т = [T]"
4.112 +| "azb2abc_aux Ћ = [Ć]"
4.113 +| "azb2abc_aux У = [U]"
4.114 +| "azb2abc_aux Ф = [F]"
4.115 +| "azb2abc_aux Х = [H]"
4.116 +| "azb2abc_aux Ц = [C]"
4.117 +| "azb2abc_aux Ч = [Č]"
4.118 +| "azb2abc_aux Џ = [D, Ž]"
4.119 +| "azb2abc_aux Ш = [Š]"
4.120 +| "azb2abc_aux azbSpc = [abcSpc]"
4.121 +
4.122 +primrec azb2abc :: "azbuka list \<Rightarrow> abeceda list"
4.123 +where
4.124 + "azb2abc [] = []"
4.125 +| "azb2abc (x # xs) = azb2abc_aux x @ azb2abc xs"
4.126 +
4.127 +value "azb2abc [Д, О, Б, А, Р, azbSpc, Д, А, Н, azbSpc, С, В, И, М, А]"
4.128 +value "azb2abc [Љ, У, Б, И, Ч, И, Ц, А, azbSpc, Н, А, azbSpc, П, О, Љ, У]"
4.129 +
4.130 +text{* The conversion from latin to cyrillic -
4.131 + this conversion is valid in most cases but there are some exceptions *}
4.132 +primrec abc2azb_aux :: "abeceda \<Rightarrow> azbuka"
4.133 +where
4.134 + "abc2azb_aux A = А"
4.135 +| "abc2azb_aux B = Б"
4.136 +| "abc2azb_aux C = Ц"
4.137 +| "abc2azb_aux Č = Ч"
4.138 +| "abc2azb_aux Ć = Ћ"
4.139 +| "abc2azb_aux D = Д"
4.140 +| "abc2azb_aux E = Е"
4.141 +| "abc2azb_aux F = Ф"
4.142 +| "abc2azb_aux G = Г"
4.143 +| "abc2azb_aux H = Х"
4.144 +| "abc2azb_aux I = И"
4.145 +| "abc2azb_aux J = Ј"
4.146 +| "abc2azb_aux K = К"
4.147 +| "abc2azb_aux L = Л"
4.148 +| "abc2azb_aux M = М"
4.149 +| "abc2azb_aux N = Н"
4.150 +| "abc2azb_aux O = О"
4.151 +| "abc2azb_aux P = П"
4.152 +| "abc2azb_aux R = Р"
4.153 +| "abc2azb_aux S = С"
4.154 +| "abc2azb_aux Š = Ш"
4.155 +| "abc2azb_aux T = Т"
4.156 +| "abc2azb_aux U = У"
4.157 +| "abc2azb_aux V = В"
4.158 +| "abc2azb_aux Z = З"
4.159 +| "abc2azb_aux Ž = Ж"
4.160 +| "abc2azb_aux abcSpc = azbSpc"
4.161 +
4.162 +fun abc2azb :: "abeceda list \<Rightarrow> azbuka list"
4.163 +where
4.164 + "abc2azb [] = []"
4.165 +| "abc2azb [x] = [abc2azb_aux x]"
4.166 +| "abc2azb (x1 # x2 # xs) =
4.167 + (if x1 = D \<and> x2 = J then
4.168 + Ђ # abc2azb xs
4.169 + else if x1 = L \<and> x2 = J then
4.170 + Љ # abc2azb xs
4.171 + else if x1 = N \<and> x2 = J then
4.172 + Њ # abc2azb xs
4.173 + else if x1 = D \<and> x2 = Ž then
4.174 + Џ # abc2azb xs
4.175 + else
4.176 + abc2azb_aux x1 # abc2azb (x2 # xs)
4.177 + )"
4.178 +
4.179 +value "abc2azb [D, O, B, A, R, abcSpc, D, A, N, abcSpc, S, V, I, M, A]"
4.180 +value "abc2azb [L, J, U, B, I, Č, I, C, A, abcSpc, N, A, abcSpc, P, O, L, J, U]"
4.181 +
4.182 +text{* Here are some invalid conversions *}
4.183 +lemma "abc2azb [N, A, D, Ž, I, V, E, T, I] = [Н, А, Џ, И, В, Е, Т, И]"
4.184 + by simp
4.185 +text{* but it should be: НАДЖИВЕТИ *}
4.186 +lemma "abc2azb [I, N, J, E, K, C, I, J, A] = [И, Њ, Е, К, Ц, И, Ј, А]"
4.187 + by simp
4.188 +text{* but it should be: ИНЈЕКЦИЈА *}
4.189 +
4.190 +text{* The conversion fails for all cyrrilic words that contain НЈ ЛЈ ДЈ ДЖ *}
4.191 +
4.192 +
4.193 +text{* Idempotency in one direction *}
4.194 +lemma [simp]: "azb2abc_aux (abc2azb_aux x) = [x]"
4.195 + by (cases x) auto
4.196 +
4.197 +lemma [simp]: "abc2azb (Ž # xs) = Ж # abc2azb xs"
4.198 + by (cases xs) auto
4.199 +
4.200 +lemma [simp]: "abc2azb (J # xs) = Ј # abc2azb xs"
4.201 + by (cases xs) auto
4.202 +
4.203 +theorem "azb2abc (abc2azb x) = x"
4.204 +proof (induct x)
4.205 + case (Cons x1 xs)
4.206 + thus ?case
4.207 + proof (cases xs)
4.208 + case (Cons x2 xss)
4.209 + thus ?thesis
4.210 + using `azb2abc (abc2azb xs) = xs`
4.211 + by auto
4.212 + qed simp
4.213 +qed simp
4.214 +
4.215 +text{* Idempotency in the other direction does not hold *}
4.216 +lemma "abc2azb (azb2abc [И, Н, Ј, Е, К, Ц, И, Ј, А]) \<noteq> [И, Н, Ј, Е, К, Ц, И, Ј, А]"
4.217 + by simp
4.218 +text{* It fails for all cyrrilic words that contain НЈ ЛЈ ДЈ ДЖ *}
4.219 +
4.220 +end