--- a/Myhill_1.thy	Tue Feb 08 15:59:47 2011 +0000
+++ b/Myhill_1.thy	Tue Feb 08 16:49:18 2011 +0000
@@ -434,21 +434,6 @@
 *}
 
 text {*
-  The functions @{text "the_r"} and @{text "the_Trn"} are used to extract
-  subcomponents from right hand side items.
-  *}
-
-fun 
-  the_r :: "rhs_item \<Rightarrow> rexp"
-where 
-  "the_r (Lam r) = r"
-
-fun 
-  the_trn_rexp:: "rhs_item \<Rightarrow> rexp"
-where 
-  "the_trn_rexp (Trn Y r) = r"
-
-text {*
   Every right-hand side item @{text "itm"} defines a language given 
   by @{text "L(itm)"}, defined as:
 *}
@@ -519,26 +504,6 @@
 definition
   "trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}"
 
-text {* 
-  The following @{text "rexp_of rhs X"} combines all regular expressions in @{text "X"}-items
-  using @{text "ALT"} to form a single regular expression. 
-  It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}.
-  *}
-
-definition 
-  "rexp_of rhs X \<equiv> \<Uplus> {r. Trn X r \<in> rhs}"
-
-text {*
-  The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"}
-  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> \<Uplus> {r. Lam r \<in> rhs}"
-
 text {*
   The following @{text "attach_rexp rexp' itm"} attach 
   the regular expression @{text "rexp'"} to
@@ -726,14 +691,12 @@
 proof -
   have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}"
     by (rule rev_finite_subset[OF fin]) (auto)
-  then have "finite (the_trn_rexp ` {Trn Y r | Y r. Trn Y r \<in> rhs})"
-    by auto
+  then have "finite ((\<lambda>(Y, r). Trn Y r) ` {(Y, r) | Y r. Trn Y r \<in> rhs})"
+    by (simp add: image_Collect)
+  then have "finite {(Y, r) | Y r. Trn Y r \<in> rhs}"
+    by (erule_tac finite_imageD) (simp add: inj_on_def)
   then show "finite {r. Trn Y r \<in> rhs}"
-    apply(erule_tac rev_finite_subset)
-    apply(auto simp add: image_def)
-    apply(rule_tac x="Trn Y x" in exI)
-    apply(auto)
-    done
+    by (erule_tac f="snd" in finite_surj) (auto simp add: image_def)
 qed
 
 lemma finite_Lam:
@@ -742,11 +705,10 @@
 proof -
   have "finite {Lam r | r. Lam r \<in> rhs}"
     by (rule rev_finite_subset[OF fin]) (auto)
-  then have "finite (the_r ` {Lam r | r. Lam r \<in> rhs})"
-    by auto
   then show "finite {r. Lam r \<in> rhs}"
-    apply(erule_tac rev_finite_subset)
-    apply(auto simp add: image_def)
+    apply(simp add: image_Collect[symmetric])
+    apply(erule finite_imageD)
+    apply(auto simp add: inj_on_def)
     done
 qed
 
@@ -931,7 +893,6 @@
   and finite: "finite rhs"
   shows "X = L (arden_variate X rhs)"
 proof -
-  thm rexp_of_def
   def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"
   def b \<equiv> "rhs - trns_of rhs X"
   def B \<equiv> "L b" 
@@ -1244,7 +1205,7 @@
   shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
 proof-
   def A \<equiv> "arden_variate X xrhs"
-  have "?P (rexp_of_lam A)"
+  have "?P (\<Uplus>{r. Lam r \<in> A})"
   proof -
     have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
     proof(rule rexp_of_lam_eq_lam_set)
@@ -1280,7 +1241,7 @@
       from Inv_ES ES_single show "finite xrhs" 
         by (simp add:Inv_def finite_rhs_def)
     qed
-    finally show ?thesis unfolding rexp_of_lam_def by simp
+    finally show ?thesis by simp
   qed
   thus ?thesis by auto
 qed