--- a/Myhill_1.thy	Mon Oct 15 13:23:52 2012 +0000
+++ b/Myhill_1.thy	Mon Dec 03 08:16:58 2012 +0000
@@ -1,3 +1,4 @@
+(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *)
 theory Myhill_1
 imports "Folds"
         "~~/src/HOL/Library/While_Combinator" 
@@ -201,29 +202,12 @@
 lemma finite_Trn:
   assumes fin: "finite rhs"
   shows "finite {r. Trn Y r \<in> rhs}"
-proof -
-  have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}"
-    by (rule rev_finite_subset[OF fin]) (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}"
-    by (erule_tac f="snd" in finite_surj) (auto simp add: image_def)
-qed
+using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
 
 lemma finite_Lam:
   assumes fin: "finite rhs"
   shows "finite {r. Lam r \<in> rhs}"
-proof -
-  have "finite {Lam r | r. Lam r \<in> rhs}"
-    by (rule rev_finite_subset[OF fin]) (auto)
-  then show "finite {r. Lam r \<in> rhs}"
-    apply(simp add: image_Collect[symmetric])
-    apply(erule finite_imageD)
-    apply(auto simp add: inj_on_def)
-    done
-qed
+using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
 
 lemma trm_soundness:
   assumes finite:"finite rhs"
@@ -286,21 +270,21 @@
     assume in_X: "x \<in> X"
     { assume empty: "x = []"
       then have "x \<in> lang_rhs rhs" using X_in_eqs in_X
-	unfolding Init_def Init_rhs_def
+        unfolding Init_def Init_rhs_def
         by auto
     }
     moreover
     { assume not_empty: "x \<noteq> []"
       then obtain s c where decom: "x = s @ [c]"
-	using rev_cases by blast
+        using rev_cases by blast
       have "X \<in> UNIV // \<approx>A" using X_in_eqs unfolding Init_def by auto
       then obtain Y where "Y \<in> UNIV // \<approx>A" "Y \<cdot> {[c]} \<subseteq> X" "s \<in> Y"
         using decom in_X every_eqclass_has_transition by metis
       then have "x \<in> lang_rhs {Trn Y (Atom c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}"
         unfolding transition_def
-	using decom by (force simp add: conc_def)
+        using decom by (force simp add: conc_def)
       then have "x \<in> lang_rhs rhs" using X_in_eqs in_X
-	unfolding Init_def Init_rhs_def by simp
+        unfolding Init_def Init_rhs_def by simp
     }
     ultimately show "x \<in> lang_rhs rhs" by blast
   qed
@@ -315,18 +299,7 @@
   fixes CS::"(('a::finite) lang) set"
   assumes finite: "finite CS"
   shows "finite (Init_rhs CS X)"
-proof-
-  def S \<equiv> "{(Y, c)| Y c::'a. Y \<in> CS \<and> Y \<cdot> {[c]} \<subseteq> X}" 
-  def h \<equiv> "\<lambda> (Y, c::'a). Trn Y (Atom c)"
-  have "finite (CS \<times> (UNIV::('a::finite) 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 (Atom c) |Y c::'a. Y \<in> CS \<and> Y \<cdot> {[c]} \<subseteq> X} = h ` S"
-    unfolding S_def h_def image_def by auto
-  ultimately
-  have "finite {Trn Y (Atom c) |Y c. Y \<in> CS \<and> Y \<cdot> {[c]} \<subseteq> X}" by auto
-  then show "finite (Init_rhs CS X)" unfolding Init_rhs_def transition_def by simp
-qed
+using assms unfolding Init_rhs_def transition_def by simp
 
 
 lemma Init_ES_satisfies_invariant:
@@ -444,15 +417,7 @@
 lemma Subst_all_preserves_finite:
   assumes finite: "finite ES"
   shows "finite (Subst_all ES Y yrhs)"
-proof -
-  def eqns \<equiv> "{(X::'a lang, rhs) |X rhs. (X, rhs) \<in> ES}"
-  def h \<equiv> "\<lambda>(X::'a lang, rhs). (X, Subst rhs Y yrhs)"
-  have "finite (h ` eqns)" using finite h_def eqns_def by auto
-  moreover 
-  have "Subst_all ES Y yrhs = h ` eqns" unfolding h_def eqns_def Subst_all_def by auto
-  ultimately
-  show "finite (Subst_all ES Y yrhs)" by simp
-qed
+using assms unfolding Subst_all_def by simp
 
 lemma Subst_all_preserves_finite_rhs:
   "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"