
diff -r 22ba25b808c8 -r c3fa11ee776e Myhill_2.thy
--- a/Myhill_2.thy	Sat Feb 19 12:01:16 2011 +0000
+++ b/Myhill_2.thy	Sat Feb 19 17:10:46 2011 +0000
@@ -63,124 +63,88 @@
    "=tag= \<equiv> {(x, y) | x y. tag x = tag y}"
 
 
-lemma equiv_tag_eq_rel:"equiv UNIV (=f=)"
-  by (auto simp:equiv_def tag_eq_rel_def refl_on_def sym_def trans_def)
-
 lemma finite_range_image: 
   assumes "finite (range f)"
   shows "finite (f ` A)"
   using assms unfolding image_def
   by (rule_tac finite_subset) (auto)
 
-thm finite_imageD
-
 lemma finite_eq_tag_rel:
   assumes rng_fnt: "finite (range tag)"
   shows "finite (UNIV // =tag=)"
 proof -
   let "?f" =  "op ` tag" and ?A = "(UNIV // =tag=)"
-  show ?thesis
-  proof (rule_tac f = "?f" and A = ?A in finite_imageD) 
-    -- {* 
-      The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}:
-      *}
-    show "finite (?f ` ?A)" 
-    proof -
-      have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp: image_def Pow_def)
-      moreover from rng_fnt have "finite (Pow (range tag))" by simp
-      ultimately have "finite (range ?f)"
-        by (auto simp only:image_def intro:finite_subset)
-      from finite_range_image [OF this] show ?thesis .
-    qed
-  next
-    -- {* 
-      The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}:
-      *}
-    show "inj_on ?f ?A" 
-    proof -
-      { fix X Y
-        assume X_in: "X \<in> ?A"
-          and  Y_in: "Y \<in> ?A"
-          and  tag_eq: "?f X = ?f Y"
-        have "X = Y"
-        proof -
-          from X_in Y_in tag_eq 
-          obtain x y 
-            where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y"
-            unfolding quotient_def Image_def str_eq_rel_def 
-                                   str_eq_def image_def tag_eq_rel_def
-            apply simp by blast
-          with X_in Y_in show "X = Y"
-	    unfolding quotient_def str_eq_rel_def str_eq_def tag_eq_rel_def
-	    by auto
-        qed
-      } thus ?thesis unfolding inj_on_def by auto
-    qed
+    -- {* The finiteness of @{text "f"}-image is a consequence of @{text "rng_fnt"} *}
+  have "finite (?f ` ?A)" 
+  proof -
+    have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp: image_def Pow_def)
+    moreover from rng_fnt have "finite (Pow (range tag))" by simp
+    ultimately have "finite (range ?f)"
+      by (auto simp only:image_def intro:finite_subset)
+    from finite_range_image [OF this] show ?thesis .
   qed
+  moreover
+    -- {* The injectivity of @{text "f"}-image follows from the definition of @{text "(=tag=)"} *}
+  have "inj_on ?f ?A" 
+  proof -
+    { fix X Y
+      assume X_in: "X \<in> ?A"
+        and  Y_in: "Y \<in> ?A"
+        and  tag_eq: "?f X = ?f Y"
+      have "X = Y"
+      proof -
+        from X_in Y_in tag_eq 
+        obtain x y 
+          where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y"
+          unfolding quotient_def Image_def image_def tag_eq_rel_def
+          by (simp) (blast)
+        with X_in Y_in show "X = Y"
+	  unfolding quotient_def str_eq_rel_def str_eq_def tag_eq_rel_def
+	  by auto
+      qed
+    } then show "inj_on ?f ?A" unfolding inj_on_def by auto
+  qed
+  ultimately 
+  show "finite (UNIV // =tag=)" by (rule finite_imageD)
 qed
 
-lemma finite_image_finite: 
-  "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)"
-  by (rule finite_subset [of _ B], auto)
-
 lemma refined_partition_finite:
-  fixes R1 R2 A
-  assumes fnt: "finite (A // R1)"
+  assumes fnt: "finite (UNIV // R1)"
   and refined: "R1 \<subseteq> R2"
-  and eq1: "equiv A R1" and eq2: "equiv A R2"
-  shows "finite (A // R2)"
+  and eq1: "equiv UNIV R1" and eq2: "equiv UNIV R2"
+  shows "finite (UNIV // R2)"
 proof -
-  let ?f = "\<lambda> X. {R1 `` {x} | x. x \<in> X}" 
-    and ?A = "(A // R2)" and ?B = "(A // R1)"
-  show ?thesis
-  proof(rule_tac f = ?f and A = ?A in finite_imageD)
-    show "finite (?f ` ?A)"
-    proof(rule finite_subset [of _ "Pow ?B"])
-      from fnt show "finite (Pow (A // R1))" by simp
-    next
-      from eq2
-      show " ?f ` A // R2 \<subseteq> Pow ?B"
-        unfolding image_def Pow_def quotient_def
-        apply auto
-        by (rule_tac x = xb in bexI, simp, 
-                 unfold equiv_def sym_def refl_on_def, blast)
-    qed
-  next
-    show "inj_on ?f ?A"
-    proof -
-      { fix X Y
-        assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" 
-          and eq_f: "?f X = ?f Y" (is "?L = ?R")
-        have "X = Y" using X_in
-        proof(rule quotientE)
-          fix x
-          assume "X = R2 `` {x}" and "x \<in> A" with eq2
-          have x_in: "x \<in> X" 
-            unfolding equiv_def quotient_def refl_on_def by auto
-          with eq_f have "R1 `` {x} \<in> ?R" by auto
-          then obtain y where 
-            y_in: "y \<in> Y" and eq_r: "R1 `` {x} = R1 ``{y}" by auto
-          have "(x, y) \<in> R1"
-          proof -
-            from x_in X_in y_in Y_in eq2
-            have "x \<in> A" and "y \<in> A" 
-              unfolding equiv_def quotient_def refl_on_def by auto
-            from eq_equiv_class_iff [OF eq1 this] and eq_r
-            show ?thesis by simp
-          qed
-          with refined have xy_r2: "(x, y) \<in> R2" by auto
-          from quotient_eqI [OF eq2 X_in Y_in x_in y_in this]
-          show ?thesis .
-        qed
-      } thus ?thesis by (auto simp:inj_on_def)
-    qed
+  let ?f = "\<lambda>X. {R1 `` {x} | x. x \<in> X}" 
+    and ?A = "UNIV // R2" and ?B = "UNIV // R1"
+  have "?f ` ?A \<subseteq> Pow ?B"
+    unfolding image_def Pow_def quotient_def by auto
+  moreover
+  have "finite (Pow ?B)" using fnt by simp
+  ultimately  
+  have "finite (?f ` ?A)" by (rule finite_subset)
+  moreover
+  have "inj_on ?f ?A"
+  proof -
+    { fix X Y
+      assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" and eq_f: "?f X = ?f Y"
+      from quotientE [OF X_in]
+      obtain x where "X = R2 `` {x}" by blast
+      with equiv_class_self[OF eq2] have x_in: "x \<in> X" by simp
+      then have "R1 ``{x} \<in> ?f X" by auto
+      with eq_f have "R1 `` {x} \<in> ?f Y" by simp
+      then obtain y 
+        where y_in: "y \<in> Y" and eq_r1_xy: "R1 `` {x} = R1 `` {y}" by auto
+      with eq_equiv_class[OF _ eq1] 
+      have "(x, y) \<in> R1" by blast
+      with refined have "(x, y) \<in> R2" by auto
+      with quotient_eqI [OF eq2 X_in Y_in x_in y_in]
+      have "X = Y" .
+    } 
+    then show "inj_on ?f ?A" unfolding inj_on_def by blast 
   qed
+  ultimately show "finite (UNIV // R2)" by (rule finite_imageD)
 qed
 
-lemma equiv_lang_eq: "equiv UNIV (\<approx>Lang)"
-  unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def
-  by blast
-
 lemma tag_finite_imageD:
   fixes tag
   assumes rng_fnt: "finite (range tag)" 
@@ -191,7 +155,7 @@
 proof -
   let ?R1 = "(=tag=)"
   show ?thesis
-  proof(rule_tac refined_partition_finite [of _ ?R1])
+  proof(rule_tac refined_partition_finite [of ?R1])
     from finite_eq_tag_rel [OF rng_fnt]
      show "finite (UNIV // =tag=)" . 
    next
@@ -199,11 +163,13 @@
      show "(=tag=) \<subseteq> (\<approx>Lang)"
        by (auto simp:tag_eq_rel_def str_eq_def)
    next
-     from equiv_tag_eq_rel
-     show "equiv UNIV (=tag=)" by blast
+     show "equiv UNIV (=tag=)"
+       unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def
+       by auto
    next
-     from equiv_lang_eq
-     show "equiv UNIV (\<approx>Lang)" by blast
+     show "equiv UNIV (\<approx>Lang)" 
+       unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def
+       by blast
   qed
 qed
 




