# HG changeset patch # User wenzelm # Date 1235853273 -3600 # Node ID c703c9368c127381f4e813c08b78d4c385361b5b # Parent 70e42a88be3761e3d0c9c898613152e3cd1a6bda A Serbian theory, by Filip Maric. diff -r 70e42a88be37 -r c703c9368c12 CONTRIBUTORS --- a/CONTRIBUTORS Sat Feb 28 20:29:20 2009 +0100 +++ b/CONTRIBUTORS Sat Feb 28 21:34:33 2009 +0100 @@ -7,6 +7,9 @@ Contributions to this Isabelle version -------------------------------------- +* February 2009: Filip Maric, Univ. of Belgrade + A Serbian theory. + * February 2009: Jasmin Christian Blanchette, TUM Misc cleanup of HOL/refute. @@ -52,7 +55,7 @@ HOLCF library improvements. * 2007/2008: Stefan Berghofer, TUM - HOL-Nominal package improvements. + HOL-Nominal package improvements. * March 2008: Markus Reiter, TUM HOL/Library/RBT: red-black trees. diff -r 70e42a88be37 -r c703c9368c12 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Feb 28 20:29:20 2009 +0100 +++ b/src/HOL/IsaMakefile Sat Feb 28 21:34:33 2009 +0100 @@ -811,34 +811,31 @@ HOL-ex: HOL $(LOG)/HOL-ex.gz $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \ - Library/Primes.thy \ - ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy ex/BT.thy \ - ex/BinEx.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \ - ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy \ - ex/Groebner_Examples.thy ex/Quickcheck_Generators.thy \ - ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \ - ex/CodegenSML_Test.thy ex/Formal_Power_Series_Examples.thy \ - ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy \ - ex/Hex_Bin_Examples.thy ex/Commutative_Ring_Complete.thy \ - ex/ExecutableContent.thy ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy \ - ex/Binary.thy ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \ + Library/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \ + ex/ApproximationEx.thy ex/Arith_Examples.thy \ + ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \ + ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \ + ex/CodegenSML_Test.thy ex/Codegenerator.thy \ + ex/Codegenerator_Pretty.thy ex/Coherent.thy \ + ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy \ + ex/Dense_Linear_Order_Ex.thy ex/Efficient_Nat_examples.thy \ + ex/Eval_Examples.thy ex/ExecutableContent.thy \ + ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy \ + ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ + ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ + ex/Hilbert_Classical.thy ex/ImperativeQuicksort.thy \ ex/Induction_Scheme.thy ex/InductiveInvariant.thy \ ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ - ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ - ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ + ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \ + ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ - ex/Quickcheck_Examples.thy \ - ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \ + ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML \ + ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ - ex/Subarray.thy ex/Sublist.thy \ - ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy \ - ex/Unification.thy ex/document/root.bib \ - ex/document/root.tex ex/Meson_Test.thy ex/set.thy \ - ex/svc_funcs.ML ex/svc_test.thy \ - ex/ImperativeQuicksort.thy \ - ex/Arithmetic_Series_Complex.thy ex/HarmonicSeries.thy \ - ex/Sqrt.thy ex/Sqrt_Script.thy \ - ex/ApproximationEx.thy + ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Subarray.thy \ + ex/Sublist.thy ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy \ + ex/Termination.thy ex/Unification.thy ex/document/root.bib \ + ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex diff -r 70e42a88be37 -r c703c9368c12 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Sat Feb 28 20:29:20 2009 +0100 +++ b/src/HOL/ex/ROOT.ML Sat Feb 28 21:34:33 2009 +0100 @@ -93,4 +93,5 @@ use_thy "Sudoku" else (); -HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"]; +HTML.with_charset "utf-8" (no_document use_thys) + ["Hebrew", "Chinese", "Serbian"]; diff -r 70e42a88be37 -r c703c9368c12 src/HOL/ex/Serbian.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Serbian.thy Sat Feb 28 21:34:33 2009 +0100 @@ -0,0 +1,217 @@ +(* -*- coding: utf-8 -*- :encoding=utf-8: + Author: Filip Maric + +Example theory involving Unicode characters (UTF-8 encoding) -- +Conversion between Serbian cyrillic and latin letters (српска ћирилица и латиница) +*) + +header {* A Serbian theory *} + +theory Serbian +imports Main +begin + +text{* Serbian cyrillic letters *} +datatype azbuka = + azbA ("А") +| azbB ("Б") +| azbV ("В") +| azbG ("Г") +| azbD ("Д") +| azbDj ("Ђ") +| azbE ("Е") +| azbZv ("Ж") +| azbZ ("З") +| azbI ("И") +| azbJ ("Ј") +| azbK ("К") +| azbL ("Л") +| azbLj ("Љ") +| azbM ("М") +| azbN ("Н") +| azbNj ("Њ") +| azbO ("О") +| azbP ("П") +| azbR ("Р") +| azbS ("С") +| azbT ("Т") +| azbC' ("Ћ") +| azbU ("У") +| azbF ("Ф") +| azbH ("Х") +| azbC ("Ц") +| azbCv ("Ч") +| azbDzv ("Џ") +| azbSv ("Ш") +| azbSpc + +thm azbuka.induct + +text{* Serbian latin letters *} +datatype abeceda = + abcA ("A") +| abcB ("B") +| abcC ("C") +| abcCv ("Č") +| abcC' ("Ć") +| abcD ("D") +| abcE ("E") +| abcF ("F") +| abcG ("G") +| abcH ("H") +| abcI ("I") +| abcJ ("J") +| abcK ("K") +| abcL ("L") +| abcM ("M") +| abcN ("N") +| abcO ("O") +| abcP ("P") +| abcR ("R") +| abcS ("S") +| abcSv ("Š") +| abcT ("T") +| abcU ("U") +| abcV ("V") +| abcZ ("Z") +| abcvZ ("Ž") +| abcSpc + +thm abeceda.induct + + +text{* Conversion from cyrillic to latin - + this conversion is valid in all cases *} +primrec azb2abc_aux :: "azbuka \ abeceda list" +where + "azb2abc_aux А = [A]" +| "azb2abc_aux Б = [B]" +| "azb2abc_aux В = [V]" +| "azb2abc_aux Г = [G]" +| "azb2abc_aux Д = [D]" +| "azb2abc_aux Ђ = [D, J]" +| "azb2abc_aux Е = [E]" +| "azb2abc_aux Ж = [Ž]" +| "azb2abc_aux З = [Z]" +| "azb2abc_aux И = [I]" +| "azb2abc_aux Ј = [J]" +| "azb2abc_aux К = [K]" +| "azb2abc_aux Л = [L]" +| "azb2abc_aux Љ = [L, J]" +| "azb2abc_aux М = [M]" +| "azb2abc_aux Н = [N]" +| "azb2abc_aux Њ = [N, J]" +| "azb2abc_aux О = [O]" +| "azb2abc_aux П = [P]" +| "azb2abc_aux Р = [R]" +| "azb2abc_aux С = [S]" +| "azb2abc_aux Т = [T]" +| "azb2abc_aux Ћ = [Ć]" +| "azb2abc_aux У = [U]" +| "azb2abc_aux Ф = [F]" +| "azb2abc_aux Х = [H]" +| "azb2abc_aux Ц = [C]" +| "azb2abc_aux Ч = [Č]" +| "azb2abc_aux Џ = [D, Ž]" +| "azb2abc_aux Ш = [Š]" +| "azb2abc_aux azbSpc = [abcSpc]" + +primrec azb2abc :: "azbuka list \ abeceda list" +where + "azb2abc [] = []" +| "azb2abc (x # xs) = azb2abc_aux x @ azb2abc xs" + +value "azb2abc [Д, О, Б, А, Р, azbSpc, Д, А, Н, azbSpc, С, В, И, М, А]" +value "azb2abc [Љ, У, Б, И, Ч, И, Ц, А, azbSpc, Н, А, azbSpc, П, О, Љ, У]" + +text{* The conversion from latin to cyrillic - + this conversion is valid in most cases but there are some exceptions *} +primrec abc2azb_aux :: "abeceda \ azbuka" +where + "abc2azb_aux A = А" +| "abc2azb_aux B = Б" +| "abc2azb_aux C = Ц" +| "abc2azb_aux Č = Ч" +| "abc2azb_aux Ć = Ћ" +| "abc2azb_aux D = Д" +| "abc2azb_aux E = Е" +| "abc2azb_aux F = Ф" +| "abc2azb_aux G = Г" +| "abc2azb_aux H = Х" +| "abc2azb_aux I = И" +| "abc2azb_aux J = Ј" +| "abc2azb_aux K = К" +| "abc2azb_aux L = Л" +| "abc2azb_aux M = М" +| "abc2azb_aux N = Н" +| "abc2azb_aux O = О" +| "abc2azb_aux P = П" +| "abc2azb_aux R = Р" +| "abc2azb_aux S = С" +| "abc2azb_aux Š = Ш" +| "abc2azb_aux T = Т" +| "abc2azb_aux U = У" +| "abc2azb_aux V = В" +| "abc2azb_aux Z = З" +| "abc2azb_aux Ž = Ж" +| "abc2azb_aux abcSpc = azbSpc" + +fun abc2azb :: "abeceda list \ azbuka list" +where + "abc2azb [] = []" +| "abc2azb [x] = [abc2azb_aux x]" +| "abc2azb (x1 # x2 # xs) = + (if x1 = D \ x2 = J then + Ђ # abc2azb xs + else if x1 = L \ x2 = J then + Љ # abc2azb xs + else if x1 = N \ x2 = J then + Њ # abc2azb xs + else if x1 = D \ x2 = Ž then + Џ # abc2azb xs + else + abc2azb_aux x1 # abc2azb (x2 # xs) + )" + +value "abc2azb [D, O, B, A, R, abcSpc, D, A, N, abcSpc, S, V, I, M, A]" +value "abc2azb [L, J, U, B, I, Č, I, C, A, abcSpc, N, A, abcSpc, P, O, L, J, U]" + +text{* Here are some invalid conversions *} +lemma "abc2azb [N, A, D, Ž, I, V, E, T, I] = [Н, А, Џ, И, В, Е, Т, И]" + by simp +text{* but it should be: НАДЖИВЕТИ *} +lemma "abc2azb [I, N, J, E, K, C, I, J, A] = [И, Њ, Е, К, Ц, И, Ј, А]" + by simp +text{* but it should be: ИНЈЕКЦИЈА *} + +text{* The conversion fails for all cyrrilic words that contain НЈ ЛЈ ДЈ ДЖ *} + + +text{* Idempotency in one direction *} +lemma [simp]: "azb2abc_aux (abc2azb_aux x) = [x]" + by (cases x) auto + +lemma [simp]: "abc2azb (Ž # xs) = Ж # abc2azb xs" + by (cases xs) auto + +lemma [simp]: "abc2azb (J # xs) = Ј # abc2azb xs" + by (cases xs) auto + +theorem "azb2abc (abc2azb x) = x" +proof (induct x) + case (Cons x1 xs) + thus ?case + proof (cases xs) + case (Cons x2 xss) + thus ?thesis + using `azb2abc (abc2azb xs) = xs` + by auto + qed simp +qed simp + +text{* Idempotency in the other direction does not hold *} +lemma "abc2azb (azb2abc [И, Н, Ј, Е, К, Ц, И, Ј, А]) \ [И, Н, Ј, Е, К, Ц, И, Ј, А]" + by simp +text{* It fails for all cyrrilic words that contain НЈ ЛЈ ДЈ ДЖ *} + +end