diff -r 8ab3a06577cf -r 426070e68b21 Myhill_1.thy
--- a/Myhill_1.thy	Sun Feb 06 11:21:12 2011 +0000
+++ b/Myhill_1.thy	Mon Feb 07 10:23:23 2011 +0000
@@ -133,27 +133,29 @@
   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: 
-  "\<lbrakk>x \<in> A\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow>(\<exists> a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>)"
+  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
 apply(induct rule: star_induct)
 apply(simp)
 apply(blast)
 done
 
-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 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 Seq_def by auto
-qed
-
 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)"
@@ -237,7 +239,7 @@
   assume eq: "X = B ;; A\<star>"
   have "A\<star> = {[]} \<union> A\<star> ;; A" 
     unfolding seq_star_comm[symmetric]
-    by (rule lang_star_cases)
+    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)"
@@ -351,7 +353,7 @@
   @{text "\<approx>A"} is an equivalence class defined by language @{text "A"}.
 *}
 definition
-  str_eq_rel ("\<approx>_" [100] 100)
+  str_eq_rel :: "lang \<Rightarrow> (string \<times> string) set" ("\<approx>_" [100] 100)
 where
   "\<approx>A \<equiv> {(x, y).  (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}"
 
@@ -361,7 +363,9 @@
 *}
 
 definition 
-   "finals A \<equiv> {\<approx>A `` {x} | x . x \<in> A}"
+  finals :: "lang \<Rightarrow> lang set"
+where
+  "finals A \<equiv> {\<approx>A `` {x} | x . x \<in> A}"
 
 text {* 
   The following lemma establishes the relationshipt between 
@@ -464,14 +468,19 @@
   @{text "CS"}, the term @{text "init_rhs CS X"} is used to extract the right hand side of
   the equation describing the formation of @{text "X"}. The definition of @{text "init_rhs"}
   is:
-  *}
+*}
+
+definition 
+  transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
+where
+  "Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<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 ;; {[c]} \<subseteq> X}
+          {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}
       else 
-          {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"
+          {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"
 
 text {*
   In the definition of @{text "init_rhs"}, the term 
@@ -483,7 +492,7 @@
 
   With the help of @{text "init_rhs"}, the equitional system descrbing the formation of every
   equivalent class inside @{text "CS"} is given by the following @{text "eqs(CS)"}.
-  *}
+*}
 
 
 definition "eqs CS \<equiv> {(X, init_rhs CS X) | X.  X \<in> CS}"
@@ -546,10 +555,11 @@
   With the help of the two functions immediately above, Ardens'
   transformation on right hand side @{text "rhs"} is implemented
   by the following function @{text "arden_variate X rhs"}.
-  After this transformation, the recursive occurent of @{text "X"}
-  in @{text "rhs"} will be eliminated, while the 
-  string set defined by @{text "rhs"} is kept unchanged.
-  *}
+  After this transformation, the recursive occurence of @{text "X"}
+  in @{text "rhs"} will be eliminated, while the string set defined 
+  by @{text "rhs"} is kept unchanged.
+*}
+
 definition 
   "arden_variate X rhs \<equiv> 
         append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))"
@@ -580,9 +590,9 @@
   "eqs_subst ES X xrhs \<equiv> {(Y, rhs_subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
 text {*
-  The computation of regular expressions for equivalent classes is accomplished
+  The computation of regular expressions for equivalence classes is accomplished
   using a iteration principle given by the following lemma.
-  *}
+*}
 
 lemma wf_iter [rule_format]: 
   fixes f
@@ -773,7 +783,7 @@
 text {*
   The following several lemmas until @{text "init_ES_satisfy_Inv"} shows that
   the initial equational system satisfies invariant @{text "Inv"}.
-  *}
+*}
 
 lemma defined_by_str:
   "\<lbrakk>s \<in> X; X \<in> UNIV // (\<approx>Lang)\<rbrakk> \<Longrightarrow> X = (\<approx>Lang) `` {s}"
@@ -824,16 +834,17 @@
         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 ;; {[c]} \<subseteq> X}"
-        using "(1)" decom
+        "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<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:eqs_def init_rhs_def)
+      thus ?thesis using X_in_eqs "(1)"	
+        by (simp add: eqs_def init_rhs_def)
     qed
   qed
 next
   show "L xrhs \<subseteq> X" using X_in_eqs
-    by (auto simp:eqs_def init_rhs_def) 
+    by (auto simp:eqs_def init_rhs_def transition_def) 
 qed
 
 lemma finite_init_rhs: 
@@ -851,7 +862,7 @@
     ultimately show ?thesis 
       by auto
   qed
-  thus ?thesis by (simp add:init_rhs_def)
+  thus ?thesis by (simp add:init_rhs_def transition_def)
 qed
 
 lemma init_ES_satisfy_Inv:
@@ -884,7 +895,8 @@
   From this point until @{text "iteration_step"}, it is proved
   that there exists iteration steps which keep @{text "Inv(ES)"} while
   decreasing the size of @{text "ES"}.
-  *}
+*}
+
 lemma arden_variate_keeps_eq:
   assumes l_eq_r: "X = L rhs"
   and not_empty: "[] \<notin> L (rexp_of rhs X)"