# HG changeset patch
# User urbanc
# Date 1305748483 0
# Node ID e93760534354f67b52a10b232003f29e89389095
# Parent  a8a442ba0dbf5802852829aedb6a51034932904c
added directory for journal version; took uptodate version of the theory files

diff -r a8a442ba0dbf -r e93760534354 Closure.thy
--- a/Closure.thy	Thu May 12 05:55:05 2011 +0000
+++ b/Closure.thy	Wed May 18 19:54:43 2011 +0000
@@ -1,223 +1,140 @@
-theory "RegSet"
-  imports "Main" 
+theory Closure
+imports Myhill_2
 begin
 
-
-text {* Sequential composition of sets *}
+section {* Closure properties of regular languages *}
 
-definition
-  lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)
-where 
-  "L1 ; L2 = {s1@s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+abbreviation
+  regular :: "lang \<Rightarrow> bool"
+where
+  "regular A \<equiv> \<exists>r::rexp. A = L r"
 
 
-section {* Kleene star for sets *}
+lemma closure_union[intro]:
+  assumes "regular A" "regular B" 
+  shows "regular (A \<union> B)"
+proof -
+  from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto
+  then have "A \<union> B = L (ALT r1 r2)" by simp
+  then show "regular (A \<union> B)" by blast
+qed
 
-inductive_set
-  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
-  for L :: "string set"
-where
-  start[intro]: "[] \<in> L\<star>"
-| step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"
+lemma closure_seq[intro]:
+  assumes "regular A" "regular B" 
+  shows "regular (A ;; B)"
+proof -
+  from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto
+  then have "A ;; B = L (SEQ r1 r2)" by simp
+  then show "regular (A ;; B)" by blast
+qed
 
-
-text {* A standard property of star *}
+lemma closure_star[intro]:
+  assumes "regular A"
+  shows "regular (A\<star>)"
+proof -
+  from assms obtain r::rexp where "L r = A" by auto
+  then have "A\<star> = L (STAR r)" by simp
+  then show "regular (A\<star>)" by blast
+qed
 
-lemma lang_star_cases:
-  shows "L\<star> =  {[]} \<union> L ; L\<star>"
-proof
-  { fix x
-    have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ; L\<star>"
-      unfolding lang_seq_def
-    by (induct rule: Star.induct) (auto)
-  }
-  then show "L\<star> \<subseteq> {[]} \<union> L ; L\<star>" by auto
-next
-  show "{[]} \<union> L ; L\<star> \<subseteq> L\<star>" 
-    unfolding lang_seq_def by auto
+lemma closure_complement[intro]:
+  assumes "regular A"
+  shows "regular (- A)"
+proof -
+  from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode)
+  then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_rel_def)
+  then show "regular (- A)" by (simp add: Myhill_Nerode)
+qed
+
+lemma closure_difference[intro]:
+  assumes "regular A" "regular B" 
+  shows "regular (A - B)"
+proof -
+  have "A - B = - (- A \<union> B)" by blast
+  moreover
+  have "regular (- (- A \<union> B))" 
+    using assms by blast
+  ultimately show "regular (A - B)" by simp
+qed
+
+lemma closure_intersection[intro]:
+  assumes "regular A" "regular B" 
+  shows "regular (A \<inter> B)"
+proof -
+  have "A \<inter> B = - (- A \<union> - B)" by blast
+  moreover
+  have "regular (- (- A \<union> - B))" 
+    using assms by blast
+  ultimately show "regular (A \<inter> B)" by simp
 qed
 
 
-lemma lang_star_cases2:
-  shows "[] \<notin> L \<Longrightarrow> L\<star> - {[]} =  L ; L\<star>"
-by (subst lang_star_cases)
-   (simp add: lang_seq_def)
-
-
-section {* Regular Expressions *}
-
-datatype rexp =
-  NULL
-| EMPTY
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-
-
-section {* Semantics of Regular Expressions *}
+text {* closure under string reversal *}
 
 fun
-  L :: "rexp \<Rightarrow> string set"
+  Rev :: "rexp \<Rightarrow> rexp"
 where
-  "L (NULL) = {}"
-| "L (EMPTY) = {[]}"
-| "L (CHAR c) = {[c]}"
-| "L (SEQ r1 r2) = (L r1) ; (L r2)"
-| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
-| "L (STAR r) = (L r)\<star>"
-
-abbreviation
-  CUNIV :: "string set"
-where
-  "CUNIV \<equiv> (\<lambda>x. [x]) ` (UNIV::char set)"
-
-lemma CUNIV_star_minus:
-  "(CUNIV\<star> - {[c]}) = {[]} \<union> (CUNIV - {[c]}; (CUNIV\<star>))"
-apply(subst lang_star_cases)
-apply(simp add: lang_seq_def)
-oops
-
+  "Rev NULL = NULL"
+| "Rev EMPTY = EMPTY"
+| "Rev (CHAR c) = CHAR c"
+| "Rev (ALT r1 r2) = ALT (Rev r1) (Rev r2)"
+| "Rev (SEQ r1 r2) = SEQ (Rev r2) (Rev r1)"
+| "Rev (STAR r) = STAR (Rev r)"
 
-lemma string_in_CUNIV:
-  shows "s \<in> CUNIV\<star>"
-proof (induct s)
-  case Nil
-  show "[] \<in> CUNIV\<star>" by (rule start)
-next
-  case (Cons c s)
-  have "[c] \<in> CUNIV" by simp
-  moreover
-  have "s \<in> CUNIV\<star>" by fact
-  ultimately have "[c] @ s \<in> CUNIV\<star>" by (rule step)
-  then show "c # s \<in> CUNIV\<star>" by simp
-qed
-
-lemma UNIV_CUNIV_star: 
-  shows "UNIV = CUNIV\<star>"
-using string_in_CUNIV
-by (auto)
-
-abbreviation 
-  reg :: "string set => bool"
-where
-  "reg L1 \<equiv> (\<exists>r. L r = L1)"
-
-lemma reg_null [intro]:
-  shows "reg {}"
-by (metis L.simps(1))
+lemma rev_Seq:
+  "(rev ` A) ;; (rev ` B) = rev ` (B ;; A)"
+unfolding Seq_def image_def
+apply(auto)
+apply(rule_tac x="xb @ xa" in exI)
+apply(auto)
+done
 
-lemma reg_empty [intro]:
-  shows "reg {[]}"
-by (metis L.simps(2))
-
-lemma reg_star [intro]:
-  shows "reg L1 \<Longrightarrow> reg (L1\<star>)"
-by (metis L.simps(6))
-
-lemma reg_seq [intro]:
-  assumes a: "reg L1" "reg L2"
-  shows "reg (L1 ; L2)"
+lemma rev_Star1:
+  assumes a: "s \<in> (rev ` A)\<star>"
+  shows "s \<in> rev ` (A\<star>)"
 using a
-by (metis L.simps(4)) 
-
-lemma reg_union [intro]:
-  assumes a: "reg L1" "reg L2"
-  shows "reg (L1 \<union> L2)"
-using a
-by (metis L.simps(5)) 
+proof(induct rule: star_induct)
+  case (step s1 s2)
+  have inj: "inj (rev::string \<Rightarrow> string)" unfolding inj_on_def by auto
+  have "s1 \<in> rev ` A" "s2 \<in> rev ` (A\<star>)" by fact+
+  then obtain x1 x2 where "x1 \<in> A" "x2 \<in> A\<star>" and eqs: "s1 = rev x1" "s2 = rev x2" by auto
+  then have "x1 \<in> A\<star>" "x2 \<in> A\<star>" by (auto intro: star_intro2)
+  then have "x2 @ x1 \<in> A\<star>" by (auto intro: star_intro1)
+  then have "rev (x2 @ x1) \<in> rev ` A\<star>" using inj by (simp only: inj_image_mem_iff)
+  then show "s1 @ s2 \<in>  rev ` A\<star>" using eqs by simp
+qed (auto)
 
-lemma reg_string [intro]:
-  fixes s::string
-  shows "reg {s}"
-proof (induct s)
-  case Nil
-  show "reg {[]}" by (rule reg_empty)
-next
-  case (Cons c s)
-  have "reg {s}" by fact
-  then obtain r where "L r = {s}" by auto
-  then have "L (SEQ (CHAR c) r) = {[c]} ; {s}" by simp
-  also have "\<dots> = {c # s}" by (simp add: lang_seq_def)
-  finally show "reg {c # s}" by blast 
-qed
+lemma rev_Star2:
+  assumes a: "s \<in> A\<star>"
+  shows "rev s \<in> (rev ` A)\<star>"
+using a
+proof(induct rule: star_induct)
+  case (step s1 s2)
+  have inj: "inj (rev::string \<Rightarrow> string)" unfolding inj_on_def by auto
+  have "s1 \<in> A"by fact
+  then have "rev s1 \<in> rev ` A" using inj by (simp only: inj_image_mem_iff)
+  then have "rev s1 \<in> (rev ` A)\<star>" by (auto intro: star_intro2)
+  moreover
+  have "rev s2 \<in> (rev ` A)\<star>" by fact
+  ultimately show "rev (s1 @ s2) \<in>  (rev ` A)\<star>" by (auto intro: star_intro1)
+qed (auto)
 
-lemma reg_finite [intro]:
-  assumes a: "finite L1"
-  shows "reg L1"
-using a
-proof(induct)
-  case empty
-  show "reg {}" by (rule reg_null)
-next
-  case (insert s S)
-  have "reg {s}" by (rule reg_string)
-  moreover 
-  have "reg S" by fact
-  ultimately have "reg ({s} \<union> S)" by (rule reg_union)
-  then show "reg (insert s S)" by simp
+lemma rev_Star:
+  "(rev ` A)\<star> = rev ` (A\<star>)"
+using rev_Star1 rev_Star2 by auto
+
+lemma rev_lang:
+  "L (Rev r) = rev ` (L r)"
+by (induct r) (simp_all add: rev_Star rev_Seq image_Un)
+
+lemma closure_reversal[intro]:
+  assumes "regular A"
+  shows "regular (rev ` A)"
+proof -
+  from assms obtain r::rexp where "L r = A" by auto
+  then have "L (Rev r) = rev ` A" by (simp add: rev_lang)
+  then show "regular (rev` A)" by blast
 qed
   
-lemma reg_cuniv [intro]:
-  shows "reg (CUNIV)"
-by (rule reg_finite) (auto)
 
-lemma reg_univ:
-  shows "reg (UNIV::string set)"
-proof -
-  have "reg CUNIV" by (rule reg_cuniv)
-  then have "reg (CUNIV\<star>)" by (rule reg_star)
-  then show "reg UNIV" by (simp add: UNIV_CUNIV_star)
-qed
-
-lemma reg_finite_subset:
-  assumes a: "finite L1"
-  and     b: "reg L1" "L2 \<subseteq> L1"
-  shows "reg L2"
-using a b
-apply(induct arbitrary: L2)
-apply(simp add: reg_empty)
-oops
-
-
-lemma reg_not:
-  shows "reg (UNIV - L r)"
-proof (induct r)
-  case NULL
-  have "reg UNIV" by (rule reg_univ)
-  then show "reg (UNIV - L NULL)" by simp
-next
-  case EMPTY
-  have "[] \<notin> CUNIV" by auto
-  moreover
-  have "reg (CUNIV; CUNIV\<star>)" by auto
-  ultimately have "reg (CUNIV\<star> - {[]})" 
-    using lang_star_cases2 by simp
-  then show "reg (UNIV - L EMPTY)" by (simp add: UNIV_CUNIV_star)
-next
-  case (CHAR c)
-  then show "?case"
-    apply(simp)
-   
-using reg_UNIV
-apply(simp)
-apply(simp add: char_star2[symmetric])
-apply(rule reg_seq)
-apply(rule reg_cuniv)
-apply(rule reg_star)
-apply(rule reg_cuniv)
-oops
-
-
-
-end    
-   
-
-
-
-  
-
-  
-  
-
-
+end
\ No newline at end of file
diff -r a8a442ba0dbf -r e93760534354 Derivs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Derivs.thy	Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,521 @@
+theory Derivs
+imports Closure
+begin
+
+section {* Experiments with Derivatives -- independent of Myhill-Nerode *}
+
+subsection {* Left-Quotients *}
+
+definition
+  Delta :: "lang \<Rightarrow> lang"
+where
+  "Delta A = (if [] \<in> A then {[]} else {})"
+
+definition
+  Der :: "char \<Rightarrow> lang \<Rightarrow> lang"
+where
+  "Der c A \<equiv> {s. [c] @ s \<in> A}"
+
+definition
+  Ders :: "string \<Rightarrow> lang \<Rightarrow> lang"
+where
+  "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+
+definition
+  Ders_set :: "lang \<Rightarrow> lang \<Rightarrow> lang"
+where
+  "Ders_set A B \<equiv> {s' | s s'. s @ s' \<in> B \<and> s \<in> A}"
+
+lemma Ders_set_Ders:
+  shows "Ders_set A B = (\<Union>s \<in> A. Ders s B)"
+unfolding Ders_set_def Ders_def
+by auto
+
+lemma Der_null [simp]:
+  shows "Der c {} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_empty [simp]:
+  shows "Der c {[]} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_char [simp]:
+  shows "Der c {[d]} = (if c = d then {[]} else {})"
+unfolding Der_def
+by auto
+
+lemma Der_union [simp]:
+  shows "Der c (A \<union> B) = Der c A \<union> Der c B"
+unfolding Der_def
+by auto
+
+lemma Der_seq [simp]:
+  shows "Der c (A ;; B) = (Der c A) ;; B \<union> (Delta A ;; Der c B)"
+unfolding Der_def Delta_def
+unfolding Seq_def
+by (auto simp add: Cons_eq_append_conv)
+
+lemma Der_star [simp]:
+  shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
+proof -
+  have incl: "Delta A ;; Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"
+    unfolding Der_def Delta_def Seq_def
+    apply(auto)
+    apply(drule star_decom)
+    apply(auto simp add: Cons_eq_append_conv)
+    done
+    
+  have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
+    by (simp only: star_cases[symmetric])
+  also have "... = Der c (A ;; A\<star>)"
+    by (simp only: Der_union Der_empty) (simp)
+  also have "... = (Der c A) ;; A\<star> \<union> (Delta A ;; Der c (A\<star>))"
+    by simp
+  also have "... =  (Der c A) ;; A\<star>"
+    using incl by auto
+  finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . 
+qed
+
+
+lemma Ders_singleton:
+  shows "Ders [c] A = Der c A"
+unfolding Der_def Ders_def
+by simp
+
+lemma Ders_append:
+  shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
+unfolding Ders_def by simp 
+
+lemma MN_Rel_Ders:
+  shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
+unfolding Ders_def str_eq_def str_eq_rel_def
+by auto
+
+subsection {* Brozowsky's derivatives of regular expressions *}
+
+fun
+  nullable :: "rexp \<Rightarrow> bool"
+where
+  "nullable (NULL) = False"
+| "nullable (EMPTY) = True"
+| "nullable (CHAR c) = False"
+| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
+| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
+| "nullable (STAR r) = True"
+
+fun
+  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
+where
+  "der c (NULL) = NULL"
+| "der c (EMPTY) = NULL"
+| "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
+| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
+| "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"
+| "der c (STAR r) = SEQ (der c r) (STAR r)"
+
+function 
+  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
+where
+  "ders [] r = r"
+| "ders (s @ [c]) r = der c (ders s r)"
+by (auto) (metis rev_cases)
+
+termination
+  by (relation "measure (length o fst)") (auto)
+
+lemma Delta_nullable:
+  shows "Delta (L r) = (if nullable r then {[]} else {})"
+unfolding Delta_def
+by (induct r) (auto simp add: Seq_def split: if_splits)
+
+lemma Der_der:
+  fixes r::rexp
+  shows "Der c (L r) = L (der c r)"
+by (induct r) (simp_all add: Delta_nullable)
+
+lemma Ders_ders:
+  fixes r::rexp
+  shows "Ders s (L r) = L (ders s r)"
+apply(induct s rule: rev_induct)
+apply(simp add: Ders_def)
+apply(simp only: ders.simps)
+apply(simp only: Ders_append)
+apply(simp only: Ders_singleton)
+apply(simp only: Der_der)
+done
+
+
+subsection {* Antimirov's Partial Derivatives *}
+
+abbreviation
+  "SEQS R r \<equiv> {SEQ r' r | r'. r' \<in> R}"
+
+fun
+  pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set"
+where
+  "pder c NULL = {NULL}"
+| "pder c EMPTY = {NULL}"
+| "pder c (CHAR c') = (if c = c' then {EMPTY} else {NULL})"
+| "pder c (ALT r1 r2) = (pder c r1) \<union> (pder c r2)"
+| "pder c (SEQ r1 r2) = SEQS (pder c r1) r2 \<union> (if nullable r1 then pder c r2 else {})"
+| "pder c (STAR r) = SEQS (pder c r) (STAR r)"
+
+abbreviation
+  "pder_set c R \<equiv> \<Union>r \<in> R. pder c r"
+
+function 
+  pders :: "string \<Rightarrow> rexp \<Rightarrow> rexp set"
+where
+  "pders [] r = {r}"
+| "pders (s @ [c]) r = pder_set c (pders s r)"
+by (auto) (metis rev_cases)
+
+termination
+  by (relation "measure (length o fst)") (auto)
+
+abbreviation
+  "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
+
+lemma pders_append:
+  "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
+apply(induct s2 arbitrary: s1 r rule: rev_induct)
+apply(simp)
+apply(subst append_assoc[symmetric])
+apply(simp only: pders.simps)
+apply(auto)
+done
+
+lemma pders_singleton:
+  "pders [c] r = pder c r"
+apply(subst append_Nil[symmetric])
+apply(simp only: pders.simps)
+apply(simp)
+done
+
+lemma pder_set_lang:
+  shows "(\<Union> (L ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L ` (pder c r)))"
+unfolding image_def 
+by auto
+
+lemma
+  shows seq_UNION_left:  "B ;; (\<Union>n\<in>C. A n) = (\<Union>n\<in>C. B ;; A n)"
+  and   seq_UNION_right: "(\<Union>n\<in>C. A n) ;; B = (\<Union>n\<in>C. A n ;; B)"
+unfolding Seq_def by auto
+
+lemma Der_pder:
+  fixes r::rexp
+  shows "Der c (L r) = \<Union> L ` (pder c r)"
+by (induct r) (auto simp add: Delta_nullable seq_UNION_right)
+
+lemma Ders_pders:
+  fixes r::rexp
+  shows "Ders s (L r) = \<Union> L ` (pders s r)"
+proof (induct s rule: rev_induct)
+  case (snoc c s)
+  have ih: "Ders s (L r) = \<Union> L ` (pders s r)" by fact
+  have "Ders (s @ [c]) (L r) = Ders [c] (Ders s (L r))"
+    by (simp add: Ders_append)
+  also have "\<dots> = Der c (\<Union> L ` (pders s r))" using ih
+    by (simp add: Ders_singleton)
+  also have "\<dots> = (\<Union>r\<in>pders s r. Der c (L r))" 
+    unfolding Der_def image_def by auto
+  also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> L `  (pder c r)))"
+    by (simp add: Der_pder)
+  also have "\<dots> = (\<Union>L ` (pder_set c (pders s r)))"
+    by (simp add: pder_set_lang)
+  also have "\<dots> = (\<Union>L ` (pders (s @ [c]) r))"
+    by simp
+  finally show "Ders (s @ [c]) (L r) = \<Union>L ` pders (s @ [c]) r" .
+qed (simp add: Ders_def)
+
+lemma Ders_set_pders_set:
+  fixes r::rexp
+  shows "Ders_set A (L r) = (\<Union> L ` (pders_set A r))"
+by (simp add: Ders_set_Ders Ders_pders)
+
+lemma pders_NULL [simp]:
+  shows "pders s NULL = {NULL}"
+by (induct s rule: rev_induct) (simp_all)
+
+lemma pders_EMPTY [simp]:
+  shows "pders s EMPTY = (if s = [] then {EMPTY} else {NULL})"
+by (induct s rule: rev_induct) (auto)
+
+lemma pders_CHAR [simp]:
+  shows "pders s (CHAR c) = (if s = [] then {CHAR c} else (if s = [c] then {EMPTY} else {NULL}))"
+by (induct s rule: rev_induct) (auto)
+
+lemma pders_ALT [simp]:
+  shows "pders s (ALT r1 r2) = (if s = [] then {ALT r1 r2} else (pders s r1) \<union> (pders s r2))"
+by (induct s rule: rev_induct) (auto)
+
+definition
+  "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
+
+lemma Suf:
+  shows "Suf (s @ [c]) = (Suf s) ;; {[c]} \<union> {[c]}"
+unfolding Suf_def Seq_def
+by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
+
+lemma Suf_Union:
+  shows "(\<Union>v \<in> Suf s ;; {[c]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))"
+by (auto simp add: Seq_def)
+
+lemma inclusion1:
+  shows "pder_set c (SEQS R r2) \<subseteq> SEQS (pder_set c R) r2 \<union> (pder c r2)"
+apply(auto simp add: if_splits)
+apply(blast)
+done
+
+lemma pders_SEQ:
+  shows "pders s (SEQ r1 r2) \<subseteq> SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"
+proof (induct s rule: rev_induct)
+  case (snoc c s)
+  have ih: "pders s (SEQ r1 r2) \<subseteq> SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" 
+    by fact
+  have "pders (s @ [c]) (SEQ r1 r2) = pder_set c (pders s (SEQ r1 r2))" by simp
+  also have "\<dots> \<subseteq> pder_set c (SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"
+    using ih by auto 
+  also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"
+    by (simp)
+  also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))"
+    by (simp)
+  also have "\<dots> \<subseteq> pder_set c (SEQS (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
+    by (auto)
+  also have "\<dots> \<subseteq> SEQS (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
+    using inclusion1 by blast
+  also have "\<dots> = SEQS (pders (s @ [c]) r1) r2 \<union> (\<Union>v \<in> Suf (s @ [c]). pders v r2)"
+    apply(subst (2) pders.simps)
+    apply(simp only: Suf)
+    apply(simp add: Suf_Union pders_singleton)
+    apply(auto)
+    done
+  finally show ?case .
+qed (simp)
+
+lemma pders_STAR:
+  assumes a: "s \<noteq> []"
+  shows "pders s (STAR r) \<subseteq> (\<Union>v \<in> Suf s. SEQS (pders v r) (STAR r))"
+using a
+proof (induct s rule: rev_induct)
+  case (snoc c s)
+  have ih: "s \<noteq> [] \<Longrightarrow> pders s (STAR r) \<subseteq> (\<Union>v\<in>Suf s. SEQS (pders v r) (STAR r))" by fact
+  { assume asm: "s \<noteq> []"
+    have "pders (s @ [c]) (STAR r) = pder_set c (pders s (STAR r))" by simp
+    also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. SEQS (pders v r) (STAR r)))"
+      using ih[OF asm] by blast
+    also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (SEQS (pders v r) (STAR r)))"
+      by simp
+    also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r) \<union> pder c (STAR r)))"
+      using inclusion1 by blast
+    also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r))) \<union> pder c (STAR r)"
+      using asm by (auto simp add: Suf_def)
+    also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (pders (v @ [c]) r) (STAR r))) \<union> (SEQS (pder c r) (STAR r))"
+      by simp
+    also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (SEQS (pders v r) (STAR r)))"
+      apply(simp only: Suf)
+      apply(simp add: Suf_Union pders_singleton)
+      apply(auto)
+      done
+    finally have ?case .
+  }
+  moreover
+  { assume asm: "s = []"
+    then have ?case
+      apply(simp add: pders_singleton Suf_def)
+      apply(auto)
+      apply(rule_tac x="[c]" in exI)
+      apply(simp add: pders_singleton)
+      done
+  }
+  ultimately show ?case by blast
+qed (simp)
+
+abbreviation 
+  "UNIV1 \<equiv> UNIV - {[]}"
+
+lemma pders_set_NULL:
+  shows "pders_set UNIV1 NULL = {NULL}"
+by auto
+
+lemma pders_set_EMPTY:
+  shows "pders_set UNIV1 EMPTY = {NULL}"
+by (auto split: if_splits)
+
+lemma pders_set_CHAR:
+  shows "pders_set UNIV1 (CHAR c) \<subseteq> {EMPTY, NULL}"
+by (auto split: if_splits)
+
+lemma pders_set_ALT:
+  shows "pders_set UNIV1 (ALT r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"
+by auto
+
+lemma pders_set_SEQ_aux:
+  assumes a: "s \<in> UNIV1"
+  shows "pders_set (Suf s) r2 \<subseteq> pders_set UNIV1 r2"
+using a by (auto simp add: Suf_def)
+
+lemma pders_set_SEQ:
+  shows "pders_set UNIV1 (SEQ r1 r2) \<subseteq> SEQS (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
+apply(rule UN_least)
+apply(rule subset_trans)
+apply(rule pders_SEQ)
+apply(simp)
+apply(rule conjI) 
+apply(auto)[1]
+apply(rule subset_trans)
+apply(rule pders_set_SEQ_aux)
+apply(auto)
+done
+
+lemma pders_set_STAR:
+  shows "pders_set UNIV1 (STAR r) \<subseteq> SEQS (pders_set UNIV1 r) (STAR r)"
+apply(rule UN_least)
+apply(rule subset_trans)
+apply(rule pders_STAR)
+apply(simp)
+apply(simp add: Suf_def)
+apply(auto)
+done
+
+lemma finite_SEQS:
+  assumes a: "finite A"
+  shows "finite (SEQS A r)"
+using a by (auto)
+
+lemma finite_pders_set_UNIV1:
+  shows "finite (pders_set UNIV1 r)"
+apply(induct r)
+apply(simp)
+apply(simp only: pders_set_EMPTY)
+apply(simp)
+apply(rule finite_subset)
+apply(rule pders_set_CHAR)
+apply(simp)
+apply(rule finite_subset)
+apply(rule pders_set_SEQ)
+apply(simp only: finite_SEQS finite_Un)
+apply(simp)
+apply(simp only: pders_set_ALT)
+apply(simp)
+apply(rule finite_subset)
+apply(rule pders_set_STAR)
+apply(simp only: finite_SEQS)
+done
+    
+lemma pders_set_UNIV_UNIV1:
+  shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"
+apply(auto)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+done
+
+lemma finite_pders_set_UNIV:
+  shows "finite (pders_set UNIV r)"
+unfolding pders_set_UNIV_UNIV1
+by (simp add: finite_pders_set_UNIV1)
+
+lemma finite_pders_set:
+  shows "finite (pders_set A r)"
+apply(rule rev_finite_subset)
+apply(rule_tac r="r" in finite_pders_set_UNIV)
+apply(auto)
+done
+
+lemma finite_pders:
+  shows "finite (pders s r)"
+using finite_pders_set[where A="{s}" and r="r"]
+by simp
+
+lemma finite_pders2:
+  shows "finite {pders s r | s. s \<in> A}"
+proof -
+  have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_set A r)" by auto
+  moreover
+  have "finite (Pow (pders_set A r))"
+    using finite_pders_set by simp
+  ultimately 
+  show "finite {pders s r | s. s \<in> A}"
+    by(rule finite_subset)
+qed
+
+
+lemma Myhill_Nerode3:
+  fixes r::"rexp"
+  shows "finite (UNIV // \<approx>(L r))"
+proof -
+  have "finite (UNIV // =(\<lambda>x. pders x r)=)"
+  proof - 
+    have "range (\<lambda>x. pders x r) \<subseteq> {pders s r | s. s \<in> UNIV}" by auto
+    moreover 
+    have "finite {pders s r | s. s \<in> UNIV}" by (rule finite_pders2)
+    ultimately
+    have "finite (range (\<lambda>x. pders x r))"
+      by (rule finite_subset)
+    then show "finite (UNIV // =(\<lambda>x. pders x r)=)" 
+      by (rule finite_eq_tag_rel)
+  qed
+  moreover 
+  have " =(\<lambda>x. pders x r)= \<subseteq> \<approx>(L r)"
+    unfolding tag_eq_rel_def
+    by (auto simp add: str_eq_def[symmetric] MN_Rel_Ders Ders_pders)
+  moreover 
+  have "equiv UNIV =(\<lambda>x. pders x r)="
+    unfolding equiv_def refl_on_def sym_def trans_def
+    unfolding tag_eq_rel_def
+    by auto
+  moreover
+  have "equiv UNIV (\<approx>(L r))"
+    unfolding equiv_def refl_on_def sym_def trans_def
+    unfolding str_eq_rel_def
+    by auto
+  ultimately show "finite (UNIV // \<approx>(L r))" 
+    by (rule refined_partition_finite)
+qed
+
+
+section {* Closure under Left-Quotients *}
+
+lemma closure_left_quotient:
+  assumes "regular A"
+  shows "regular (Ders_set B A)"
+proof -
+  from assms obtain r::rexp where eq: "L r = A" by auto
+  have fin: "finite (pders_set B r)" by (rule finite_pders_set)
+  
+  have "Ders_set B (L r) = (\<Union> L ` (pders_set B r))"
+    by (simp add: Ders_set_pders_set)
+  also have "\<dots> = L (\<Uplus>(pders_set B r))" using fin by simp
+  finally have "Ders_set B A = L (\<Uplus>(pders_set B r))" using eq
+    by simp
+  then show "regular (Ders_set B A)" by auto
+qed
+
+
+section {* Relating standard and partial derivations *}
+
+lemma
+  shows "(\<Union> L ` (pder c r)) = L (der c r)"
+unfolding Der_der[symmetric] Der_pder by simp
+
+lemma
+  shows "(\<Union> L ` (pders s r)) = L (ders s r)"
+unfolding Ders_ders[symmetric] Ders_pders by simp
+
+
+
+fun
+  width :: "rexp \<Rightarrow> nat"
+where
+  "width (NULL) = 0"
+| "width (EMPTY) = 0"
+| "width (CHAR c) = 1"
+| "width (ALT r1 r2) = width r1 + width r2"
+| "width (SEQ r1 r2) = width r1 + width r2"
+| "width (STAR r) = width r"
+
+
+ 
+end
\ No newline at end of file
diff -r a8a442ba0dbf -r e93760534354 IsaMakefile
--- a/IsaMakefile	Thu May 12 05:55:05 2011 +0000
+++ b/IsaMakefile	Wed May 18 19:54:43 2011 +0000
@@ -69,6 +69,20 @@
 	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
 	cp Paper/generated/root.pdf paper.pdf     
 
+## Journal Version
+
+session4: Journal/ROOT.ML \
+	Journal/document/root* \
+	Journal/*.thy
+	@$(USEDIR) -D generated -f ROOT.ML HOL Journal
+
+journal: session4
+	rm -f Journal/generated/*.aux # otherwise latex will fall over       
+	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
+	cd Journal/generated ; bibtex root
+	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+	cp Journal/generated/root.pdf journal.pdf     
+
 
 ## clean
 
diff -r a8a442ba0dbf -r e93760534354 Journal/Paper.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/Paper.thy	Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,1403 @@
+(*<*)
+theory Paper
+imports "../Derivs" "~~/src/HOL/Library/LaTeXsugar" 
+begin
+
+declare [[show_question_marks = false]]
+
+consts
+ REL :: "(string \<times> string) \<Rightarrow> bool"
+ UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
+
+abbreviation
+  "EClass x R \<equiv> R `` {x}"
+
+abbreviation 
+  "Append_rexp2 r_itm r \<equiv> Append_rexp r r_itm"
+
+
+notation (latex output)
+  str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
+  str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
+  Seq (infixr "\<cdot>" 100) and
+  Star ("_\<^bsup>\<star>\<^esup>") and
+  pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
+  Suc ("_+1" [100] 100) and
+  quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
+  REL ("\<approx>") and
+  UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
+  L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
+  Lam ("\<lambda>'(_')" [100] 100) and 
+  Trn ("'(_, _')" [100, 100] 100) and 
+  EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
+  transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
+  Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
+  Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
+  Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
+  uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
+  tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
+  tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
+  tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
+  tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
+  tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
+  tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)
+lemma meta_eq_app:
+  shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
+  by auto
+
+(*>*)
+
+
+section {* Introduction *}
+
+text {*
+  Regular languages are an important and well-understood subject in Computer
+  Science, with many beautiful theorems and many useful algorithms. There is a
+  wide range of textbooks on this subject, many of which are aimed at students
+  and contain very detailed `pencil-and-paper' proofs
+  (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by
+  formalising the theorems and by verifying formally the algorithms.
+
+  There is however a problem: the typical approach to regular languages is to
+  introduce finite automata and then define everything in terms of them.  For
+  example, a regular language is normally defined as one whose strings are
+  recognised by a finite deterministic automaton. This approach has many
+  benefits. Among them is the fact that it is easy to convince oneself that
+  regular languages are closed under complementation: one just has to exchange
+  the accepting and non-accepting states in the corresponding automaton to
+  obtain an automaton for the complement language.  The problem, however, lies with
+  formalising such reasoning in a HOL-based theorem prover, in our case
+  Isabelle/HOL. Automata are built up from states and transitions that 
+  need to be represented as graphs, matrices or functions, none
+  of which can be defined as an inductive datatype. 
+
+  In case of graphs and matrices, this means we have to build our own
+  reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
+  HOLlight support them with libraries. Even worse, reasoning about graphs and
+  matrices can be a real hassle in HOL-based theorem provers.  Consider for
+  example the operation of sequencing two automata, say $A_1$ and $A_2$, by
+  connecting the accepting states of $A_1$ to the initial state of $A_2$:\\[-5.5mm]  
+  %  
+  \begin{center}
+  \begin{tabular}{ccc}
+  \begin{tikzpicture}[scale=0.8]
+  %\draw[step=2mm] (-1,-1) grid (1,1);
+  
+  \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+  \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+
+  \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  
+  \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+  \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+  \draw (-0.6,0.0) node {\footnotesize$A_1$};
+  \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+  \end{tikzpicture}
+
+  & 
+
+  \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
+
+  &
+
+  \begin{tikzpicture}[scale=0.8]
+  %\draw[step=2mm] (-1,-1) grid (1,1);
+  
+  \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+  \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+
+  \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  
+  \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+  \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  
+  \draw (C) to [very thick, bend left=45] (B);
+  \draw (D) to [very thick, bend right=45] (B);
+
+  \draw (-0.6,0.0) node {\footnotesize$A_1$};
+  \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+  \end{tikzpicture}
+
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  On `paper' we can define the corresponding graph in terms of the disjoint 
+  union of the state nodes. Unfortunately in HOL, the standard definition for disjoint 
+  union, namely 
+  %
+  \begin{equation}\label{disjointunion}
+  @{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"}
+  \end{equation}
+
+  \noindent
+  changes the type---the disjoint union is not a set, but a set of pairs. 
+  Using this definition for disjoint union means we do not have a single type for automata
+  and hence will not be able to state certain properties about \emph{all}
+  automata, since there is no type quantification available in HOL (unlike in Coq, for example). An
+  alternative, which provides us with a single type for automata, is to give every 
+  state node an identity, for example a natural
+  number, and then be careful to rename these identities apart whenever
+  connecting two automata. This results in clunky proofs
+  establishing that properties are invariant under renaming. Similarly,
+  connecting two automata represented as matrices results in very adhoc
+  constructions, which are not pleasant to reason about.
+
+  Functions are much better supported in Isabelle/HOL, but they still lead to similar
+  problems as with graphs.  Composing, for example, two non-deterministic automata in parallel
+  requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98} 
+  dismisses for this the option of using identities, because it leads according to 
+  him to ``messy proofs''. He
+  opts for a variant of \eqref{disjointunion} using bit lists, but writes 
+
+  \begin{quote}
+  \it%
+  \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
+  `` & All lemmas appear obvious given a picture of the composition of automata\ldots
+       Yet their proofs require a painful amount of detail.''
+  \end{tabular}
+  \end{quote}
+
+  \noindent
+  and
+  
+  \begin{quote}
+  \it%
+  \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
+  `` & If the reader finds the above treatment in terms of bit lists revoltingly
+       concrete, I cannot disagree. A more abstract approach is clearly desirable.''
+  \end{tabular}
+  \end{quote}
+
+
+  \noindent
+  Moreover, it is not so clear how to conveniently impose a finiteness condition 
+  upon functions in order to represent \emph{finite} automata. The best is
+  probably to resort to more advanced reasoning frameworks, such as \emph{locales}
+  or \emph{type classes},
+  which are \emph{not} available in all HOL-based theorem provers.
+
+  {\bf add commnets from Brozowski}
+
+  Because of these problems to do with representing automata, there seems
+  to be no substantial formalisation of automata theory and regular languages 
+  carried out in HOL-based theorem provers. Nipkow  \cite{Nipkow98} establishes
+  the link between regular expressions and automata in
+  the context of lexing. Berghofer and Reiter \cite{BerghoferReiter09} 
+  formalise automata working over 
+  bit strings in the context of Presburger arithmetic.
+  The only larger formalisations of automata theory 
+  are carried out in Nuprl \cite{Constable00} and in Coq \cite{Filliatre97}.
+  
+  In this paper, we will not attempt to formalise automata theory in
+  Isabelle/HOL, but take a different approach to regular
+  languages. Instead of defining a regular language as one where there exists
+  an automaton that recognises all strings of the language, we define a
+  regular language as:
+
+  \begin{definition}
+  A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
+  strings of @{text "A"}.
+  \end{definition}
+  
+  \noindent
+  The reason is that regular expressions, unlike graphs, matrices and functions, can
+  be easily defined as inductive datatype. Consequently a corresponding reasoning 
+  infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation
+  of regular expression matching based on derivatives \cite{OwensSlind08} and
+  with an equivalence checker for regular expressions in Isabelle/HOL \cite{KraussNipkow11}.  
+  The purpose of this paper is to
+  show that a central result about regular languages---the Myhill-Nerode theorem---can 
+  be recreated by only using regular expressions. This theorem gives necessary
+  and sufficient conditions for when a language is regular. As a corollary of this
+  theorem we can easily establish the usual closure properties, including 
+  complementation, for regular languages.\smallskip
+  
+  \noindent
+  {\bf Contributions:} 
+  There is an extensive literature on regular languages.
+  To our best knowledge, our proof of the Myhill-Nerode theorem is the
+  first that is based on regular expressions, only. We prove the part of this theorem 
+  stating that a regular expression has only finitely many partitions using certain 
+  tagging-functions. Again to our best knowledge, these tagging-functions have
+  not been used before to establish the Myhill-Nerode theorem.
+*}
+
+section {* Preliminaries *}
+
+text {*
+  Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
+  being represented by the empty list, written @{term "[]"}.  \emph{Languages}
+  are sets of strings. The language containing all strings is written in
+  Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages 
+  is written @{term "A ;; B"} and a language raised to the power @{text n} is written 
+  @{term "A \<up> n"}. They are defined as usual
+
+  \begin{center}
+  @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
+  \hspace{7mm}
+  @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]}
+  \hspace{7mm}
+  @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
+  \end{center}
+
+  \noindent
+  where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}
+  is defined as the union over all powers, namely @{thm Star_def}. In the paper
+  we will make use of the following properties of these constructions.
+  
+  \begin{proposition}\label{langprops}\mbox{}\\
+  \begin{tabular}{@ {}ll}
+  (i)   & @{thm star_cases}     \\ 
+  (ii)  & @{thm[mode=IfThen] pow_length}\\
+  (iii) & @{thm seq_Union_left} \\ 
+  \end{tabular}
+  \end{proposition}
+
+  \noindent
+  In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
+  string; this property states that if \mbox{@{term "[] \<notin> A"}} then the lengths of
+  the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}.  We omit
+  the proofs for these properties, but invite the reader to consult our
+  formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}}
+
+  The notation in Isabelle/HOL for the quotient of a language @{text A} according to an 
+  equivalence relation @{term REL} is @{term "A // REL"}. We will write 
+  @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined 
+  as \mbox{@{text "{y | y \<approx> x}"}}.
+
+
+  Central to our proof will be the solution of equational systems
+  involving equivalence classes of languages. For this we will use Arden's Lemma \cite{Brzozowski64},
+  which solves equations of the form @{term "X = A ;; X \<union> B"} provided
+  @{term "[] \<notin> A"}. However we will need the following `reverse' 
+  version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A ;; X"} to
+  \mbox{@{term "X ;; A"}}).
+
+  \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
+  If @{thm (prem 1) arden} then
+  @{thm (lhs) arden} if and only if
+  @{thm (rhs) arden}.
+  \end{lemma}
+
+  \begin{proof}
+  For the right-to-left direction we assume @{thm (rhs) arden} and show
+  that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"} 
+  we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
+  which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both 
+  sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
+  is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. 
+
+  For the other direction we assume @{thm (lhs) arden}. By a simple induction
+  on @{text n}, we can establish the property
+
+  \begin{center}
+  @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
+  \end{center}
+  
+  \noindent
+  Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for
+  all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using the definition
+  of @{text "\<star>"}.
+  For the inclusion in the other direction we assume a string @{text s}
+  with length @{text k} is an element in @{text X}. Since @{thm (prem 1) arden}
+  we know by Prop.~\ref{langprops}@{text "(ii)"} that 
+  @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
+  (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). 
+  From @{text "(*)"} it follows then that
+  @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
+  implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"} 
+  this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
+  \end{proof}
+
+  \noindent
+  Regular expressions are defined as the inductive datatype
+
+  \begin{center}
+  @{text r} @{text "::="}
+  @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
+  @{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
+  @{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
+  @{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
+  @{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
+  @{term "STAR r"}
+  \end{center}
+
+  \noindent
+  and the language matched by a regular expression is defined as
+
+  \begin{center}
+  \begin{tabular}{c@ {\hspace{10mm}}c}
+  \begin{tabular}{rcl}
+  @{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\
+  @{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\
+  @{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\
+  \end{tabular}
+  &
+  \begin{tabular}{rcl}
+  @{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+       @{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+       @{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} &
+      @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\
+  \end{tabular}
+  \end{tabular}
+  \end{center}
+
+  Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating 
+  a regular expression that matches the union of all languages of @{text rs}. We only need to know the 
+  existence
+  of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
+  @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the 
+  set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs}
+  %
+  \begin{equation}\label{uplus}
+  \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
+  \end{equation}
+
+  \noindent
+  holds, whereby @{text "\<calL> ` rs"} stands for the 
+  image of the set @{text rs} under function @{text "\<calL>"}.
+*}
+
+
+section {* The Myhill-Nerode Theorem, First Part *}
+
+text {*
+  The key definition in the Myhill-Nerode theorem is the
+  \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two 
+  strings are related, provided there is no distinguishing extension in this
+  language. This can be defined as a tertiary relation.
+
+  \begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
+  @{text y} are Myhill-Nerode related provided
+  \begin{center}
+  @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
+  \end{center}
+  \end{definition}
+
+  \noindent
+  It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
+  partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
+  equivalence classes. To illustrate this quotient construction, let us give a simple 
+  example: consider the regular language containing just
+  the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
+  into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and  @{text "X\<^isub>3"}
+  as follows
+  
+  \begin{center}
+  @{text "X\<^isub>1 = {[]}"}\hspace{5mm}
+  @{text "X\<^isub>2 = {[c]}"}\hspace{5mm}
+  @{text "X\<^isub>3 = UNIV - {[], [c]}"}
+  \end{center}
+
+  One direction of the Myhill-Nerode theorem establishes 
+  that if there are finitely many equivalence classes, like in the example above, then 
+  the language is regular. In our setting we therefore have to show:
+  
+  \begin{theorem}\label{myhillnerodeone}
+  @{thm[mode=IfThen] Myhill_Nerode1}
+  \end{theorem}
+
+  \noindent
+  To prove this theorem, we first define the set @{term "finals A"} as those equivalence
+  classes from @{term "UNIV // \<approx>A"} that contain strings of @{text A}, namely
+  %
+  \begin{equation} 
+  @{thm finals_def}
+  \end{equation}
+
+  \noindent
+  In our running example, @{text "X\<^isub>2"} is the only 
+  equivalence class in @{term "finals {[c]}"}.
+  It is straightforward to show that in general @{thm lang_is_union_of_finals} and 
+  @{thm finals_in_partitions} hold. 
+  Therefore if we know that there exists a regular expression for every
+  equivalence class in \mbox{@{term "finals A"}} (which by assumption must be
+  a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression 
+  that matches every string in @{text A}.
+
+
+  Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a
+  regular expression for \emph{every} equivalence class, not just the ones 
+  in @{term "finals A"}. We
+  first define the notion of \emph{one-character-transition} between 
+  two equivalence classes
+  %
+  \begin{equation} 
+  @{thm transition_def}
+  \end{equation}
+
+  \noindent
+  which means that if we concatenate the character @{text c} to the end of all 
+  strings in the equivalence class @{text Y}, we obtain a subset of 
+  @{text X}. Note that we do not define an automaton here, we merely relate two sets
+  (with the help of a character). In our concrete example we have 
+  @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any 
+  other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
+  
+  Next we construct an \emph{initial equational system} that
+  contains an equation for each equivalence class. We first give
+  an informal description of this construction. Suppose we have 
+  the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
+  contains the empty string @{text "[]"} (since equivalence classes are disjoint).
+  Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
+  
+  \begin{center}
+  \begin{tabular}{rcl}
+  @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) + \<lambda>(EMPTY)"} \\
+  @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, CHAR c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, CHAR c\<^isub>2\<^isub>o)"} \\
+  & $\vdots$ \\
+  @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"}
+  stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
+  X\<^isub>i"}. 
+  %The intuition behind the equational system is that every 
+  %equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
+  %corresponds roughly to a state of an automaton whose name is @{text X\<^isub>i} and its predecessor states 
+  %are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these 
+  %predecessor states to @{text X\<^isub>i}. 
+  There can only be
+  finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side 
+  since by assumption there are only finitely many
+  equivalence classes and only finitely many characters.
+  The term @{text "\<lambda>(EMPTY)"} in the first equation acts as a marker for the initial state, that
+  is the equivalence class
+  containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
+  single `initial' state in the equational system, which is different from
+  the method by Brzozowski \cite{Brzozowski64}, where he marks the
+  `terminal' states. We are forced to set up the equational system in our
+  way, because the Myhill-Nerode relation determines the `direction' of the
+  transitions---the successor `state' of an equivalence class @{text Y} can
+  be reached by adding a character to the end of @{text Y}. This is also the
+  reason why we have to use our reverse version of Arden's Lemma.}
+  %In our initial equation system there can only be
+  %finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side 
+  %since by assumption there are only finitely many
+  %equivalence classes and only finitely many characters. 
+  Overloading the function @{text \<calL>} for the two kinds of terms in the
+  equational system, we have
+  
+  \begin{center}
+  @{text "\<calL>(Y, r) \<equiv>"} %
+  @{thm (rhs) L_rhs_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+  @{thm L_rhs_trm.simps(1)[where r="r", THEN eq_reflection]}
+  \end{center}
+
+  \noindent
+  and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
+  %
+  \begin{equation}\label{inv1}
+  @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
+  \end{equation}
+
+  \noindent
+  hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
+  %
+  \begin{equation}\label{inv2}
+  @{text "X\<^isub>1 = \<calL>(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
+  \end{equation}
+
+  \noindent
+  holds. The reason for adding the @{text \<lambda>}-marker to our initial equational system is 
+  to obtain this equation: it only holds with the marker, since none of 
+  the other terms contain the empty string. The point of the initial equational system is
+  that solving it means we will be able to extract a regular expression for every equivalence class. 
+
+  Our representation for the equations in Isabelle/HOL are pairs,
+  where the first component is an equivalence class (a set of strings)
+  and the second component
+  is a set of terms. Given a set of equivalence
+  classes @{text CS}, our initial equational system @{term "Init CS"} is thus 
+  formally defined as
+  %
+  \begin{equation}\label{initcs}
+  \mbox{\begin{tabular}{rcl}     
+  @{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} & 
+  @{text "if"}~@{term "[] \<in> X"}\\
+  & & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\
+  & & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
+  @{thm (lhs) Init_def}     & @{text "\<equiv>"} & @{thm (rhs) Init_def}
+  \end{tabular}}
+  \end{equation}
+
+  
+
+  \noindent
+  Because we use sets of terms 
+  for representing the right-hand sides of equations, we can 
+  prove \eqref{inv1} and \eqref{inv2} more concisely as
+  %
+  \begin{lemma}\label{inv}
+  If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
+  \end{lemma}
+
+  \noindent
+  Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
+  initial equational system into one in \emph{solved form} maintaining the invariant
+  in Lem.~\ref{inv}. From the solved form we will be able to read
+  off the regular expressions. 
+
+  In order to transform an equational system into solved form, we have two 
+  operations: one that takes an equation of the form @{text "X = rhs"} and removes
+  any recursive occurrences of @{text X} in the @{text rhs} using our variant of Arden's 
+  Lemma. The other operation takes an equation @{text "X = rhs"}
+  and substitutes @{text X} throughout the rest of the equational system
+  adjusting the remaining regular expressions appropriately. To define this adjustment 
+  we define the \emph{append-operation} taking a term and a regular expression as argument
+
+  \begin{center}
+  @{thm Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+  @{thm Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+  \end{center}
+
+  \noindent
+  We lift this operation to entire right-hand sides of equations, written as
+  @{thm (lhs) Append_rexp_rhs_def[where rexp="r"]}. With this we can define
+  the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
+  %
+  \begin{equation}\label{arden_def}
+  \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+  @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\ 
+   & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+   & & @{text "r' ="}   & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
+   & &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\ 
+  \end{tabular}}
+  \end{equation}
+
+  \noindent
+  In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
+  then we calculate the combined regular expressions for all @{text r} coming 
+  from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
+  finally we append this regular expression to @{text rhs'}. It can be easily seen 
+  that this operation mimics Arden's Lemma on the level of equations. To ensure
+  the non-emptiness condition of Arden's Lemma we say that a right-hand side is
+  @{text ardenable} provided
+
+  \begin{center}
+  @{thm ardenable_def}
+  \end{center}
+
+  \noindent
+  This allows us to prove a version of Arden's Lemma on the level of equations.
+
+  \begin{lemma}\label{ardenable}
+  Given an equation @{text "X = rhs"}.
+  If @{text "X = \<Union>\<calL> ` rhs"},
+  @{thm (prem 2) Arden_keeps_eq}, and
+  @{thm (prem 3) Arden_keeps_eq}, then
+  @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
+  \end{lemma}
+  
+  \noindent
+  Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
+  but we can still ensure that it holds troughout our algorithm of transforming equations
+  into solved form. The \emph{substitution-operation} takes an equation
+  of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
+
+  \begin{center}
+  \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+  @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\ 
+   & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+   & & @{text "r' ="}   & @{term "\<Uplus> {r. Trn X r \<in> rhs}"}\\
+   & &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> append_rhs_rexp xrhs r'"}}\\ 
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  We again delete first all occurrences of @{text "(X, r)"} in @{text rhs}; we then calculate
+  the regular expression corresponding to the deleted terms; finally we append this
+  regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
+  the substitution operation we will arrange it so that @{text "xrhs"} does not contain
+  any occurrence of @{text X}.
+
+  With these two operations in place, we can define the operation that removes one equation
+  from an equational systems @{text ES}. The operation @{const Subst_all}
+  substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES}; 
+  @{const Remove} then completely removes such an equation from @{text ES} by substituting 
+  it to the rest of the equational system, but first eliminating all recursive occurrences
+  of @{text X} by applying @{const Arden} to @{text "xrhs"}.
+
+  \begin{center}
+  \begin{tabular}{rcl}
+  @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\
+  @{thm (lhs) Remove_def}    & @{text "\<equiv>"} & @{thm (rhs) Remove_def}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  Finally, we can define how an equational system should be solved. For this 
+  we will need to iterate the process of eliminating equations until only one equation
+  will be left in the system. However, we do not just want to have any equation
+  as being the last one, but the one involving the equivalence class for 
+  which we want to calculate the regular 
+  expression. Let us suppose this equivalence class is @{text X}. 
+  Since @{text X} is the one to be solved, in every iteration step we have to pick an
+  equation to be eliminated that is different from @{text X}. In this way 
+  @{text X} is kept to the final step. The choice is implemented using Hilbert's choice 
+  operator, written @{text SOME} in the definition below.
+  
+  \begin{center}
+  \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
+  @{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\ 
+   & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\
+   & &  \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\ 
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The last definition we need applies @{term Iter} over and over until a condition 
+  @{text Cond} is \emph{not} satisfied anymore. This condition states that there
+  are more than one equation left in the equational system @{text ES}. To solve
+  an equational system we use Isabelle/HOL's @{text while}-operator as follows:
+  
+  \begin{center}
+  @{thm Solve_def}
+  \end{center}
+
+  \noindent
+  We are not concerned here with the definition of this operator
+  (see Berghofer and Nipkow \cite{BerghoferNipkow00}), but note that we eliminate
+  in each @{const Iter}-step a single equation, and therefore 
+  have a well-founded termination order by taking the cardinality 
+  of the equational system @{text ES}. This enables us to prove
+  properties about our definition of @{const Solve} when we `call' it with
+  the equivalence class @{text X} and the initial equational system 
+  @{term "Init (UNIV // \<approx>A)"} from
+  \eqref{initcs} using the principle:
+  %
+  \begin{equation}\label{whileprinciple}
+  \mbox{\begin{tabular}{l}
+  @{term "invariant (Init (UNIV // \<approx>A))"} \\
+  @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\
+  @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\
+  @{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\
+  \hline
+  \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}}
+  \end{tabular}}
+  \end{equation}
+
+  \noindent
+  This principle states that given an invariant (which we will specify below) 
+  we can prove a property
+  @{text "P"} involving @{const Solve}. For this we have to discharge the following
+  proof obligations: first the
+  initial equational system satisfies the invariant; second the iteration
+  step @{text "Iter"} preserves the invariant as long as the condition @{term Cond} holds;
+  third @{text "Iter"} decreases the termination order, and fourth that
+  once the condition does not hold anymore then the property @{text P} must hold.
+
+  The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
+  returns with a single equation @{text "X = xrhs"} for some @{text "xrhs"}, and
+  that this equational system still satisfies the invariant. In order to get
+  the proof through, the invariant is composed of the following six properties:
+
+  \begin{center}
+  \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}}
+  @{text "invariant ES"} & @{text "\<equiv>"} &
+      @{term "finite ES"} & @{text "(finiteness)"}\\
+  & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
+  & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
+  & @{text "\<and>"} & @{thm (rhs) distinctness_def}\\
+  &             &  & @{text "(distinctness)"}\\
+  & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\   
+  & @{text "\<and>"} & @{thm (rhs) validity_def} & @{text "(validity)"}\\
+  \end{tabular}
+  \end{center}
+ 
+  \noindent
+  The first two ensure that the equational system is always finite (number of equations
+  and number of terms in each equation); the third makes sure the `meaning' of the 
+  equations is preserved under our transformations. The other properties are a bit more
+  technical, but are needed to get our proof through. Distinctness states that every
+  equation in the system is distinct. @{text Ardenable} ensures that we can always
+  apply the @{text Arden} operation. 
+  The last property states that every @{text rhs} can only contain equivalence classes
+  for which there is an equation. Therefore @{text lhss} is just the set containing 
+  the first components of an equational system,
+  while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the 
+  form @{term "Trn X r"}. That means formally @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"} 
+  and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}.
+  
+
+  It is straightforward to prove that the initial equational system satisfies the
+  invariant.
+
+  \begin{lemma}\label{invzero}
+  @{thm[mode=IfThen] Init_ES_satisfies_invariant}
+  \end{lemma}
+
+  \begin{proof}
+  Finiteness is given by the assumption and the way how we set up the 
+  initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
+  follows from the fact that the equivalence classes are disjoint. The @{text ardenable}
+  property also follows from the setup of the initial equational system, as does 
+  validity.\qed
+  \end{proof}
+
+  \noindent
+  Next we show that @{text Iter} preserves the invariant.
+
+  \begin{lemma}\label{iterone}
+  @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
+  \end{lemma}
+
+  \begin{proof} 
+  The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
+  and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"} 
+  preserves the invariant.
+  We prove this as follows:
+
+  \begin{center}
+  @{text "\<forall> ES."} @{thm (prem 1) Subst_all_satisfies_invariant} implies
+  @{thm (concl) Subst_all_satisfies_invariant}
+  \end{center}
+
+  \noindent
+  Finiteness is straightforward, as the @{const Subst} and @{const Arden} operations 
+  keep the equational system finite. These operations also preserve soundness 
+  and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
+  The property @{text ardenable} is clearly preserved because the append-operation
+  cannot make a regular expression to match the empty string. Validity is
+  given because @{const Arden} removes an equivalence class from @{text yrhs}
+  and then @{const Subst_all} removes @{text Y} from the equational system.
+  Having proved the implication above, we can instantiate @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
+  which matches with our proof-obligation of @{const "Subst_all"}. Since
+  \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use the assumption 
+  to complete the proof.\qed 
+  \end{proof}
+
+  \noindent
+  We also need the fact that @{text Iter} decreases the termination measure.
+
+  \begin{lemma}\label{itertwo}
+  @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
+  \end{lemma}
+
+  \begin{proof}
+  By assumption we know that @{text "ES"} is finite and has more than one element.
+  Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with 
+  @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
+  that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
+  removes the equation @{text "Y = yrhs"} from the system, and therefore 
+  the cardinality of @{const Iter} strictly decreases.\qed
+  \end{proof}
+
+  \noindent
+  This brings us to our property we want to establish for @{text Solve}.
+
+
+  \begin{lemma}
+  If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
+  a @{text rhs} such that  @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
+  and @{term "invariant {(X, rhs)}"}.
+  \end{lemma}
+
+  \begin{proof} 
+  In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
+  stronger invariant since Lem.~\ref{iterone} and \ref{itertwo} have the precondition 
+  that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed
+  in order to choose in the @{const Iter}-step an equation that is not \mbox{@{term "X = rhs"}}.
+  Therefore our invariant cannot be just @{term "invariant ES"}, but must be 
+  @{term "invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"}. By assumption 
+  @{thm (prem 2) Solve} and Lem.~\ref{invzero}, the more general invariant holds for
+  the initial equational system. This is premise 1 of~\eqref{whileprinciple}.
+  Premise 2 is given by Lem.~\ref{iterone} and the fact that @{const Iter} might
+  modify the @{text rhs} in the equation @{term "X = rhs"}, but does not remove it.
+  Premise 3 of~\eqref{whileprinciple} is by Lem.~\ref{itertwo}. Now in premise 4
+  we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"}
+  and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"}
+  does not holds. By the stronger invariant we know there exists such a @{text "rhs"}
+  with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
+  of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the set @{text "{(X, rhs)}"},
+  for which the invariant holds. This allows us to conclude that 
+  @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold,
+  as needed.\qed
+  \end{proof}
+
+  \noindent
+  With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
+  there exists a regular expression.
+
+  \begin{lemma}\label{every_eqcl_has_reg}
+  @{thm[mode=IfThen] every_eqcl_has_reg}
+  \end{lemma}
+
+  \begin{proof}
+  By the preceding lemma, we know that there exists a @{text "rhs"} such
+  that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
+  and that the invariant holds for this equation. That means we 
+  know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
+  this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the 
+  invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
+  we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the @{text Arden} operation
+  removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
+  This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
+  So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = L (\<Uplus>rs)"}.
+  With this we can conclude the proof.\qed
+  \end{proof}
+
+  \noindent
+  Lem.~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
+  of the Myhill-Nerode theorem.
+
+  \begin{proof}[of Thm.~\ref{myhillnerodeone}]
+  By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular expression for
+  every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
+  a subset of  @{term "UNIV // \<approx>A"}, we also know that for every equivalence class
+  in @{term "finals A"} there exists a regular expression. Moreover by assumption 
+  we know that @{term "finals A"} must be finite, and therefore there must be a finite
+  set of regular expressions @{text "rs"} such that
+  @{term "\<Union>(finals A) = L (\<Uplus>rs)"}.
+  Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"} 
+  as the regular expression that is needed in the theorem.\qed
+  \end{proof}
+*}
+
+
+
+
+section {* Myhill-Nerode, Second Part *}
+
+text {*
+  We will prove in this section the second part of the Myhill-Nerode
+  theorem. It can be formulated in our setting as follows:
+
+  \begin{theorem}
+  Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
+  \end{theorem}  
+
+  \noindent
+  The proof will be by induction on the structure of @{text r}. It turns out
+  the base cases are straightforward.
+
+
+  \begin{proof}[Base Cases]
+  The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because 
+  we can easily establish that
+
+  \begin{center}
+  \begin{tabular}{l}
+  @{thm quot_null_eq}\\
+  @{thm quot_empty_subset}\\
+  @{thm quot_char_subset}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed
+  \end{proof}
+
+  \noindent
+  Much more interesting, however, are the inductive cases. They seem hard to solve 
+  directly. The reader is invited to try. 
+
+  Our proof will rely on some
+  \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will 
+  be easy to prove that the \emph{range} of these tagging-functions is finite
+  (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}).
+  With this we will be able to infer that the tagging-functions, seen as relations,
+  give rise to finitely many equivalence classes of @{const UNIV}. Finally we 
+  will show that the tagging-relations are more refined than @{term "\<approx>(L r)"}, which
+  implies that @{term "UNIV // \<approx>(L r)"} must also be finite (a relation @{text "R\<^isub>1"} 
+  is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}).
+  We formally define the notion of a \emph{tagging-relation} as follows.
+
+  \begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
+  and @{text y} are \emph{tag-related} provided
+  \begin{center}
+  @{text "x =tag= y \<equiv> tag x = tag y"}\;.
+  \end{center}
+  \end{definition}
+
+
+  In order to establish finiteness of a set @{text A}, we shall use the following powerful
+  principle from Isabelle/HOL's library.
+  %
+  \begin{equation}\label{finiteimageD}
+  @{thm[mode=IfThen] finite_imageD}
+  \end{equation}
+
+  \noindent
+  It states that if an image of a set under an injective function @{text f} (injective over this set) 
+  is finite, then the set @{text A} itself must be finite. We can use it to establish the following 
+  two lemmas.
+
+  \begin{lemma}\label{finone}
+  @{thm[mode=IfThen] finite_eq_tag_rel}
+  \end{lemma}
+
+  \begin{proof}
+  We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
+  @{text "range f"} to be a subset of @{term "Pow (range tag)"}, which we know must be
+  finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"},
+  and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
+  assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
+  From the assumptions we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with 
+  @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in 
+  turn means that the equivalence classes @{text X}
+  and @{text Y} must be equal.\qed
+  \end{proof}
+
+  \begin{lemma}\label{fintwo} 
+  Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
+  @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
+  If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+  then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
+  \end{lemma}
+
+  \begin{proof}
+  We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
+  be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that 
+  @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^isub>1)"},
+  which is finite by assumption. What remains to be shown is that @{text f} is injective
+  on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence 
+  classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
+  @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
+  @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
+  We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {x}"}}. 
+  From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
+  and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
+  such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
+  are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
+  they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
+  \end{proof}
+
+  \noindent
+  Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
+  that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging-function whose
+  range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
+  Let us attempt the @{const ALT}-case first.
+
+  \begin{proof}[@{const "ALT"}-Case] 
+  We take as tagging-function 
+  %
+  \begin{center}
+  @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
+  \end{center}
+
+  \noindent
+  where @{text "A"} and @{text "B"} are some arbitrary languages.
+  We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+  then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
+  @{term "tag_str_ALT A B"} is a subset of this product set---so finite. It remains to be shown
+  that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to 
+  showing
+  %
+  \begin{center}
+  @{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
+  \end{center}
+  %
+  \noindent
+  which by unfolding the Myhill-Nerode relation is identical to
+  %
+  \begin{equation}\label{pattern}
+  @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
+  \end{equation}
+  %
+  \noindent
+  since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
+  \eqref{pattern} we just have to unfold the definition of the tagging-function and analyse 
+  in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. 
+  The definition of the tagging-function will give us in each case the
+  information to infer that @{text "y @ z \<in> A \<union> B"}.
+  Finally we
+  can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
+  \end{proof}
+
+
+  \noindent
+  The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
+  they are slightly more complicated. In the @{const SEQ}-case we essentially have
+  to be able to infer that 
+  %
+  \begin{center}
+  @{text "\<dots>"}@{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+  \end{center}
+  %
+  \noindent
+  using the information given by the appropriate tagging-function. The complication 
+  is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}
+  (this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the
+  notions of \emph{string prefixes} 
+  %
+  \begin{center}
+  @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
+  @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
+  \end{center}
+  %
+  \noindent
+  and \emph{string subtraction}:
+  %
+  \begin{center}
+  @{text "[] - y \<equiv> []"}\hspace{10mm}
+  @{text "x - [] \<equiv> x"}\hspace{10mm}
+  @{text "cx - dy \<equiv> if c = d then x - y else cx"}
+  \end{center}
+  %
+  \noindent
+  where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. 
+  
+  Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split' 
+  this string to be in @{term "A ;; B"}:
+  %
+  \begin{center}
+  \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+  \scalebox{0.7}{
+  \begin{tikzpicture}
+    \node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+               node[midway, above=0.5em]{@{text x}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (z.north west) -- ($(z.north east)+(0em,0em)$)
+               node[midway, above=0.5em]{@{text z}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+               node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{term "x' \<in> A"}};
+  \end{tikzpicture}}
+  &
+  \scalebox{0.7}{
+  \begin{tikzpicture}
+    \node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z - z'"}\hspace{2.6em}$  };
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (x.north west) -- ($(za.north west)+(0em,0em)$)
+               node[midway, above=0.5em]{@{text x}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
+               node[midway, above=0.5em]{@{text z}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
+               node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
+  \end{tikzpicture}}
+  \end{tabular}
+  \end{center}
+  %
+  \noindent
+  Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture),
+  or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).
+  In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the 
+  following tagging-function
+  %
+  \begin{center}
+  @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
+  \end{center}
+
+  \noindent
+  with the idea that in the first split we have to make sure that @{text "(x - x') @ z"}
+  is in the language @{text B}.
+
+  \begin{proof}[@{const SEQ}-Case]
+  If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+  then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
+  @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.
+  We have to show injectivity of this tagging-function as
+  %
+  \begin{center}
+  @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+  \end{center}
+  %
+  \noindent
+  There are two cases to be considered (see pictures above). First, there exists 
+  a @{text "x'"} such that
+  @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have
+  %
+  \begin{center}
+  @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}
+  \end{center}
+  %
+  \noindent
+  and by the assumption about @{term "tag_str_SEQ A B"} also 
+  %
+  \begin{center}
+  @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
+  \end{center}
+  %
+  \noindent
+  That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and 
+  @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
+  @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode
+  relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we
+  have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore
+  @{term "y @ z \<in> A ;; B"}, as needed in this case.
+
+  Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
+  By the assumption about @{term "tag_str_SEQ A B"} we have
+  @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
+  relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case
+  with @{term "y @ z \<in> A ;; B"}. We again can complete the @{const SEQ}-case
+  by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed 
+  \end{proof}
+  
+  \noindent
+  The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When
+  we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the 
+  empty string, we 
+  have the following picture:
+  %
+  \begin{center}
+  \scalebox{0.7}{
+  \begin{tikzpicture}
+    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{4em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{0.5em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ };
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+               node[midway, above=0.5em]{@{text x}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (za.north west) -- ($(zb.north east)+(0em,0em)$)
+               node[midway, above=0.5em]{@{text z}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
+               node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{term "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
+               node[midway, below=0.5em]{@{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
+  \end{tikzpicture}}
+  \end{center}
+  %
+  \noindent
+  We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},
+  @{text "x' < x"} and the rest @{term "(x - x') @ z \<in> A\<star>"}. For example the empty string 
+  @{text "[]"} would do.
+  There are potentially many such prefixes, but there can only be finitely many of them (the 
+  string @{text x} is finite). Let us therefore choose the longest one and call it 
+  @{text "x'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we
+  know it is in @{term "A\<star>"}. By definition of @{term "A\<star>"}, we can separate
+  this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
+  and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"},
+  otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a}
+  `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and
+   @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and
+  @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
+  such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the
+  `border' of @{text x} and @{text z}. This string is @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a"}.
+
+  In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
+  the following tagging-function:
+  %
+  \begin{center}
+  @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
+  \end{center}
+
+  \begin{proof}[@{const STAR}-Case]
+  If @{term "finite (UNIV // \<approx>A)"} 
+  then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
+  @{term "tag_str_STAR A"} is a subset of this set, and therefore finite.
+  Again we have to show injectivity of this tagging-function as  
+  %
+  \begin{center}
+  @{term "\<forall>z. tag_str_STAR A x = tag_str_STAR A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
+  \end{center}  
+  %
+  \noindent
+  We first need to consider the case that @{text x} is the empty string.
+  From the assumption we can infer @{text y} is the empty string and
+  clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
+  string, we can divide the string @{text "x @ z"} as shown in the picture 
+  above. By the tagging-function we have
+  %
+  \begin{center}
+  @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"}
+  \end{center}
+  %
+  \noindent
+  which by assumption is equal to
+  %
+  \begin{center}
+  @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"}
+  \end{center}
+  %
+  \noindent 
+  and we know that we have a @{term "y' \<in> A\<star>"} and @{text "y' < y"}
+  and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode
+  relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
+  Therefore @{term "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
+  @{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{term "L r"} and
+  complete the proof.\qed
+  \end{proof}
+*}
+
+section {* Second Part based on Partial Derivatives *}
+
+text {*
+   We briefly considered using the method Brzozowski presented in the
+  Appendix of~\cite{Brzozowski64} in order to prove the second
+  direction of the Myhill-Nerode theorem. There he calculates the
+  derivatives for regular expressions and shows that for every
+  language there can be only finitely many of them %derivations (if
+  regarded equal modulo ACI). We could have used as tagging-function
+  the set of derivatives of a regular expression with respect to a
+  language.  Using the fact that two strings are Myhill-Nerode related
+  whenever their derivative is the same, together with the fact that
+  there are only finitely such derivatives would give us a similar
+  argument as ours. However it seems not so easy to calculate the set
+  of derivatives modulo ACI. Therefore we preferred our direct method
+  of using tagging-functions. 
+
+*}
+
+section {* Closure Properties *}
+
+
+section {* Conclusion and Related Work *}
+
+text {*
+  In this paper we took the view that a regular language is one where there
+  exists a regular expression that matches all of its strings. Regular
+  expressions can conveniently be defined as a datatype in HOL-based theorem
+  provers. For us it was therefore interesting to find out how far we can push
+  this point of view. We have established in Isabelle/HOL both directions 
+  of the Myhill-Nerode theorem.
+  %
+  \begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\
+  A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
+  \end{theorem}
+  %
+  \noindent
+  Having formalised this theorem means we
+  pushed our point of view quite far. Using this theorem we can obviously prove when a language
+  is \emph{not} regular---by establishing that it has infinitely many
+  equivalence classes generated by the Myhill-Nerode relation (this is usually
+  the purpose of the pumping lemma \cite{Kozen97}).  We can also use it to
+  establish the standard textbook results about closure properties of regular
+  languages. Interesting is the case of closure under complement, because
+  it seems difficult to construct a regular expression for the complement
+  language by direct means. However the existence of such a regular expression
+  can be easily proved using the Myhill-Nerode theorem since 
+  %
+  \begin{center}
+  @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
+  \end{center}
+  %
+  \noindent
+  holds for any strings @{text "s\<^isub>1"} and @{text
+  "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
+  partitions.  Proving the existence of such a regular expression via automata 
+  using the standard method would 
+  be quite involved. It includes the
+  steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
+  "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
+  regular expression.
+
+  While regular expressions are convenient in formalisations, they have some
+  limitations. One is that there seems to be no method of calculating a
+  minimal regular expression (for example in terms of length) for a regular
+  language, like there is
+  for automata. On the other hand, efficient regular expression matching,
+  without using automata, poses no problem \cite{OwensReppyTuron09}.
+  For an implementation of a simple regular expression matcher,
+  whose correctness has been formally established, we refer the reader to
+  Owens and Slind \cite{OwensSlind08}.
+
+
+  Our formalisation consists of 780 lines of Isabelle/Isar code for the first
+  direction and 460 for the second, plus around 300 lines of standard material about
+  regular languages. While this might be seen as too large to count as a
+  concise proof pearl, this should be seen in the context of the work done by
+  Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem
+  in Nuprl using automata. They write that their four-member team needed
+  something on the magnitude of 18 months for their formalisation. The
+  estimate for our formalisation is that we needed approximately 3 months and
+  this included the time to find our proof arguments. Unlike Constable et al,
+  who were able to follow the proofs from \cite{HopcroftUllman69}, we had to
+  find our own arguments.  So for us the formalisation was not the
+  bottleneck. It is hard to gauge the size of a formalisation in Nurpl, but
+  from what is shown in the Nuprl Math Library about their development it
+  seems substantially larger than ours. The code of ours can be found in the
+  Mercurial Repository at
+  \mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
+
+
+  Our proof of the first direction is very much inspired by \emph{Brzozowski's
+  algebraic method} used to convert a finite automaton to a regular
+  expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence
+  classes as the states of the minimal automaton for the regular language.
+  However there are some subtle differences. Since we identify equivalence
+  classes with the states of the automaton, then the most natural choice is to
+  characterise each state with the set of strings starting from the initial
+  state leading up to that state. Usually, however, the states are characterised as the
+  strings starting from that state leading to the terminal states.  The first
+  choice has consequences about how the initial equational system is set up. We have
+  the $\lambda$-term on our `initial state', while Brzozowski has it on the
+  terminal states. This means we also need to reverse the direction of Arden's
+  Lemma.
+
+  This is also where our method shines, because we can completely
+  side-step the standard argument \cite{Kozen97} where automata need
+  to be composed, which as stated in the Introduction is not so easy
+  to formalise in a HOL-based theorem prover. However, it is also the
+  direction where we had to spend most of the `conceptual' time, as
+  our proof-argument based on tagging-functions is new for
+  establishing the Myhill-Nerode theorem. All standard proofs of this
+  direction proceed by arguments over automata.\medskip
+  
+  \noindent
+  {\bf Acknowledgements:} We are grateful for the comments we received from Larry
+  Paulson.
+
+*}
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff -r a8a442ba0dbf -r e93760534354 Journal/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/ROOT.ML	Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,6 @@
+no_document use_thy "../Myhill";
+no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
+no_document use_thy "../Derivs";
+no_document use_thy "../Closure";
+
+use_thy "Paper"
\ No newline at end of file
diff -r a8a442ba0dbf -r e93760534354 Journal/document/llncs.cls
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/llncs.cls	Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,1189 @@
+% LLNCS DOCUMENT CLASS -- version 2.13 (28-Jan-2002)
+% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
+%
+%%
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%%   Dollar        \$     Percent       \%     Ampersand     \&
+%%   Acute accent  \'     Left paren    \(     Right paren   \)
+%%   Asterisk      \*     Plus          \+     Comma         \,
+%%   Minus         \-     Point         \.     Solidus       \/
+%%   Colon         \:     Semicolon     \;     Less than     \<
+%%   Equals        \=     Greater than  \>     Question mark \?
+%%   Commercial at \@     Left bracket  \[     Backslash     \\
+%%   Right bracket \]     Circumflex    \^     Underscore    \_
+%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%%   Right brace   \}     Tilde         \~}
+%%
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{llncs}[2002/01/28 v2.13
+^^J LaTeX document class for Lecture Notes in Computer Science]
+% Options
+\let\if@envcntreset\iffalse
+\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
+\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
+\DeclareOption{oribibl}{\let\oribibl=Y}
+\let\if@custvec\iftrue
+\DeclareOption{orivec}{\let\if@custvec\iffalse}
+\let\if@envcntsame\iffalse
+\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
+\let\if@envcntsect\iffalse
+\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
+\let\if@runhead\iffalse
+\DeclareOption{runningheads}{\let\if@runhead\iftrue}
+
+\let\if@openbib\iffalse
+\DeclareOption{openbib}{\let\if@openbib\iftrue}
+
+% languages
+\let\switcht@@therlang\relax
+\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
+\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
+
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
+
+\ProcessOptions
+
+\LoadClass[twoside]{article}
+\RequirePackage{multicol} % needed for the list of participants, index
+
+\setlength{\textwidth}{12.2cm}
+\setlength{\textheight}{19.3cm}
+\renewcommand\@pnumwidth{2em}
+\renewcommand\@tocrmarg{3.5em}
+%
+\def\@dottedtocline#1#2#3#4#5{%
+  \ifnum #1>\c@tocdepth \else
+    \vskip \z@ \@plus.2\p@
+    {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
+               \parfillskip -\rightskip \pretolerance=10000
+     \parindent #2\relax\@afterindenttrue
+     \interlinepenalty\@M
+     \leavevmode
+     \@tempdima #3\relax
+     \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
+     {#4}\nobreak
+     \leaders\hbox{$\m@th
+        \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
+        mu$}\hfill
+     \nobreak
+     \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
+     \par}%
+  \fi}
+%
+\def\switcht@albion{%
+\def\abstractname{Abstract.}
+\def\ackname{Acknowledgement.}
+\def\andname{and}
+\def\lastandname{\unskip, and}
+\def\appendixname{Appendix}
+\def\chaptername{Chapter}
+\def\claimname{Claim}
+\def\conjecturename{Conjecture}
+\def\contentsname{Table of Contents}
+\def\corollaryname{Corollary}
+\def\definitionname{Definition}
+\def\examplename{Example}
+\def\exercisename{Exercise}
+\def\figurename{Fig.}
+\def\keywordname{{\bf Key words:}}
+\def\indexname{Index}
+\def\lemmaname{Lemma}
+\def\contriblistname{List of Contributors}
+\def\listfigurename{List of Figures}
+\def\listtablename{List of Tables}
+\def\mailname{{\it Correspondence to\/}:}
+\def\noteaddname{Note added in proof}
+\def\notename{Note}
+\def\partname{Part}
+\def\problemname{Problem}
+\def\proofname{Proof}
+\def\propertyname{Property}
+\def\propositionname{Proposition}
+\def\questionname{Question}
+\def\remarkname{Remark}
+\def\seename{see}
+\def\solutionname{Solution}
+\def\subclassname{{\it Subject Classifications\/}:}
+\def\tablename{Table}
+\def\theoremname{Theorem}}
+\switcht@albion
+% Names of theorem like environments are already defined
+% but must be translated if another language is chosen
+%
+% French section
+\def\switcht@francais{%\typeout{On parle francais.}%
+ \def\abstractname{R\'esum\'e.}%
+ \def\ackname{Remerciements.}%
+ \def\andname{et}%
+ \def\lastandname{ et}%
+ \def\appendixname{Appendice}
+ \def\chaptername{Chapitre}%
+ \def\claimname{Pr\'etention}%
+ \def\conjecturename{Hypoth\`ese}%
+ \def\contentsname{Table des mati\`eres}%
+ \def\corollaryname{Corollaire}%
+ \def\definitionname{D\'efinition}%
+ \def\examplename{Exemple}%
+ \def\exercisename{Exercice}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bf Mots-cl\'e:}}
+ \def\indexname{Index}
+ \def\lemmaname{Lemme}%
+ \def\contriblistname{Liste des contributeurs}
+ \def\listfigurename{Liste des figures}%
+ \def\listtablename{Liste des tables}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
+ \def\notename{Remarque}%
+ \def\partname{Partie}%
+ \def\problemname{Probl\`eme}%
+ \def\proofname{Preuve}%
+ \def\propertyname{Caract\'eristique}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Question}%
+ \def\remarkname{Remarque}%
+ \def\seename{voir}
+ \def\solutionname{Solution}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tableau}%
+ \def\theoremname{Th\'eor\`eme}%
+}
+%
+% German section
+\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
+ \def\abstractname{Zusammenfassung.}%
+ \def\ackname{Danksagung.}%
+ \def\andname{und}%
+ \def\lastandname{ und}%
+ \def\appendixname{Anhang}%
+ \def\chaptername{Kapitel}%
+ \def\claimname{Behauptung}%
+ \def\conjecturename{Hypothese}%
+ \def\contentsname{Inhaltsverzeichnis}%
+ \def\corollaryname{Korollar}%
+%\def\definitionname{Definition}%
+ \def\examplename{Beispiel}%
+ \def\exercisename{\"Ubung}%
+ \def\figurename{Abb.}%
+ \def\keywordname{{\bf Schl\"usselw\"orter:}}
+ \def\indexname{Index}
+%\def\lemmaname{Lemma}%
+ \def\contriblistname{Mitarbeiter}
+ \def\listfigurename{Abbildungsverzeichnis}%
+ \def\listtablename{Tabellenverzeichnis}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Nachtrag}%
+ \def\notename{Anmerkung}%
+ \def\partname{Teil}%
+%\def\problemname{Problem}%
+ \def\proofname{Beweis}%
+ \def\propertyname{Eigenschaft}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Frage}%
+ \def\remarkname{Anmerkung}%
+ \def\seename{siehe}
+ \def\solutionname{L\"osung}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tabelle}%
+%\def\theoremname{Theorem}%
+}
+
+% Ragged bottom for the actual page
+\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
+\global\let\@textbottom\relax}}
+
+\renewcommand\small{%
+   \@setfontsize\small\@ixpt{11}%
+   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+   \abovedisplayshortskip \z@ \@plus2\p@
+   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+   \def\@listi{\leftmargin\leftmargini
+               \parsep 0\p@ \@plus1\p@ \@minus\p@
+               \topsep 8\p@ \@plus2\p@ \@minus4\p@
+               \itemsep0\p@}%
+   \belowdisplayskip \abovedisplayskip
+}
+
+\frenchspacing
+\widowpenalty=10000
+\clubpenalty=10000
+
+\setlength\oddsidemargin   {63\p@}
+\setlength\evensidemargin  {63\p@}
+\setlength\marginparwidth  {90\p@}
+
+\setlength\headsep   {16\p@}
+
+\setlength\footnotesep{7.7\p@}
+\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep   {8mm\@plus 2\p@ \@minus 2\p@}
+
+\setcounter{secnumdepth}{2}
+
+\newcounter {chapter}
+\renewcommand\thechapter      {\@arabic\c@chapter}
+
+\newif\if@mainmatter \@mainmattertrue
+\newcommand\frontmatter{\cleardoublepage
+            \@mainmatterfalse\pagenumbering{Roman}}
+\newcommand\mainmatter{\cleardoublepage
+       \@mainmattertrue\pagenumbering{arabic}}
+\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
+      \@mainmatterfalse}
+
+\renewcommand\part{\cleardoublepage
+                 \thispagestyle{empty}%
+                 \if@twocolumn
+                     \onecolumn
+                     \@tempswatrue
+                   \else
+                     \@tempswafalse
+                 \fi
+                 \null\vfil
+                 \secdef\@part\@spart}
+
+\def\@part[#1]#2{%
+    \ifnum \c@secnumdepth >-2\relax
+      \refstepcounter{part}%
+      \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
+    \else
+      \addcontentsline{toc}{part}{#1}%
+    \fi
+    \markboth{}{}%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \ifnum \c@secnumdepth >-2\relax
+       \huge\bfseries \partname~\thepart
+       \par
+       \vskip 20\p@
+     \fi
+     \Huge \bfseries #2\par}%
+    \@endpart}
+\def\@spart#1{%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \Huge \bfseries #1\par}%
+    \@endpart}
+\def\@endpart{\vfil\newpage
+              \if@twoside
+                \null
+                \thispagestyle{empty}%
+                \newpage
+              \fi
+              \if@tempswa
+                \twocolumn
+              \fi}
+
+\newcommand\chapter{\clearpage
+                    \thispagestyle{empty}%
+                    \global\@topnum\z@
+                    \@afterindentfalse
+                    \secdef\@chapter\@schapter}
+\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
+                       \if@mainmatter
+                         \refstepcounter{chapter}%
+                         \typeout{\@chapapp\space\thechapter.}%
+                         \addcontentsline{toc}{chapter}%
+                                  {\protect\numberline{\thechapter}#1}%
+                       \else
+                         \addcontentsline{toc}{chapter}{#1}%
+                       \fi
+                    \else
+                      \addcontentsline{toc}{chapter}{#1}%
+                    \fi
+                    \chaptermark{#1}%
+                    \addtocontents{lof}{\protect\addvspace{10\p@}}%
+                    \addtocontents{lot}{\protect\addvspace{10\p@}}%
+                    \if@twocolumn
+                      \@topnewpage[\@makechapterhead{#2}]%
+                    \else
+                      \@makechapterhead{#2}%
+                      \@afterheading
+                    \fi}
+\def\@makechapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \ifnum \c@secnumdepth >\m@ne
+      \if@mainmatter
+        \large\bfseries \@chapapp{} \thechapter
+        \par\nobreak
+        \vskip 20\p@
+      \fi
+    \fi
+    \interlinepenalty\@M
+    \Large \bfseries #1\par\nobreak
+    \vskip 40\p@
+  }}
+\def\@schapter#1{\if@twocolumn
+                   \@topnewpage[\@makeschapterhead{#1}]%
+                 \else
+                   \@makeschapterhead{#1}%
+                   \@afterheading
+                 \fi}
+\def\@makeschapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \normalfont
+    \interlinepenalty\@M
+    \Large \bfseries  #1\par\nobreak
+    \vskip 40\p@
+  }}
+
+\renewcommand\section{\@startsection{section}{1}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {12\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\large\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {8\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\normalsize\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\bfseries\boldmath}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
+                       {-12\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\itshape}}
+\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use
+                  \string\subparagraph\space with this class}\vskip0.5cm
+You should not use \verb|\subparagraph| with this class.\vskip0.5cm}
+
+\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
+\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
+\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
+\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
+\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
+\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
+\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
+\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
+\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
+\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
+\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
+
+\let\footnotesize\small
+
+\if@custvec
+\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}}
+{\mbox{\boldmath$\textstyle#1$}}
+{\mbox{\boldmath$\scriptstyle#1$}}
+{\mbox{\boldmath$\scriptscriptstyle#1$}}}
+\fi
+
+\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
+\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
+\penalty50\hskip1em\null\nobreak\hfil\squareforqed
+\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
+
+\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+\gets\cr\to\cr}}}}}
+\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+<\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
+>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.8pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
+\def\bbbr{{\rm I\!R}} %reelle Zahlen
+\def\bbbm{{\rm I\!M}}
+\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
+\def\bbbf{{\rm I\!F}}
+\def\bbbh{{\rm I\!H}}
+\def\bbbk{{\rm I\!K}}
+\def\bbbp{{\rm I\!P}}
+\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
+{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
+\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
+\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbs{{\mathchoice
+{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
+\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}}
+{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}}
+
+\let\ts\,
+
+\setlength\leftmargini  {17\p@}
+\setlength\leftmargin    {\leftmargini}
+\setlength\leftmarginii  {\leftmargini}
+\setlength\leftmarginiii {\leftmargini}
+\setlength\leftmarginiv  {\leftmargini}
+\setlength  \labelsep  {.5em}
+\setlength  \labelwidth{\leftmargini}
+\addtolength\labelwidth{-\labelsep}
+
+\def\@listI{\leftmargin\leftmargini
+            \parsep 0\p@ \@plus1\p@ \@minus\p@
+            \topsep 8\p@ \@plus2\p@ \@minus4\p@
+            \itemsep0\p@}
+\let\@listi\@listI
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+              \labelwidth\leftmarginii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus2\p@ \@minus\p@}
+\def\@listiii{\leftmargin\leftmarginiii
+              \labelwidth\leftmarginiii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus\p@\@minus\p@
+              \parsep    \z@
+              \partopsep \p@ \@plus\z@ \@minus\p@}
+
+\renewcommand\labelitemi{\normalfont\bfseries --}
+\renewcommand\labelitemii{$\m@th\bullet$}
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}%
+                                                    {{\contentsname}}}
+ \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}}
+ \def\lastand{\ifnum\value{auco}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{auco}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \@starttoc{toc}\if@restonecol\twocolumn\fi}
+
+\def\l@part#1#2{\addpenalty{\@secpenalty}%
+   \addvspace{2em plus\p@}%  % space above part line
+   \begingroup
+     \parindent \z@
+     \rightskip \z@ plus 5em
+     \hrule\vskip5pt
+     \large               % same size as for a contribution heading
+     \bfseries\boldmath   % set line in boldface
+     \leavevmode          % TeX command to enter horizontal mode.
+     #1\par
+     \vskip5pt
+     \hrule
+     \vskip1pt
+     \nobreak             % Never break after part entry
+   \endgroup}
+
+\def\@dotsep{2}
+
+\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
+{chapter.\thechapter}\fi}
+
+\def\addnumcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
+                     {\thechapter}#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmarkwop#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}
+
+\def\@adcmk[#1]{\ifcase #1 \or
+\def\@gtempa{\addnumcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmarkwop}%
+  \fi\@gtempa{toc}{chapter}}
+\def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}}
+
+\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
+ \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ {\large\bfseries\boldmath#1}\ifx0#2\hfil\null
+ \else
+      \nobreak
+      \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+      \@dotsep mu$}\hfill
+      \nobreak\hbox to\@pnumwidth{\hss #2}%
+ \fi\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@title#1#2{\addpenalty{-\@highpenalty}
+ \addvspace{8pt plus 1pt}
+ \@tempdima \z@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ #1\nobreak
+ \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+ \@dotsep mu$}\hfill
+ \nobreak\hbox to\@pnumwidth{\hss #2}\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@author#1#2{\addpenalty{\@highpenalty}
+ \@tempdima=\z@ %15\p@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip
+ \textit{#1}\par
+ \penalty\@highpenalty \endgroup}
+
+%\setcounter{tocdepth}{0}
+\newdimen\tocchpnum
+\newdimen\tocsecnum
+\newdimen\tocsectotal
+\newdimen\tocsubsecnum
+\newdimen\tocsubsectotal
+\newdimen\tocsubsubsecnum
+\newdimen\tocsubsubsectotal
+\newdimen\tocparanum
+\newdimen\tocparatotal
+\newdimen\tocsubparanum
+\tocchpnum=\z@            % no chapter numbers
+\tocsecnum=15\p@          % section 88. plus 2.222pt
+\tocsubsecnum=23\p@       % subsection 88.8 plus 2.222pt
+\tocsubsubsecnum=27\p@    % subsubsection 88.8.8 plus 1.444pt
+\tocparanum=35\p@         % paragraph 88.8.8.8 plus 1.666pt
+\tocsubparanum=43\p@      % subparagraph 88.8.8.8.8 plus 1.888pt
+\def\calctocindent{%
+\tocsectotal=\tocchpnum
+\advance\tocsectotal by\tocsecnum
+\tocsubsectotal=\tocsectotal
+\advance\tocsubsectotal by\tocsubsecnum
+\tocsubsubsectotal=\tocsubsectotal
+\advance\tocsubsubsectotal by\tocsubsubsecnum
+\tocparatotal=\tocsubsubsectotal
+\advance\tocparatotal by\tocparanum}
+\calctocindent
+
+\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
+\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
+\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
+\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
+\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
+
+\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}}
+ \@starttoc{lof}\if@restonecol\twocolumn\fi}
+\def\l@figure{\@dottedtocline{1}{0em}{1.5em}}
+
+\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}}
+ \@starttoc{lot}\if@restonecol\twocolumn\fi}
+\let\l@table\l@figure
+
+\renewcommand\listoffigures{%
+    \section*{\listfigurename
+      \@mkboth{\listfigurename}{\listfigurename}}%
+    \@starttoc{lof}%
+    }
+
+\renewcommand\listoftables{%
+    \section*{\listtablename
+      \@mkboth{\listtablename}{\listtablename}}%
+    \@starttoc{lot}%
+    }
+
+\ifx\oribibl\undefined
+\ifx\citeauthoryear\undefined
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \def\@biblabel##1{##1.}
+      \small
+      \list{\@biblabel{\@arabic\c@enumiv}}%
+           {\settowidth\labelwidth{\@biblabel{#1}}%
+            \leftmargin\labelwidth
+            \advance\leftmargin\labelsep
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
+     {\let\protect\noexpand\immediate
+     \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+\newcount\@tempcntc
+\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
+  \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
+    {\@ifundefined
+       {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
+        ?}\@warning
+       {Citation `\@citeb' on page \thepage \space undefined}}%
+    {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
+     \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
+       \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}%
+     \else
+      \advance\@tempcntb\@ne
+      \ifnum\@tempcntb=\@tempcntc
+      \else\advance\@tempcntb\m@ne\@citeo
+      \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
+\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
+               \@citea\def\@citea{,\,\hskip\z@skip}%
+               \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
+               {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else
+                \def\@citea{--}\fi
+      \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
+\else
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \small
+      \list{}%
+           {\settowidth\labelwidth{}%
+            \leftmargin\parindent
+            \itemindent=-\parindent
+            \labelsep=\z@
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+      \def\@cite#1{#1}%
+      \def\@lbibitem[#1]#2{\item[]\if@filesw
+        {\def\protect##1{\string ##1\space}\immediate
+      \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+   \fi
+\else
+\@cons\@openbib@code{\noexpand\small}
+\fi
+
+\def\idxquad{\hskip 10\p@}% space that divides entry from number
+
+\def\@idxitem{\par\hangindent 10\p@}
+
+\def\subitem{\par\setbox0=\hbox{--\enspace}% second order
+                \noindent\hangindent\wd0\box0}% index entry
+
+\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third
+                \noindent\hangindent\wd0\box0}% order index entry
+
+\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}
+
+\renewenvironment{theindex}
+               {\@mkboth{\indexname}{\indexname}%
+                \thispagestyle{empty}\parindent\z@
+                \parskip\z@ \@plus .3\p@\relax
+                \let\item\par
+                \def\,{\relax\ifmmode\mskip\thinmuskip
+                             \else\hskip0.2em\ignorespaces\fi}%
+                \normalfont\small
+                \begin{multicols}{2}[\@makeschapterhead{\indexname}]%
+                }
+                {\end{multicols}}
+
+\renewcommand\footnoterule{%
+  \kern-3\p@
+  \hrule\@width 2truecm
+  \kern2.6\p@}
+  \newdimen\fnindent
+  \fnindent1em
+\long\def\@makefntext#1{%
+    \parindent \fnindent%
+    \leftskip \fnindent%
+    \noindent
+    \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
+
+\long\def\@makecaption#1#2{%
+  \vskip\abovecaptionskip
+  \sbox\@tempboxa{{\bfseries #1.} #2}%
+  \ifdim \wd\@tempboxa >\hsize
+    {\bfseries #1.} #2\par
+  \else
+    \global \@minipagefalse
+    \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}%
+  \fi
+  \vskip\belowcaptionskip}
+
+\def\fps@figure{htbp}
+\def\fnum@figure{\figurename\thinspace\thefigure}
+\def \@floatboxreset {%
+        \reset@font
+        \small
+        \@setnobreak
+        \@setminipage
+}
+\def\fps@table{htbp}
+\def\fnum@table{\tablename~\thetable}
+\renewenvironment{table}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@float{table}}
+               {\end@float}
+\renewenvironment{table*}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@dblfloat{table}}
+               {\end@dblfloat}
+
+\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
+  ext@#1\endcsname}{#1}{\protect\numberline{\csname
+  the#1\endcsname}{\ignorespaces #2}}\begingroup
+    \@parboxrestore
+    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+  \endgroup}
+
+% LaTeX does not provide a command to enter the authors institute
+% addresses. The \institute command is defined here.
+
+\newcounter{@inst}
+\newcounter{@auth}
+\newcounter{auco}
+\newdimen\instindent
+\newbox\authrun
+\newtoks\authorrunning
+\newtoks\tocauthor
+\newbox\titrun
+\newtoks\titlerunning
+\newtoks\toctitle
+
+\def\clearheadinfo{\gdef\@author{No Author Given}%
+                   \gdef\@title{No Title Given}%
+                   \gdef\@subtitle{}%
+                   \gdef\@institute{No Institute Given}%
+                   \gdef\@thanks{}%
+                   \global\titlerunning={}\global\authorrunning={}%
+                   \global\toctitle={}\global\tocauthor={}}
+
+\def\institute#1{\gdef\@institute{#1}}
+
+\def\institutename{\par
+ \begingroup
+ \parskip=\z@
+ \parindent=\z@
+ \setcounter{@inst}{1}%
+ \def\and{\par\stepcounter{@inst}%
+ \noindent$^{\the@inst}$\enspace\ignorespaces}%
+ \setbox0=\vbox{\def\thanks##1{}\@institute}%
+ \ifnum\c@@inst=1\relax
+   \gdef\fnnstart{0}%
+ \else
+   \xdef\fnnstart{\c@@inst}%
+   \setcounter{@inst}{1}%
+   \noindent$^{\the@inst}$\enspace
+ \fi
+ \ignorespaces
+ \@institute\par
+ \endgroup}
+
+\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or
+   {\star\star\star}\or \dagger\or \ddagger\or
+   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
+   \or \ddagger\ddagger \else\@ctrerr\fi}}
+
+\def\inst#1{\unskip$^{#1}$}
+\def\fnmsep{\unskip$^,$}
+\def\email#1{{\tt#1}}
+\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}%
+\@ifpackageloaded{babel}{%
+\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
+\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
+\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
+}{\switcht@@therlang}%
+}
+\def\homedir{\~{ }}
+
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\clearheadinfo
+
+\renewcommand\maketitle{\newpage
+  \refstepcounter{chapter}%
+  \stepcounter{section}%
+  \setcounter{section}{0}%
+  \setcounter{subsection}{0}%
+  \setcounter{figure}{0}
+  \setcounter{table}{0}
+  \setcounter{equation}{0}
+  \setcounter{footnote}{0}%
+  \begingroup
+    \parindent=\z@
+    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+    \if@twocolumn
+      \ifnum \col@number=\@ne
+        \@maketitle
+      \else
+        \twocolumn[\@maketitle]%
+      \fi
+    \else
+      \newpage
+      \global\@topnum\z@   % Prevents figures from going at top of page.
+      \@maketitle
+    \fi
+    \thispagestyle{empty}\@thanks
+%
+    \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}%
+    \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
+    \instindent=\hsize
+    \advance\instindent by-\headlineindent
+%    \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
+%       \addcontentsline{toc}{title}{\the\toctitle}\fi
+    \if@runhead
+       \if!\the\titlerunning!\else
+         \edef\@title{\the\titlerunning}%
+       \fi
+       \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}%
+       \ifdim\wd\titrun>\instindent
+          \typeout{Title too long for running head. Please supply}%
+          \typeout{a shorter form with \string\titlerunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\titrun=\hbox{\small\rm
+          Title Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@title{\copy\titrun}%
+    \fi
+%
+    \if!\the\tocauthor!\relax
+      {\def\and{\noexpand\protect\noexpand\and}%
+      \protected@xdef\toc@uthor{\@author}}%
+    \else
+      \def\\{\noexpand\protect\noexpand\newline}%
+      \protected@xdef\scratch{\the\tocauthor}%
+      \protected@xdef\toc@uthor{\scratch}%
+    \fi
+%    \addcontentsline{toc}{author}{\toc@uthor}%
+    \if@runhead
+       \if!\the\authorrunning!
+         \value{@inst}=\value{@auth}%
+         \setcounter{@auth}{1}%
+       \else
+         \edef\@author{\the\authorrunning}%
+       \fi
+       \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}%
+       \ifdim\wd\authrun>\instindent
+          \typeout{Names of authors too long for running head. Please supply}%
+          \typeout{a shorter form with \string\authorrunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\authrun=\hbox{\small\rm
+          Authors Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@author{\copy\authrun}%
+       \markboth{\@author}{\@title}%
+     \fi
+  \endgroup
+  \setcounter{footnote}{\fnnstart}%
+  \clearheadinfo}
+%
+\def\@maketitle{\newpage
+ \markboth{}{}%
+ \def\lastand{\ifnum\value{@inst}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{@inst}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \begin{center}%
+ \let\newline\\
+ {\Large \bfseries\boldmath
+  \pretolerance=10000
+  \@title \par}\vskip .8cm
+\if!\@subtitle!\else {\large \bfseries\boldmath
+  \vskip -.65cm
+  \pretolerance=10000
+  \@subtitle \par}\vskip .8cm\fi
+ \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}%
+ \def\thanks##1{}\@author}%
+ \global\value{@inst}=\value{@auth}%
+ \global\value{auco}=\value{@auth}%
+ \setcounter{@auth}{1}%
+{\lineskip .5em
+\noindent\ignorespaces
+\@author\vskip.35cm}
+ {\small\institutename}
+ \end{center}%
+ }
+
+% definition of the "\spnewtheorem" command.
+%
+% Usage:
+%
+%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
+% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
+% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
+%
+% New is "cap_font" and "body_font". It stands for
+% fontdefinition of the caption and the text itself.
+%
+% "\spnewtheorem*" gives a theorem without number.
+%
+% A defined spnewthoerem environment is used as described
+% by Lamport.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@thmcountersep{}
+\def\@thmcounterend{.}
+
+\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
+
+% definition of \spnewtheorem with number
+
+\def\@spnthm#1#2{%
+  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
+\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
+
+\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}\@addtoreset{#1}{#3}%
+   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
+     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
+                              \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}%
+   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
+                               \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spothm#1[#2]#3#4#5{%
+  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
+  {\expandafter\@ifdefinable\csname #1\endcsname
+  {\global\@namedef{the#1}{\@nameuse{the#2}}%
+  \expandafter\xdef\csname #1name\endcsname{#3}%
+  \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
+  \global\@namedef{end#1}{\@endtheorem}}}}
+
+\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\refstepcounter{#1}%
+\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
+
+\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
+                    \ignorespaces}
+
+\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
+       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
+
+\def\@spbegintheorem#1#2#3#4{\trivlist
+                 \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4}
+
+\def\@spopargbegintheorem#1#2#3#4#5{\trivlist
+      \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5}
+
+% definition of \spnewtheorem* without number
+
+\def\@sthm#1#2{\@Ynthm{#1}{#2}}
+
+\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
+    \expandafter\xdef\csname #1name\endcsname{#2}%
+    \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
+
+\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
+
+\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
+       {#4}{#2}{#3}\ignorespaces}
+
+\def\@Begintheorem#1#2#3{#3\trivlist
+                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
+
+\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
+      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
+
+\if@envcntsect
+   \def\@thmcountersep{.}
+   \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
+\else
+   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
+   \if@envcntreset
+      \@addtoreset{theorem}{section}
+   \else
+      \@addtoreset{theorem}{chapter}
+   \fi
+\fi
+
+%definition of divers theorem environments
+\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
+\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
+\if@envcntsame % alle Umgebungen wie Theorem.
+   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
+\else % alle Umgebungen mit eigenem Zaehler
+   \if@envcntsect % mit section numeriert
+      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
+   \else % nicht mit section numeriert
+      \if@envcntreset
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{section}}
+      \else
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{chapter}}%
+      \fi
+   \fi
+\fi
+\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
+\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
+\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
+\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
+\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
+\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily}
+\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
+\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
+\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily}
+\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
+\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
+\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
+\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily}
+\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
+
+\def\@takefromreset#1#2{%
+    \def\@tempa{#1}%
+    \let\@tempd\@elt
+    \def\@elt##1{%
+        \def\@tempb{##1}%
+        \ifx\@tempa\@tempb\else
+            \@addtoreset{##1}{#2}%
+        \fi}%
+    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
+    \expandafter\def\csname cl@#2\endcsname{}%
+    \@tempc
+    \let\@elt\@tempd}
+
+\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+      \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
+                  \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
+      \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}
+      }
+
+\renewenvironment{abstract}{%
+      \list{}{\advance\topsep by0.35cm\relax\small
+      \leftmargin=1cm
+      \labelwidth=\z@
+      \listparindent=\z@
+      \itemindent\listparindent
+      \rightmargin\leftmargin}\item[\hskip\labelsep
+                                    \bfseries\abstractname]}
+    {\endlist}
+
+\newdimen\headlineindent             % dimension for space between
+\headlineindent=1.166cm              % number and text of headings.
+
+\def\ps@headings{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \leftmark\hfil}
+   \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\def\ps@titlepage{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \hfil}
+   \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\if@runhead\ps@headings\else
+\ps@empty\fi
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\endinput
+%end of file llncs.cls
diff -r a8a442ba0dbf -r e93760534354 Journal/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/root.bib	Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,111 @@
+@article{OwensReppyTuron09,
+  author = {S.~Owens and J.~Reppy and A.~Turon},
+  title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},
+  journal = {Journal of Functional Programming},
+  volume = 19,
+  number = {2},
+  year = 2009,
+  pages = {173--190}
+}
+
+
+
+@Unpublished{KraussNipkow11,
+  author = 	 {A.~Kraus and T.~Nipkow},
+  title = 	 {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
+  note = 	 {To appear in Journal of Automated Reasoning},
+  year = 	 {2011}
+}
+
+@Book{Kozen97,
+  author = 	 {D.~Kozen},
+  title = 	 {{A}utomata and {C}omputability},
+  publisher = 	 {Springer Verlag},
+  year = 	 {1997}
+}
+
+
+@incollection{Constable00,
+  author    = {R.~L.~Constable and
+               P.~B.~Jackson and
+               P.~Naumov and
+               J.~C.~Uribe},
+  title     = {{C}onstructively {F}ormalizing {A}utomata {T}heory},
+  booktitle = {Proof, Language, and Interaction},
+  year      = {2000},
+  publisher = {MIT Press},
+  pages     = {213-238}
+}
+
+
+@techreport{Filliatre97,
+  author = {J.-C. Filli\^atre},
+  institution = {LIP - ENS Lyon},
+  number = {97--04},
+  title = {{F}inite {A}utomata {T}heory in {C}oq: 
+           {A} {C}onstructive {P}roof of {K}leene's {T}heorem},
+  type = {Research Report},
+  year = {1997}
+}
+
+@article{OwensSlind08,
+  author    = {S.~Owens and K.~Slind},
+  title     = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},
+  journal   = {Higher-Order and Symbolic Computation},
+  volume    = {21},
+  number    = {4},
+  year      = {2008},
+  pages     = {377--409}
+}
+
+@article{Brzozowski64,
+ author = {J.~A.~Brzozowski},
+ title = {{D}erivatives of {R}egular {E}xpressions},
+ journal = {J.~ACM},
+ volume = {11},
+ issue = {4},
+ year = {1964},
+ pages = {481--494},
+ publisher = {ACM}
+} 
+
+@inproceedings{Nipkow98,
+ author={T.~Nipkow},
+ title={{V}erified {L}exical {A}nalysis},
+ booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics},
+ series={LNCS},
+ volume=1479,
+ pages={1--15},
+ year=1998
+}
+
+@inproceedings{BerghoferNipkow00,
+  author={S.~Berghofer and T.~Nipkow},
+  title={{E}xecuting {H}igher {O}rder {L}ogic},
+  booktitle={Proc.~of the International Workshop on Types for Proofs and Programs},
+  year=2002,
+  series={LNCS},
+  volume=2277,
+  pages="24--40"
+}
+
+@book{HopcroftUllman69,
+  author    = {J.~E.~Hopcroft and
+               J.~D.~Ullman},
+  title     = {{F}ormal {L}anguages and {T}heir {R}elation to {A}utomata},
+  publisher = {Addison-Wesley},
+  year      = {1969}
+}
+
+
+@inproceedings{BerghoferReiter09,
+  author    = {S.~Berghofer and
+               M.~Reiter},
+  title     = {{F}ormalizing the {L}ogic-{A}utomaton {C}onnection},
+  booktitle = {Proc.~of the 22nd International
+               Conference on Theorem Proving in Higher Order Logics},
+  year      = {2009},
+  pages     = {147-163},
+  series    = {LNCS},
+  volume    = {5674}
+}
\ No newline at end of file
diff -r a8a442ba0dbf -r e93760534354 Journal/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/root.tex	Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,73 @@
+\documentclass[runningheads]{llncs}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{tikz}
+\usepackage{pgf}
+\usetikzlibrary{arrows,automata,decorations,fit,calc}
+\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
+\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
+\usetikzlibrary{matrix}
+\usepackage{pdfsetup}
+\usepackage{ot1patch}
+\usepackage{times}
+%%\usepackage{proof}
+%%\usepackage{mathabx}
+\usepackage{stmaryrd}
+
+\titlerunning{Myhill-Nerode using Regular Expressions}
+
+
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\it}%
+
+
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+
+\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
+\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
+
+\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
+\begin{document}
+
+\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
+  Expressions (Proof Pearl)}
+\author{Chunhan Wu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
+\institute{PLA University of Science and Technology, China \and TU Munich, Germany}
+\maketitle
+
+%\mbox{}\\[-10mm]
+\begin{abstract} 
+There are numerous textbooks on regular languages. Nearly all of them
+introduce the subject by describing finite automata and only mentioning on the
+side a connection with regular expressions. Unfortunately, automata are difficult
+to formalise in HOL-based theorem provers. The reason is that
+they need to be represented as graphs, matrices or functions, none of which
+are inductive datatypes. Also convenient operations for disjoint unions of
+graphs and functions are not easily formalisiable in HOL. In contrast, regular
+expressions can be defined conveniently as a datatype and a corresponding
+reasoning infrastructure comes for free. We show in this paper that a central
+result from formal language theory---the Myhill-Nerode theorem---can be
+recreated using only regular expressions.
+
+\end{abstract}
+
+
+\input{session}
+
+%%\mbox{}\\[-10mm]
+\bibliographystyle{plain}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff -r a8a442ba0dbf -r e93760534354 Myhill_1.thy
--- a/Myhill_1.thy	Thu May 12 05:55:05 2011 +0000
+++ b/Myhill_1.thy	Wed May 18 19:54:43 2011 +0000
@@ -1,315 +1,10 @@
 theory Myhill_1
-imports Main Folds 
-        "~~/src/HOL/Library/While_Combinator"
+imports Main Folds Regular
+        "~~/src/HOL/Library/While_Combinator" 
 begin
 
-section {* Preliminary definitions *}
-
-types lang = "string set"
-
-
-text {*  Sequential composition of two languages *}
-
-definition 
-  Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)
-where 
-  "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
-
-
-text {* Some properties of operator @{text ";;"}. *}
-
-lemma seq_add_left:
-  assumes a: "A = B"
-  shows "C ;; A = C ;; B"
-using a by simp
-
-lemma seq_union_distrib_right:
-  shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"
-unfolding Seq_def by auto
-
-lemma seq_union_distrib_left:
-  shows "C ;; (A \<union> B) = (C ;; A) \<union> (C ;; B)"
-unfolding Seq_def by  auto
-
-lemma seq_intro:
-  assumes a: "x \<in> A" "y \<in> B"
-  shows "x @ y \<in> A ;; B "
-using a by (auto simp: Seq_def)
-
-lemma seq_assoc:
-  shows "(A ;; B) ;; C = A ;; (B ;; C)"
-unfolding Seq_def
-apply(auto)
-apply(blast)
-by (metis append_assoc)
-
-lemma seq_empty [simp]:
-  shows "A ;; {[]} = A"
-  and   "{[]} ;; A = A"
-by (simp_all add: Seq_def)
-
-
-text {* Power and Star of a language *}
-
-fun 
-  pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)
-where
-  "A \<up> 0 = {[]}"
-| "A \<up> (Suc n) =  A ;; (A \<up> n)" 
-
-definition
-  Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
-where
-  "A\<star> \<equiv> (\<Union>n. A \<up> n)"
-
-
-lemma star_start[intro]:
-  shows "[] \<in> A\<star>"
-proof -
-  have "[] \<in> A \<up> 0" by auto
-  then show "[] \<in> A\<star>" unfolding Star_def by blast
-qed
-
-lemma star_step [intro]:
-  assumes a: "s1 \<in> A" 
-  and     b: "s2 \<in> A\<star>"
-  shows "s1 @ s2 \<in> A\<star>"
-proof -
-  from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto
-  then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def)
-  then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast
-qed
-
-lemma star_induct[consumes 1, case_names start step]:
-  assumes a: "x \<in> A\<star>" 
-  and     b: "P []"
-  and     c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)"
-  shows "P x"
-proof -
-  from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto
-  then show "P x"
-    by (induct n arbitrary: x)
-       (auto intro!: b c simp add: Seq_def Star_def)
-qed
-    
-lemma star_intro1:
-  assumes a: "x \<in> A\<star>"
-  and     b: "y \<in> A\<star>"
-  shows "x @ y \<in> A\<star>"
-using a b
-by (induct rule: star_induct) (auto)
-
-lemma star_intro2: 
-  assumes a: "y \<in> A"
-  shows "y \<in> A\<star>"
-proof -
-  from a have "y @ [] \<in> A\<star>" by blast
-  then show "y \<in> A\<star>" by simp
-qed
-
-lemma star_intro3:
-  assumes a: "x \<in> A\<star>"
-  and     b: "y \<in> A"
-  shows "x @ y \<in> A\<star>"
-using a b by (blast intro: star_intro1 star_intro2)
-
-lemma star_cases:
-  shows "A\<star> =  {[]} \<union> A ;; A\<star>"
-proof
-  { fix x
-    have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A ;; A\<star>"
-      unfolding Seq_def
-    by (induct rule: star_induct) (auto)
-  }
-  then show "A\<star> \<subseteq> {[]} \<union> A ;; A\<star>" by auto
-next
-  show "{[]} \<union> A ;; A\<star> \<subseteq> A\<star>"
-    unfolding Seq_def by auto
-qed
-
-lemma star_decom: 
-  assumes a: "x \<in> A\<star>" "x \<noteq> []"
-  shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"
-using a
-by (induct rule: star_induct) (blast)+
-
-lemma
-  shows seq_Union_left:  "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"
-  and   seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"
-unfolding Seq_def by auto
-
-lemma seq_pow_comm:
-  shows "A ;; (A \<up> n) = (A \<up> n) ;; A"
-by (induct n) (simp_all add: seq_assoc[symmetric])
-
-lemma seq_star_comm:
-  shows "A ;; A\<star> = A\<star> ;; A"
-unfolding Star_def seq_Union_left
-unfolding seq_pow_comm seq_Union_right 
-by simp
-
-
-text {* Two lemmas about the length of strings in @{text "A \<up> n"} *}
-
-lemma pow_length:
-  assumes a: "[] \<notin> A"
-  and     b: "s \<in> A \<up> Suc n"
-  shows "n < length s"
-using b
-proof (induct n arbitrary: s)
-  case 0
-  have "s \<in> A \<up> Suc 0" by fact
-  with a have "s \<noteq> []" by auto
-  then show "0 < length s" by auto
-next
-  case (Suc n)
-  have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact
-  have "s \<in> A \<up> Suc (Suc n)" by fact
-  then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"
-    by (auto simp add: Seq_def)
-  from ih ** have "n < length s2" by simp
-  moreover have "0 < length s1" using * a by auto
-  ultimately show "Suc n < length s" unfolding eq 
-    by (simp only: length_append)
-qed
-
-lemma seq_pow_length:
-  assumes a: "[] \<notin> A"
-  and     b: "s \<in> B ;; (A \<up> Suc n)"
-  shows "n < length s"
-proof -
-  from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A \<up> Suc n"
-    unfolding Seq_def by auto
-  from * have " n < length s2" by (rule pow_length[OF a])
-  then show "n < length s" using eq by simp
-qed
-
-
-section {* A modified version of Arden's lemma *}
-
-text {*  A helper lemma for Arden *}
-
-lemma arden_helper:
-  assumes eq: "X = X ;; A \<union> B"
-  shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"
-proof (induct n)
-  case 0 
-  show "X = X ;; (A \<up> Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B ;; (A \<up> m))"
-    using eq by simp
-next
-  case (Suc n)
-  have ih: "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" by fact
-  also have "\<dots> = (X ;; A \<union> B) ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" using eq by simp
-  also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (B ;; (A \<up> Suc n)) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"
-    by (simp add: seq_union_distrib_right seq_assoc)
-  also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))"
-    by (auto simp add: le_Suc_eq)
-  finally show "X = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))" .
-qed
-
-theorem arden:
-  assumes nemp: "[] \<notin> A"
-  shows "X = X ;; A \<union> B \<longleftrightarrow> X = B ;; A\<star>"
-proof
-  assume eq: "X = B ;; A\<star>"
-  have "A\<star> = {[]} \<union> A\<star> ;; A" 
-    unfolding seq_star_comm[symmetric]
-    by (rule star_cases)
-  then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"
-    by (rule seq_add_left)
-  also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"
-    unfolding seq_union_distrib_left by simp
-  also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" 
-    by (simp only: seq_assoc)
-  finally show "X = X ;; A \<union> B" 
-    using eq by blast 
-next
-  assume eq: "X = X ;; A \<union> B"
-  { fix n::nat
-    have "B ;; (A \<up> n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto }
-  then have "B ;; A\<star> \<subseteq> X" 
-    unfolding Seq_def Star_def UNION_def by auto
-  moreover
-  { fix s::string
-    obtain k where "k = length s" by auto
-    then have not_in: "s \<notin> X ;; (A \<up> Suc k)" 
-      using seq_pow_length[OF nemp] by blast
-    assume "s \<in> X"
-    then have "s \<in> X ;; (A \<up> Suc k) \<union> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))"
-      using arden_helper[OF eq, of "k"] by auto
-    then have "s \<in> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))" using not_in by auto
-    moreover
-    have "(\<Union>m\<in>{0..k}. B ;; (A \<up> m)) \<subseteq> (\<Union>n. B ;; (A \<up> n))" by auto
-    ultimately 
-    have "s \<in> B ;; A\<star>" 
-      unfolding seq_Union_left Star_def by auto }
-  then have "X \<subseteq> B ;; A\<star>" by auto
-  ultimately 
-  show "X = B ;; A\<star>" by simp
-qed
-
-
-section {* Regular Expressions *}
-
-datatype rexp =
-  NULL
-| EMPTY
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-
-
-text {* 
-  The function @{text L} is overloaded, with the idea that @{text "L x"} 
-  evaluates to the language represented by the object @{text x}.
-*}
-
-consts L:: "'a \<Rightarrow> lang"
-
-overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> lang"
-begin
-fun
-  L_rexp :: "rexp \<Rightarrow> lang"
-where
-    "L_rexp (NULL) = {}"
-  | "L_rexp (EMPTY) = {[]}"
-  | "L_rexp (CHAR c) = {[c]}"
-  | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"
-  | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
-  | "L_rexp (STAR r) = (L_rexp r)\<star>"
-end
-
-
-text {* ALT-combination of a set or regulare expressions *}
-
-abbreviation
-  Setalt  ("\<Uplus>_" [1000] 999) 
-where
-  "\<Uplus>A \<equiv> folds ALT NULL A"
-
-text {* 
-  For finite sets, @{term Setalt} is preserved under @{term L}.
-*}
-
-lemma folds_alt_simp [simp]:
-  fixes rs::"rexp set"
-  assumes a: "finite rs"
-  shows "L (\<Uplus>rs) = \<Union> (L ` rs)"
-unfolding folds_def
-apply(rule set_eqI)
-apply(rule someI2_ex)
-apply(rule_tac finite_imp_fold_graph[OF a])
-apply(erule fold_graph.induct)
-apply(auto)
-done
-
-
 section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
 
-
-text {* Just a technical lemma for collections and pairs *}
-
 lemma Pair_Collect[simp]:
   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 by simp
@@ -321,26 +16,17 @@
 where
   "\<approx>A \<equiv> {(x, y).  (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}"
 
-text {* 
-  Among the equivalence clases of @{text "\<approx>A"}, the set @{text "finals A"} 
-  singles out those which contains the strings from @{text A}.
-*}
-
 definition 
   finals :: "lang \<Rightarrow> lang set"
 where
   "finals A \<equiv> {\<approx>A `` {s} | s . s \<in> A}"
 
-
 lemma lang_is_union_of_finals: 
   shows "A = \<Union> finals A"
 unfolding finals_def
 unfolding Image_def
 unfolding str_eq_rel_def
-apply(auto)
-apply(drule_tac x = "[]" in spec)
-apply(auto)
-done
+by (auto) (metis append_Nil2)
 
 lemma finals_in_partitions:
   shows "finals A \<subseteq> (UNIV // \<approx>A)"
@@ -351,28 +37,32 @@
 
 text {* The two kinds of terms in the rhs of equations. *}
 
-datatype rhs_item = 
+datatype rhs_trm = 
    Lam "rexp"            (* Lambda-marker *)
  | Trn "lang" "rexp"     (* Transition *)
 
 
-overloading L_rhs_item \<equiv> "L:: rhs_item \<Rightarrow> lang"
+overloading L_rhs_trm \<equiv> "L:: rhs_trm \<Rightarrow> lang"
 begin
-  fun L_rhs_item:: "rhs_item \<Rightarrow> lang"
+  fun L_rhs_trm:: "rhs_trm \<Rightarrow> lang"
   where
-    "L_rhs_item (Lam r) = L r" 
-  | "L_rhs_item (Trn X r) = X ;; L r"
+    "L_rhs_trm (Lam r) = L r" 
+  | "L_rhs_trm (Trn X r) = X ;; L r"
 end
 
-overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> lang"
+overloading L_rhs \<equiv> "L:: rhs_trm set \<Rightarrow> lang"
 begin
-   fun L_rhs:: "rhs_item set \<Rightarrow> lang"
+   fun L_rhs:: "rhs_trm set \<Rightarrow> lang"
    where 
      "L_rhs rhs = \<Union> (L ` rhs)"
 end
 
+lemma L_rhs_set:
+  shows "L {Trn X r | r. P r} = \<Union>{L (Trn X r) | r. P r}"
+by (auto simp del: L_rhs_trm.simps)
+
 lemma L_rhs_union_distrib:
-  fixes A B::"rhs_item set"
+  fixes A B::"rhs_trm set"
   shows "L A \<union> L B = L (A \<union> B)"
 by simp
 
@@ -398,60 +88,34 @@
   "Init CS \<equiv> {(X, Init_rhs CS X) | X.  X \<in> CS}"
 
 
-
 section {* Arden Operation on equations *}
 
-text {*
-  The function @{text "attach_rexp r item"} SEQ-composes @{text r} to the
-  right of every rhs-item.
-*}
-
 fun 
-  append_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
+  Append_rexp :: "rexp \<Rightarrow> rhs_trm \<Rightarrow> rhs_trm"
 where
-  "append_rexp r (Lam rexp)   = Lam (SEQ rexp r)"
-| "append_rexp r (Trn X rexp) = Trn X (SEQ rexp r)"
+  "Append_rexp r (Lam rexp)   = Lam (SEQ rexp r)"
+| "Append_rexp r (Trn X rexp) = Trn X (SEQ rexp r)"
 
 
 definition
-  "append_rhs_rexp rhs rexp \<equiv> (append_rexp rexp) ` rhs"
+  "Append_rexp_rhs rhs rexp \<equiv> (Append_rexp rexp) ` rhs"
 
 definition 
   "Arden X rhs \<equiv> 
-     append_rhs_rexp (rhs - {Trn X r | r. Trn X r \<in> rhs}) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
+     Append_rexp_rhs (rhs - {Trn X r | r. Trn X r \<in> rhs}) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
 
 
 section {* Substitution Operation on equations *}
 
-text {* 
-  Suppose and equation @{text "X = xrhs"}, @{text "Subst"} substitutes 
-  all occurences of @{text "X"} in @{text "rhs"} by @{text "xrhs"}.
-*}
-
 definition 
   "Subst rhs X xrhs \<equiv> 
-        (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
-
-text {*
-  @{text "eqs_subst ES X xrhs"} substitutes @{text xrhs} into every 
-  equation of the equational system @{text ES}.
-*}
-
-types esystem = "(lang \<times> rhs_item set) set"
+        (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (Append_rexp_rhs xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
 
 definition
-  Subst_all :: "esystem \<Rightarrow> lang \<Rightarrow> rhs_item set \<Rightarrow> esystem"
+  Subst_all :: "(lang \<times> rhs_trm set) set \<Rightarrow> lang \<Rightarrow> rhs_trm set \<Rightarrow> (lang \<times> rhs_trm set) set"
 where
   "Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
-text {*
-  The following term @{text "remove ES Y yrhs"} removes the equation
-  @{text "Y = yrhs"} from equational system @{text "ES"} by replacing
-  all occurences of @{text "Y"} by its definition (using @{text "eqs_subst"}).
-  The @{text "Y"}-definition is made non-recursive using Arden's transformation
-  @{text "arden_variate Y yrhs"}.
-  *}
-
 definition
   "Remove ES X xrhs \<equiv> 
       Subst_all  (ES - {(X, xrhs)}) X (Arden X xrhs)"
@@ -459,11 +123,6 @@
 
 section {* While-combinator *}
 
-text {*
-  The following term @{text "Iter X ES"} represents one iteration in the while loop.
-  It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove.
-*}
-
 definition 
   "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
                 in Remove ES Y yrhs)"
@@ -476,64 +135,28 @@
 unfolding Iter_def using assms
 by (rule_tac a="(Y, yrhs)" in someI2) (auto)
 
-
-text {*
-  The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations
-  for unknowns other than @{text "X"} until one is left.
-*}
-
 abbreviation
   "Cond ES \<equiv> card ES \<noteq> 1"
 
 definition 
   "Solve X ES \<equiv> while Cond (Iter X) ES"
 
-text {*
-  Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},
-  the induction principle @{thm [source] while_rule} is used to proved the desired properties
-  of @{text "Solve X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
-  in terms of a series of auxilliary predicates:
-*}
 
 section {* Invariants *}
 
-text {* Every variable is defined at most once in @{text ES}. *}
-
 definition 
-  "distinct_equas ES \<equiv> 
+  "distinctness ES \<equiv> 
      \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
 
-
-text {* 
-  Every equation in @{text ES} (represented by @{text "(X, rhs)"}) 
-  is valid, i.e. @{text "X = L rhs"}.
-*}
-
 definition 
-  "sound_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
-
-text {*
-  @{text "ardenable rhs"} requires regular expressions occuring in 
-  transitional items of @{text "rhs"} do not contain empty string. This is 
-  necessary for the application of Arden's transformation to @{text "rhs"}.
-*}
+  "soundness ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
 
 definition 
   "ardenable rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
 
-text {*
-  The following @{text "ardenable_all ES"} requires that Arden's transformation 
-  is applicable to every equation of equational system @{text "ES"}.
-*}
-
 definition 
   "ardenable_all ES \<equiv> \<forall>(X, rhs) \<in> ES. ardenable rhs"
 
-
-text {* 
-  @{text "finite_rhs ES"} requires every equation in @{text "rhs"} 
-  be finite.
-*}
 definition
   "finite_rhs ES \<equiv> \<forall>(X, rhs) \<in> ES. finite rhs"
 
@@ -541,56 +164,42 @@
   "finite_rhs ES = (\<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs)"
 unfolding finite_rhs_def by auto
 
-text {*
-  @{text "classes_of rhs"} returns all variables (or equivalent classes)
-  occuring in @{text "rhs"}.
-  *}
-
 definition 
   "rhss rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
 
-text {*
-  @{text "lefts_of ES"} returns all variables defined by an 
-  equational system @{text "ES"}.
-*}
 definition
   "lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
 
-text {*
-  The following @{text "valid_eqs ES"} requires that every variable occuring 
-  on the right hand side of equations is already defined by some equation in @{text "ES"}.
-*}
 definition 
-  "valid_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
+  "validity ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
+
+lemma rhss_union_distrib:
+  shows "rhss (A \<union> B) = rhss A \<union> rhss B"
+by (auto simp add: rhss_def)
+
+lemma lhss_union_distrib:
+  shows "lhss (A \<union> B) = lhss A \<union> lhss B"
+by (auto simp add: lhss_def)
 
 
-text {*
-  The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
-  *}
 definition 
   "invariant ES \<equiv> finite ES
                 \<and> finite_rhs ES
-                \<and> sound_eqs ES 
-                \<and> distinct_equas ES 
+                \<and> soundness ES 
+                \<and> distinctness ES 
                 \<and> ardenable_all ES 
-                \<and> valid_eqs ES"
+                \<and> validity ES"
 
 
 lemma invariantI:
-  assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable_all ES" 
-          "finite_rhs ES" "valid_eqs ES"
+  assumes "soundness ES" "finite ES" "distinctness ES" "ardenable_all ES" 
+          "finite_rhs ES" "validity ES"
   shows "invariant ES"
 using assms by (simp add: invariant_def)
 
+
 subsection {* The proof of this direction *}
 
-subsubsection {* Basic properties *}
-
-text {*
-  The following are some basic properties of the above definitions.
-*}
-
-
 lemma finite_Trn:
   assumes fin: "finite rhs"
   shows "finite {r. Trn Y r \<in> rhs}"
@@ -618,55 +227,30 @@
     done
 qed
 
-lemma rexp_of_empty:
-  assumes finite: "finite rhs"
-  and nonempty: "ardenable rhs"
-  shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
-using finite nonempty ardenable_def
-using finite_Trn[OF finite]
-by auto
-
-lemma lang_of_rexp_of:
+lemma rhs_trm_soundness:
   assumes finite:"finite rhs"
   shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
 proof -
   have "finite {r. Trn X r \<in> rhs}" 
     by (rule finite_Trn[OF finite]) 
-  then show ?thesis
-    apply(auto simp add: Seq_def)
-    apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI)
-    apply(auto)
-    apply(rule_tac x= "Trn X xa" in exI)
-    apply(auto simp add: Seq_def)
-    done
+  then show "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
+    by (simp only: L_rhs_set L_rhs_trm.simps) (auto simp add: Seq_def)
 qed
 
-lemma lang_of_append:
-  "L (append_rexp r rhs_item) = L rhs_item ;; L r"
-by (induct rule: append_rexp.induct)
+lemma lang_of_append_rexp:
+  "L (Append_rexp r rhs_trm) = L rhs_trm ;; L r"
+by (induct rule: Append_rexp.induct)
    (auto simp add: seq_assoc)
 
-lemma lang_of_append_rhs:
-  "L (append_rhs_rexp rhs r) = L rhs ;; L r"
-unfolding append_rhs_rexp_def
-by (auto simp add: Seq_def lang_of_append)
+lemma lang_of_append_rexp_rhs:
+  "L (Append_rexp_rhs rhs r) = L rhs ;; L r"
+unfolding Append_rexp_rhs_def
+by (auto simp add: Seq_def lang_of_append_rexp)
 
-lemma rhss_union_distrib:
-  shows "rhss (A \<union> B) = rhss A \<union> rhss B"
-by (auto simp add: rhss_def)
-
-lemma lhss_union_distrib:
-  shows "lhss (A \<union> B) = lhss A \<union> lhss B"
-by (auto simp add: lhss_def)
 
 
 subsubsection {* Intialization *}
 
-text {*
-  The following several lemmas until @{text "init_ES_satisfy_invariant"} shows that
-  the initial equational system satisfies invariant @{text "invariant"}.
-*}
-
 lemma defined_by_str:
   assumes "s \<in> X" "X \<in> UNIV // \<approx>A" 
   shows "X = \<approx>A `` {s}"
@@ -702,42 +286,37 @@
   show "X \<subseteq> L rhs"
   proof
     fix x
-    assume "(1)": "x \<in> X"
-    show "x \<in> L rhs"          
-    proof (cases "x = []")
-      assume empty: "x = []"
-      thus ?thesis using X_in_eqs "(1)"
-        by (auto simp: Init_def Init_rhs_def)
-    next
-      assume not_empty: "x \<noteq> []"
-      then obtain clist c where decom: "x = clist @ [c]"
-        by (case_tac x rule:rev_cases, auto)
-      have "X \<in> UNIV // \<approx>A" using X_in_eqs by (auto simp:Init_def)
-      then obtain Y 
-        where "Y \<in> UNIV // \<approx>A" 
-        and "Y ;; {[c]} \<subseteq> X"
-        and "clist \<in> Y"
-        using decom "(1)" every_eqclass_has_transition by blast
-      hence 
-        "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}"
+    assume in_X: "x \<in> X"
+    { assume empty: "x = []"
+      then have "x \<in> L rhs" using X_in_eqs in_X
+	unfolding Init_def Init_rhs_def
+        by auto
+    }
+    moreover
+    { assume not_empty: "x \<noteq> []"
+      then obtain s c where decom: "x = s @ [c]"
+	using rev_cases by blast
+      have "X \<in> UNIV // \<approx>A" using X_in_eqs unfolding Init_def by auto
+      then obtain Y where "Y \<in> UNIV // \<approx>A" "Y ;; {[c]} \<subseteq> X" "s \<in> Y"
+        using decom in_X every_eqclass_has_transition by blast
+      then have "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}"
         unfolding transition_def
-	using "(1)" decom
-        by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
-      thus ?thesis using X_in_eqs "(1)"	
-        by (simp add: Init_def Init_rhs_def)
-    qed
+	using decom by (force simp add: Seq_def)
+      then have "x \<in> L rhs" using X_in_eqs in_X
+	unfolding Init_def Init_rhs_def by simp
+    }
+    ultimately show "x \<in> L rhs" by blast
   qed
 next
   show "L rhs \<subseteq> X" using X_in_eqs
-    by (auto simp:Init_def Init_rhs_def transition_def) 
+    unfolding Init_def Init_rhs_def transition_def
+    by auto 
 qed
 
 lemma test:
   assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
   shows "X = \<Union> (L `  rhs)"
-using assms
-by (drule_tac l_eq_r_in_eqs) (simp)
-
+using assms l_eq_r_in_eqs by (simp)
 
 lemma finite_Init_rhs: 
   assumes finite: "finite CS"
@@ -759,31 +338,26 @@
   assumes finite_CS: "finite (UNIV // \<approx>A)"
   shows "invariant (Init (UNIV // \<approx>A))"
 proof (rule invariantI)
-  show "sound_eqs (Init (UNIV // \<approx>A))"
-    unfolding sound_eqs_def 
+  show "soundness (Init (UNIV // \<approx>A))"
+    unfolding soundness_def 
     using l_eq_r_in_eqs by auto
   show "finite (Init (UNIV // \<approx>A))" using finite_CS
     unfolding Init_def by simp
-  show "distinct_equas (Init (UNIV // \<approx>A))"     
-    unfolding distinct_equas_def Init_def by simp
+  show "distinctness (Init (UNIV // \<approx>A))"     
+    unfolding distinctness_def Init_def by simp
   show "ardenable_all (Init (UNIV // \<approx>A))"
     unfolding ardenable_all_def Init_def Init_rhs_def ardenable_def
    by auto 
   show "finite_rhs (Init (UNIV // \<approx>A))"
     using finite_Init_rhs[OF finite_CS]
     unfolding finite_rhs_def Init_def by auto
-  show "valid_eqs (Init (UNIV // \<approx>A))"
-    unfolding valid_eqs_def Init_def Init_rhs_def rhss_def lhss_def
+  show "validity (Init (UNIV // \<approx>A))"
+    unfolding validity_def Init_def Init_rhs_def rhss_def lhss_def
     by auto
 qed
 
 subsubsection {* Interation step *}
 
-text {*
-  From this point until @{text "iteration_step"}, 
-  the correctness of the iteration step @{text "Iter X ES"} is proved.
-*}
-
 lemma Arden_keeps_eq:
   assumes l_eq_r: "X = L rhs"
   and not_empty: "ardenable rhs"
@@ -791,40 +365,39 @@
   shows "X = L (Arden X rhs)"
 proof -
   def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"
-  def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}"
-  def B \<equiv> "L b" 
-  have "X = B ;; A\<star>"
-  proof -
-    have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)
-    also have "\<dots> = X ;; A \<union> B"
-      unfolding L_rhs_union_distrib[symmetric]
-      by (simp only: lang_of_rexp_of finite B_def A_def)
-    finally show ?thesis
-      apply(rule_tac arden[THEN iffD1])
-      apply(simp (no_asm) add: A_def)
-      using finite_Trn[OF finite] not_empty
-      apply(simp add: ardenable_def)
-      using l_eq_r
-      apply(simp)
-      done
-  qed
-  moreover have "L (Arden X rhs) = B ;; A\<star>"
-    by (simp only:Arden_def L_rhs_union_distrib lang_of_append_rhs 
-                  B_def A_def b_def L_rexp.simps seq_union_distrib_left)
-   ultimately show ?thesis by simp
+  def b \<equiv> "{Trn X r | r. Trn X r \<in> rhs}"
+  def B \<equiv> "L (rhs - b)"
+  have not_empty2: "[] \<notin> A" 
+    using finite_Trn[OF finite] not_empty
+    unfolding A_def ardenable_def by simp
+  have "X = L rhs" using l_eq_r by simp
+  also have "\<dots> = L (b \<union> (rhs - b))" unfolding b_def by auto
+  also have "\<dots> = L b \<union> B" unfolding B_def by (simp only: L_rhs_union_distrib)
+  also have "\<dots> = X ;; A \<union> B"
+    unfolding b_def
+    unfolding rhs_trm_soundness[OF finite]
+    unfolding A_def
+    by blast
+  finally have "X = X ;; A \<union> B" . 
+  then have "X = B ;; A\<star>"
+    by (simp add: arden[OF not_empty2])
+  also have "\<dots> = L (Arden X rhs)"
+    unfolding Arden_def A_def B_def b_def
+    by (simp only: lang_of_append_rexp_rhs L_rexp.simps)
+  finally show "X = L (Arden X rhs)" by simp
 qed 
 
-lemma append_keeps_finite:
-  "finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"
-by (auto simp:append_rhs_rexp_def)
+lemma Append_keeps_finite:
+  "finite rhs \<Longrightarrow> finite (Append_rexp_rhs rhs r)"
+by (auto simp:Append_rexp_rhs_def)
 
 lemma Arden_keeps_finite:
   "finite rhs \<Longrightarrow> finite (Arden X rhs)"
-by (auto simp:Arden_def append_keeps_finite)
+by (auto simp:Arden_def Append_keeps_finite)
 
-lemma append_keeps_nonempty:
-  "ardenable rhs \<Longrightarrow> ardenable (append_rhs_rexp rhs r)"
-apply (auto simp:ardenable_def append_rhs_rexp_def)
+lemma Append_keeps_nonempty:
+  "ardenable rhs \<Longrightarrow> ardenable (Append_rexp_rhs rhs r)"
+apply (auto simp:ardenable_def Append_rexp_rhs_def)
 by (case_tac x, auto simp:Seq_def)
 
 lemma nonempty_set_sub:
@@ -837,12 +410,12 @@
 
 lemma Arden_keeps_nonempty:
   "ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)"
-by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub)
+by (simp only:Arden_def Append_keeps_nonempty nonempty_set_sub)
 
 
 lemma Subst_keeps_nonempty:
   "\<lbrakk>ardenable rhs; ardenable xrhs\<rbrakk> \<Longrightarrow> ardenable (Subst rhs X xrhs)"
-by (simp only:Subst_def append_keeps_nonempty  nonempty_set_union nonempty_set_sub)
+by (simp only: Subst_def Append_keeps_nonempty nonempty_set_union nonempty_set_sub)
 
 lemma Subst_keeps_eq:
   assumes substor: "X = L xrhs"
@@ -850,7 +423,7 @@
   shows "L (Subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
 proof-
   def A \<equiv> "L (rhs - {Trn X r | r. Trn X r \<in> rhs})"
-  have "?Left = A \<union> L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
+  have "?Left = A \<union> L (Append_rexp_rhs xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
     unfolding Subst_def
     unfolding L_rhs_union_distrib[symmetric]
     by (simp add: A_def)
@@ -862,14 +435,14 @@
       unfolding L_rhs_union_distrib
       by simp
   qed
-  moreover have "L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})" 
-    using finite substor  by (simp only:lang_of_append_rhs lang_of_rexp_of)
+  moreover have "L (Append_rexp_rhs xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})" 
+    using finite substor by (simp only: lang_of_append_rexp_rhs rhs_trm_soundness)
   ultimately show ?thesis by simp
 qed
 
 lemma Subst_keeps_finite_rhs:
   "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)"
-by (auto simp:Subst_def append_keeps_finite)
+by (auto simp: Subst_def Append_keeps_finite)
 
 lemma Subst_all_keeps_finite:
   assumes finite: "finite ES"
@@ -889,8 +462,8 @@
 by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def)
 
 lemma append_rhs_keeps_cls:
-  "rhss (append_rhs_rexp rhs r) = rhss rhs"
-apply (auto simp:rhss_def append_rhs_rexp_def)
+  "rhss (Append_rexp_rhs rhs r) = rhss rhs"
+apply (auto simp:rhss_def Append_rexp_rhs_def)
 apply (case_tac xa, auto simp:image_def)
 by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
 
@@ -909,9 +482,9 @@
 apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib)
 by (auto simp:rhss_def)
 
-lemma Subst_all_keeps_valid_eqs:
-  assumes sc: "valid_eqs (ES \<union> {(Y, yrhs)})"        (is "valid_eqs ?A")
-  shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))"  (is "valid_eqs ?B")
+lemma Subst_all_keeps_validity:
+  assumes sc: "validity (ES \<union> {(Y, yrhs)})"        (is "validity ?A")
+  shows "validity (Subst_all ES Y (Arden Y yrhs))"  (is "validity ?B")
 proof -
   { fix X xrhs'
     assume "(X, xrhs') \<in> ?B"
@@ -930,16 +503,16 @@
           thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
         qed
         moreover have "rhss xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
-          apply (simp only:valid_eqs_def lhss_union_distrib)
+          apply (simp only:validity_def lhss_union_distrib)
           by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def)
         moreover have "rhss (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}" 
           using sc 
-          by (auto simp add:Arden_removes_cl valid_eqs_def lhss_def)
+          by (auto simp add:Arden_removes_cl validity_def lhss_def)
         ultimately show ?thesis by auto
       qed
       ultimately show ?thesis by simp
     qed
-  } thus ?thesis by (auto simp only:Subst_all_def valid_eqs_def)
+  } thus ?thesis by (auto simp only:Subst_all_def validity_def)
 qed
 
 lemma Subst_all_satisfies_invariant:
@@ -947,12 +520,12 @@
   shows "invariant (Subst_all ES Y (Arden Y yrhs))"
 proof (rule invariantI)
   have Y_eq_yrhs: "Y = L yrhs" 
-    using invariant_ES by (simp only:invariant_def sound_eqs_def, blast)
+    using invariant_ES by (simp only:invariant_def soundness_def, blast)
    have finite_yrhs: "finite yrhs" 
     using invariant_ES by (auto simp:invariant_def finite_rhs_def)
   have nonempty_yrhs: "ardenable yrhs" 
     using invariant_ES by (auto simp:invariant_def ardenable_all_def)
-  show "sound_eqs (Subst_all ES Y (Arden Y yrhs))"
+  show "soundness (Subst_all ES Y (Arden Y yrhs))"
   proof -
     have "Y = L (Arden Y yrhs)" 
       using Y_eq_yrhs invariant_ES finite_yrhs
@@ -963,19 +536,19 @@
       apply(auto)
       done
     thus ?thesis using invariant_ES
-      unfolding invariant_def finite_rhs_def2 sound_eqs_def Subst_all_def
+      unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def
       by (auto simp add: Subst_keeps_eq simp del: L_rhs.simps)
   qed
   show "finite (Subst_all ES Y (Arden Y yrhs))" 
     using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
-  show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" 
+  show "distinctness (Subst_all ES Y (Arden Y yrhs))" 
     using invariant_ES 
-    unfolding distinct_equas_def Subst_all_def invariant_def by auto
+    unfolding distinctness_def Subst_all_def invariant_def by auto
   show "ardenable_all (Subst_all ES Y (Arden Y yrhs))"
   proof - 
     { fix X rhs
       assume "(X, rhs) \<in> ES"
-      hence "ardenable rhs"  using prems invariant_ES  
+      hence "ardenable rhs"  using invariant_ES  
         by (auto simp add:invariant_def ardenable_all_def)
       with nonempty_yrhs 
       have "ardenable (Subst rhs Y (Arden Y yrhs))"
@@ -996,8 +569,8 @@
     ultimately show ?thesis 
       by (simp add:Subst_all_keeps_finite_rhs)
   qed
-  show "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
-    using invariant_ES Subst_all_keeps_valid_eqs by (simp add:invariant_def)
+  show "validity (Subst_all ES Y (Arden Y yrhs))"
+    using invariant_ES Subst_all_keeps_validity by (simp add:invariant_def)
 qed
 
 lemma Remove_in_card_measure:
@@ -1049,7 +622,7 @@
     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
     using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
-    using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+    using X_in_ES Inv_ES unfolding invariant_def distinctness_def
     by auto
   then show "(Iter X ES, ES) \<in> measure card" 
   apply(rule IterI2)
@@ -1069,7 +642,7 @@
     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
     using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
   then have "(Y, yrhs) \<in> ES" "X \<noteq> Y" 
-    using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+    using X_in_ES Inv_ES unfolding invariant_def distinctness_def
     by auto
   then show "invariant (Iter X ES)" 
   proof(rule IterI2)
@@ -1078,7 +651,6 @@
     then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
     then show "invariant (Remove ES Y yrhs)" unfolding Remove_def
       using Inv_ES
-      thm Subst_all_satisfies_invariant
       by (rule_tac Subst_all_satisfies_invariant) (simp) 
   qed
 qed
@@ -1091,10 +663,10 @@
 proof -
   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
   then obtain Y yrhs 
-    where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
+    where "(Y, yrhs) \<in> ES" "(X, xrhs) \<noteq> (Y, yrhs)" 
     using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
-    using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+    using X_in_ES Inv_ES unfolding invariant_def distinctness_def
     by auto
   then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" 
   apply(rule IterI2)
@@ -1159,7 +731,7 @@
 
   def A \<equiv> "Arden X xrhs"
   have "rhss xrhs \<subseteq> {X}" using Inv_ES 
-    unfolding valid_eqs_def invariant_def rhss_def lhss_def
+    unfolding validity_def invariant_def rhss_def lhss_def
     by auto
   then have "rhss A = {}" unfolding A_def 
     by (simp add: Arden_removes_cl)
@@ -1170,7 +742,7 @@
     using Arden_keeps_finite by auto
   then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam)
 
-  have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def
+  have "X = L xrhs" using Inv_ES unfolding invariant_def soundness_def
     by simp
   then have "X = L A" using Inv_ES 
     unfolding A_def invariant_def ardenable_all_def finite_rhs_def 
diff -r a8a442ba0dbf -r e93760534354 Myhill_2.thy
--- a/Myhill_2.thy	Thu May 12 05:55:05 2011 +0000
+++ b/Myhill_2.thy	Wed May 18 19:54:43 2011 +0000
@@ -1,64 +1,15 @@
 theory Myhill_2
-  imports Myhill_1 
-          Prefix_subtract
+  imports Myhill_1 Prefix_subtract
           "~~/src/HOL/Library/List_Prefix"
 begin
 
 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
 
-subsection {* The scheme*}
-
-text {* 
-  The following convenient notation @{text "x \<approx>A y"} means:
-  string @{text "x"} and @{text "y"} are equivalent with respect to 
-  language @{text "A"}.
-  *}
-
 definition
   str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
 where
   "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
 
-text {*
-  The main lemma (@{text "rexp_imp_finite"}) is proved by a structural
-  induction over regular expressions.  where base cases (cases for @{const
-  "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to
-  proof. Real difficulty lies in inductive cases.  By inductive hypothesis,
-  languages defined by sub-expressions induce finite partitiions. Under such
-  hypothsis, we need to prove that the language defined by the composite
-  regular expression gives rise to finite partion.  The basic idea is to
-  attach a tag @{text "tag(x)"} to every string @{text "x"}. The tagging
-  fuction @{text "tag"} is carefully devised, which returns tags made of
-  equivalent classes of the partitions induced by subexpressoins, and
-  therefore has a finite range. Let @{text "Lang"} be the composite language,
-  it is proved that:
-  \begin{quote}
-  If strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as:
-  \[
-  @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}
-  \]
-  then the partition induced by @{text "Lang"} must be finite.
-  \end{quote}
-  There are two arguments for this. The first goes as the following:
-  \begin{enumerate}
-    \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"} 
-          (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}).
-    \item It is shown that: if the range of @{text "tag"} (denoted @{text "range(tag)"}) is finite, 
-           the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}).
-           Since tags are made from equivalent classes from component partitions, and the inductive
-           hypothesis ensures the finiteness of these partitions, it is not difficult to prove
-           the finiteness of @{text "range(tag)"}.
-    \item It is proved that if equivalent relation @{text "R1"} is more refined than @{text "R2"}
-           (expressed as @{text "R1 \<subseteq> R2"}),
-           and the partition induced by @{text "R1"} is finite, then the partition induced by @{text "R2"}
-           is finite as well (lemma @{text "refined_partition_finite"}).
-    \item The injectivity assumption @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} implies that
-            @{text "(=tag=)"} is more refined than @{text "(\<approx>Lang)"}.
-    \item Combining the points above, we have: the partition induced by language @{text "Lang"}
-          is finite (lemma @{text "tag_finite_imageD"}).
-  \end{enumerate}
-*}
-
 definition 
    tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=")
 where
@@ -69,7 +20,6 @@
   shows "finite (UNIV // =tag=)"
 proof -
   let "?f" =  "\<lambda>X. tag ` X" and ?A = "(UNIV // =tag=)"
-    -- {* The finiteness of @{text "f"}-image is a consequence of @{text "rng_fnt"} *}
   have "finite (?f ` ?A)" 
   proof -
     have "range ?f \<subseteq> (Pow (range tag))" unfolding Pow_def by auto
@@ -82,25 +32,23 @@
     ultimately show "finite (?f ` ?A)" by (rule rev_finite_subset) 
   qed
   moreover
-    -- {* The injectivity of @{text "f"}-image follows from the definition of @{text "(=tag=)"} *}
   have "inj_on ?f ?A"
   proof -
     { fix X Y
       assume X_in: "X \<in> ?A"
         and  Y_in: "Y \<in> ?A"
         and  tag_eq: "?f X = ?f Y"
-      then
-      obtain x y 
+      then obtain x y 
         where "x \<in> X" "y \<in> Y" "tag x = tag y"
         unfolding quotient_def Image_def image_def tag_eq_rel_def
         by (simp) (blast)
       with X_in Y_in 
       have "X = Y"
 	unfolding quotient_def tag_eq_rel_def by auto
-    } then show "inj_on ?f ?A" unfolding inj_on_def by auto
+    } 
+    then show "inj_on ?f ?A" unfolding inj_on_def by auto
   qed
-  ultimately 
-  show "finite (UNIV // =tag=)" by (rule finite_imageD)
+  ultimately show "finite (UNIV // =tag=)" by (rule finite_imageD)
 qed
 
 lemma refined_partition_finite:
@@ -142,7 +90,7 @@
 
 lemma tag_finite_imageD:
   assumes rng_fnt: "finite (range tag)" 
-  and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>A n"
+  and same_tag_eqvt: "\<And>m n. tag m = tag n \<Longrightarrow> m \<approx>A n"
   shows "finite (UNIV // \<approx>A)"
 proof (rule_tac refined_partition_finite [of "=tag="])
   show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])
@@ -161,48 +109,23 @@
 qed
 
 
-subsection {* The proof*}
-
-text {*
-  Each case is given in a separate section, as well as the final main lemma. Detailed explainations accompanied by
-  illustrations are given for non-trivial cases.
-
-  For ever inductive case, there are two tasks, the easier one is to show the range finiteness of
-  of the tagging function based on the finiteness of component partitions, the
-  difficult one is to show that strings with the same tag are equivalent with respect to the 
-  composite language. Suppose the composite language be @{text "Lang"}, tagging function be 
-  @{text "tag"}, it amounts to show:
-  \[
-  @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}
-  \]
-  expanding the definition of @{text "\<approx>Lang"}, it amounts to show:
-  \[
-  @{text "tag(x) = tag(y) \<Longrightarrow> (\<forall> z. x@z \<in> Lang \<longleftrightarrow> y@z \<in> Lang)"}
-  \]
-  Because the assumed tag equlity @{text "tag(x) = tag(y)"} is symmetric,
-  it is suffcient to show just one direction:
-  \[
-  @{text "\<And> x y z. \<lbrakk>tag(x) = tag(y); x@z \<in> Lang\<rbrakk> \<Longrightarrow> y@z \<in> Lang"}
-  \]
-  This is the pattern followed by every inductive case.
-  *}
+subsection {* The proof *}
 
 subsubsection {* The base case for @{const "NULL"} *}
 
 lemma quot_null_eq:
-  shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)"
-  unfolding quotient_def Image_def str_eq_rel_def by auto
+  shows "UNIV // \<approx>{} = {UNIV}"
+unfolding quotient_def Image_def str_eq_rel_def by auto
 
 lemma quot_null_finiteI [intro]:
-  shows "finite ((UNIV // \<approx>{})::lang set)"
+  shows "finite (UNIV // \<approx>{})"
 unfolding quot_null_eq by simp
 
 
 subsubsection {* The base case for @{const "EMPTY"} *}
 
-
 lemma quot_empty_subset:
-  "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
+  shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}"
 proof
   fix x
   assume "x \<in> UNIV // \<approx>{[]}"
@@ -221,7 +144,7 @@
 qed
 
 lemma quot_empty_finiteI [intro]:
-  shows "finite (UNIV // (\<approx>{[]}))"
+  shows "finite (UNIV // \<approx>{[]})"
 by (rule finite_subset[OF quot_empty_subset]) (simp)
 
 
@@ -237,23 +160,24 @@
   show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}"
   proof -
     { assume "y = []" hence "x = {[]}" using h 
-        by (auto simp:str_eq_rel_def)
-    } moreover {
-      assume "y = [c]" hence "x = {[c]}" using h 
-        by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def)
-    } moreover {
-      assume "y \<noteq> []" and "y \<noteq> [c]"
+        by (auto simp:str_eq_rel_def) } 
+    moreover 
+    { assume "y = [c]" hence "x = {[c]}" using h 
+        by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def) } 
+    moreover 
+    { assume "y \<noteq> []" and "y \<noteq> [c]"
       hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto)
       moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])" 
         by (case_tac p, auto)
       ultimately have "x = UNIV - {[],[c]}" using h
         by (auto simp add:str_eq_rel_def)
-    } ultimately show ?thesis by blast
+    } 
+    ultimately show ?thesis by blast
   qed
 qed
 
 lemma quot_char_finiteI [intro]:
-  shows "finite (UNIV // (\<approx>{[c]}))"
+  shows "finite (UNIV // \<approx>{[c]})"
 by (rule finite_subset[OF quot_char_subset]) (simp)
 
 
@@ -265,7 +189,6 @@
   "tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
 
 lemma quot_union_finiteI [intro]:
-  fixes L1 L2::"lang"
   assumes finite1: "finite (UNIV // \<approx>A)"
   and     finite2: "finite (UNIV // \<approx>B)"
   shows "finite (UNIV // \<approx>(A \<union> B))"
@@ -283,140 +206,79 @@
     by auto
 qed
 
+
 subsubsection {* The inductive case for @{text "SEQ"}*}
 
-text {*
-  For case @{const "SEQ"}, the language @{text "L"} is @{text "L\<^isub>1 ;; L\<^isub>2"}.
-  Given @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"}, according to the defintion of @{text " L\<^isub>1 ;; L\<^isub>2"},
-  string @{text "x @ z"} can be splitted with the prefix in @{text "L\<^isub>1"} and suffix in @{text "L\<^isub>2"}.
-  The split point can either be in @{text "x"} (as shown in Fig. \ref{seq_first_split}),
-  or in @{text "z"} (as shown in Fig. \ref{seq_snd_split}). Whichever way it goes, the structure
-  on @{text "x @ z"} cn be transfered faithfully onto @{text "y @ z"} 
-  (as shown in Fig. \ref{seq_trans_first_split} and \ref{seq_trans_snd_split}) with the the help of the assumed 
-  tag equality. The following tag function @{text "tag_str_SEQ"} is such designed to facilitate
-  such transfers and lemma @{text "tag_str_SEQ_injI"} formalizes the informal argument above. The details 
-  of structure transfer will be given their.
-\input{fig_seq}
-
-  *}
-
 definition 
   tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
 where
   "tag_str_SEQ L1 L2 \<equiv>
-     (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - x'}) | x'.  x' \<le> x \<and> x' \<in> L1}))"
-
-text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*}
+     (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"
 
-lemma append_seq_elim:
-  assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2"
-  shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> 
-          (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"
-proof-
-  from assms obtain s\<^isub>1 s\<^isub>2 
-    where eq_xys: "x @ y = s\<^isub>1 @ s\<^isub>2" 
-    and in_seq: "s\<^isub>1 \<in> L\<^isub>1 \<and> s\<^isub>2 \<in> L\<^isub>2" 
-    by (auto simp:Seq_def)
-  from app_eq_dest [OF eq_xys]
-  have
-    "(x \<le> s\<^isub>1 \<and> (s\<^isub>1 - x) @ s\<^isub>2 = y) \<or> (s\<^isub>1 \<le> x \<and> (x - s\<^isub>1) @ y = s\<^isub>2)" 
-               (is "?Split1 \<or> ?Split2") .
-  moreover have "?Split1 \<Longrightarrow> \<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2" 
-    using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE)
-  moreover have "?Split2 \<Longrightarrow> \<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2" 
-    using in_seq by (rule_tac x = s\<^isub>1 in exI, auto)
-  ultimately show ?thesis by blast
-qed
-
+lemma Seq_in_cases:
+  assumes "x @ z \<in> A ;; B"
+  shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> 
+         (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)"
+using assms
+unfolding Seq_def prefix_def
+by (auto simp add: append_eq_append_conv2)
 
 lemma tag_str_SEQ_injI:
-  fixes v w 
-  assumes eq_tag: "tag_str_SEQ L\<^isub>1 L\<^isub>2 v = tag_str_SEQ L\<^isub>1 L\<^isub>2 w" 
-  shows "v \<approx>(L\<^isub>1 ;; L\<^isub>2) w"
-proof-
-    -- {* As explained before, a pattern for just one direction needs to be dealt with:*}
+  assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y" 
+  shows "x \<approx>(A ;; B) y"
+proof -
   { fix x y z
-    assume xz_in_seq: "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"
-    and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
-    have"y @ z \<in> L\<^isub>1 ;; L\<^isub>2" 
-    proof-
-      -- {* There are two ways to split @{text "x@z"}: *}
-      from append_seq_elim [OF xz_in_seq]
-      have "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or> 
-               (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)" .
-      -- {* It can be shown that @{text "?thesis"} holds in either case: *}
-      moreover {
-        -- {* The case for the first split:*}
-        fix xa
-        assume h1: "xa \<le> x" and h2: "xa \<in> L\<^isub>1" and h3: "(x - xa) @ z \<in> L\<^isub>2"
-        -- {* The following subgoal implements the structure transfer:*}
-        obtain ya 
-          where "ya \<le> y" 
-          and "ya \<in> L\<^isub>1" 
-          and "(y - ya) @ z \<in> L\<^isub>2"
+    assume xz_in_seq: "x @ z \<in> A ;; B"
+    and tag_xy: "tag_str_SEQ A B x = tag_str_SEQ A B y"
+    have"y @ z \<in> A ;; B" 
+    proof -
+      { (* first case with x' in A and (x - x') @ z in B *)
+        fix x'
+        assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B"
+        obtain y' 
+          where "y' \<le> y" 
+          and "y' \<in> A" 
+          and "(y - y') @ z \<in> B"
         proof -
-        -- {*
-            \begin{minipage}{0.8\textwidth}
-            By expanding the definition of 
-            @{thm [display] "tag_xy"}
-            and extracting the second compoent, we get:
-            \end{minipage}
-            *}
-          have "{\<approx>L\<^isub>2 `` {x - xa} |xa. xa \<le> x \<and> xa \<in> L\<^isub>1} = 
-                   {\<approx>L\<^isub>2 `` {y - ya} |ya. ya \<le> y \<and> ya \<in> L\<^isub>1}" (is "?Left = ?Right")
+          have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} = 
+                {\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right")
             using tag_xy unfolding tag_str_SEQ_def by simp
-            -- {* Since @{thm "h1"} and @{thm "h2"} hold, it is not difficult to show: *}
-          moreover have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Left" using h1 h2 by auto
-            -- {* 
-            \begin{minipage}{0.7\textwidth}
-            Through tag equality, equivalent class @{term "\<approx>L\<^isub>2 `` {x - xa}"} also 
-                  belongs to the @{text "?Right"}:
-            \end{minipage}
-            *}
-          ultimately have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Right" by simp
-            -- {* From this, the counterpart of @{text "xa"} in @{text "y"} is obtained:*}
-          then obtain ya 
-            where eq_xya: "\<approx>L\<^isub>2 `` {x - xa} = \<approx>L\<^isub>2 `` {y - ya}" 
-            and pref_ya: "ya \<le> y" and ya_in: "ya \<in> L\<^isub>1"
+          moreover 
+	  have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto
+          ultimately 
+	  have "\<approx>B `` {x - x'} \<in> ?Right" by simp
+          then obtain y' 
+            where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}" 
+            and pref_y': "y' \<le> y" and y'_in: "y' \<in> A"
             by simp blast
-          -- {* It can be proved that @{text "ya"} has the desired property:*}
-          have "(y - ya)@z \<in> L\<^isub>2" 
-          proof -
-            from eq_xya have "(x - xa)  \<approx>L\<^isub>2 (y - ya)" 
-              unfolding Image_def str_eq_rel_def str_eq_def by auto
-            with h3 show ?thesis unfolding str_eq_rel_def str_eq_def by simp
-          qed
-          -- {* Now, @{text "ya"} has all properties to be a qualified candidate:*}
-          with pref_ya ya_in 
+	  
+	  have "(x - x')  \<approx>B (y - y')" using eq_xy'
+            unfolding Image_def str_eq_rel_def str_eq_def by auto
+          with h3 have "(y - y') @ z \<in> B" 
+	    unfolding str_eq_rel_def str_eq_def by simp
+          with pref_y' y'_in 
           show ?thesis using that by blast
         qed
-          -- {* From the properties of @{text "ya"}, @{text "y @ z \<in> L\<^isub>1 ;; L\<^isub>2"} is derived easily.*}
-        hence "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def)
-      } moreover {
-        -- {* The other case is even more simpler: *}
-        fix za
-        assume h1: "za \<le> z" and h2: "(x @ za) \<in> L\<^isub>1" and h3: "z - za \<in> L\<^isub>2"
-        have "y @ za \<in> L\<^isub>1"
-        proof-
-          have "\<approx>L\<^isub>1 `` {x} = \<approx>L\<^isub>1 `` {y}" 
-            using tag_xy unfolding tag_str_SEQ_def by simp
-          with h2 show ?thesis
+	then have "y @ z \<in> A ;; B" by (erule_tac prefixE) (auto simp: Seq_def)
+      } 
+      moreover 
+      { (* second case with x @ z' in A and z - z' in B *)
+        fix z'
+        assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B"
+	 have "\<approx>A `` {x} = \<approx>A `` {y}" 
+           using tag_xy unfolding tag_str_SEQ_def by simp
+         with h2 have "y @ z' \<in> A"
             unfolding Image_def str_eq_rel_def str_eq_def by auto
-        qed
-        with h1 h3 have "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" 
-          by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE)
+        with h1 h3 have "y @ z \<in> A ;; B"
+	  unfolding prefix_def Seq_def
+	  by (auto) (metis append_assoc)
       }
-      ultimately show ?thesis by blast
+      ultimately show "y @ z \<in> A ;; B" 
+	using Seq_in_cases [OF xz_in_seq] by blast
     qed
-  } 
-  -- {* 
-      \begin{minipage}{0.8\textwidth}
-      @{text "?thesis"} is proved by exploiting the symmetry of 
-      @{thm [source] "eq_tag"}:
-      \end{minipage}
-      *}
+  }
   from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
-    show ?thesis unfolding str_eq_def str_eq_rel_def by blast
+    show "x \<approx>(A ;; B) y" unfolding str_eq_def str_eq_rel_def by blast
 qed 
 
 lemma quot_seq_finiteI [intro]:
@@ -437,53 +299,13 @@
     by auto
 qed
 
+
 subsubsection {* The inductive case for @{const "STAR"} *}
 
-text {* 
-  This turned out to be the trickiest case. The essential goal is 
-  to proved @{text "y @ z \<in>  L\<^isub>1*"} under the assumptions that @{text "x @ z \<in>  L\<^isub>1*"}
-  and that @{text "x"} and @{text "y"} have the same tag. The reasoning goes as the following:
-  \begin{enumerate}
-    \item Since @{text "x @ z \<in>  L\<^isub>1*"} holds, a prefix @{text "xa"} of @{text "x"} can be found
-          such that @{text "xa \<in> L\<^isub>1*"} and @{text "(x - xa)@z \<in> L\<^isub>1*"}, as shown in Fig. \ref{first_split}.
-          Such a prefix always exists, @{text "xa = []"}, for example, is one. 
-    \item There could be many but fintie many of such @{text "xa"}, from which we can find the longest
-          and name it @{text "xa_max"}, as shown in Fig. \ref{max_split}.
-    \item The next step is to split @{text "z"} into @{text "za"} and @{text "zb"} such that
-           @{text "(x - xa_max) @ za \<in> L\<^isub>1"} and @{text "zb \<in> L\<^isub>1*"}  as shown in Fig. \ref{last_split}.
-          Such a split always exists because:
-          \begin{enumerate}
-            \item Because @{text "(x - x_max) @ z \<in> L\<^isub>1*"}, it can always be splitted into prefix @{text "a"}
-              and suffix @{text "b"}, such that @{text "a \<in> L\<^isub>1"} and @{text "b \<in> L\<^isub>1*"},
-              as shown in Fig. \ref{ab_split}.
-            \item But the prefix @{text "a"} CANNOT be shorter than @{text "x - xa_max"} 
-              (as shown in Fig. \ref{ab_split_wrong}), becasue otherwise,
-                   @{text "ma_max@a"} would be in the same kind as @{text "xa_max"} but with 
-                   a larger size, conflicting with the fact that @{text "xa_max"} is the longest.
-          \end{enumerate}
-    \item  \label{tansfer_step} 
-         By the assumption that @{text "x"} and @{text "y"} have the same tag, the structure on @{text "x @ z"}
-          can be transferred to @{text "y @ z"} as shown in Fig. \ref{trans_split}. The detailed steps are:
-          \begin{enumerate}
-            \item A @{text "y"}-prefix @{text "ya"} corresponding to @{text "xa"} can be found, 
-                  which satisfies conditions: @{text "ya \<in> L\<^isub>1*"} and @{text "(y - ya)@za \<in> L\<^isub>1"}.
-            \item Since we already know @{text "zb \<in> L\<^isub>1*"}, we get @{text "(y - ya)@za@zb \<in> L\<^isub>1*"},
-                  and this is just @{text "(y - ya)@z \<in> L\<^isub>1*"}.
-            \item With fact @{text "ya \<in> L\<^isub>1*"}, we finally get @{text "y@z \<in> L\<^isub>1*"}.
-          \end{enumerate}
-  \end{enumerate}
-
-  The formal proof of lemma @{text "tag_str_STAR_injI"} faithfully follows this informal argument 
-  while the tagging function @{text "tag_str_STAR"} is defined to make the transfer in step
-  \ref{ansfer_step} feasible.
-
-  \input{fig_star}
-*} 
-
 definition 
   tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
 where
-  "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - x'} | x'. x' < x \<and> x' \<in> L1\<star>})"
+  "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
 
 text {* A technical lemma. *}
 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> 
@@ -513,7 +335,8 @@
 qed
 
 
-text {* The following is a technical lemma.which helps to show the range finiteness of tag function. *}
+text {* The following is a technical lemma, which helps to show the range finiteness of tag function. *}
+
 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"
 apply (induct x rule:rev_induct, simp)
 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
@@ -521,46 +344,26 @@
 
 
 lemma tag_str_STAR_injI:
-  fixes v w
   assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
-  shows "(v::string) \<approx>(L\<^isub>1\<star>) w"
+  shows "v \<approx>(L\<^isub>1\<star>) w"
 proof-
-    -- {* As explained before, a pattern for just one direction needs to be dealt with:*}
   { fix x y z
     assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" 
       and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
     have "y @ z \<in> L\<^isub>1\<star>"
     proof(cases "x = []")
-      -- {* 
-        The degenerated case when @{text "x"} is a null string is easy to prove:
-        *}
       case True
       with tag_xy have "y = []" 
         by (auto simp add: tag_str_STAR_def strict_prefix_def)
       thus ?thesis using xz_in_star True by simp
     next
-        -- {* The nontrival case:
-        *}
       case False
-      -- {* 
-        \begin{minipage}{0.8\textwidth}
-        Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splitted
-        by a prefix @{text "xa"} together with its suffix @{text "x - xa"}, such
-        that both @{text "xa"} and @{text "(x - xa) @ z"} are in @{text "L\<^isub>1\<star>"},
-        and there could be many such splittings.Therefore, the following set @{text "?S"} 
-        is nonempty, and finite as well:
-        \end{minipage}
-        *}
       let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
       have "finite ?S"
         by (rule_tac B = "{xa. xa < x}" in finite_subset, 
           auto simp:finite_strict_prefix_set)
       moreover have "?S \<noteq> {}" using False xz_in_star
         by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)
-      -- {* \begin{minipage}{0.7\textwidth} 
-            Since @{text "?S"} is finite, we can always single out the longest and name it @{text "xa_max"}: 
-            \end{minipage}
-          *}
       ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max" 
         using finite_set_has_max by blast
       then obtain xa_max 
@@ -570,12 +373,6 @@
         and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>  
                                      \<longrightarrow> length xa \<le> length xa_max"
         by blast
-      -- {*
-          \begin{minipage}{0.8\textwidth}
-          By the equality of tags, the counterpart of @{text "xa_max"} among 
-          @{text "y"}-prefixes, named @{text "ya"}, can be found:
-          \end{minipage}
-          *}
       obtain ya 
         where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" 
         and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)"
@@ -588,47 +385,25 @@
         thus ?thesis using that 
           apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast
       qed 
-      -- {*
-          \begin{minipage}{0.8\textwidth}
-          The @{text "?thesis"}, @{prop "y @ z \<in> L\<^isub>1\<star>"}, is a simple consequence
-          of the following proposition:
-          \end{minipage}
-          *}
       have "(y - ya) @ z \<in> L\<^isub>1\<star>" 
       proof-
-        -- {* The idea is to split the suffix @{text "z"} into @{text "za"} and @{text "zb"}, 
-          such that: *}
         obtain za zb where eq_zab: "z = za @ zb" 
           and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"
         proof -
-          -- {* 
-            \begin{minipage}{0.8\textwidth}
-            Since @{thm "h1"}, @{text "x"} can be splitted into
-            @{text "a"} and @{text "b"} such that:
-            \end{minipage}
-            *}
           from h1 have "(x - xa_max) @ z \<noteq> []" 
             by (auto simp:strict_prefix_def elim:prefixE)
           from star_decom [OF h3 this]
           obtain a b where a_in: "a \<in> L\<^isub>1" 
             and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 
             and ab_max: "(x - xa_max) @ z = a @ b" by blast
-          -- {* Now the candiates for @{text "za"} and @{text "zb"} are found:*}
           let ?za = "a - (x - xa_max)" and ?zb = "b"
           have pfx: "(x - xa_max) \<le> a" (is "?P1") 
             and eq_z: "z = ?za @ ?zb" (is "?P2")
           proof -
-            -- {* 
-              \begin{minipage}{0.8\textwidth}
-              Since @{text "(x - xa_max) @ z = a @ b"}, string @{text "(x - xa_max) @ z"}
-              can be splitted in two ways:
-              \end{minipage}
-              *}
             have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or> 
               (a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)" 
-              using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
+              using append_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
             moreover {
-              -- {* However, the undsired way can be refuted by absurdity: *}
               assume np: "a < (x - xa_max)" 
                 and b_eqs: "((x - xa_max) - a) @ z = b"
               have "False"
@@ -639,24 +414,19 @@
                 moreover have "?xa_max' \<in> L\<^isub>1\<star>" 
                   using a_in h2 by (simp add:star_intro3) 
                 moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>" 
-                  using b_eqs b_in np h1 by (simp add:diff_diff_appd)
+                  using b_eqs b_in np h1 by (simp add:diff_diff_append)
                 moreover have "\<not> (length ?xa_max' \<le> length xa_max)" 
                   using a_neq by simp
                 ultimately show ?thesis using h4 by blast
               qed }
-            -- {* Now it can be shown that the splitting goes the way we desired. *}
             ultimately show ?P1 and ?P2 by auto
           qed
           hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)
-          -- {* Now candidates @{text "?za"} and @{text "?zb"} have all the requred properteis. *}
           with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1" 
             by (auto simp:str_eq_def str_eq_rel_def)
            with eq_z and b_in 
           show ?thesis using that by blast
         qed
-        -- {* 
-           @{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}:
-            *}
         have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using  l_za ls_zb by blast
         with eq_zab show ?thesis by simp
       qed
@@ -664,123 +434,11 @@
         by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
     qed
   } 
-  -- {* By instantiating the reasoning pattern just derived for both directions:*} 
   from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
-  -- {* The thesis is proved as a trival consequence: *} 
-    show  ?thesis unfolding str_eq_def str_eq_rel_def by blast
-qed
-
-lemma -- {* The oringal version with less explicit details. *}
-  fixes v w
-  assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
-  shows "(v::string) \<approx>(L\<^isub>1\<star>) w"
-proof-
-    -- {* 
-    \begin{minipage}{0.8\textwidth}
-    According to the definition of @{text "\<approx>Lang"}, 
-    proving @{text "v \<approx>(L\<^isub>1\<star>) w"} amounts to
-    showing: for any string @{text "u"},
-    if @{text "v @ u \<in> (L\<^isub>1\<star>)"} then @{text "w @ u \<in> (L\<^isub>1\<star>)"} and vice versa.
-    The reasoning pattern for both directions are the same, as derived
-    in the following:
-    \end{minipage}
-    *}
-  { fix x y z
-    assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" 
-      and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
-    have "y @ z \<in> L\<^isub>1\<star>"
-    proof(cases "x = []")
-      -- {* 
-        The degenerated case when @{text "x"} is a null string is easy to prove:
-        *}
-      case True
-      with tag_xy have "y = []" 
-        by (auto simp:tag_str_STAR_def strict_prefix_def)
-      thus ?thesis using xz_in_star True by simp
-    next
-        -- {*
-        \begin{minipage}{0.8\textwidth}
-        The case when @{text "x"} is not null, and
-        @{text "x @ z"} is in @{text "L\<^isub>1\<star>"}, 
-        \end{minipage}
-        *}
-      case False
-      obtain x_max 
-        where h1: "x_max < x" 
-        and h2: "x_max \<in> L\<^isub>1\<star>" 
-        and h3: "(x - x_max) @ z \<in> L\<^isub>1\<star>" 
-        and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star> 
-                                     \<longrightarrow> length xa \<le> length x_max"
-      proof-
-        let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
-        have "finite ?S"
-          by (rule_tac B = "{xa. xa < x}" in finite_subset, 
-                                auto simp:finite_strict_prefix_set)
-        moreover have "?S \<noteq> {}" using False xz_in_star
-          by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)
-        ultimately have "\<exists> max \<in> ?S. \<forall> a \<in> ?S. length a \<le> length max" 
-          using finite_set_has_max by blast
-        thus ?thesis using that by blast
-      qed
-      obtain ya 
-        where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" and h7: "(x - x_max) \<approx>L\<^isub>1 (y - ya)"
-      proof-
-        from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = 
-          {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")
-          by (auto simp:tag_str_STAR_def)
-        moreover have "\<approx>L\<^isub>1 `` {x - x_max} \<in> ?left" using h1 h2 by auto
-        ultimately have "\<approx>L\<^isub>1 `` {x - x_max} \<in> ?right" by simp
-        with that show ?thesis apply 
-          (simp add:Image_def str_eq_rel_def str_eq_def) by blast
-      qed      
-      have "(y - ya) @ z \<in> L\<^isub>1\<star>" 
-      proof-
-        from h3 h1 obtain a b where a_in: "a \<in> L\<^isub>1" 
-          and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 
-          and ab_max: "(x - x_max) @ z = a @ b" 
-          by (drule_tac star_decom, auto simp:strict_prefix_def elim:prefixE)
-        have "(x - x_max) \<le> a \<and> (a - (x - x_max)) @ b = z" 
-        proof -
-          have "((x - x_max) \<le> a \<and> (a - (x - x_max)) @ b = z) \<or> 
-                            (a < (x - x_max) \<and> ((x - x_max) - a) @ z = b)" 
-            using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
-          moreover { 
-            assume np: "a < (x - x_max)" and b_eqs: " ((x - x_max) - a) @ z = b"
-            have "False"
-            proof -
-              let ?x_max' = "x_max @ a"
-              have "?x_max' < x" 
-                using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) 
-              moreover have "?x_max' \<in> L\<^isub>1\<star>" 
-                using a_in h2 by (simp add:star_intro3) 
-              moreover have "(x - ?x_max') @ z \<in> L\<^isub>1\<star>" 
-                using b_eqs b_in np h1 by (simp add:diff_diff_appd)
-              moreover have "\<not> (length ?x_max' \<le> length x_max)" 
-                using a_neq by simp
-              ultimately show ?thesis using h4 by blast
-            qed 
-          } ultimately show ?thesis by blast
-        qed
-        then obtain za where z_decom: "z = za @ b" 
-          and x_za: "(x - x_max) @ za \<in> L\<^isub>1" 
-          using a_in by (auto elim:prefixE)        
-        from x_za h7 have "(y - ya) @ za \<in> L\<^isub>1" 
-          by (auto simp:str_eq_def str_eq_rel_def)
-	with b_in have "((y - ya) @ za) @ b \<in> L\<^isub>1\<star>" by blast
-        with z_decom show ?thesis by auto 
-      qed
-      with h5 h6 show ?thesis 
-        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
-    qed
-  } 
-  -- {* By instantiating the reasoning pattern just derived for both directions:*} 
-  from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
-  -- {* The thesis is proved as a trival consequence: *} 
     show  ?thesis unfolding str_eq_def str_eq_rel_def by blast
 qed
 
 lemma quot_star_finiteI [intro]:
-  fixes L1::"lang"
   assumes finite1: "finite (UNIV // \<approx>L1)"
   shows "finite (UNIV // \<approx>(L1\<star>))"
 proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD)
@@ -803,76 +461,9 @@
   shows "finite (UNIV // \<approx>(L r))"
 by (induct r) (auto)
 
+
 theorem Myhill_Nerode:
   shows "(\<exists>r::rexp. A = L r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
-using Myhill_Nerode1 Myhill_Nerode2 by metis
-
-(*
-section {* Closure properties *}
-
-abbreviation
-  reg :: "lang \<Rightarrow> bool"
-where
-  "reg A \<equiv> \<exists>r::rexp. A = L r"
-
-
-
-lemma closure_union[intro]:
-  assumes "reg A" "reg B" 
-  shows "reg (A \<union> B)"
-using assms
-apply(auto)
-apply(rule_tac x="ALT r ra" in exI)
-apply(auto)
-done
-
-lemma closure_seq[intro]:
-  assumes "reg A" "reg B" 
-  shows "reg (A ;; B)"
-using assms
-apply(auto)
-apply(rule_tac x="SEQ r ra" in exI)
-apply(auto)
-done
-
-lemma closure_star[intro]:
-  assumes "reg A"
-  shows "reg (A\<star>)"
-using assms
-apply(auto)
-apply(rule_tac x="STAR r" in exI)
-apply(auto)
-done
-
-lemma closure_complement[intro]:
-  assumes "reg A"
-  shows "reg (- A)"
-using assms
-unfolding Myhill_Nerode
-unfolding str_eq_rel_def
-by auto
-
-lemma closure_difference[intro]:
-  assumes "reg A" "reg B" 
-  shows "reg (A - B)"
-proof -
-  have "A - B = - ((- A) \<union> B)" by blast
-  moreover
-  have "reg (- ((- A) \<union> B))" 
-    using assms by blast
-  ultimately show "reg (A - B)" by simp
-qed
-
-lemma closure_intersection[intro]:
-  assumes "reg A" "reg B" 
-  shows "reg (A \<inter> B)"
-proof -
-  have "A \<inter> B = - ((- A) \<union> (- B))" by blast
-  moreover
-  have "reg (- ((- A) \<union> (- B)))" 
-    using assms by blast
-  ultimately show "reg (A \<inter> B)" by simp
-qed
-*)
+using Myhill_Nerode1 Myhill_Nerode2 by auto
 
 end
diff -r a8a442ba0dbf -r e93760534354 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu May 12 05:55:05 2011 +0000
+++ b/Paper/Paper.thy	Wed May 18 19:54:43 2011 +0000
@@ -12,9 +12,8 @@
 abbreviation
   "EClass x R \<equiv> R `` {x}"
 
-abbreviation 
-  "append_rexp2 r_itm r \<equiv> append_rexp r r_itm"
-
+abbreviation
+  "Append_rexp2 r_itm r == Append_rexp r r_itm"
 
 notation (latex output)
   str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
@@ -32,8 +31,9 @@
   EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
   transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
   Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
-  append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
-  append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
+  Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
+  Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
+  
   uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
   tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
   tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
@@ -494,8 +494,8 @@
   
   \begin{center}
   @{text "\<calL>(Y, r) \<equiv>"} %
-  @{thm (rhs) L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
-  @{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]}
+  @{thm (rhs) L_rhs_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+  @{thm L_rhs_trm.simps(1)[where r="r", THEN eq_reflection]}
   \end{center}
 
   \noindent
@@ -561,13 +561,13 @@
   we define the \emph{append-operation} taking a term and a regular expression as argument
 
   \begin{center}
-  @{thm append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
-  @{thm append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+  @{thm Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+  @{thm Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
   \end{center}
 
   \noindent
   We lift this operation to entire right-hand sides of equations, written as
-  @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
+  @{thm (lhs) Append_rexp_rhs_def[where rexp="r"]}. With this we can define
   the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
   %
   \begin{equation}\label{arden_def}
@@ -712,10 +712,10 @@
       @{term "finite ES"} & @{text "(finiteness)"}\\
   & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
   & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
-  & @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\
+  & @{text "\<and>"} & @{thm (rhs) distinctness_def}\\
   &             &  & @{text "(distinctness)"}\\
   & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\   
-  & @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\
+  & @{text "\<and>"} & @{thm (rhs) validity_def} & @{text "(validity)"}\\
   \end{tabular}
   \end{center}
  
diff -r a8a442ba0dbf -r e93760534354 Prefix_subtract.thy
--- a/Prefix_subtract.thy	Thu May 12 05:55:05 2011 +0000
+++ b/Prefix_subtract.thy	Wed May 18 19:54:43 2011 +0000
@@ -1,59 +1,60 @@
 theory Prefix_subtract
-  imports Main 
-          "~~/src/HOL/Library/List_Prefix"
+  imports Main "~~/src/HOL/Library/List_Prefix"
 begin
 
+
 section {* A small theory of prefix subtraction *}
 
 text {*
-  The notion of @{text "prefix_subtract"} is need to make proofs more readable.
-  *}
+  The notion of @{text "prefix_subtract"} makes 
+  the second direction of the Myhill-Nerode theorem 
+  more readable.
+*}
+
+instantiation list :: (type) minus
+begin
 
-fun prefix_subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51)
+fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 
 where
-  "prefix_subtract []     xs     = []" 
-| "prefix_subtract (x#xs) []     = x#xs" 
-| "prefix_subtract (x#xs) (y#ys) = (if x = y then prefix_subtract xs ys else (x#xs))"
+  "minus_list []     xs     = []" 
+| "minus_list (x#xs) []     = x#xs" 
+| "minus_list (x#xs) (y#ys) = (if x = y then minus_list xs ys else (x#xs))"
+
+instance by default
+
+end
+
+lemma [simp]: "x - [] = x"
+by (induct x) (auto)
 
 lemma [simp]: "(x @ y) - x = y"
-apply (induct x)
-by (case_tac y, simp+)
+by (induct x) (auto)
 
 lemma [simp]: "x - x = []"
-by (induct x, auto)
-
-lemma [simp]: "x = xa @ y \<Longrightarrow> x - xa = y "
-by (induct x, auto)
-
-lemma [simp]: "x - [] = x"
-by (induct x, auto)
+by (induct x) (auto)
 
-lemma [simp]: "(x - y = []) \<Longrightarrow> (x \<le> y)"
-proof-   
-  have "\<exists>xa. x = xa @ (x - y) \<and> xa \<le> y"
-    apply (rule prefix_subtract.induct[of _ x y], simp+)
-    by (clarsimp, rule_tac x = "y # xa" in exI, simp+)
-  thus "(x - y = []) \<Longrightarrow> (x \<le> y)" by simp
-qed
+lemma [simp]: "x = z @ y \<Longrightarrow> x - z = y "
+by (induct x) (auto)
 
 lemma diff_prefix:
   "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"
-by (auto elim:prefixE)
+by (auto elim: prefixE)
 
-lemma diff_diff_appd: 
+lemma diff_diff_append: 
   "\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)"
 apply (clarsimp simp:strict_prefix_def)
 by (drule diff_prefix, auto elim:prefixE)
 
-lemma app_eq_cases[rule_format]:
-  "\<forall> x . x @ y = m @ n \<longrightarrow> (x \<le> m \<or> m \<le> x)"
-apply (induct y, simp)
-apply (clarify, drule_tac x = "x @ [a]" in spec)
-by (clarsimp, auto simp:prefix_def)
+lemma append_eq_cases:
+  assumes a: "x @ y = m @ n"
+  shows "x \<le> m \<or> m \<le> x"
+unfolding prefix_def using a
+by (auto simp add: append_eq_append_conv2)
 
-lemma app_eq_dest:
-  "x @ y = m @ n \<Longrightarrow> 
-               (x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"
-by (frule_tac app_eq_cases, auto elim:prefixE)
+lemma append_eq_dest:
+  assumes a: "x @ y = m @ n" 
+  shows "(x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"
+using append_eq_cases[OF a] a
+by (auto elim: prefixE)
 
 end