A Serbian theory, by Filip Maric.
authorwenzelm
Sat Feb 28 21:34:33 2009 +0100 (2009-02-28)
changeset 30179c703c9368c12
parent 30178 70e42a88be37
child 30180 6d29a873141f
child 30182 db768c888dfa
A Serbian theory, by Filip Maric.
CONTRIBUTORS
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
src/HOL/ex/Serbian.thy
     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