src/HOL/ex/Serbian.thy

no longer declare .psimps rules as [simp].

This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.

(* -*- 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 \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> azbuka list"
where
  "abc2azb [] = []"
| "abc2azb [x] = [abc2azb_aux x]"
| "abc2azb (x1 # x2 # xs) = 
       (if x1 = D \<and> x2 = J then
           Ђ # abc2azb xs
        else if x1 = L \<and> x2 = J then
           Љ # abc2azb xs
        else if x1 = N \<and> x2 = J then
           Њ # abc2azb xs
        else if x1 = D \<and> 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 [И, Н, Ј, Е, К, Ц, И, Ј, А]) \<noteq> [И, Н, Ј, Е, К, Ц, И, Ј, А]"
  by simp
text{* It fails for all cyrrilic words that contain НЈ ЛЈ ДЈ ДЖ *}

end