# HG changeset patch # User urbanc # Date 1312108061 0 # Node ID 97090fc7aa9fe850a65adfb0cef95dd81ced3371 # Parent b755090d0f3d8be8cfff920825221917cf6a7ccb some experiments with the proofs in Myhill_2 diff -r b755090d0f3d -r 97090fc7aa9f Closures.thy --- a/Closures.thy Thu Jul 28 17:52:36 2011 +0000 +++ b/Closures.thy Sun Jul 31 10:27:41 2011 +0000 @@ -48,7 +48,7 @@ shows "regular (- A)" proof - from assms have "finite (UNIV // \A)" by (simp add: Myhill_Nerode) - then have "finite (UNIV // \(-A))" by (simp add: str_eq_rel_def) + then have "finite (UNIV // \(-A))" by (simp add: str_eq_def) then show "regular (- A)" by (simp add: Myhill_Nerode) qed diff -r b755090d0f3d -r 97090fc7aa9f Derivatives.thy --- a/Derivatives.thy Thu Jul 28 17:52:36 2011 +0000 +++ b/Derivatives.thy Sun Jul 31 10:27:41 2011 +0000 @@ -417,7 +417,7 @@ lemma MN_Rel_Ders: shows "x \A y \ Ders x A = Ders y A" -unfolding Ders_def str_eq_def str_eq_rel_def +unfolding Ders_def str_eq_def by auto subsection {* @@ -442,20 +442,17 @@ qed moreover have "=(\x. pders x r)= \ \(lang r)" - unfolding tag_eq_rel_def - unfolding str_eq_def2 - unfolding MN_Rel_Ders - unfolding Ders_pders - by auto + unfolding tag_eq_def + by (auto simp add: MN_Rel_Ders Ders_pders) moreover have "equiv UNIV =(\x. pders x r)=" unfolding equiv_def refl_on_def sym_def trans_def - unfolding tag_eq_rel_def + unfolding tag_eq_def by auto moreover have "equiv UNIV (\(lang r))" unfolding equiv_def refl_on_def sym_def trans_def - unfolding str_eq_rel_def + unfolding str_eq_def by auto ultimately show "finite (UNIV // \(lang r))" by (rule refined_partition_finite) diff -r b755090d0f3d -r 97090fc7aa9f Journal/Paper.thy --- a/Journal/Paper.thy Thu Jul 28 17:52:36 2011 +0000 +++ b/Journal/Paper.thy Sun Jul 31 10:27:41 2011 +0000 @@ -39,8 +39,8 @@ notation (latex output) - str_eq_rel ("\\<^bsub>_\<^esub>") and - str_eq ("_ \\<^bsub>_\<^esub> _") and + str_eq ("\\<^bsub>_\<^esub>") and + str_eq_applied ("_ \\<^bsub>_\<^esub> _") and conc (infixr "\" 100) and star ("_\<^bsup>\\<^esup>") and pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and @@ -59,13 +59,13 @@ Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and - tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and - tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and - tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and - tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and - tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and - tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and - tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and + tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and + tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and + tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and + tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and + tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and + tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and + tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and Delta ("\'(_')") and nullable ("\'(_')") and Cons ("_ :: _" [100, 100] 100) @@ -74,6 +74,10 @@ shows "f \ \x. g x \ f x \ g x" by auto +lemma str_eq_def': + shows "x \A y \ (\z. x @ z \ A \ y @ z \ A)" +unfolding str_eq_def by simp + lemma conc_def': "A \ B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \ A \ s\<^isub>2 \ B}" unfolding conc_def by simp @@ -174,7 +178,7 @@ \begin{center} \begin{tabular}{ccc} - \begin{tikzpicture}[scale=0.9] + \begin{tikzpicture}[scale=1] %\draw[step=2mm] (-1,-1) grid (1,1); \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3); @@ -190,8 +194,8 @@ \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; - \draw (-0.6,0.0) node {\footnotesize$A_1$}; - \draw ( 0.6,0.0) node {\footnotesize$A_2$}; + \draw (-0.6,0.0) node {\small$A_1$}; + \draw ( 0.6,0.0) node {\small$A_2$}; \end{tikzpicture} & @@ -200,7 +204,7 @@ & - \begin{tikzpicture}[scale=0.9] + \begin{tikzpicture}[scale=1] %\draw[step=2mm] (-1,-1) grid (1,1); \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3); @@ -219,8 +223,8 @@ \draw (C) to [very thick, bend left=45] (B); \draw (D) to [very thick, bend right=45] (B); - \draw (-0.6,0.0) node {\footnotesize$A_1$}; - \draw ( 0.6,0.0) node {\footnotesize$A_2$}; + \draw (-0.6,0.0) node {\small$A_1$}; + \draw ( 0.6,0.0) node {\small$A_2$}; \end{tikzpicture} \end{tabular} @@ -300,7 +304,7 @@ everything is crystal clear. However, paper proofs about automata often involve subtle side-conditions which are easily overlooked, but which make formal reasoning rather painful. For example Kozen's proof of the - Myhill-Nerode theorem requires that the automata do not have inaccessible + Myhill-Nerode theorem requires that automata do not have inaccessible states \cite{Kozen97}. Another subtle side-condition is completeness of automata, that is automata need to have total transition functions and at most one `sink' state from which there is no connection to a final state (Brozowski @@ -346,7 +350,7 @@ To our best knowledge, our proof of the Myhill-Nerode theorem is the first that is based on regular expressions, only. The part of this theorem stating that finitely many partitions imply regularity of the language is proved by - an argument about solving equational sytems. This argument appears to be + an argument about solving equational systems. This argument appears to be folklore. For the other part, we give two proofs: one direct proof using certain tagging-functions, and another indirect proof using Antimirov's partial derivatives \cite{Antimirov95}. Again to our best knowledge, the @@ -403,10 +407,11 @@ the proofs for these properties, but invite the reader to consult our formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}} - The notation in Isabelle/HOL for the quotient of a language @{text A} according to an - equivalence relation @{term REL} is @{term "A // REL"}. We will write - @{text "\x\\<^isub>\"} for the equivalence class defined - as \mbox{@{text "{y | y \ x}"}}. + The notation in Isabelle/HOL for the quotient of a language @{text A} + according to an equivalence relation @{term REL} is @{term "A // REL"}. We + will write @{text "\x\\<^isub>\"} for the equivalence class defined as + \mbox{@{text "{y | y \ x}"}}, and have @{text "x \ y"} if and only if @{text + "\x\\<^isub>\ = \y\\<^isub>\"}. Central to our proof will be the solution of equational systems @@ -426,9 +431,9 @@ \begin{proof} For the right-to-left direction we assume @{thm (rhs) arden} and show that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"} - we have @{term "A\ = {[]} \ A \ A\"}, - which is equal to @{term "A\ = {[]} \ A\ \ A"}. Adding @{text B} to both - sides gives @{term "B \ A\ = B \ ({[]} \ A\ \ A)"}, whose right-hand side + we have @{term "A\ = A \ A\ \ {[]}"}, + which is equal to @{term "A\ = A\ \ A \ {[]}"}. Adding @{text B} to both + sides gives @{term "B \ A\ = B \ (A\ \ A \ {[]})"}, whose right-hand side is equal to @{term "(B \ A\) \ A \ B"}. This completes this direction. For the other direction we assume @{thm (lhs) arden}. By a simple induction @@ -515,7 +520,7 @@ Given a language @{text A}, two strings @{text x} and @{text y} are Myhill-Nerode related provided \begin{center} - @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]} + @{thm str_eq_def'} \end{center} \end{dfntn} @@ -641,7 +646,7 @@ \noindent where @{text "d\<^isub>1\d\<^isub>n"} is the sequence of all characters - except @{text c}, and @{text "c\<^isub>1\c\<^isub>m"} is the sequence of all + but not containing @{text c}, and @{text "c\<^isub>1\c\<^isub>m"} is the sequence of all characters. Overloading the function @{text \} for the two kinds of terms in the @@ -1067,7 +1072,7 @@ text {* \noindent - In this section and the next we will give two proofs for establishing the second + In this section we will give a proof for establishing the second part of the Myhill-Nerode theorem. It can be formulated in our setting as follows: \begin{thrm} @@ -1075,7 +1080,7 @@ \end{thrm} \noindent - The first proof will be by induction on the structure of @{text r}. It turns out + The proof will be by induction on the structure of @{text r}. It turns out the base cases are straightforward. @@ -1099,11 +1104,11 @@ Much more interesting, however, are the inductive cases. They seem hard to solve directly. The reader is invited to try. - In order how to see how our first proof proceeds we use the following suggestive picture - from Constable et al \cite{Constable00}: + In order to see how our proof proceeds consider the following suggestive picture + taken from Constable et al \cite{Constable00}: - \begin{center} - \begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c} + \begin{equation}\label{pics} + \mbox{\begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c} \begin{tikzpicture}[scale=1] %Circle \draw[thick] (0,0) circle (1.1); @@ -1129,10 +1134,17 @@ \draw (\a: 0.77) node {$a_{\l}$}; \end{tikzpicture}\\ @{term UNIV} & @{term "UNIV // (\(lang r))"} & @{term "UNIV // R"} - \end{tabular} - \end{center} + \end{tabular}} + \end{equation} - Our first proof will rely on some + \noindent + The relation @{term "\(lang r)"} partitions the set of all strings into some + equivalence classes. To show that there are only finitely many of + them, it suffices to show in each induction step the existence of another + relation, say @{text R}, for which we can show that there are finitely many + equivalence classes and which refines @{term "\(lang r)"}. A relation @{text + "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text + "R\<^isub>1 \ R\<^isub>2"}. For constructing @{text R} will rely on some \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will be easy to prove that the \emph{range} of these tagging-functions is finite. The range of a function @{text f} is defined as @@ -1142,13 +1154,14 @@ \end{center} \noindent - that means we take the image of @{text f} w.r.t.~all elements in the domain. - With this we will be able to infer that the tagging-functions, seen as relations, - give rise to finitely many equivalence classes of @{const UNIV}. Finally we - will show that the tagging-relations are more refined than @{term "\(lang r)"}, which - implies that @{term "UNIV // \(lang 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 formally define the notion of a \emph{tagging-relation} as follows. + that means we take the image of @{text f} w.r.t.~all elements in the + domain. With this we will be able to infer that the tagging-functions, seen + as relations, give rise to finitely many equivalence classes of @{const + UNIV}. Finally we will show that the tagging-relations are more refined than + @{term "\(lang r)"}, which implies that @{term "UNIV // \(lang r)"} must + also be finite. We formally define the notion of a \emph{tagging-relation} + as follows. + \begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x} and @{text y} are \emph{tag-related} provided @@ -1212,7 +1225,7 @@ \noindent Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show - that @{term "UNIV // \(lang r)"} is finite, we have to find a tagging-function whose + that @{term "UNIV // \(lang r)"} is finite, we have to construct a tagging-function whose range can be shown to be finite and whose tagging-relation refines @{term "\(lang r)"}. Let us attempt the @{const PLUS}-case first. @@ -1220,14 +1233,14 @@ We take as tagging-function % \begin{center} - @{thm tag_str_Plus_def[where A="A" and B="B", THEN meta_eq_app]} + @{thm tag_Plus_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_Plus A B"} is a subset of this product set---so finite. It remains to be shown + @{term "tag_Plus A B"} is a subset of this product set---so finite. It remains to be shown that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\(A \ B)"}. This amounts to showing % @@ -1269,17 +1282,21 @@ notions of \emph{string prefixes} % \begin{center} - @{text "x \ y \ \z. y = x @ z"}\hspace{10mm} + \begin{tabular}{l} + @{text "x \ y \ \z. y = x @ z"}\\ @{text "x < y \ x \ y \ x \ y"} + \end{tabular} \end{center} % \noindent and \emph{string subtraction}: % \begin{center} - @{text "[] - y \ []"}\hspace{10mm} - @{text "x - [] \ x"}\hspace{10mm} - @{text "cx - dy \ if c = d then x - y else cx"} + \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l} + @{text "[] - y"} & @{text "\"} & @{text "[]"}\\ + @{text "x - []"} & @{text "\"} & @{text "x"}\\ + @{text "cx - dy"} & @{text "\"} & @{text "if c = d then x - y else cx"} + \end{tabular} \end{center} % \noindent @@ -1289,8 +1306,8 @@ this string to be in @{term "A \ B"}: % \begin{center} - \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}} - \scalebox{0.7}{ + \begin{tabular}{c} + \scalebox{0.9}{ \begin{tikzpicture} \node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ }; \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ }; @@ -1316,8 +1333,8 @@ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$) node[midway, below=0.5em]{@{term "x' \ A"}}; \end{tikzpicture}} - & - \scalebox{0.7}{ + \\ + \scalebox{0.9}{ \begin{tikzpicture} \node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ }; \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ }; @@ -1353,7 +1370,7 @@ following tagging-function % \begin{center} - @{thm tag_str_Times_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]} + @{thm tag_Times_def[where ?A="A" and ?B="B", THEN meta_eq_app]} \end{center} \noindent @@ -1363,11 +1380,11 @@ \begin{proof}[@{const TIMES}-Case] If @{term "finite (UNIV // \A)"} and @{term "finite (UNIV // \B)"} then @{term "finite ((UNIV // \A) \ (Pow (UNIV // \B)))"} holds. The range of - @{term "tag_str_TIMES A B"} is a subset of this product set, and therefore finite. + @{term "tag_Times A B"} is a subset of this product set, and therefore finite. We have to show injectivity of this tagging-function as % \begin{center} - @{term "\z. tag_str_TIMES A B x = tag_str_TIMES A B y \ x @ z \ A \ B \ y @ z \ A \ B"} + @{term "\z. tag_Times A B x = tag_Times A B y \ x @ z \ A \ B \ y @ z \ A \ B"} \end{center} % \noindent @@ -1380,7 +1397,7 @@ \end{center} % \noindent - and by the assumption about @{term "tag_str_TIMES A B"} also + and by the assumption about @{term "tag_Times A B"} also % \begin{center} @{term "(\B `` {x - x'}) \ ({\B `` {y - y'} |y'. y' \ y \ y' \ A})"} @@ -1395,7 +1412,7 @@ @{term "y @ z \ A \ B"}, as needed in this case. Second, there exists a @{text "z'"} such that @{term "x @ z' \ A"} and @{text "z - z' \ B"}. - By the assumption about @{term "tag_str_TIMES A B"} we have + By the assumption about @{term "tag_Times A B"} we have @{term "\A `` {x} = \A `` {y}"} and thus @{term "x \A y"}. Which means by the Myhill-Nerode relation that @{term "y @ z' \ A"} holds. Using @{text "z - z' \ B"}, we can conclude also in this case with @{term "y @ z \ A \ B"}. We again can complete the @{const TIMES}-case @@ -1467,17 +1484,17 @@ the following tagging-function: % \begin{center} - @{thm tag_str_Star_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip + @{thm tag_Star_def[where ?A="A", THEN meta_eq_app]}\smallskip \end{center} \begin{proof}[@{const Star}-Case] If @{term "finite (UNIV // \A)"} then @{term "finite (Pow (UNIV // \A))"} holds. The range of - @{term "tag_str_Star A"} is a subset of this set, and therefore finite. + @{term "tag_Star A"} is a subset of this set, and therefore finite. Again we have to show injectivity of this tagging-function as % \begin{center} - @{term "\z. tag_str_Star A x = tag_str_Star A y \ x @ z \ A\ \ y @ z \ A\"} + @{term "\z. tag_Star A x = tag_Star A y \ x @ z \ A\ \ y @ z \ A\"} \end{center} % \noindent diff -r b755090d0f3d -r 97090fc7aa9f Myhill_1.thy --- a/Myhill_1.thy Thu Jul 28 17:52:36 2011 +0000 +++ b/Myhill_1.thy Sun Jul 31 10:27:41 2011 +0000 @@ -11,11 +11,17 @@ text {* Myhill-Nerode relation *} + definition - str_eq_rel :: "'a lang \ ('a list \ 'a list) set" ("\_" [100] 100) + str_eq :: "'a lang \ ('a list \ 'a list) set" ("\_" [100] 100) where "\A \ {(x, y). (\z. x @ z \ A \ y @ z \ A)}" +abbreviation + str_eq_applied :: "'a list \ 'a lang \ 'a list \ bool" ("_ \_ _") +where + "x \A y \ (x, y) \ \A" + definition finals :: "'a lang \ 'a lang set" where @@ -25,7 +31,7 @@ shows "A = \ finals A" unfolding finals_def unfolding Image_def -unfolding str_eq_rel_def +unfolding str_eq_def by (auto) (metis append_Nil2) lemma finals_in_partitions: @@ -247,7 +253,7 @@ assumes "s \ X" "X \ UNIV // \A" shows "X = \A `` {s}" using assms -unfolding quotient_def Image_def str_eq_rel_def +unfolding quotient_def Image_def str_eq_def by auto lemma every_eqclass_has_transition: @@ -263,11 +269,11 @@ using has_str in_CS defined_by_str by blast then have "Y \ {[c]} \ X" unfolding Y_def Image_def conc_def - unfolding str_eq_rel_def + unfolding str_eq_def by clarsimp moreover have "s \ Y" unfolding Y_def - unfolding Image_def str_eq_rel_def by simp + unfolding Image_def str_eq_def by simp ultimately show thesis using that by blast qed diff -r b755090d0f3d -r 97090fc7aa9f Myhill_2.thy --- a/Myhill_2.thy Thu Jul 28 17:52:36 2011 +0000 +++ b/Myhill_2.thy Sun Jul 31 10:27:41 2011 +0000 @@ -5,21 +5,30 @@ section {* Direction @{text "regular language \ finite partition"} *} -definition - str_eq :: "'a list \ 'a lang \ 'a list \ bool" ("_ \_ _") -where - "x \A y \ (x, y) \ (\A)" - -lemma str_eq_def2: - shows "\A = {(x, y) | x y. x \A y}" -unfolding str_eq_def -by simp - definition - tag_eq_rel :: "('a list \ 'b) \ ('a list \ 'a list) set" ("=_=") + tag_eq :: "('a list \ 'b) \ ('a list \ 'a list) set" ("=_=") where "=tag= \ {(x, y). tag x = tag y}" +abbreviation + tag_eq_applied :: "'a list \ ('a list \ 'b) \ 'a list \ bool" ("_ =_= _") +where + "x =tag= y \ (x, y) \ =tag=" + +lemma test: + shows "(\A) `` {x} = (\A) `` {y} \ x \A y" +unfolding str_eq_def +by auto + +lemma test_refined_intro: + assumes "\x y z. \x =tag= y; x @ z \ A\ \ y @ z \ A" + shows "=tag= \ \A" +using assms +unfolding str_eq_def tag_eq_def +apply(clarify, simp (no_asm_use)) +by metis + + lemma finite_eq_tag_rel: assumes rng_fnt: "finite (range tag)" shows "finite (UNIV // =tag=)" @@ -45,11 +54,11 @@ 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 + unfolding quotient_def Image_def image_def tag_eq_def by (simp) (blast) with X_in Y_in have "X = Y" - unfolding quotient_def tag_eq_rel_def by auto + unfolding quotient_def tag_eq_def by auto } then show "inj_on ?f ?A" unfolding inj_on_def by auto qed @@ -101,15 +110,15 @@ 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 + show "=tag= \ \A" unfolding tag_eq_def str_eq_def + by blast next show "equiv UNIV =tag=" - unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def + unfolding equiv_def tag_eq_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 + unfolding equiv_def str_eq_def sym_def refl_on_def trans_def by blast qed @@ -120,7 +129,7 @@ lemma quot_zero_eq: shows "UNIV // \{} = {UNIV}" -unfolding quotient_def Image_def str_eq_rel_def by auto +unfolding quotient_def Image_def str_eq_def by auto lemma quot_zero_finiteI [intro]: shows "finite (UNIV // \{})" @@ -139,11 +148,11 @@ show "x \ {{[]}, UNIV - {[]}}" proof (cases "y = []") case True with h - have "x = {[]}" by (auto simp: str_eq_rel_def) + have "x = {[]}" by (auto simp: str_eq_def) thus ?thesis by simp next case False with h - have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def) + have "x = UNIV - {[]}" by (auto simp: str_eq_def) thus ?thesis by simp qed qed @@ -165,17 +174,17 @@ show "x \ {{[]},{[c]}, UNIV - {[], [c]}}" proof - { assume "y = []" hence "x = {[]}" using h - by (auto simp:str_eq_rel_def) } + by (auto simp: str_eq_def) } moreover { assume "y = [c]" hence "x = {[c]}" using h - by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def) } + by (auto dest!: spec[where x = "[]"] simp: str_eq_def) } moreover { assume "y \ []" and "y \ [c]" hence "\ z. (y @ z) \ [c]" by (case_tac y, auto) moreover have "\ p. (p \ [] \ p \ [c]) = (\ q. p @ q \ [c])" by (case_tac p, auto) ultimately have "x = UNIV - {[],[c]}" using h - by (auto simp add:str_eq_rel_def) + by (auto simp add: str_eq_def) } ultimately show ?thesis by blast qed @@ -189,38 +198,126 @@ subsubsection {* The inductive case for @{const Plus} *} definition - tag_str_Plus :: "'a lang \ 'a lang \ 'a list \ ('a lang \ 'a lang)" + tag_Plus :: "'a lang \ 'a lang \ 'a list \ ('a lang \ 'a lang)" where - "tag_str_Plus A B \ (\x. (\A `` {x}, \B `` {x}))" + "tag_Plus A B \ (\x. (\A `` {x}, \B `` {x}))" -lemma quot_union_finiteI [intro]: +lemma quot_plus_finiteI [intro]: assumes finite1: "finite (UNIV // \A)" and finite2: "finite (UNIV // \B)" shows "finite (UNIV // \(A \ B))" -proof (rule_tac tag = "tag_str_Plus A B" in tag_finite_imageD) +proof (rule_tac tag = "tag_Plus A B" in tag_finite_imageD) have "finite ((UNIV // \A) \ (UNIV // \B))" using finite1 finite2 by auto - then show "finite (range (tag_str_Plus A B))" - unfolding tag_str_Plus_def quotient_def + then show "finite (range (tag_Plus A B))" + unfolding tag_Plus_def quotient_def by (rule rev_finite_subset) (auto) next - show "\x y. tag_str_Plus A B x = tag_str_Plus A B y \ x \(A \ B) y" - unfolding tag_str_Plus_def + show "\x y. tag_Plus A B x = tag_Plus A B y \ x \(A \ B) y" + unfolding tag_Plus_def unfolding str_eq_def - unfolding str_eq_rel_def by auto qed subsubsection {* The inductive case for @{text "Times"}*} +definition + "Partitions s \ {(u, v). u @ v = s}" + +lemma conc_elim: + assumes "x \ A \ B" + shows "\(u, v) \ Partitions x. u \ A \ v \ B" +using assms +unfolding conc_def Partitions_def +by auto + +lemma conc_intro: + assumes "(u, v) \ Partitions x \ u \ A \ v \ B" + shows "x \ A \ B" +using assms +unfolding conc_def Partitions_def +by auto + + +lemma y: + "\x \ A; x \A y\ \ y \ A" +apply(simp add: str_eq_def) +apply(drule_tac x="[]" in spec) +apply(simp) +done + definition - tag_str_Times :: "'a lang \ 'a lang \ 'a list \ ('a lang \ 'a lang set)" + tag_Times3a :: "'a lang \ 'a lang \ 'a list \ 'a lang" +where + "tag_Times3a A B \ (\x. \A `` {x})" + +definition + tag_Times3b :: "'a lang \ 'a lang \ 'a list \ ('a lang \ 'a lang) set" +where + "tag_Times3b A B \ + (\x. ({(\A `` {u}, \B `` {v}) | u v. (u, v) \ Partitions x}))" + +definition + tag_Times3 :: "'a lang \ 'a lang \ 'a list \ 'a lang \ ('a lang \ 'a lang) set" where - "tag_str_Times L1 L2 \ - (\x. (\L1 `` {x}, {(\L2 `` {x - xa}) | xa. xa \ x \ xa \ L1}))" + "tag_Times3 A B \ + (\x. (tag_Times3a A B x, tag_Times3b A B x))" -lemma Seq_in_cases: +lemma + assumes a: "tag_Times3a A B x = tag_Times3a A B y" + and b: "tag_Times3b A B x = tag_Times3b A B y" + and c: "x @ z \ A \ B" + shows "y @ z \ A \ B" +proof - + from c obtain u v where + h1: "(u, v) \ Partitions (x @ z)" and + h2: "u \ A" and + h3: "v \ B" by (auto dest: conc_elim) + from h1 have "x @ z = u @ v" unfolding Partitions_def by simp + then obtain us + where "(x = u @ us \ us @ z = v) \ (x @ us = u \ z = us @ v)" + by (auto simp add: append_eq_append_conv2) + moreover + { assume eq: "x = u @ us" "us @ z = v" + have "(\A `` {u}, \B `` {us}) \ tag_Times3b A B x" + unfolding tag_Times3b_def Partitions_def using eq by auto + then have "(\A `` {u}, \B `` {us}) \ tag_Times3b A B y" + using b by simp + then obtain u' us' where + q1: "\A `` {u} = \A `` {u'}" and + q2: "\B `` {us} = \B `` {us'}" and + q3: "(u', us') \ Partitions y" + by (auto simp add: tag_Times3b_def) + from q1 h2 have "u' \ A" + using y unfolding Image_def str_eq_def by blast + moreover from q2 h3 eq + have "us' @ z \ B" + unfolding Image_def str_eq_def by auto + ultimately have "y @ z \ A \ B" using q3 + unfolding Partitions_def by auto + } + moreover + { assume eq: "x @ us = u" "z = us @ v" + have "(\A `` {x}) = tag_Times3a A B x" + unfolding tag_Times3a_def by simp + then have "(\A `` {x}) = tag_Times3a A B y" + using a by simp + then have "\A `` {x} = \A `` {y}" + unfolding tag_Times3a_def by simp + moreover + have "x @ us \ A" using h2 eq by simp + ultimately + have "y @ us \ A" using y + unfolding Image_def str_eq_def by blast + then have "(y @ us) @ v \ A \ B" + using h3 unfolding conc_def by blast + then have "y @ z \ A \ B" using eq by simp + } + ultimately show "y @ z \ A \ B" by blast +qed + +lemma conc_in_cases2: assumes "x @ z \ A \ B" shows "(\ x' \ x. x' \ A \ (x - x') @ z \ B) \ (\ z' \ z. (x @ z') \ A \ (z - z') \ B)" @@ -228,13 +325,19 @@ unfolding conc_def prefix_def by (auto simp add: append_eq_append_conv2) -lemma tag_str_Times_injI: - assumes eq_tag: "tag_str_Times A B x = tag_str_Times A B y" +definition + tag_Times :: "'a lang \ 'a lang \ 'a list \ ('a lang \ 'a lang set)" +where + "tag_Times A B \ + (\x. (\