--- a/Myhill_2.thy Sat Feb 19 17:10:46 2011 +0000
+++ b/Myhill_2.thy Sat Feb 19 19:27:33 2011 +0000
@@ -62,46 +62,39 @@
where
"=tag= \<equiv> {(x, y) | x y. tag x = tag y}"
-
-lemma finite_range_image:
- assumes "finite (range f)"
- shows "finite (f ` A)"
- using assms unfolding image_def
- by (rule_tac finite_subset) (auto)
-
lemma finite_eq_tag_rel:
assumes rng_fnt: "finite (range tag)"
shows "finite (UNIV // =tag=)"
proof -
- let "?f" = "op ` tag" and ?A = "(UNIV // =tag=)"
+ let "?f" = "\<lambda>X. tag ` X" and ?A = "(UNIV // =tag=)"
-- {* 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 .
+ have "range ?f \<subseteq> (Pow (range tag))" unfolding Pow_def by auto
+ moreover
+ have "finite (Pow (range tag))" using rng_fnt by simp
+ ultimately
+ have "finite (range ?f)" unfolding image_def by (blast intro: finite_subset)
+ moreover
+ have "?f ` ?A \<subseteq> range ?f" by auto
+ ultimately show "finite (?f ` ?A)" by (rule rev_finite_subset)
qed
moreover
-- {* The injectivity of @{text "f"}-image follows from the definition of @{text "(=tag=)"} *}
- have "inj_on ?f ?A"
+ 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"
+ then
+ obtain x y
+ where "x \<in> X" "y \<in> Y" "tag x = tag y"
+ unfolding quotient_def Image_def image_def tag_eq_rel_def
+ by (simp) (blast)
+ with X_in Y_in
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
+ unfolding quotient_def tag_eq_rel_def by auto
} then show "inj_on ?f ?A" unfolding inj_on_def by auto
qed
ultimately
@@ -146,92 +139,25 @@
qed
lemma tag_finite_imageD:
- fixes tag
assumes rng_fnt: "finite (range tag)"
- -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *}
- and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n"
- -- {* And strings with same tag are equivalent *}
- shows "finite (UNIV // (\<approx>Lang))"
-proof -
- let ?R1 = "(=tag=)"
- show ?thesis
- proof(rule_tac refined_partition_finite [of ?R1])
- from finite_eq_tag_rel [OF rng_fnt]
- show "finite (UNIV // =tag=)" .
- next
- from same_tag_eqvt
- show "(=tag=) \<subseteq> (\<approx>Lang)"
- by (auto simp:tag_eq_rel_def str_eq_def)
- next
- show "equiv UNIV (=tag=)"
- unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def
- by auto
- next
- show "equiv UNIV (\<approx>Lang)"
- unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def
- by blast
- qed
+ and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>A n"
+ shows "finite (UNIV // \<approx>A)"
+proof (rule_tac refined_partition_finite [of "=tag="])
+ show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])
+next
+ from same_tag_eqvt
+ show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_rel_def str_eq_def
+ by auto
+next
+ show "equiv UNIV =tag="
+ unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def
+ by auto
+next
+ show "equiv UNIV (\<approx>A)"
+ unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def
+ by blast
qed
-text {*
- A more concise, but less intelligible argument for @{text "tag_finite_imageD"}
- is given as the following. The basic idea is still using standard library
- lemma @{thm [source] "finite_imageD"}:
- \[
- @{thm "finite_imageD" [no_vars]}
- \]
- which says: if the image of injective function @{text "f"} over set @{text "A"} is
- finite, then @{text "A"} must be finte, as we did in the lemmas above.
- *}
-
-lemma
- fixes tag
- assumes rng_fnt: "finite (range tag)"
- -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *}
- and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n"
- -- {* And strings with same tag are equivalent *}
- shows "finite (UNIV // (\<approx>Lang))"
- -- {* Then the partition generated by @{text "(\<approx>Lang)"} is finite. *}
-proof -
- -- {* The particular @{text "f"} and @{text "A"} used in @{thm [source] "finite_imageD"} are:*}
- let "?f" = "op ` tag" and ?A = "(UNIV // \<approx>Lang)"
- 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"} is the consequence of assumption @{text "same_tag_eqvt"}:
- *}
- 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
- apply simp by blast
- from same_tag_eqvt [OF eq_tg] have "x \<approx>Lang y" .
- with X_in Y_in x_in y_in
- show ?thesis by (auto simp:quotient_def str_eq_rel_def str_eq_def)
- qed
- } thus ?thesis unfolding inj_on_def by auto
- qed
- qed
-qed
subsection {* The proof*}
@@ -334,28 +260,25 @@
definition
tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
where
- "tag_str_ALT L1 L2 \<equiv> (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"
+ "tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
lemma quot_union_finiteI [intro]:
fixes L1 L2::"lang"
- assumes finite1: "finite (UNIV // \<approx>L1)"
- and finite2: "finite (UNIV // \<approx>L2)"
- shows "finite (UNIV // \<approx>(L1 \<union> L2))"
-proof (rule_tac tag = "tag_str_ALT L1 L2" in tag_finite_imageD)
- show "\<And>x y. tag_str_ALT L1 L2 x = tag_str_ALT L1 L2 y \<Longrightarrow> x \<approx>(L1 \<union> L2) y"
+ assumes finite1: "finite (UNIV // \<approx>A)"
+ and finite2: "finite (UNIV // \<approx>B)"
+ shows "finite (UNIV // \<approx>(A \<union> B))"
+proof (rule_tac tag = "tag_str_ALT A B" in tag_finite_imageD)
+ have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"
+ using finite1 finite2 by auto
+ then show "finite (range (tag_str_ALT A B))"
+ unfolding tag_str_ALT_def quotient_def
+ by (rule rev_finite_subset) (auto)
+next
+ show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
unfolding tag_str_ALT_def
unfolding str_eq_def
- unfolding Image_def
unfolding str_eq_rel_def
by auto
-next
- have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))"
- using finite1 finite2 by auto
- show "finite (range (tag_str_ALT L1 L2))"
- unfolding tag_str_ALT_def
- apply(rule finite_subset[OF _ *])
- unfolding quotient_def
- by auto
qed
subsubsection {* The inductive case for @{text "SEQ"}*}