# HG changeset patch # User urbanc # Date 1298116876 0 # Node ID 22ba25b808c8242977ff3a094db27b15d2f5fdae # Parent 342983676c8f95d211721510af647d6066958c06 updated second direction diff -r 342983676c8f -r 22ba25b808c8 Myhill_2.thy --- a/Myhill_2.thy Sat Feb 19 10:23:51 2011 +0000 +++ b/Myhill_2.thy Sat Feb 19 12:01:16 2011 +0000 @@ -58,12 +58,13 @@ *} definition - f_eq_rel ("=_=") + tag_eq_rel :: "(string \ 'b) \ (string \ string) set" ("=_=") where - "=f= \ {(x, y) | x y. f x = f y}" + "=tag= \ {(x, y) | x y. tag x = tag y}" + -lemma equiv_f_eq_rel:"equiv UNIV (=f=)" - by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def) +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)" @@ -71,7 +72,9 @@ using assms unfolding image_def by (rule_tac finite_subset) (auto) -lemma finite_eq_f_rel: +thm finite_imageD + +lemma finite_eq_tag_rel: assumes rng_fnt: "finite (range tag)" shows "finite (UNIV // =tag=)" proof - @@ -83,7 +86,7 @@ *} show "finite (?f ` ?A)" proof - - have "\ X. ?f X \ (Pow (range tag))" by (auto simp:image_def Pow_def) + 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) @@ -94,7 +97,7 @@ The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}: *} show "inj_on ?f ?A" - proof- + proof - { fix X Y assume X_in: "X \ ?A" and Y_in: "Y \ ?A" @@ -105,10 +108,11 @@ 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 f_eq_rel_def + str_eq_def image_def tag_eq_rel_def apply simp by blast - with X_in Y_in show ?thesis - by (auto simp:quotient_def str_eq_rel_def str_eq_def f_eq_rel_def) + 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 @@ -188,14 +192,14 @@ let ?R1 = "(=tag=)" show ?thesis proof(rule_tac refined_partition_finite [of _ ?R1]) - from finite_eq_f_rel [OF rng_fnt] + from finite_eq_tag_rel [OF rng_fnt] show "finite (UNIV // =tag=)" . next from same_tag_eqvt show "(=tag=) \ (\Lang)" - by (auto simp:f_eq_rel_def str_eq_def) + by (auto simp:tag_eq_rel_def str_eq_def) next - from equiv_f_eq_rel + from equiv_tag_eq_rel show "equiv UNIV (=tag=)" by blast next from equiv_lang_eq diff -r 342983676c8f -r 22ba25b808c8 Paper/Paper.thy --- a/Paper/Paper.thy Sat Feb 19 10:23:51 2011 +0000 +++ b/Paper/Paper.thy Sat Feb 19 12:01:16 2011 +0000 @@ -365,10 +365,13 @@ The key definition in the Myhill-Nerode theorem is the \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two strings are related, provided there is no distinguishing extension in this - language. This can be defined as tertiary relation: + language. This can be defined as tertiary relation. - \begin{definition}[Myhill-Nerode Relation]\mbox{}\\ + \begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and + @{text y} are related provided + \begin{center} @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]} + \end{center} \end{definition} \noindent @@ -877,10 +880,52 @@ \end{proof} \noindent - Much more interesting are the inductive cases, which seem hard to be solved - directly. The reader is invited to try. Our method will rely on some + Much more interesting, however, are the inductive cases. They seem hard to be solved + directly. The reader is invited to try. + + Our method will rely on some \emph{tagging} functions of 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 "\(L r)"}, which + implies that @{term "UNIV // \(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). + + \begin{definition}[Tag-Relation] Given a tag-function @{text tag}, then two strings @{text x} + and @{text y} are tag-related provided + \begin{center} + @{text "x =tag= y \ tag x = tag y"} + \end{center} + \end{definition} + + \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"]}. + \end{lemma} + + \begin{proof} + + \end{proof} + + \noindent + Stringing 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)"}. + @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]} @@ -890,6 +935,7 @@ *} + section {* Conclusion and Related Work *} text {*