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= \ {(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 "\ X. ?f X \ (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 \ ?A" - and Y_in: "Y \ ?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 \ X" and y_in: "y \ 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 "\ X. ?f X \ (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 \ ?A" + and Y_in: "Y \ ?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 \ X" and y_in: "y \ 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: - "\\ x \ A. f x \ B; finite B\ \ 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 \ 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 = "\ X. {R1 `` {x} | x. x \ 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 \ 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 \ ?A" and Y_in: "Y \ ?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 \ A" with eq2 - have x_in: "x \ X" - unfolding equiv_def quotient_def refl_on_def by auto - with eq_f have "R1 `` {x} \ ?R" by auto - then obtain y where - y_in: "y \ Y" and eq_r: "R1 `` {x} = R1 ``{y}" by auto - have "(x, y) \ R1" - proof - - from x_in X_in y_in Y_in eq2 - have "x \ A" and "y \ 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) \ 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 = "\X. {R1 `` {x} | x. x \ X}" + and ?A = "UNIV // R2" and ?B = "UNIV // R1" + have "?f ` ?A \ 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 \ ?A" and Y_in: "Y \ ?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 \ X" by simp + then have "R1 ``{x} \ ?f X" by auto + with eq_f have "R1 `` {x} \ ?f Y" by simp + then obtain y + where y_in: "y \ Y" and eq_r1_xy: "R1 `` {x} = R1 `` {y}" by auto + with eq_equiv_class[OF _ eq1] + have "(x, y) \ R1" by blast + with refined have "(x, y) \ 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 (\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=) \ (\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 (\Lang)" by blast + show "equiv UNIV (\Lang)" + unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def + by blast qed qed