--- 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
--- a/Paper/Paper.thy Sat Feb 19 12:01:16 2011 +0000
+++ b/Paper/Paper.thy Sat Feb 19 17:10:46 2011 +0000
@@ -884,13 +884,14 @@
directly. The reader is invited to try.
Our method will rely on some
- \emph{tagging} functions of strings. Given the inductive hypothesis, it will
+ \emph{tagging functions} defined over strings. Given the inductive hypothesis, it will
be easy to prove that the range of these tagging functions is finite.
With this we will be able to infer that the tagging functions, seen as a relation,
give rise to finitely many equivalence classes of @{const UNIV}. Finally we
will show that the tagging relation is more refined than @{term "\<approx>(L r)"}, which
- implies that @{term "UNIV // \<approx>(L r)"} must also be finite. For this we define the
- notion of a \emph{tag-relation} (which is often also called a kernel relation).
+ implies that @{term "UNIV // \<approx>(L r)"} must also be finite.
+ A relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
+ We also define formally the notion of a \emph{tag-relation} as follows.
\begin{definition}[Tag-Relation] Given a tag-function @{text tag}, then two strings @{text x}
and @{text y} are tag-related provided
@@ -899,26 +900,49 @@
\end{center}
\end{definition}
+ \noindent
+ In order to establis finiteness of a set @{text A} we shall use the following powerful
+ principle from Isabelle/HOL's library.
+ %
+ \begin{equation}\label{finiteimageD}
+ @{thm[mode=IfThen] finite_imageD}
+ \end{equation}
+
+ \noindent
+ It states that if an image of a set under an injective function @{text f} (over this set)
+ is finite, then @{text A} itself must be finite. We can use it to establish the following
+ two lemmas.
+
\begin{lemma}\label{finone}
@{thm[mode=IfThen] finite_eq_tag_rel}
\end{lemma}
\begin{proof}
-
+
\end{proof}
- \noindent
-
-
\begin{lemma}\label{fintwo}
- Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, then
- if @{thm (prem 1) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
- and @{thm (prem 2) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
- then @{thm (concl) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
+ Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, where
+ @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
+ If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+ then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
\end{lemma}
\begin{proof}
-
+ We prove this lemma again using \eqref{finiteimageD}. For this we set @{text f} to
+ be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that
+ @{text "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{text "Pow (UNIV // R\<^isub>1)"},
+ which is finite by assumption. What remains to be shown is that @{text f} is injective
+ on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence
+ classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
+ @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
+ @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
+ We know there exists a @{text x} with @{term "X = R\<^isub>2 `` {x}"}
+ and @{text "x \<in> X"}. From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
+ and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. From this we can obtain a @{text y}
+ such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. This means @{text x} and @{text y}
+ are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
+ they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
\end{proof}
\noindent