--- a/Myhill_1.thy	Sun Feb 13 10:36:53 2011 +0000
+++ b/Myhill_1.thy	Mon Feb 14 07:42:16 2011 +0000
@@ -487,14 +487,6 @@
 definition 
   "Solve X ES \<equiv> while Test (Iter X) ES"
 
-
-(* test *)
-partial_function (tailrec)
-  solve
-where
-  "solve X ES = (if (card ES = 1) then ES else solve X (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
@@ -666,19 +658,22 @@
 *}
 
 lemma defined_by_str:
-  "\<lbrakk>s \<in> X; X \<in> UNIV // (\<approx>Lang)\<rbrakk> \<Longrightarrow> X = (\<approx>Lang) `` {s}"
-by (auto simp:quotient_def Image_def str_eq_rel_def)
+  assumes "s \<in> X" "X \<in> UNIV // \<approx>A" 
+  shows "X = \<approx>A `` {s}"
+using assms
+unfolding quotient_def Image_def str_eq_rel_def
+by auto
 
 lemma every_eqclass_has_transition:
   assumes has_str: "s @ [c] \<in> X"
-  and     in_CS:   "X \<in> UNIV // (\<approx>Lang)"
-  obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"
+  and     in_CS:   "X \<in> UNIV // \<approx>A"
+  obtains Y where "Y \<in> UNIV // \<approx>A" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"
 proof -
-  def Y \<equiv> "(\<approx>Lang) `` {s}"
-  have "Y \<in> UNIV // (\<approx>Lang)" 
+  def Y \<equiv> "\<approx>A `` {s}"
+  have "Y \<in> UNIV // \<approx>A" 
     unfolding Y_def quotient_def by auto
   moreover
-  have "X = (\<approx>Lang) `` {s @ [c]}" 
+  have "X = \<approx>A `` {s @ [c]}" 
     using has_str in_CS defined_by_str by blast
   then have "Y ;; {[c]} \<subseteq> X" 
     unfolding Y_def Image_def Seq_def
@@ -687,18 +682,18 @@
   moreover
   have "s \<in> Y" unfolding Y_def 
     unfolding Image_def str_eq_rel_def by simp
-  ultimately show thesis by (blast intro: that)
+  ultimately show thesis using that by blast
 qed
 
 lemma l_eq_r_in_eqs:
-  assumes X_in_eqs: "(X, xrhs) \<in> (Init (UNIV // (\<approx>Lang)))"
-  shows "X = L xrhs"
+  assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
+  shows "X = L rhs"
 proof 
-  show "X \<subseteq> L xrhs"
+  show "X \<subseteq> L rhs"
   proof
     fix x
     assume "(1)": "x \<in> X"
-    show "x \<in> L xrhs"          
+    show "x \<in> L rhs"          
     proof (cases "x = []")
       assume empty: "x = []"
       thus ?thesis using X_in_eqs "(1)"
@@ -707,14 +702,14 @@
       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>Lang)" using X_in_eqs by (auto simp:Init_def)
+      have "X \<in> UNIV // \<approx>A" using X_in_eqs by (auto simp:Init_def)
       then obtain Y 
-        where "Y \<in> UNIV // (\<approx>Lang)" 
+        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>Lang) \<and> Y \<Turnstile>c\<Rightarrow> X}"
+        "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)
@@ -723,10 +718,17 @@
     qed
   qed
 next
-  show "L xrhs \<subseteq> X" using X_in_eqs
+  show "L rhs \<subseteq> X" using X_in_eqs
     by (auto simp:Init_def Init_rhs_def transition_def) 
 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)
+
+
 lemma finite_Init_rhs: 
   assumes finite: "finite CS"
   shows "finite (Init_rhs CS X)"