# HG changeset patch # User urbanc # Date 1298143653 0 # Node ID ece3f197b92b26aa34ed534b11a8eb36010792c3 # Parent c3fa11ee776e982ebc5296428ef7cb8813b83e94 first two proofs in 2 direction diff -r c3fa11ee776e -r ece3f197b92b Myhill_2.thy --- 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= \ {(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" = "\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 "\ 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 . + have "range ?f \ (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 \ 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 \ ?A" and Y_in: "Y \ ?A" and tag_eq: "?f X = ?f Y" + then + obtain x y + where "x \ X" "y \ 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 \ 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 + 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: "\ m n. tag m = tag (n::string) \ m \Lang n" - -- {* And strings with same tag are equivalent *} - shows "finite (UNIV // (\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=) \ (\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 (\Lang)" - unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def - by blast - qed + and same_tag_eqvt: "\ m n. tag m = tag (n::string) \ m \A n" + shows "finite (UNIV // \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= \ \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 (\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: "\ m n. tag m = tag (n::string) \ m \Lang n" - -- {* And strings with same tag are equivalent *} - shows "finite (UNIV // (\Lang))" - -- {* Then the partition generated by @{text "(\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 // \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 "\ 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"} is the consequence of assumption @{text "same_tag_eqvt"}: - *} - 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 - apply simp by blast - from same_tag_eqvt [OF eq_tg] have "x \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 \ lang \ string \ (lang \ lang)" where - "tag_str_ALT L1 L2 \ (\x. (\L1 `` {x}, \L2 `` {x}))" + "tag_str_ALT A B \ (\x. (\A `` {x}, \B `` {x}))" lemma quot_union_finiteI [intro]: fixes L1 L2::"lang" - assumes finite1: "finite (UNIV // \L1)" - and finite2: "finite (UNIV // \L2)" - shows "finite (UNIV // \(L1 \ L2))" -proof (rule_tac tag = "tag_str_ALT L1 L2" in tag_finite_imageD) - show "\x y. tag_str_ALT L1 L2 x = tag_str_ALT L1 L2 y \ x \(L1 \ L2) y" + assumes finite1: "finite (UNIV // \A)" + and finite2: "finite (UNIV // \B)" + shows "finite (UNIV // \(A \ B))" +proof (rule_tac tag = "tag_str_ALT A B" in tag_finite_imageD) + have "finite ((UNIV // \A) \ (UNIV // \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 "\x y. tag_str_ALT A B x = tag_str_ALT A B y \ x \(A \ 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 // \L1) \ (UNIV // \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"}*} diff -r c3fa11ee776e -r ece3f197b92b Paper/Paper.thy --- 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 \ \x. g x \ f x \ 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 \ 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 "\(L r)"}, which implies that @{term "UNIV // \(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 \ 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 \ 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 \ 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 \ "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}. + From the assumption we can obtain a @{text "x \ X"} and @{text "y \ 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 // \(L r)"} is finite, we have to find a tagging function whose - range is finite and whose tagging-relation refines @{term "\(L r)"}. + range can be shown to be finite and whose tagging-relation refines @{term "\(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 // \A)"} and @{term "finite (UNIV // \B)"} + then @{term "finite ((UNIV // \A) \ (UNIV // \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 "\(A \ 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"]}