--- a/Myhill_1.thy	Mon Feb 07 13:17:01 2011 +0000
+++ b/Myhill_1.thy	Mon Feb 07 20:30:10 2011 +0000
@@ -1,5 +1,5 @@
 theory Myhill_1
-  imports Main List_Prefix Prefix_subtract Prelude
+  imports Main 
 begin
 
 (*
@@ -334,7 +334,7 @@
 lemma folds_alt_simp [simp]:
   assumes a: "finite rs"
   shows "L (folds ALT NULL rs) = \<Union> (L ` rs)"
-apply(rule set_eq_intro)
+apply(rule set_eqI)
 apply(simp add: folds_def)
 apply(rule someI2_ex)
 apply(rule_tac finite_imp_fold_graph[OF a])
@@ -345,7 +345,7 @@
 
 text {* Just a technical lemma for collections and pairs *}
 
-lemma [simp]:
+lemma Pair_Collect[simp]:
   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 by simp
 
@@ -471,16 +471,16 @@
 *}
 
 definition 
-  transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
+  transition :: "lang \<Rightarrow> rexp \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
 where
-  "Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<subseteq> X"
+  "Y \<Turnstile>r\<Rightarrow> X \<equiv> Y ;; (L r) \<subseteq> X"
 
 definition
   "init_rhs CS X \<equiv>  
       if ([] \<in> X) then 
-          {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}
+          {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}
       else 
-          {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"
+          {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"
 
 text {*
   In the definition of @{text "init_rhs"}, the term 
@@ -496,6 +496,9 @@
 
 
 definition "eqs CS \<equiv> {(X, init_rhs CS X) | X.  X \<in> CS}"
+
+
+
 (************ arden's lemma variation ********************)
 
 text {* 
@@ -516,7 +519,7 @@
 
 text {* 
   The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}.
-  *}
+*}
 
 definition
   "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"
@@ -526,7 +529,7 @@
   using @{text "ALT"} to form a single regular expression. 
   When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"}
   is used to compute compute the regular expression corresponds to @{text "rhs"}.
-  *}
+*}
 
 definition
   "rexp_of_lam rhs \<equiv> folds ALT NULL (the_r ` lam_of rhs)"
@@ -535,7 +538,7 @@
   The following @{text "attach_rexp rexp' itm"} attach 
   the regular expression @{text "rexp'"} to
   the right of right hand side item @{text "itm"}.
-  *}
+*}
 
 fun 
   attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
@@ -546,7 +549,7 @@
 text {* 
   The following @{text "append_rhs_rexp rhs rexp"} attaches 
   @{text "rexp"} to every item in @{text "rhs"}.
-  *}
+*}
 
 definition
   "append_rhs_rexp rhs rexp \<equiv> (attach_rexp rexp) ` rhs"
@@ -622,7 +625,7 @@
 qed
 
 text {*
-  The @{text "P"} in lemma @{text "wf_iter"} is an invaiant kept throughout the iteration procedure.
+  The @{text "P"} in lemma @{text "wf_iter"} is an invariant kept throughout the iteration procedure.
   The particular invariant used to solve our problem is defined by function @{text "Inv(ES)"},
   an invariant over equal system @{text "ES"}.
   Every definition starting next till @{text "Inv"} stipulates a property to be satisfied by @{text "ES"}.
@@ -631,6 +634,7 @@
 text {* 
   Every variable is defined at most onece in @{text "ES"}.
   *}
+
 definition 
   "distinct_equas ES \<equiv> 
             \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
@@ -834,7 +838,7 @@
         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>Lang) \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"
         unfolding transition_def
 	using "(1)" decom
         by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)