--- 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"}*}
--- a/Paper/Paper.thy Sat Feb 19 17:10:46 2011 +0000
+++ b/Paper/Paper.thy Sat Feb 19 19:27:33 2011 +0000
@@ -34,8 +34,14 @@
Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
- uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100)
-
+ uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
+ tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
+ tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100)
+
+lemma meta_eq_app:
+ shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
+ by auto
+
(*>*)
@@ -885,23 +891,24 @@
Our method will rely on some
\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.
+ be easy to prove that the range of these tagging functions is finite
+ (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}).
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.
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.
+ We formally define 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
+ \begin{definition}[Tagging-Relation] Given a tag-function @{text tag}, then two strings @{text x}
+ and @{text y} are \emph{tag-related} provided
\begin{center}
@{text "x =tag= y \<equiv> tag x = tag y"}
\end{center}
\end{definition}
\noindent
- In order to establis finiteness of a set @{text A} we shall use the following powerful
+ In order to establish finiteness of a set @{text A} we shall use the following powerful
principle from Isabelle/HOL's library.
%
\begin{equation}\label{finiteimageD}
@@ -918,7 +925,14 @@
\end{lemma}
\begin{proof}
-
+ We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
+ @{text "range f"} to be subset of @{term "Pow (range tag)"}, which we know must be
+ finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"},
+ and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
+ assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
+ From the assumption we can obtain a @{text "x \<in> X"} and @{text "y \<in> Y"} with
+ @{text "tag x = tag y"}. This in turn means that the equivalence classes @{text X}
+ and @{text Y} must be equal.\qed
\end{proof}
\begin{lemma}\label{fintwo}
@@ -946,12 +960,27 @@
\end{proof}
\noindent
- Stringing Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
+ Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging function whose
- range is finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
+ range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
+ Let us attempt the @{const ALT}-case.
+
+ \begin{proof}[@{const "ALT"}-Case]
+ We take as tagging function
+
+ \begin{center}
+ @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
+ \end{center}
+ \noindent
+ where @{text "A"} and @{text "B"} are some arbitrary languages.
+ We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+ then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
+ @{term "tag_str_ALT A B"} is a subset of this. It remains to be shown
+ that @{text "=tag\<^isub>A\<^isub>L\<^isub>T="} refines @{text "\<approx>(A \<union> B)"}.
- @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]}
+ \end{proof}
+
@{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]}