--- 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