--- a/Myhill_1.thy	Fri Aug 19 20:39:07 2011 +0000
+++ b/Myhill_1.thy	Mon Aug 22 12:49:27 2011 +0000
@@ -1,9 +1,13 @@
 theory Myhill_1
-imports More_Regular_Set
+imports "Folds"
         "~~/src/HOL/Library/While_Combinator" 
 begin
 
-section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
+section {* First direction of MN: @{text "finite partition \<Rightarrow> regular language"} *}
+
+notation 
+  conc (infixr "\<cdot>" 100) and
+  star ("_\<star>" [101] 102)
 
 lemma Pair_Collect [simp]:
   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
@@ -11,7 +15,6 @@
 
 text {* Myhill-Nerode relation *}
 
-
 definition
   str_eq :: "'a lang \<Rightarrow> ('a list \<times> 'a list) set" ("\<approx>_" [100] 100)
 where
@@ -39,7 +42,7 @@
 unfolding finals_def quotient_def
 by auto
 
-section {* Equational systems *}
+subsection {* Equational systems *}
 
 text {* The two kinds of terms in the rhs of equations. *}
 
@@ -87,7 +90,7 @@
   "Init CS \<equiv> {(X, Init_rhs CS X) | X.  X \<in> CS}"
 
 
-section {* Arden Operation on equations *}
+subsection {* Arden Operation on equations *}
 
 fun 
   Append_rexp :: "'a rexp \<Rightarrow> 'a trm \<Rightarrow> 'a trm"
@@ -104,7 +107,7 @@
      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 *}
+subsection {* Substitution Operation on equations *}
 
 definition 
   "Subst rhs X xrhs \<equiv> 
@@ -120,7 +123,7 @@
       Subst_all  (ES - {(X, xrhs)}) X (Arden X xrhs)"
 
 
-section {* While-combinator *}
+subsection {* While-combinator and invariants *}
 
 definition 
   "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
@@ -141,8 +144,6 @@
   "Solve X ES \<equiv> while Cond (Iter X) ES"
 
 
-section {* Invariants *}
-
 definition 
   "distinctness ES \<equiv> 
      \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
@@ -197,8 +198,6 @@
 using assms by (simp add: invariant_def)
 
 
-subsection {* The proof of this direction *}
-
 lemma finite_Trn:
   assumes fin: "finite rhs"
   shows "finite {r. Trn Y r \<in> rhs}"
@@ -247,7 +246,7 @@
 by (auto simp add: conc_def lang_of_append_rexp)
 
 
-subsubsection {* Intial Equational System *}
+subsection {* Intial Equational Systems *}
 
 lemma defined_by_str:
   assumes "s \<in> X" "X \<in> UNIV // \<approx>A" 
@@ -353,7 +352,7 @@
     by auto
 qed
 
-subsubsection {* Interation step *}
+subsection {* Interations *}
 
 lemma Arden_preserves_soundness:
   assumes l_eq_r: "X = lang_rhs rhs"
@@ -377,7 +376,7 @@
     by blast
   finally have "X = X \<cdot> A \<union> B" . 
   then have "X = B \<cdot> A\<star>"
-    by (simp add: arden[OF not_empty2])
+    by (simp add: reversed_Arden[OF not_empty2])
   also have "\<dots> = lang_rhs (Arden X rhs)"
     unfolding Arden_def A_def B_def b_def
     by (simp only: lang_of_append_rexp_rhs lang.simps)
@@ -676,7 +675,7 @@
 qed
 
 
-subsubsection {* Conclusion of the proof *}
+subsection {* The conclusion of the first direction *}
 
 lemma Solve:
   fixes A::"('a::finite) lang"