--- a/Myhill_1.thy	Tue Feb 15 08:08:04 2011 +0000
+++ b/Myhill_1.thy	Tue Feb 15 10:37:56 2011 +0000
@@ -742,18 +742,16 @@
   assumes finite: "finite CS"
   shows "finite (Init_rhs CS X)"
 proof-
-  have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" (is "finite ?A")
-  proof -
-    def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" 
-    def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"
-    have "finite (CS \<times> (UNIV::char set))" using finite by auto
-    hence "finite S" using S_def 
-      by (rule_tac B = "CS \<times> UNIV" in finite_subset, auto)
-    moreover have "?A = h ` S" by (auto simp: S_def h_def image_def)
-    ultimately show ?thesis 
-      by auto
-  qed
-  thus ?thesis by (simp add:Init_rhs_def transition_def)
+  def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" 
+  def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"
+  have "finite (CS \<times> (UNIV::char set))" using finite by auto
+  then have "finite S" using S_def 
+    by (rule_tac B = "CS \<times> UNIV" in finite_subset) (auto)
+  moreover have "{Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X} = h ` S"
+    unfolding S_def h_def image_def by auto
+  ultimately
+  have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" by auto
+  then show "finite (Init_rhs CS X)" unfolding Init_rhs_def transition_def by simp
 qed
 
 lemma Init_ES_satisfies_invariant:
@@ -1045,33 +1043,33 @@
 lemma iteration_step_measure:
   assumes Inv_ES: "invariant ES"
   and    X_in_ES: "(X, xrhs) \<in> ES"
-  and    not_T: "Cond ES "
+  and    Cnd:     "Cond ES "
   shows "(Iter X ES, ES) \<in> measure card"
 proof -
-  have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
+  have fin: "finite ES" using Inv_ES unfolding invariant_def by simp
   then obtain Y yrhs 
     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
-    using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
+    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
     by auto
   then show "(Iter X ES, ES) \<in> measure card" 
   apply(rule IterI2)
   apply(rule Remove_in_card_measure)
-  apply(simp_all add: finite_ES)
+  apply(simp_all add: fin)
   done
 qed
 
 lemma iteration_step_invariant:
   assumes Inv_ES: "invariant ES"
   and    X_in_ES: "(X, xrhs) \<in> ES"
-  and    not_T: "Cond ES"
+  and    Cnd: "Cond ES"
   shows "invariant (Iter X ES)"
 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)" 
-    using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
+    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
     by auto
@@ -1088,13 +1086,13 @@
 lemma iteration_step_ex:
   assumes Inv_ES: "invariant ES"
   and    X_in_ES: "(X, xrhs) \<in> ES"
-  and    not_T: "Cond ES"
+  and    Cnd: "Cond ES"
   shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
 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)" 
-    using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
+    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
     by auto
@@ -1155,38 +1153,25 @@
   shows "\<exists>r::rexp. L r = X" 
 proof-
   def A \<equiv> "Arden X xrhs"
-  have eq: "{Lam r | r. Lam r \<in> A} = A"
-  proof -
-    have "rhss A = {}" using Inv_ES 
-      unfolding A_def valid_eqs_def invariant_def lhss_def
-      by (simp add: Arden_removes_cl) 
-    thus ?thesis unfolding A_def rhss_def
-      apply(auto simp only:)
-      apply(case_tac x)
-      apply(auto)
-      done
-  qed
+  have "rhss xrhs \<subseteq> {X}" using Inv_ES 
+    unfolding valid_eqs_def invariant_def rhss_def lhss_def
+    by auto
+  then have "rhss A = {}" unfolding A_def 
+    by (simp add: Arden_removes_cl)
+  then have eq: "{Lam r | r. Lam r \<in> A} = A" unfolding rhss_def
+    by (auto, case_tac x, auto)
+  
   have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
     using Arden_keeps_finite by auto
-  then have "finite {r. Lam r \<in> A}" by (rule finite_Lam)
-  then have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
-    by auto
-  also have "\<dots> = L A" by (simp add: eq)
-  also have "\<dots> = X" 
-  proof -
-    have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def
-      by auto
-    moreover
-    from Inv_ES have "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
-      unfolding invariant_def ardenable_def finite_rhs_def
-      by(simp add: rexp_of_empty)
-    moreover
-    from Inv_ES have "finite xrhs"  unfolding invariant_def finite_rhs_def
-      by simp
-    ultimately show "L A = X" unfolding A_def
-      by (rule  Arden_keeps_eq[symmetric])
-  qed
-  finally have "L (\<Uplus>{r. Lam r \<in> A}) = X" .
+  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
+    by simp
+  then have "X = L A" using Inv_ES 
+    unfolding A_def invariant_def ardenable_def finite_rhs_def rhs_nonempty_def
+    by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn)
+  then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp
+  then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto
   then show "\<exists>r::rexp. L r = X" by blast
 qed
 
@@ -1216,14 +1201,14 @@
   assumes finite_CS: "finite (UNIV // \<approx>A)"
   shows   "\<exists>r::rexp. A = L r"
 proof -
-  have f: "finite (finals A)" 
+  have fin: "finite (finals A)" 
     using finals_in_partitions finite_CS by (rule finite_subset)
   have "\<forall>X \<in> (UNIV // \<approx>A). \<exists>r::rexp. X = L r" 
     using finite_CS every_eqcl_has_reg by blast
   then have a: "\<forall>X \<in> finals A. \<exists>r::rexp. X = L r"
     using finals_in_partitions by auto
   then obtain rs::"rexp set" where "\<Union> (finals A) = \<Union>(L ` rs)" "finite rs"
-    using f by (auto dest: bchoice_finite_set)
+    using fin by (auto dest: bchoice_finite_set)
   then have "A = L (\<Uplus>rs)" 
     unfolding lang_is_union_of_finals[symmetric] by simp
   then show "\<exists>r::rexp. A = L r" by blast

--- a/Paper/Paper.thy	Tue Feb 15 08:08:04 2011 +0000
+++ b/Paper/Paper.thy	Tue Feb 15 10:37:56 2011 +0000
@@ -667,10 +667,21 @@
   The first two ensure that the equational system is always finite (number of equations
   and number of terms in each equation); \ldots
 
+  It is straightforward to prove that the inital equational system satisfies the
+  invariant.
+
   \begin{lemma}
   @{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 ardenable
+  property also follows from the setup of the equational system as does 
+  validity.\qed
+  \end{proof}
+
   \begin{lemma}
   @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
   \end{lemma}
@@ -679,15 +690,54 @@
   @{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 distictness 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}
+
   \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{lemma}\label{every_eqcl_has_reg}
+  @{thm[mode=IfThen] every_eqcl_has_reg}
+  \end{lemma}
+
+  \begin{proof}
+  By the preceeding 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 @{text "\<Union>\<calL> ` (Arden X rhs)"} using ???.
+
+  \end{proof}
+
   \begin{theorem}
   @{thm[mode=IfThen] Myhill_Nerode1}
   \end{theorem}
+
+  \begin{proof}
+  By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular language 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 equvalence class
+  in @{term "finals A"} there exists a regular language. Moreover by assumption 
+  we know that @{term "finals A"} must be finite, therefore there must be a finite
+  set of regular expressions @{text "rs"} such that
+
+  \begin{center}
+  @{term "\<Union>(finals A) = L (\<Uplus>rs)"}
+  \end{center}
+
+  \noindent
+  Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"} 
+  as the regular expression that solves the goal.\qed
+  \end{proof}
 *}