# HG changeset patch # User zhang # Date 1295957671 0 # Node ID b6815473ee2eeb3f653ce037c4ba779ff621d477 # Parent f5db9e08effc6e15a349a4a794d12544af9057ca 1. Myhill.thy is proved to correct some typos. 2. Some sections are added to the first direction. 3. The small theory of list difference is now separated into Prefix_subtract.thy and the ROOT.ML diff -r f5db9e08effc -r b6815473ee2e IsaMakefile --- a/IsaMakefile Mon Jan 24 11:29:55 2011 +0000 +++ b/IsaMakefile Tue Jan 25 12:14:31 2011 +0000 @@ -31,7 +31,7 @@ session2: tphols-2011/ROOT.ML \ tphols-2011/document/root* \ - ../*.thy + *.thy @$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011 paper: session2 diff -r f5db9e08effc -r b6815473ee2e Myhill.thy --- a/Myhill.thy Mon Jan 24 11:29:55 2011 +0000 +++ b/Myhill.thy Tue Jan 25 12:14:31 2011 +0000 @@ -1,1570 +1,1492 @@ -theory Myhill - imports Main List_Prefix -begin - -section {* Preliminary definitions *} - -text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *} -definition Seq :: "string set \ string set \ string set" ("_ ;; _" [100,100] 100) -where - "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \ L1 \ s2 \ L2}" - -text {* Transitive closure of language @{text "L"}. *} -inductive_set - Star :: "string set \ string set" ("_\" [101] 102) - for L :: "string set" -where - start[intro]: "[] \ L\" -| step[intro]: "\s1 \ L; s2 \ L\\ \ s1@s2 \ L\" - -text {* Some properties of operator @{text ";;"}.*} - -lemma seq_union_distrib: - "(A \ B) ;; C = (A ;; C) \ (B ;; C)" -by (auto simp:Seq_def) - -lemma seq_intro: - "\x \ A; y \ B\ \ x @ y \ A ;; B " -by (auto simp:Seq_def) - -lemma seq_assoc: - "(A ;; B) ;; C = A ;; (B ;; C)" -apply(auto simp:Seq_def) -apply blast -by (metis append_assoc) - -lemma star_intro1[rule_format]: "x \ lang\ \ \ y. y \ lang\ \ x @ y \ lang\" -by (erule Star.induct, auto) - -lemma star_intro2: "y \ lang \ y \ lang\" -by (drule step[of y lang "[]"], auto simp:start) - -lemma star_intro3[rule_format]: - "x \ lang\ \ \y . y \ lang \ x @ y \ lang\" -by (erule Star.induct, auto intro:star_intro2) - -lemma star_decom: - "\x \ lang\; x \ []\ \(\ a b. x = a @ b \ a \ [] \ a \ lang \ b \ lang\)" -by (induct x rule: Star.induct, simp, blast) - -lemma star_decom': - "\x \ lang\; x \ []\ \ \a b. x = a @ b \ a \ lang\ \ b \ lang" -apply (induct x rule:Star.induct, simp) -apply (case_tac "s2 = []") -apply (rule_tac x = "[]" in exI, rule_tac x = s1 in exI, simp add:start) -apply (simp, (erule exE| erule conjE)+) -by (rule_tac x = "s1 @ a" in exI, rule_tac x = b in exI, simp add:step) - -text {* Ardens lemma expressed at the level of language, rather than the level of regular expression. *} - -theorem ardens_revised: - assumes nemp: "[] \ A" - shows "(X = X ;; A \ B) \ (X = B ;; A\)" -proof - assume eq: "X = B ;; A\" - have "A\ = {[]} \ A\ ;; A" - by (auto simp:Seq_def star_intro3 star_decom') - then have "B ;; A\ = B ;; ({[]} \ A\ ;; A)" - unfolding Seq_def by simp - also have "\ = B \ B ;; (A\ ;; A)" - unfolding Seq_def by auto - also have "\ = B \ (B ;; A\) ;; A" - by (simp only:seq_assoc) - finally show "X = X ;; A \ B" - using eq by blast -next - assume eq': "X = X ;; A \ B" - hence c1': "\ x. x \ B \ x \ X" - and c2': "\ x y. \x \ X; y \ A\ \ x @ y \ X" - using Seq_def by auto - show "X = B ;; A\" - proof - show "B ;; A\ \ X" - proof- - { fix x y - have "\y \ A\; x \ X\ \ x @ y \ X " - apply (induct arbitrary:x rule:Star.induct, simp) - by (auto simp only:append_assoc[THEN sym] dest:c2') - } thus ?thesis using c1' by (auto simp:Seq_def) - qed - next - show "X \ B ;; A\" - proof- - { fix x - have "x \ X \ x \ B ;; A\" - proof (induct x taking:length rule:measure_induct) - fix z - assume hyps: - "\y. length y < length z \ y \ X \ y \ B ;; A\" - and z_in: "z \ X" - show "z \ B ;; A\" - proof (cases "z \ B") - case True thus ?thesis by (auto simp:Seq_def start) - next - case False hence "z \ X ;; A" using eq' z_in by auto - then obtain za zb where za_in: "za \ X" - and zab: "z = za @ zb \ zb \ A" and zbne: "zb \ []" - using nemp unfolding Seq_def by blast - from zbne zab have "length za < length z" by auto - with za_in hyps have "za \ B ;; A\" by blast - hence "za @ zb \ B ;; A\" using zab - by (clarsimp simp:Seq_def, blast dest:star_intro3) - thus ?thesis using zab by simp - qed - qed - } thus ?thesis by blast - qed - qed -qed - - -text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *} -datatype rexp = - NULL -| EMPTY -| CHAR char -| SEQ rexp rexp -| ALT rexp rexp -| STAR rexp - - -text {* - The following @{text "L"} is an overloaded operator, where @{text "L(x)"} evaluates to - the language represented by the syntactic object @{text "x"}. -*} -consts L:: "'a \ string set" - - -text {* - The @{text "L(rexp)"} for regular expression @{text "rexp"} is defined by the - following overloading function @{text "L_rexp"}. -*} -overloading L_rexp \ "L:: rexp \ string set" -begin -fun - L_rexp :: "rexp \ string set" -where - "L_rexp (NULL) = {}" - | "L_rexp (EMPTY) = {[]}" - | "L_rexp (CHAR c) = {[c]}" - | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)" - | "L_rexp (ALT r1 r2) = (L_rexp r1) \ (L_rexp r2)" - | "L_rexp (STAR r) = (L_rexp r)\" -end - -text {* - To obtain equational system out of finite set of equivalent classes, a fold operation - on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"} - more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"} - makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"}, - while @{text "fold f"} does not. -*} - -definition - folds :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b" -where - "folds f z S \ SOME x. fold_graph f z S x" - -text {* - The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"} - does not affect the @{text "L"}-value of the resultant regular expression. - *} -lemma folds_alt_simp [simp]: - "finite rs \ L (folds ALT NULL rs) = \ (L ` rs)" -apply (rule set_ext, simp add:folds_def) -apply (rule someI2_ex, erule finite_imp_fold_graph) -by (erule fold_graph.induct, auto) - -(* Just a technical lemma. *) -lemma [simp]: - shows "(x, y) \ {(x, y). P x y} \ P x y" -by simp - - -text {* - @{text "\L"} is an equivalent class defined by language @{text "Lang"}. -*} -definition - str_eq_rel ("\_") -where - "\Lang \ {(x, y). (\z. x @ z \ Lang \ y @ z \ Lang)}" - -text {* - Among equivlant clases of @{text "\Lang"}, the set @{text "finals(Lang)"} singles out - those which contains strings from @{text "Lang"}. -*} - -definition - "finals Lang \ {\Lang `` {x} | x . x \ Lang}" - -text {* - The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}. -*} -lemma lang_is_union_of_finals: - "Lang = \ finals(Lang)" -proof - show "Lang \ \ (finals Lang)" - proof - fix x - assume "x \ Lang" - thus "x \ \ (finals Lang)" - apply (simp add:finals_def, rule_tac x = "(\Lang) `` {x}" in exI) - by (auto simp:Image_def str_eq_rel_def) - qed -next - show "\ (finals Lang) \ Lang" - apply (clarsimp simp:finals_def str_eq_rel_def) - by (drule_tac x = "[]" in spec, auto) -qed - -section {* Direction @{text "finite partition \ regular language"}*} - -text {* - The relationship between equivalent classes can be described by an - equational system. - For example, in equational system \eqref{example_eqns}, $X_0, X_1$ are equivalent - classes. The first equation says every string in $X_0$ is obtained either by - appending one $b$ to a string in $X_0$ or by appending one $a$ to a string in - $X_1$ or just be an empty string (represented by the regular expression $\lambda$). Similary, - the second equation tells how the strings inside $X_1$ are composed. - \begin{equation}\label{example_eqns} - \begin{aligned} - X_0 & = X_0 b + X_1 a + \lambda \\ - X_1 & = X_0 a + X_1 b - \end{aligned} - \end{equation} - The summands on the right hand side is represented by the following data type - @{text "rhs_item"}, mnemonic for 'right hand side item'. - Generally, there are two kinds of right hand side items, one kind corresponds to - pure regular expressions, like the $\lambda$ in \eqref{example_eqns}, the other kind corresponds to - transitions from one one equivalent class to another, like the $X_0 b, X_1 a$ etc. - *} - -datatype rhs_item = - Lam "rexp" (* Lambda *) - | Trn "(string set)" "rexp" (* Transition *) - -text {* - In this formalization, pure regular expressions like $\lambda$ is - repsented by @{text "Lam(EMPTY)"}, while transitions like $X_0 a$ is represented by $Trn~X_0~(CHAR~a)$. - *} - -text {* - The functions @{text "the_r"} and @{text "the_Trn"} are used to extract - subcomponents from right hand side items. - *} - -fun the_r :: "rhs_item \ rexp" -where "the_r (Lam r) = r" - -fun the_Trn:: "rhs_item \ (string set \ rexp)" -where "the_Trn (Trn Y r) = (Y, r)" - -text {* - Every right hand side item @{text "itm"} defines a string set given - @{text "L(itm)"}, defined as: -*} -overloading L_rhs_e \ "L:: rhs_item \ string set" -begin - fun L_rhs_e:: "rhs_item \ string set" - where - "L_rhs_e (Lam r) = L r" | - "L_rhs_e (Trn X r) = X ;; L r" -end - -text {* - The right hand side of every equation is represented by a set of - items. The string set defined by such a set @{text "itms"} is given - by @{text "L(itms)"}, defined as: -*} - -overloading L_rhs \ "L:: rhs_item set \ string set" -begin - fun L_rhs:: "rhs_item set \ string set" - where "L_rhs rhs = \ (L ` rhs)" -end - -text {* - Given a set of equivalent classses @{text "CS"} and one equivalent class @{text "X"} among - @{text "CS"}, the term @{text "init_rhs CS X"} is used to extract the right hand side of - the equation describing the formation of @{text "X"}. The definition of @{text "init_rhs"} - is: - *} - -definition - "init_rhs CS X \ - if ([] \ X) then - {Lam(EMPTY)} \ {Trn Y (CHAR c) | Y c. Y \ CS \ Y ;; {[c]} \ X} - else - {Trn Y (CHAR c)| Y c. Y \ CS \ Y ;; {[c]} \ X}" - -text {* - In the definition of @{text "init_rhs"}, the term - @{text "{Trn Y (CHAR c)| Y c. Y \ CS \ Y ;; {[c]} \ X}"} appearing on both branches - describes the formation of strings in @{text "X"} out of transitions, while - the term @{text "{Lam(EMPTY)}"} describes the empty string which is intrinsically contained in - @{text "X"} rather than by transition. This @{text "{Lam(EMPTY)}"} corresponds to - the $\lambda$ in \eqref{example_eqns}. - - With the help of @{text "init_rhs"}, the equitional system descrbing the formation of every - equivalent class inside @{text "CS"} is given by the following @{text "eqs(CS)"}. - *} - -definition "eqs CS \ {(X, init_rhs CS X) | X. X \ CS}" -(************ arden's lemma variation ********************) - -text {* - The following @{text "items_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}. - *} -definition - "items_of rhs X \ {Trn X r | r. (Trn X r) \ rhs}" - -text {* - The following @{text "rexp_of rhs X"} combines all regular expressions in @{text "X"}-items - using @{text "ALT"} to form a single regular expression. - It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}. - *} - -definition - "rexp_of rhs X \ folds ALT NULL ((snd o the_Trn) ` items_of rhs X)" - -text {* - The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}. - *} - -definition - "lam_of rhs \ {Lam r | r. Lam r \ rhs}" - -text {* - The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"} - using @{text "ALT"} to form a single regular expression. - When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"} - is used to compute compute the regular expression corresponds to @{text "rhs"}. - *} - -definition - "rexp_of_lam rhs \ folds ALT NULL (the_r ` lam_of rhs)" - -text {* - The following @{text "attach_rexp rexp' itm"} attach - the regular expression @{text "rexp'"} to - the right of right hand side item @{text "itm"}. - *} - -fun attach_rexp :: "rexp \ rhs_item \ rhs_item" -where - "attach_rexp rexp' (Lam rexp) = Lam (SEQ rexp rexp')" -| "attach_rexp rexp' (Trn X rexp) = Trn X (SEQ rexp rexp')" - -text {* - The following @{text "append_rhs_rexp rhs rexp"} attaches - @{text "rexp"} to every item in @{text "rhs"}. - *} - -definition - "append_rhs_rexp rhs rexp \ (attach_rexp rexp) ` rhs" - -text {* - With the help of the two functions immediately above, Ardens' - transformation on right hand side @{text "rhs"} is implemented - by the following function @{text "arden_variate X rhs"}. - After this transformation, the recursive occurent of @{text "X"} - in @{text "rhs"} will be eliminated, while the - string set defined by @{text "rhs"} is kept unchanged. - *} -definition - "arden_variate X rhs \ - append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))" - - -(*********** substitution of ES *************) - -text {* - Suppose the equation defining @{text "X"} is $X = xrhs$, - the purpose of @{text "rhs_subst"} is to substitute all occurences of @{text "X"} in - @{text "rhs"} by @{text "xrhs"}. - A litte thought may reveal that the final result - should be: first append $(a_1 | a_2 | \ldots | a_n)$ to every item of @{text "xrhs"} and then - union the result with all non-@{text "X"}-items of @{text "rhs"}. - *} -definition - "rhs_subst rhs X xrhs \ - (rhs - (items_of rhs X)) \ (append_rhs_rexp xrhs (rexp_of rhs X))" - -text {* - Suppose the equation defining @{text "X"} is $X = xrhs$, the follwing - @{text "eqs_subst ES X xrhs"} substitute @{text "xrhs"} into every equation - of the equational system @{text "ES"}. - *} - -definition - "eqs_subst ES X xrhs \ {(Y, rhs_subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \ ES}" - -text {* - The computation of regular expressions for equivalent classes is accomplished - using a iteration principle given by the following lemma. - *} - -lemma wf_iter [rule_format]: - fixes f - assumes step: "\ e. \P e; \ Q e\ \ (\ e'. P e' \ (f(e'), f(e)) \ less_than)" - shows pe: "P e \ (\ e'. P e' \ Q e')" -proof(induct e rule: wf_induct - [OF wf_inv_image[OF wf_less_than, where f = "f"]], clarify) - fix x - assume h [rule_format]: - "\y. (y, x) \ inv_image less_than f \ P y \ (\e'. P e' \ Q e')" - and px: "P x" - show "\e'. P e' \ Q e'" - proof(cases "Q x") - assume "Q x" with px show ?thesis by blast - next - assume nq: "\ Q x" - from step [OF px nq] - obtain e' where pe': "P e'" and ltf: "(f e', f x) \ less_than" by auto - show ?thesis - proof(rule h) - from ltf show "(e', x) \ inv_image less_than f" - by (simp add:inv_image_def) - next - from pe' show "P e'" . - qed - qed -qed - -text {* - The @{text "P"} in lemma @{text "wf_iter"} is an invaiant kept throughout the iteration procedure. - The particular invariant used to solve our problem is defined by function @{text "Inv(ES)"}, - an invariant over equal system @{text "ES"}. - Every definition starting next till @{text "Inv"} stipulates a property to be satisfied by @{text "ES"}. -*} - -text {* - Every variable is defined at most onece in @{text "ES"}. - *} -definition - "distinct_equas ES \ - \ X rhs rhs'. (X, rhs) \ ES \ (X, rhs') \ ES \ rhs = rhs'" -text {* - Every equation in @{text "ES"} (represented by @{text "(X, rhs)"}) is valid, i.e. @{text "(X = L rhs)"}. - *} -definition - "valid_eqns ES \ \ X rhs. (X, rhs) \ ES \ (X = L rhs)" - -text {* - @{text "rhs_nonempty rhs"} requires regular expressions occuring in transitional - items of @{text "rhs"} does not contain empty string. This is necessary for - the application of Arden's transformation to @{text "rhs"}. - *} -definition - "rhs_nonempty rhs \ (\ Y r. Trn Y r \ rhs \ [] \ L r)" - -text {* - @{text "ardenable ES"} requires that Arden's transformation is applicable - to every equation of equational system @{text "ES"}. - *} -definition - "ardenable ES \ \ X rhs. (X, rhs) \ ES \ rhs_nonempty rhs" - -(* The following non_empty seems useless. *) -definition - "non_empty ES \ \ X rhs. (X, rhs) \ ES \ X \ {}" - -text {* - The following @{text "finite_rhs ES"} requires every equation in @{text "rhs"} be finite. - *} -definition - "finite_rhs ES \ \ X rhs. (X, rhs) \ ES \ finite rhs" - -text {* - The following @{text "classes_of rhs"} returns all variables (or equivalent classes) - occuring in @{text "rhs"}. - *} -definition - "classes_of rhs \ {X. \ r. Trn X r \ rhs}" - -text {* - The following @{text "lefts_of ES"} returns all variables - defined by equational system @{text "ES"}. - *} -definition - "lefts_of ES \ {Y | Y yrhs. (Y, yrhs) \ ES}" - -text {* - The following @{text "self_contained ES"} requires that every - variable occuring on the right hand side of equations is already defined by some - equation in @{text "ES"}. - *} -definition - "self_contained ES \ \ (X, xrhs) \ ES. classes_of xrhs \ lefts_of ES" - - -text {* - The invariant @{text "Inv(ES)"} is obtained by conjunctioning all the previous - defined constaints on @{text "ES"}. - *} -definition - "Inv ES \ valid_eqns ES \ finite ES \ distinct_equas ES \ ardenable ES \ - non_empty ES \ finite_rhs ES \ self_contained ES" - -subsection {* Proof for this direction *} - - - -text {* - The following are some basic properties of the above definitions. -*} - -lemma L_rhs_union_distrib: - " L (A::rhs_item set) \ L B = L (A \ B)" -by simp - -lemma finite_snd_Trn: - assumes finite:"finite rhs" - shows "finite {r\<^isub>2. Trn Y r\<^isub>2 \ rhs}" (is "finite ?B") -proof- - def rhs' \ "{e \ rhs. \ r. e = Trn Y r}" - have "?B = (snd o the_Trn) ` rhs'" using rhs'_def by (auto simp:image_def) - moreover have "finite rhs'" using finite rhs'_def by auto - ultimately show ?thesis by simp -qed - -lemma rexp_of_empty: - assumes finite:"finite rhs" - and nonempty:"rhs_nonempty rhs" - shows "[] \ L (rexp_of rhs X)" -using finite nonempty rhs_nonempty_def -by (drule_tac finite_snd_Trn[where Y = X], auto simp:rexp_of_def items_of_def) - -lemma [intro!]: - "P (Trn X r) \ (\a. (\r. a = Trn X r \ P a))" by auto - -lemma finite_items_of: - "finite rhs \ finite (items_of rhs X)" -by (auto simp:items_of_def intro:finite_subset) - -lemma lang_of_rexp_of: - assumes finite:"finite rhs" - shows "L (items_of rhs X) = X ;; (L (rexp_of rhs X))" -proof - - have "finite ((snd \ the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto - thus ?thesis - apply (auto simp:rexp_of_def Seq_def items_of_def) - apply (rule_tac x = s1 in exI, rule_tac x = s2 in exI, auto) - by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def) -qed - -lemma rexp_of_lam_eq_lam_set: - assumes finite: "finite rhs" - shows "L (rexp_of_lam rhs) = L (lam_of rhs)" -proof - - have "finite (the_r ` {Lam r |r. Lam r \ rhs})" using finite - by (rule_tac finite_imageI, auto intro:finite_subset) - thus ?thesis by (auto simp:rexp_of_lam_def lam_of_def) -qed - -lemma [simp]: - " L (attach_rexp r xb) = L xb ;; L r" -apply (cases xb, auto simp:Seq_def) -by (rule_tac x = "s1 @ s1a" in exI, rule_tac x = s2a in exI,auto simp:Seq_def) - -lemma lang_of_append_rhs: - "L (append_rhs_rexp rhs r) = L rhs ;; L r" -apply (auto simp:append_rhs_rexp_def image_def) -apply (auto simp:Seq_def) -apply (rule_tac x = "L xb ;; L r" in exI, auto simp add:Seq_def) -by (rule_tac x = "attach_rexp r xb" in exI, auto simp:Seq_def) - -lemma classes_of_union_distrib: - "classes_of A \ classes_of B = classes_of (A \ B)" -by (auto simp add:classes_of_def) - -lemma lefts_of_union_distrib: - "lefts_of A \ lefts_of B = lefts_of (A \ B)" -by (auto simp:lefts_of_def) - - -text {* - The following several lemmas until @{text "init_ES_satisfy_Inv"} are - to prove that initial equational system satisfies invariant @{text "Inv"}. - *} - -lemma defined_by_str: - "\s \ X; X \ UNIV // (\Lang)\ \ X = (\Lang) `` {s}" -by (auto simp:quotient_def Image_def str_eq_rel_def) - -lemma every_eqclass_has_transition: - assumes has_str: "s @ [c] \ X" - and in_CS: "X \ UNIV // (\Lang)" - obtains Y where "Y \ UNIV // (\Lang)" and "Y ;; {[c]} \ X" and "s \ Y" -proof - - def Y \ "(\Lang) `` {s}" - have "Y \ UNIV // (\Lang)" - unfolding Y_def quotient_def by auto - moreover - have "X = (\Lang) `` {s @ [c]}" - using has_str in_CS defined_by_str by blast - then have "Y ;; {[c]} \ X" - unfolding Y_def Image_def Seq_def - unfolding str_eq_rel_def - by clarsimp - moreover - have "s \ Y" unfolding Y_def - unfolding Image_def str_eq_rel_def by simp - ultimately show thesis by (blast intro: that) -qed - -lemma l_eq_r_in_eqs: - assumes X_in_eqs: "(X, xrhs) \ (eqs (UNIV // (\Lang)))" - shows "X = L xrhs" -proof - show "X \ L xrhs" - proof - fix x - assume "(1)": "x \ X" - show "x \ L xrhs" - proof (cases "x = []") - assume empty: "x = []" - thus ?thesis using X_in_eqs "(1)" - by (auto simp:eqs_def init_rhs_def) - next - assume not_empty: "x \ []" - then obtain clist c where decom: "x = clist @ [c]" - by (case_tac x rule:rev_cases, auto) - have "X \ UNIV // (\Lang)" using X_in_eqs by (auto simp:eqs_def) - then obtain Y - where "Y \ UNIV // (\Lang)" - and "Y ;; {[c]} \ X" - and "clist \ Y" - using decom "(1)" every_eqclass_has_transition by blast - hence - "x \ L {Trn Y (CHAR c)| Y c. Y \ UNIV // (\Lang) \ Y ;; {[c]} \ X}" - using "(1)" decom - by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def) - thus ?thesis using X_in_eqs "(1)" - by (simp add:eqs_def init_rhs_def) - qed - qed -next - show "L xrhs \ X" using X_in_eqs - by (auto simp:eqs_def init_rhs_def) -qed - -lemma finite_init_rhs: - assumes finite: "finite CS" - shows "finite (init_rhs CS X)" -proof- - have "finite {Trn Y (CHAR c) |Y c. Y \ CS \ Y ;; {[c]} \ X}" (is "finite ?A") - proof - - def S \ "{(Y, c)| Y c. Y \ CS \ Y ;; {[c]} \ X}" - def h \ "\ (Y, c). Trn Y (CHAR c)" - have "finite (CS \ (UNIV::char set))" using finite by auto - hence "finite S" using S_def - by (rule_tac B = "CS \ UNIV" in finite_subset, auto) - moreover have "?A = h ` S" by (auto simp: S_def h_def image_def) - ultimately show ?thesis - by auto - qed - thus ?thesis by (simp add:init_rhs_def) -qed - -lemma init_ES_satisfy_Inv: - assumes finite_CS: "finite (UNIV // (\Lang))" - shows "Inv (eqs (UNIV // (\Lang)))" -proof - - have "finite (eqs (UNIV // (\Lang)))" using finite_CS - by (simp add:eqs_def) - moreover have "distinct_equas (eqs (UNIV // (\Lang)))" - by (simp add:distinct_equas_def eqs_def) - moreover have "ardenable (eqs (UNIV // (\Lang)))" - by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps) - moreover have "valid_eqns (eqs (UNIV // (\Lang)))" - using l_eq_r_in_eqs by (simp add:valid_eqns_def) - moreover have "non_empty (eqs (UNIV // (\Lang)))" - by (auto simp:non_empty_def eqs_def quotient_def Image_def str_eq_rel_def) - moreover have "finite_rhs (eqs (UNIV // (\Lang)))" - using finite_init_rhs[OF finite_CS] - by (auto simp:finite_rhs_def eqs_def) - moreover have "self_contained (eqs (UNIV // (\Lang)))" - by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def) - ultimately show ?thesis by (simp add:Inv_def) -qed - -text {* - From this point until @{text "iteration_step"}, we are trying to prove - that there exists iteration steps which keep @{text "Inv(ES)"} while - decreasing the size of @{text "ES"} with every iteration. - *} -lemma arden_variate_keeps_eq: - assumes l_eq_r: "X = L rhs" - and not_empty: "[] \ L (rexp_of rhs X)" - and finite: "finite rhs" - shows "X = L (arden_variate X rhs)" -proof - - def A \ "L (rexp_of rhs X)" - def b \ "rhs - items_of rhs X" - def B \ "L b" - have "X = B ;; A\" - proof- - have "rhs = items_of rhs X \ b" by (auto simp:b_def items_of_def) - hence "L rhs = L(items_of rhs X \ b)" by simp - hence "L rhs = L(items_of rhs X) \ B" by (simp only:L_rhs_union_distrib B_def) - with lang_of_rexp_of - have "L rhs = X ;; A \ B " using finite by (simp only:B_def b_def A_def) - thus ?thesis - using l_eq_r not_empty - apply (drule_tac B = B and X = X in ardens_revised) - by (auto simp:A_def simp del:L_rhs.simps) - qed - moreover have "L (arden_variate X rhs) = (B ;; A\)" (is "?L = ?R") - by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs - B_def A_def b_def L_rexp.simps seq_union_distrib) - ultimately show ?thesis by simp -qed - -lemma append_keeps_finite: - "finite rhs \ finite (append_rhs_rexp rhs r)" -by (auto simp:append_rhs_rexp_def) - -lemma arden_variate_keeps_finite: - "finite rhs \ finite (arden_variate X rhs)" -by (auto simp:arden_variate_def append_keeps_finite) - -lemma append_keeps_nonempty: - "rhs_nonempty rhs \ rhs_nonempty (append_rhs_rexp rhs r)" -apply (auto simp:rhs_nonempty_def append_rhs_rexp_def) -by (case_tac x, auto simp:Seq_def) - -lemma nonempty_set_sub: - "rhs_nonempty rhs \ rhs_nonempty (rhs - A)" -by (auto simp:rhs_nonempty_def) - -lemma nonempty_set_union: - "\rhs_nonempty rhs; rhs_nonempty rhs'\ \ rhs_nonempty (rhs \ rhs')" -by (auto simp:rhs_nonempty_def) - -lemma arden_variate_keeps_nonempty: - "rhs_nonempty rhs \ rhs_nonempty (arden_variate X rhs)" -by (simp only:arden_variate_def append_keeps_nonempty nonempty_set_sub) - - -lemma rhs_subst_keeps_nonempty: - "\rhs_nonempty rhs; rhs_nonempty xrhs\ \ rhs_nonempty (rhs_subst rhs X xrhs)" -by (simp only:rhs_subst_def append_keeps_nonempty nonempty_set_union nonempty_set_sub) - -lemma rhs_subst_keeps_eq: - assumes substor: "X = L xrhs" - and finite: "finite rhs" - shows "L (rhs_subst rhs X xrhs) = L rhs" (is "?Left = ?Right") -proof- - def A \ "L (rhs - items_of rhs X)" - have "?Left = A \ L (append_rhs_rexp xrhs (rexp_of rhs X))" - by (simp only:rhs_subst_def L_rhs_union_distrib A_def) - moreover have "?Right = A \ L (items_of rhs X)" - proof- - have "rhs = (rhs - items_of rhs X) \ (items_of rhs X)" by (auto simp:items_of_def) - thus ?thesis by (simp only:L_rhs_union_distrib A_def) - qed - moreover have "L (append_rhs_rexp xrhs (rexp_of rhs X)) = L (items_of rhs X)" - using finite substor by (simp only:lang_of_append_rhs lang_of_rexp_of) - ultimately show ?thesis by simp -qed - -lemma rhs_subst_keeps_finite_rhs: - "\finite rhs; finite yrhs\ \ finite (rhs_subst rhs Y yrhs)" -by (auto simp:rhs_subst_def append_keeps_finite) - -lemma eqs_subst_keeps_finite: - assumes finite:"finite (ES:: (string set \ rhs_item set) set)" - shows "finite (eqs_subst ES Y yrhs)" -proof - - have "finite {(Ya, rhs_subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \ ES}" - (is "finite ?A") - proof- - def eqns' \ "{((Ya::string set), yrhsa)| Ya yrhsa. (Ya, yrhsa) \ ES}" - def h \ "\ ((Ya::string set), yrhsa). (Ya, rhs_subst yrhsa Y yrhs)" - have "finite (h ` eqns')" using finite h_def eqns'_def by auto - moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def) - ultimately show ?thesis by auto - qed - thus ?thesis by (simp add:eqs_subst_def) -qed - -lemma eqs_subst_keeps_finite_rhs: - "\finite_rhs ES; finite yrhs\ \ finite_rhs (eqs_subst ES Y yrhs)" -by (auto intro:rhs_subst_keeps_finite_rhs simp add:eqs_subst_def finite_rhs_def) - -lemma append_rhs_keeps_cls: - "classes_of (append_rhs_rexp rhs r) = classes_of rhs" -apply (auto simp:classes_of_def append_rhs_rexp_def) -apply (case_tac xa, auto simp:image_def) -by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+) - -lemma arden_variate_removes_cl: - "classes_of (arden_variate Y yrhs) = classes_of yrhs - {Y}" -apply (simp add:arden_variate_def append_rhs_keeps_cls items_of_def) -by (auto simp:classes_of_def) - -lemma lefts_of_keeps_cls: - "lefts_of (eqs_subst ES Y yrhs) = lefts_of ES" -by (auto simp:lefts_of_def eqs_subst_def) - -lemma rhs_subst_updates_cls: - "X \ classes_of xrhs \ - classes_of (rhs_subst rhs X xrhs) = classes_of rhs \ classes_of xrhs - {X}" -apply (simp only:rhs_subst_def append_rhs_keeps_cls - classes_of_union_distrib[THEN sym]) -by (auto simp:classes_of_def items_of_def) - -lemma eqs_subst_keeps_self_contained: - fixes Y - assumes sc: "self_contained (ES \ {(Y, yrhs)})" (is "self_contained ?A") - shows "self_contained (eqs_subst ES Y (arden_variate Y yrhs))" - (is "self_contained ?B") -proof- - { fix X xrhs' - assume "(X, xrhs') \ ?B" - then obtain xrhs - where xrhs_xrhs': "xrhs' = rhs_subst xrhs Y (arden_variate Y yrhs)" - and X_in: "(X, xrhs) \ ES" by (simp add:eqs_subst_def, blast) - have "classes_of xrhs' \ lefts_of ?B" - proof- - have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def eqs_subst_def) - moreover have "classes_of xrhs' \ lefts_of ES" - proof- - have "classes_of xrhs' \ - classes_of xrhs \ classes_of (arden_variate Y yrhs) - {Y}" - proof- - have "Y \ classes_of (arden_variate Y yrhs)" - using arden_variate_removes_cl by simp - thus ?thesis using xrhs_xrhs' by (auto simp:rhs_subst_updates_cls) - qed - moreover have "classes_of xrhs \ lefts_of ES \ {Y}" using X_in sc - apply (simp only:self_contained_def lefts_of_union_distrib[THEN sym]) - by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def) - moreover have "classes_of (arden_variate Y yrhs) \ lefts_of ES \ {Y}" - using sc - by (auto simp add:arden_variate_removes_cl self_contained_def lefts_of_def) - ultimately show ?thesis by auto - qed - ultimately show ?thesis by simp - qed - } thus ?thesis by (auto simp only:eqs_subst_def self_contained_def) -qed - -lemma eqs_subst_satisfy_Inv: - assumes Inv_ES: "Inv (ES \ {(Y, yrhs)})" - shows "Inv (eqs_subst ES Y (arden_variate Y yrhs))" -proof - - have finite_yrhs: "finite yrhs" - using Inv_ES by (auto simp:Inv_def finite_rhs_def) - have nonempty_yrhs: "rhs_nonempty yrhs" - using Inv_ES by (auto simp:Inv_def ardenable_def) - have Y_eq_yrhs: "Y = L yrhs" - using Inv_ES by (simp only:Inv_def valid_eqns_def, blast) - have "distinct_equas (eqs_subst ES Y (arden_variate Y yrhs))" - using Inv_ES - by (auto simp:distinct_equas_def eqs_subst_def Inv_def) - moreover have "finite (eqs_subst ES Y (arden_variate Y yrhs))" - using Inv_ES by (simp add:Inv_def eqs_subst_keeps_finite) - moreover have "finite_rhs (eqs_subst ES Y (arden_variate Y yrhs))" - proof- - have "finite_rhs ES" using Inv_ES - by (simp add:Inv_def finite_rhs_def) - moreover have "finite (arden_variate Y yrhs)" - proof - - have "finite yrhs" using Inv_ES - by (auto simp:Inv_def finite_rhs_def) - thus ?thesis using arden_variate_keeps_finite by simp - qed - ultimately show ?thesis - by (simp add:eqs_subst_keeps_finite_rhs) - qed - moreover have "ardenable (eqs_subst ES Y (arden_variate Y yrhs))" - proof - - { fix X rhs - assume "(X, rhs) \ ES" - hence "rhs_nonempty rhs" using prems Inv_ES - by (simp add:Inv_def ardenable_def) - with nonempty_yrhs - have "rhs_nonempty (rhs_subst rhs Y (arden_variate Y yrhs))" - by (simp add:nonempty_yrhs - rhs_subst_keeps_nonempty arden_variate_keeps_nonempty) - } thus ?thesis by (auto simp add:ardenable_def eqs_subst_def) - qed - moreover have "valid_eqns (eqs_subst ES Y (arden_variate Y yrhs))" - proof- - have "Y = L (arden_variate Y yrhs)" - using Y_eq_yrhs Inv_ES finite_yrhs nonempty_yrhs - by (rule_tac arden_variate_keeps_eq, (simp add:rexp_of_empty)+) - thus ?thesis using Inv_ES - by (clarsimp simp add:valid_eqns_def - eqs_subst_def rhs_subst_keeps_eq Inv_def finite_rhs_def - simp del:L_rhs.simps) - qed - moreover have - non_empty_subst: "non_empty (eqs_subst ES Y (arden_variate Y yrhs))" - using Inv_ES by (auto simp:Inv_def non_empty_def eqs_subst_def) - moreover - have self_subst: "self_contained (eqs_subst ES Y (arden_variate Y yrhs))" - using Inv_ES eqs_subst_keeps_self_contained by (simp add:Inv_def) - ultimately show ?thesis using Inv_ES by (simp add:Inv_def) -qed - -lemma eqs_subst_card_le: - assumes finite: "finite (ES::(string set \ rhs_item set) set)" - shows "card (eqs_subst ES Y yrhs) <= card ES" -proof- - def f \ "\ x. ((fst x)::string set, rhs_subst (snd x) Y yrhs)" - have "eqs_subst ES Y yrhs = f ` ES" - apply (auto simp:eqs_subst_def f_def image_def) - by (rule_tac x = "(Ya, yrhsa)" in bexI, simp+) - thus ?thesis using finite by (auto intro:card_image_le) -qed - -lemma eqs_subst_cls_remains: - "(X, xrhs) \ ES \ \ xrhs'. (X, xrhs') \ (eqs_subst ES Y yrhs)" -by (auto simp:eqs_subst_def) - -lemma card_noteq_1_has_more: - assumes card:"card S \ 1" - and e_in: "e \ S" - and finite: "finite S" - obtains e' where "e' \ S \ e \ e'" -proof- - have "card (S - {e}) > 0" - proof - - have "card S > 1" using card e_in finite - by (case_tac "card S", auto) - thus ?thesis using finite e_in by auto - qed - hence "S - {e} \ {}" using finite by (rule_tac notI, simp) - thus "(\e'. e' \ S \ e \ e' \ thesis) \ thesis" by auto -qed - -lemma iteration_step: - assumes Inv_ES: "Inv ES" - and X_in_ES: "(X, xrhs) \ ES" - and not_T: "card ES \ 1" - shows "\ ES'. (Inv ES' \ (\ xrhs'.(X, xrhs') \ ES')) \ - (card ES', card ES) \ less_than" (is "\ ES'. ?P ES'") -proof - - have finite_ES: "finite ES" using Inv_ES by (simp add:Inv_def) - then obtain Y yrhs - where Y_in_ES: "(Y, yrhs) \ ES" and not_eq: "(X, xrhs) \ (Y, yrhs)" - using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto) - def ES' == "ES - {(Y, yrhs)}" - let ?ES'' = "eqs_subst ES' Y (arden_variate Y yrhs)" - have "?P ?ES''" - proof - - have "Inv ?ES''" using Y_in_ES Inv_ES - by (rule_tac eqs_subst_satisfy_Inv, simp add:ES'_def insert_absorb) - moreover have "\xrhs'. (X, xrhs') \ ?ES''" using not_eq X_in_ES - by (rule_tac ES = ES' in eqs_subst_cls_remains, auto simp add:ES'_def) - moreover have "(card ?ES'', card ES) \ less_than" - proof - - have "finite ES'" using finite_ES ES'_def by auto - moreover have "card ES' < card ES" using finite_ES Y_in_ES - by (auto simp:ES'_def card_gt_0_iff intro:diff_Suc_less) - ultimately show ?thesis - by (auto dest:eqs_subst_card_le elim:le_less_trans) - qed - ultimately show ?thesis by simp - qed - thus ?thesis by blast -qed - -text {* - From this point until @{text "hard_direction"}, the hard direction is proved - through a simple application of the iteration principle. -*} - -lemma iteration_conc: - assumes history: "Inv ES" - and X_in_ES: "\ xrhs. (X, xrhs) \ ES" - shows - "\ ES'. (Inv ES' \ (\ xrhs'. (X, xrhs') \ ES')) \ card ES' = 1" - (is "\ ES'. ?P ES'") -proof (cases "card ES = 1") - case True - thus ?thesis using history X_in_ES - by blast -next - case False - thus ?thesis using history iteration_step X_in_ES - by (rule_tac f = card in wf_iter, auto) -qed - -lemma last_cl_exists_rexp: - assumes ES_single: "ES = {(X, xrhs)}" - and Inv_ES: "Inv ES" - shows "\ (r::rexp). L r = X" (is "\ r. ?P r") -proof- - let ?A = "arden_variate X xrhs" - have "?P (rexp_of_lam ?A)" - proof - - have "L (rexp_of_lam ?A) = L (lam_of ?A)" - proof(rule rexp_of_lam_eq_lam_set) - show "finite (arden_variate X xrhs)" using Inv_ES ES_single - by (rule_tac arden_variate_keeps_finite, - auto simp add:Inv_def finite_rhs_def) - qed - also have "\ = L ?A" - proof- - have "lam_of ?A = ?A" - proof- - have "classes_of ?A = {}" using Inv_ES ES_single - by (simp add:arden_variate_removes_cl - self_contained_def Inv_def lefts_of_def) - thus ?thesis - by (auto simp only:lam_of_def classes_of_def, case_tac x, auto) - qed - thus ?thesis by simp - qed - also have "\ = X" - proof(rule arden_variate_keeps_eq [THEN sym]) - show "X = L xrhs" using Inv_ES ES_single - by (auto simp only:Inv_def valid_eqns_def) - next - from Inv_ES ES_single show "[] \ L (rexp_of xrhs X)" - by(simp add:Inv_def ardenable_def rexp_of_empty finite_rhs_def) - next - from Inv_ES ES_single show "finite xrhs" - by (simp add:Inv_def finite_rhs_def) - qed - finally show ?thesis by simp - qed - thus ?thesis by auto -qed - -lemma every_eqcl_has_reg: - assumes finite_CS: "finite (UNIV // (\Lang))" - and X_in_CS: "X \ (UNIV // (\Lang))" - shows "\ (reg::rexp). L reg = X" (is "\ r. ?E r") -proof - - from X_in_CS have "\ xrhs. (X, xrhs) \ (eqs (UNIV // (\Lang)))" - by (auto simp:eqs_def init_rhs_def) - then obtain ES xrhs where Inv_ES: "Inv ES" - and X_in_ES: "(X, xrhs) \ ES" - and card_ES: "card ES = 1" - using finite_CS X_in_CS init_ES_satisfy_Inv iteration_conc - by blast - hence ES_single_equa: "ES = {(X, xrhs)}" - by (auto simp:Inv_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) - thus ?thesis using Inv_ES - by (rule last_cl_exists_rexp) -qed - -lemma finals_in_partitions: - "finals Lang \ (UNIV // (\Lang))" - by (auto simp:finals_def quotient_def) - -theorem hard_direction: - assumes finite_CS: "finite (UNIV // (\Lang))" - shows "\ (reg::rexp). Lang = L reg" -proof - - have "\ X \ (UNIV // (\Lang)). \ (reg::rexp). X = L reg" - using finite_CS every_eqcl_has_reg by blast - then obtain f - where f_prop: "\ X \ (UNIV // (\Lang)). X = L ((f X)::rexp)" - by (auto dest:bchoice) - def rs \ "f ` (finals Lang)" - have "Lang = \ (finals Lang)" using lang_is_union_of_finals by auto - also have "\ = L (folds ALT NULL rs)" - proof - - have "finite rs" - proof - - have "finite (finals Lang)" - using finite_CS finals_in_partitions[of "Lang"] - by (erule_tac finite_subset, simp) - thus ?thesis using rs_def by auto - qed - thus ?thesis - using f_prop rs_def finals_in_partitions[of "Lang"] by auto - qed - finally show ?thesis by blast -qed - -section {* Direction: @{text "regular language \finite partition"} *} - -subsection {* The scheme for this direction *} - -text {* - The following convenient notation @{text "x \Lang y"} means: - string @{text "x"} and @{text "y"} are equivalent with respect to - language @{text "Lang"}. - *} - -definition - str_eq ("_ \_ _") -where - "x \Lang y \ (x, y) \ (\Lang)" - -text {* - The very basic scheme to show the finiteness of the partion generated by a language @{text "Lang"} - is by attaching tags to every string. The set of tags are carfully choosen to make it finite. - If it can be proved that strings with the same tag are equivlent with respect @{text "Lang"}, - then the partition given rise by @{text "Lang"} must be finite. The reason for this is a lemma - in standard library (@{text "finite_imageD"}), which says: if the image of an injective - function on a set @{text "A"} is finite, then @{text "A"} is finite. It can be shown that - the function obtained by llifting @{text "tag"} - to the level of equalent classes (i.e. @{text "((op `) tag)"}) is injective - (by lemma @{text "tag_image_injI"}) and the image of this function is finite - (with the help of lemma @{text "finite_tag_imageI"}). - - BUT, I think this argument can be encapsulated by one lemma instead of the current presentation. - *} - -lemma eq_class_equalI: - "\X \ UNIV // \lang; Y \ UNIV // \lang; x \ X; y \ Y; x \lang y\ - \ X = Y" -by (auto simp:quotient_def str_eq_rel_def str_eq_def) - -lemma tag_image_injI: - assumes str_inj: "\ x y. tag x = tag (y::string) \ x \lang y" - shows "inj_on ((op `) tag) (UNIV // \lang)" -proof- - { fix X Y - assume X_in: "X \ UNIV // \lang" - and Y_in: "Y \ UNIV // \lang" - and tag_eq: "tag ` X = tag ` Y" - then obtain x y where "x \ X" and "y \ Y" and "tag x = tag y" - unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def - apply simp by blast - with X_in Y_in str_inj - have "X = Y" by (rule_tac eq_class_equalI, simp+) - } - thus ?thesis unfolding inj_on_def by auto -qed - -lemma finite_tag_imageI: - "finite (range tag) \ finite (((op `) tag) ` S)" -apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset) -by (auto simp add:image_def Pow_def) - - -subsection {* A small theory for list difference *} - -text {* - The notion of list diffrence is need to make proofs more readable. - *} - -(* list_diff:: list substract, once different return tailer *) -fun list_diff :: "'a list \ 'a list \ 'a list" (infix "-" 51) -where - "list_diff [] xs = []" | - "list_diff (x#xs) [] = x#xs" | - "list_diff (x#xs) (y#ys) = (if x = y then list_diff xs ys else (x#xs))" - -lemma [simp]: "(x @ y) - x = y" -apply (induct x) -by (case_tac y, simp+) - -lemma [simp]: "x - x = []" -by (induct x, auto) - -lemma [simp]: "x = xa @ y \ x - xa = y " -by (induct x, auto) - -lemma [simp]: "x - [] = x" -by (induct x, auto) - -lemma [simp]: "(x - y = []) \ (x \ y)" -proof- - have "\xa. x = xa @ (x - y) \ xa \ y" - apply (rule list_diff.induct[of _ x y], simp+) - by (clarsimp, rule_tac x = "y # xa" in exI, simp+) - thus "(x - y = []) \ (x \ y)" by simp -qed - -lemma diff_prefix: - "\c \ a - b; b \ a\ \ b @ c \ a" -by (auto elim:prefixE) - -lemma diff_diff_appd: - "\c < a - b; b < a\ \ (a - b) - c = a - (b @ c)" -apply (clarsimp simp:strict_prefix_def) -by (drule diff_prefix, auto elim:prefixE) - -lemma app_eq_cases[rule_format]: - "\ x . x @ y = m @ n \ (x \ m \ m \ x)" -apply (induct y, simp) -apply (clarify, drule_tac x = "x @ [a]" in spec) -by (clarsimp, auto simp:prefix_def) - -lemma app_eq_dest: - "x @ y = m @ n \ - (x \ m \ (m - x) @ n = y) \ (m \ x \ (x - m) @ y = n)" -by (frule_tac app_eq_cases, auto elim:prefixE) - -subsection {* Lemmas for basic cases *} - -text {* - The the final result of this direction is in @{text "easier_direction"}, which - is an induction on the structure of regular expressions. There is one case - for each regular expression operator. For basic operators such as @{text "NULL, EMPTY, CHAR c"}, - the finiteness of their language partition can be established directly with no need - of taggiing. This section contains several technical lemma for these base cases. - - The inductive cases involve operators @{text "ALT, SEQ"} and @{text "STAR"}. - Tagging functions need to be defined individually for each of them. There will be one - dedicated section for each of these cases, and each section goes virtually the same way: - gives definition of the tagging function and prove that strings - with the same tag are equivalent. - *} - -lemma quot_empty_subset: - "UNIV // (\{[]}) \ {{[]}, UNIV - {[]}}" -proof - fix x - assume "x \ UNIV // \{[]}" - then obtain y where h: "x = {z. (y, z) \ \{[]}}" - unfolding quotient_def Image_def by blast - show "x \ {{[]}, UNIV - {[]}}" - proof (cases "y = []") - case True with h - have "x = {[]}" by (auto simp:str_eq_rel_def) - thus ?thesis by simp - next - case False with h - have "x = UNIV - {[]}" by (auto simp:str_eq_rel_def) - thus ?thesis by simp - qed -qed - -lemma quot_char_subset: - "UNIV // (\{[c]}) \ {{[]},{[c]}, UNIV - {[], [c]}}" -proof - fix x - assume "x \ UNIV // \{[c]}" - then obtain y where h: "x = {z. (y, z) \ \{[c]}}" - unfolding quotient_def Image_def by blast - show "x \ {{[]},{[c]}, UNIV - {[], [c]}}" - proof - - { assume "y = []" hence "x = {[]}" using h - by (auto simp:str_eq_rel_def) - } moreover { - assume "y = [c]" hence "x = {[c]}" using h - by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_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) - } ultimately show ?thesis by blast - qed -qed - -subsection {* The case for @{text "SEQ"}*} - -definition - "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \ - ((\L\<^isub>1) `` {x}, {(\L\<^isub>2) `` {x - xa}| xa. xa \ x \ xa \ L\<^isub>1})" - -lemma tag_str_seq_range_finite: - "\finite (UNIV // \L\<^isub>1); finite (UNIV // \L\<^isub>2)\ - \ finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))" -apply (rule_tac B = "(UNIV // \L\<^isub>1) \ (Pow (UNIV // \L\<^isub>2))" in finite_subset) -by (auto simp:tag_str_SEQ_def Image_def quotient_def split:if_splits) - -lemma append_seq_elim: - assumes "x @ y \ L\<^isub>1 ;; L\<^isub>2" - shows "(\ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ y \ L\<^isub>2) \ - (\ ya \ y. (x @ ya) \ L\<^isub>1 \ (y - ya) \ L\<^isub>2)" -proof- - from assms obtain s\<^isub>1 s\<^isub>2 - where "x @ y = s\<^isub>1 @ s\<^isub>2" - and in_seq: "s\<^isub>1 \ L\<^isub>1 \ s\<^isub>2 \ L\<^isub>2" - by (auto simp:Seq_def) - hence "(x \ s\<^isub>1 \ (s\<^isub>1 - x) @ s\<^isub>2 = y) \ (s\<^isub>1 \ x \ (x - s\<^isub>1) @ y = s\<^isub>2)" - using app_eq_dest by auto - moreover have "\x \ s\<^isub>1; (s\<^isub>1 - x) @ s\<^isub>2 = y\ \ - \ ya \ y. (x @ ya) \ L\<^isub>1 \ (y - ya) \ L\<^isub>2" - using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE) - moreover have "\s\<^isub>1 \ x; (x - s\<^isub>1) @ y = s\<^isub>2\ \ - \ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ y \ L\<^isub>2" - using in_seq by (rule_tac x = s\<^isub>1 in exI, auto) - ultimately show ?thesis by blast -qed - -lemma tag_str_SEQ_injI: - "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \ m \(L\<^isub>1 ;; L\<^isub>2) n" -proof- - { fix x y z - assume xz_in_seq: "x @ z \ L\<^isub>1 ;; L\<^isub>2" - and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y" - have"y @ z \ L\<^isub>1 ;; L\<^isub>2" - proof- - have "(\ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ z \ L\<^isub>2) \ - (\ za \ z. (x @ za) \ L\<^isub>1 \ (z - za) \ L\<^isub>2)" - using xz_in_seq append_seq_elim by simp - moreover { - fix xa - assume h1: "xa \ x" and h2: "xa \ L\<^isub>1" and h3: "(x - xa) @ z \ L\<^isub>2" - obtain ya where "ya \ y" and "ya \ L\<^isub>1" and "(y - ya) @ z \ L\<^isub>2" - proof - - have "\ ya. ya \ y \ ya \ L\<^isub>1 \ (x - xa) \L\<^isub>2 (y - ya)" - proof - - have "{\L\<^isub>2 `` {x - xa} |xa. xa \ x \ xa \ L\<^isub>1} = - {\L\<^isub>2 `` {y - xa} |xa. xa \ y \ xa \ L\<^isub>1}" - (is "?Left = ?Right") - using h1 tag_xy by (auto simp:tag_str_SEQ_def) - moreover have "\L\<^isub>2 `` {x - xa} \ ?Left" using h1 h2 by auto - ultimately have "\L\<^isub>2 `` {x - xa} \ ?Right" by simp - thus ?thesis by (auto simp:Image_def str_eq_rel_def str_eq_def) - qed - with prems show ?thesis by (auto simp:str_eq_rel_def str_eq_def) - qed - hence "y @ z \ L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def) - } moreover { - fix za - assume h1: "za \ z" and h2: "(x @ za) \ L\<^isub>1" and h3: "z - za \ L\<^isub>2" - hence "y @ za \ L\<^isub>1" - proof- - have "\L\<^isub>1 `` {x} = \L\<^isub>1 `` {y}" - using h1 tag_xy by (auto simp:tag_str_SEQ_def) - with h2 show ?thesis - by (auto simp:Image_def str_eq_rel_def str_eq_def) - qed - with h1 h3 have "y @ z \ L\<^isub>1 ;; L\<^isub>2" - by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE) - } - ultimately show ?thesis by blast - qed - } thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \ m \(L\<^isub>1 ;; L\<^isub>2) n" - by (auto simp add: str_eq_def str_eq_rel_def) -qed - -lemma quot_seq_finiteI: - assumes finite1: "finite (UNIV // \(L\<^isub>1::string set))" - and finite2: "finite (UNIV // \L\<^isub>2)" - shows "finite (UNIV // \(L\<^isub>1 ;; L\<^isub>2))" -proof(rule_tac f = "(op `) (tag_str_SEQ L\<^isub>1 L\<^isub>2)" in finite_imageD) - show "finite (op ` (tag_str_SEQ L\<^isub>1 L\<^isub>2) ` UNIV // \L\<^isub>1 ;; L\<^isub>2)" - using finite1 finite2 - by (auto intro:finite_tag_imageI tag_str_seq_range_finite) -next - show "inj_on (op ` (tag_str_SEQ L\<^isub>1 L\<^isub>2)) (UNIV // \L\<^isub>1 ;; L\<^isub>2)" - apply (rule tag_image_injI) - apply (rule tag_str_SEQ_injI) - by (auto intro:tag_image_injI tag_str_SEQ_injI simp:) -qed - -subsection {* The case for @{text "ALT"} *} - -definition - "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \ ((\L\<^isub>1) `` {x}, (\L\<^isub>2) `` {x})" - -lemma tag_str_alt_range_finite: - "\finite (UNIV // \L\<^isub>1); finite (UNIV // \L\<^isub>2)\ - \ finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" -apply (rule_tac B = "(UNIV // \L\<^isub>1) \ (UNIV // \L\<^isub>2)" in finite_subset) -by (auto simp:tag_str_ALT_def Image_def quotient_def) - -lemma quot_union_finiteI: - assumes finite1: "finite (UNIV // \(L\<^isub>1::string set))" - and finite2: "finite (UNIV // \L\<^isub>2)" - shows "finite (UNIV // \(L\<^isub>1 \ L\<^isub>2))" -proof(rule_tac f = "(op `) (tag_str_ALT L\<^isub>1 L\<^isub>2)" in finite_imageD) - show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` UNIV // \L\<^isub>1 \ L\<^isub>2)" - using finite1 finite2 - by (auto intro:finite_tag_imageI tag_str_alt_range_finite) -next - show "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (UNIV // \L\<^isub>1 \ L\<^isub>2)" - proof- - have "\m n. tag_str_ALT L\<^isub>1 L\<^isub>2 m = tag_str_ALT L\<^isub>1 L\<^isub>2 n - \ m \(L\<^isub>1 \ L\<^isub>2) n" - unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by auto - thus ?thesis by (auto intro:tag_image_injI) - qed -qed - - -subsection {* - The case for @{text "STAR"} - *} - -text {* - This turned out to be the most tricky case. - *} (* I will make some illustrations for it. *) - -definition - "tag_str_STAR L\<^isub>1 x \ {(\L\<^isub>1) `` {x - xa} | xa. xa < x \ xa \ L\<^isub>1\}" - -lemma finite_set_has_max: "\finite A; A \ {}\ \ - (\ max \ A. \ a \ A. f a <= (f max :: nat))" -proof (induct rule:finite.induct) - case emptyI thus ?case by simp -next - case (insertI A a) - show ?case - proof (cases "A = {}") - case True thus ?thesis by (rule_tac x = a in bexI, auto) - next - case False - with prems obtain max - where h1: "max \ A" - and h2: "\a\A. f a \ f max" by blast - show ?thesis - proof (cases "f a \ f max") - assume "f a \ f max" - with h1 h2 show ?thesis by (rule_tac x = max in bexI, auto) - next - assume "\ (f a \ f max)" - thus ?thesis using h2 by (rule_tac x = a in bexI, auto) - qed - qed -qed - -lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}" -apply (induct x rule:rev_induct, simp) -apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \ {xs}") -by (auto simp:strict_prefix_def) - - -lemma tag_str_star_range_finite: - "finite (UNIV // \L\<^isub>1) \ finite (range (tag_str_STAR L\<^isub>1))" -apply (rule_tac B = "Pow (UNIV // \L\<^isub>1)" in finite_subset) -by (auto simp:tag_str_STAR_def Image_def - quotient_def split:if_splits) - -lemma tag_str_STAR_injI: - "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \ m \(L\<^isub>1\) n" -proof- - { fix x y z - assume xz_in_star: "x @ z \ L\<^isub>1\" - and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y" - have "y @ z \ L\<^isub>1\" - proof(cases "x = []") - case True - with tag_xy have "y = []" - by (auto simp:tag_str_STAR_def strict_prefix_def) - thus ?thesis using xz_in_star True by simp - next - case False - obtain x_max - where h1: "x_max < x" - and h2: "x_max \ L\<^isub>1\" - and h3: "(x - x_max) @ z \ L\<^isub>1\" - and h4:"\ xa < x. xa \ L\<^isub>1\ \ (x - xa) @ z \ L\<^isub>1\ - \ length xa \ length x_max" - proof- - let ?S = "{xa. xa < x \ xa \ L\<^isub>1\ \ (x - xa) @ z \ L\<^isub>1\}" - have "finite ?S" - by (rule_tac B = "{xa. xa < x}" in finite_subset, - auto simp:finite_strict_prefix_set) - moreover have "?S \ {}" using False xz_in_star - by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def) - ultimately have "\ max \ ?S. \ a \ ?S. length a \ length max" - using finite_set_has_max by blast - with prems show ?thesis by blast - qed - obtain ya - where h5: "ya < y" and h6: "ya \ L\<^isub>1\" and h7: "(x - x_max) \L\<^isub>1 (y - ya)" - proof- - from tag_xy have "{\L\<^isub>1 `` {x - xa} |xa. xa < x \ xa \ L\<^isub>1\} = - {\L\<^isub>1 `` {y - xa} |xa. xa < y \ xa \ L\<^isub>1\}" (is "?left = ?right") - by (auto simp:tag_str_STAR_def) - moreover have "\L\<^isub>1 `` {x - x_max} \ ?left" using h1 h2 by auto - ultimately have "\L\<^isub>1 `` {x - x_max} \ ?right" by simp - with prems show ?thesis apply - (simp add:Image_def str_eq_rel_def str_eq_def) by blast - qed - have "(y - ya) @ z \ L\<^isub>1\" - proof- - from h3 h1 obtain a b where a_in: "a \ L\<^isub>1" - and a_neq: "a \ []" and b_in: "b \ L\<^isub>1\" - and ab_max: "(x - x_max) @ z = a @ b" - by (drule_tac star_decom, auto simp:strict_prefix_def elim:prefixE) - have "(x - x_max) \ a \ (a - (x - x_max)) @ b = z" - proof - - have "((x - x_max) \ a \ (a - (x - x_max)) @ b = z) \ - (a < (x - x_max) \ ((x - x_max) - a) @ z = b)" - using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def) - moreover { - assume np: "a < (x - x_max)" and b_eqs: " ((x - x_max) - a) @ z = b" - have "False" - proof - - let ?x_max' = "x_max @ a" - have "?x_max' < x" - using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) - moreover have "?x_max' \ L\<^isub>1\" - using a_in h2 by (simp add:star_intro3) - moreover have "(x - ?x_max') @ z \ L\<^isub>1\" - using b_eqs b_in np h1 by (simp add:diff_diff_appd) - moreover have "\ (length ?x_max' \ length x_max)" - using a_neq by simp - ultimately show ?thesis using h4 by blast - qed - } ultimately show ?thesis by blast - qed - then obtain za where z_decom: "z = za @ b" - and x_za: "(x - x_max) @ za \ L\<^isub>1" - using a_in by (auto elim:prefixE) - from x_za h7 have "(y - ya) @ za \ L\<^isub>1" - by (auto simp:str_eq_def str_eq_rel_def) - with z_decom b_in show ?thesis by (auto dest!:step[of "(y - ya) @ za"]) - qed - with h5 h6 show ?thesis - by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) - qed - } thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \ m \(L\<^isub>1\) n" - by (auto simp add:str_eq_def str_eq_rel_def) -qed - -lemma quot_star_finiteI: - assumes finite: "finite (UNIV // \(L\<^isub>1::string set))" - shows "finite (UNIV // \(L\<^isub>1\))" -proof(rule_tac f = "(op `) (tag_str_STAR L\<^isub>1)" in finite_imageD) - show "finite (op ` (tag_str_STAR L\<^isub>1) ` UNIV // \L\<^isub>1\)" using finite - by (auto intro:finite_tag_imageI tag_str_star_range_finite) -next - show "inj_on (op ` (tag_str_STAR L\<^isub>1)) (UNIV // \L\<^isub>1\)" - by (auto intro:tag_image_injI tag_str_STAR_injI) -qed - -subsection {* - The main lemma - *} - -lemma easier_directio\: - "Lang = L (r::rexp) \ finite (UNIV // (\Lang))" -proof (induct arbitrary:Lang rule:rexp.induct) - case NULL - have "UNIV // (\{}) \ {UNIV} " - by (auto simp:quotient_def str_eq_rel_def str_eq_def) - with prems show "?case" by (auto intro:finite_subset) -next - case EMPTY - have "UNIV // (\{[]}) \ {{[]}, UNIV - {[]}}" - by (rule quot_empty_subset) - with prems show ?case by (auto intro:finite_subset) -next - case (CHAR c) - have "UNIV // (\{[c]}) \ {{[]},{[c]}, UNIV - {[], [c]}}" - by (rule quot_char_subset) - with prems show ?case by (auto intro:finite_subset) -next - case (SEQ r\<^isub>1 r\<^isub>2) - have "\finite (UNIV // \(L r\<^isub>1)); finite (UNIV // \(L r\<^isub>2))\ - \ finite (UNIV // \(L r\<^isub>1 ;; L r\<^isub>2))" - by (erule quot_seq_finiteI, simp) - with prems show ?case by simp -next - case (ALT r\<^isub>1 r\<^isub>2) - have "\finite (UNIV // \(L r\<^isub>1)); finite (UNIV // \(L r\<^isub>2))\ - \ finite (UNIV // \(L r\<^isub>1 \ L r\<^isub>2))" - by (erule quot_union_finiteI, simp) - with prems show ?case by simp -next - case (STAR r) - have "finite (UNIV // \(L r)) - \ finite (UNIV // \((L r)\))" - by (erule quot_star_finiteI) - with prems show ?case by simp -qed - -end - +theory Myhill + imports Main List_Prefix Prefix_subtract +begin + +section {* Preliminary definitions *} + +text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *} +definition Seq :: "string set \ string set \ string set" ("_ ;; _" [100,100] 100) +where + "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \ L1 \ s2 \ L2}" + +text {* Transitive closure of language @{text "L"}. *} +inductive_set + Star :: "string set \ string set" ("_\" [101] 102) + for L :: "string set" +where + start[intro]: "[] \ L\" +| step[intro]: "\s1 \ L; s2 \ L\\ \ s1@s2 \ L\" + +text {* Some properties of operator @{text ";;"}.*} + +lemma seq_union_distrib: + "(A \ B) ;; C = (A ;; C) \ (B ;; C)" +by (auto simp:Seq_def) + +lemma seq_intro: + "\x \ A; y \ B\ \ x @ y \ A ;; B " +by (auto simp:Seq_def) + +lemma seq_assoc: + "(A ;; B) ;; C = A ;; (B ;; C)" +apply(auto simp:Seq_def) +apply blast +by (metis append_assoc) + +lemma star_intro1[rule_format]: "x \ lang\ \ \ y. y \ lang\ \ x @ y \ lang\" +by (erule Star.induct, auto) + +lemma star_intro2: "y \ lang \ y \ lang\" +by (drule step[of y lang "[]"], auto simp:start) + +lemma star_intro3[rule_format]: + "x \ lang\ \ \y . y \ lang \ x @ y \ lang\" +by (erule Star.induct, auto intro:star_intro2) + +lemma star_decom: + "\x \ lang\; x \ []\ \(\ a b. x = a @ b \ a \ [] \ a \ lang \ b \ lang\)" +by (induct x rule: Star.induct, simp, blast) + +lemma star_decom': + "\x \ lang\; x \ []\ \ \a b. x = a @ b \ a \ lang\ \ b \ lang" +apply (induct x rule:Star.induct, simp) +apply (case_tac "s2 = []") +apply (rule_tac x = "[]" in exI, rule_tac x = s1 in exI, simp add:start) +apply (simp, (erule exE| erule conjE)+) +by (rule_tac x = "s1 @ a" in exI, rule_tac x = b in exI, simp add:step) + +text {* Ardens lemma expressed at the level of language, rather than the level of regular expression. *} + +theorem ardens_revised: + assumes nemp: "[] \ A" + shows "(X = X ;; A \ B) \ (X = B ;; A\)" +proof + assume eq: "X = B ;; A\" + have "A\ = {[]} \ A\ ;; A" + by (auto simp:Seq_def star_intro3 star_decom') + then have "B ;; A\ = B ;; ({[]} \ A\ ;; A)" + unfolding Seq_def by simp + also have "\ = B \ B ;; (A\ ;; A)" + unfolding Seq_def by auto + also have "\ = B \ (B ;; A\) ;; A" + by (simp only:seq_assoc) + finally show "X = X ;; A \ B" + using eq by blast +next + assume eq': "X = X ;; A \ B" + hence c1': "\ x. x \ B \ x \ X" + and c2': "\ x y. \x \ X; y \ A\ \ x @ y \ X" + using Seq_def by auto + show "X = B ;; A\" + proof + show "B ;; A\ \ X" + proof- + { fix x y + have "\y \ A\; x \ X\ \ x @ y \ X " + apply (induct arbitrary:x rule:Star.induct, simp) + by (auto simp only:append_assoc[THEN sym] dest:c2') + } thus ?thesis using c1' by (auto simp:Seq_def) + qed + next + show "X \ B ;; A\" + proof- + { fix x + have "x \ X \ x \ B ;; A\" + proof (induct x taking:length rule:measure_induct) + fix z + assume hyps: + "\y. length y < length z \ y \ X \ y \ B ;; A\" + and z_in: "z \ X" + show "z \ B ;; A\" + proof (cases "z \ B") + case True thus ?thesis by (auto simp:Seq_def start) + next + case False hence "z \ X ;; A" using eq' z_in by auto + then obtain za zb where za_in: "za \ X" + and zab: "z = za @ zb \ zb \ A" and zbne: "zb \ []" + using nemp unfolding Seq_def by blast + from zbne zab have "length za < length z" by auto + with za_in hyps have "za \ B ;; A\" by blast + hence "za @ zb \ B ;; A\" using zab + by (clarsimp simp:Seq_def, blast dest:star_intro3) + thus ?thesis using zab by simp + qed + qed + } thus ?thesis by blast + qed + qed +qed + + +text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *} +datatype rexp = + NULL +| EMPTY +| CHAR char +| SEQ rexp rexp +| ALT rexp rexp +| STAR rexp + + +text {* + The following @{text "L"} is an overloaded operator, where @{text "L(x)"} evaluates to + the language represented by the syntactic object @{text "x"}. +*} +consts L:: "'a \ string set" + + +text {* + The @{text "L(rexp)"} for regular expression @{text "rexp"} is defined by the + following overloading function @{text "L_rexp"}. +*} +overloading L_rexp \ "L:: rexp \ string set" +begin +fun + L_rexp :: "rexp \ string set" +where + "L_rexp (NULL) = {}" + | "L_rexp (EMPTY) = {[]}" + | "L_rexp (CHAR c) = {[c]}" + | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)" + | "L_rexp (ALT r1 r2) = (L_rexp r1) \ (L_rexp r2)" + | "L_rexp (STAR r) = (L_rexp r)\" +end + +text {* + To obtain equational system out of finite set of equivalent classes, a fold operation + on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"} + more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"} + makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"}, + while @{text "fold f"} does not. +*} + +definition + folds :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b" +where + "folds f z S \ SOME x. fold_graph f z S x" + +text {* + The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"} + does not affect the @{text "L"}-value of the resultant regular expression. + *} +lemma folds_alt_simp [simp]: + "finite rs \ L (folds ALT NULL rs) = \ (L ` rs)" +apply (rule set_ext, simp add:folds_def) +apply (rule someI2_ex, erule finite_imp_fold_graph) +by (erule fold_graph.induct, auto) + +(* Just a technical lemma. *) +lemma [simp]: + shows "(x, y) \ {(x, y). P x y} \ P x y" +by simp + +text {* + @{text "\L"} is an equivalent class defined by language @{text "Lang"}. +*} +definition + str_eq_rel ("\_") +where + "\Lang \ {(x, y). (\z. x @ z \ Lang \ y @ z \ Lang)}" + +text {* + Among equivlant clases of @{text "\Lang"}, the set @{text "finals(Lang)"} singles out + those which contains strings from @{text "Lang"}. +*} + +definition + "finals Lang \ {\Lang `` {x} | x . x \ Lang}" + +text {* + The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}. +*} +lemma lang_is_union_of_finals: + "Lang = \ finals(Lang)" +proof + show "Lang \ \ (finals Lang)" + proof + fix x + assume "x \ Lang" + thus "x \ \ (finals Lang)" + apply (simp add:finals_def, rule_tac x = "(\Lang) `` {x}" in exI) + by (auto simp:Image_def str_eq_rel_def) + qed +next + show "\ (finals Lang) \ Lang" + apply (clarsimp simp:finals_def str_eq_rel_def) + by (drule_tac x = "[]" in spec, auto) +qed + +section {* Direction @{text "finite partition \ regular language"}*} + +text {* + The relationship between equivalent classes can be described by an + equational system. + For example, in equational system \eqref{example_eqns}, $X_0, X_1$ are equivalent + classes. The first equation says every string in $X_0$ is obtained either by + appending one $b$ to a string in $X_0$ or by appending one $a$ to a string in + $X_1$ or just be an empty string (represented by the regular expression $\lambda$). Similary, + the second equation tells how the strings inside $X_1$ are composed. + \begin{equation}\label{example_eqns} + \begin{aligned} + X_0 & = X_0 b + X_1 a + \lambda \\ + X_1 & = X_0 a + X_1 b + \end{aligned} + \end{equation} + The summands on the right hand side is represented by the following data type + @{text "rhs_item"}, mnemonic for 'right hand side item'. + Generally, there are two kinds of right hand side items, one kind corresponds to + pure regular expressions, like the $\lambda$ in \eqref{example_eqns}, the other kind corresponds to + transitions from one one equivalent class to another, like the $X_0 b, X_1 a$ etc. + *} + +datatype rhs_item = + Lam "rexp" (* Lambda *) + | Trn "(string set)" "rexp" (* Transition *) + +text {* + In this formalization, pure regular expressions like $\lambda$ is + repsented by @{text "Lam(EMPTY)"}, while transitions like $X_0 a$ is represented by $Trn~X_0~(CHAR~a)$. + *} + +text {* + The functions @{text "the_r"} and @{text "the_Trn"} are used to extract + subcomponents from right hand side items. + *} + +fun the_r :: "rhs_item \ rexp" +where "the_r (Lam r) = r" + +fun the_Trn:: "rhs_item \ (string set \ rexp)" +where "the_Trn (Trn Y r) = (Y, r)" + +text {* + Every right hand side item @{text "itm"} defines a string set given + @{text "L(itm)"}, defined as: +*} +overloading L_rhs_e \ "L:: rhs_item \ string set" +begin + fun L_rhs_e:: "rhs_item \ string set" + where + "L_rhs_e (Lam r) = L r" | + "L_rhs_e (Trn X r) = X ;; L r" +end + +text {* + The right hand side of every equation is represented by a set of + items. The string set defined by such a set @{text "itms"} is given + by @{text "L(itms)"}, defined as: +*} + +overloading L_rhs \ "L:: rhs_item set \ string set" +begin + fun L_rhs:: "rhs_item set \ string set" + where "L_rhs rhs = \ (L ` rhs)" +end + +text {* + Given a set of equivalent classses @{text "CS"} and one equivalent class @{text "X"} among + @{text "CS"}, the term @{text "init_rhs CS X"} is used to extract the right hand side of + the equation describing the formation of @{text "X"}. The definition of @{text "init_rhs"} + is: + *} + +definition + "init_rhs CS X \ + if ([] \ X) then + {Lam(EMPTY)} \ {Trn Y (CHAR c) | Y c. Y \ CS \ Y ;; {[c]} \ X} + else + {Trn Y (CHAR c)| Y c. Y \ CS \ Y ;; {[c]} \ X}" + +text {* + In the definition of @{text "init_rhs"}, the term + @{text "{Trn Y (CHAR c)| Y c. Y \ CS \ Y ;; {[c]} \ X}"} appearing on both branches + describes the formation of strings in @{text "X"} out of transitions, while + the term @{text "{Lam(EMPTY)}"} describes the empty string which is intrinsically contained in + @{text "X"} rather than by transition. This @{text "{Lam(EMPTY)}"} corresponds to + the $\lambda$ in \eqref{example_eqns}. + + With the help of @{text "init_rhs"}, the equitional system descrbing the formation of every + equivalent class inside @{text "CS"} is given by the following @{text "eqs(CS)"}. + *} + +definition "eqs CS \ {(X, init_rhs CS X) | X. X \ CS}" +(************ arden's lemma variation ********************) + +text {* + The following @{text "items_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}. + *} +definition + "items_of rhs X \ {Trn X r | r. (Trn X r) \ rhs}" + +text {* + The following @{text "rexp_of rhs X"} combines all regular expressions in @{text "X"}-items + using @{text "ALT"} to form a single regular expression. + It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}. + *} + +definition + "rexp_of rhs X \ folds ALT NULL ((snd o the_Trn) ` items_of rhs X)" + +text {* + The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}. + *} + +definition + "lam_of rhs \ {Lam r | r. Lam r \ rhs}" + +text {* + The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"} + using @{text "ALT"} to form a single regular expression. + When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"} + is used to compute compute the regular expression corresponds to @{text "rhs"}. + *} + +definition + "rexp_of_lam rhs \ folds ALT NULL (the_r ` lam_of rhs)" + +text {* + The following @{text "attach_rexp rexp' itm"} attach + the regular expression @{text "rexp'"} to + the right of right hand side item @{text "itm"}. + *} + +fun attach_rexp :: "rexp \ rhs_item \ rhs_item" +where + "attach_rexp rexp' (Lam rexp) = Lam (SEQ rexp rexp')" +| "attach_rexp rexp' (Trn X rexp) = Trn X (SEQ rexp rexp')" + +text {* + The following @{text "append_rhs_rexp rhs rexp"} attaches + @{text "rexp"} to every item in @{text "rhs"}. + *} + +definition + "append_rhs_rexp rhs rexp \ (attach_rexp rexp) ` rhs" + +text {* + With the help of the two functions immediately above, Ardens' + transformation on right hand side @{text "rhs"} is implemented + by the following function @{text "arden_variate X rhs"}. + After this transformation, the recursive occurent of @{text "X"} + in @{text "rhs"} will be eliminated, while the + string set defined by @{text "rhs"} is kept unchanged. + *} +definition + "arden_variate X rhs \ + append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))" + + +(*********** substitution of ES *************) + +text {* + Suppose the equation defining @{text "X"} is $X = xrhs$, + the purpose of @{text "rhs_subst"} is to substitute all occurences of @{text "X"} in + @{text "rhs"} by @{text "xrhs"}. + A litte thought may reveal that the final result + should be: first append $(a_1 | a_2 | \ldots | a_n)$ to every item of @{text "xrhs"} and then + union the result with all non-@{text "X"}-items of @{text "rhs"}. + *} +definition + "rhs_subst rhs X xrhs \ + (rhs - (items_of rhs X)) \ (append_rhs_rexp xrhs (rexp_of rhs X))" + +text {* + Suppose the equation defining @{text "X"} is $X = xrhs$, the follwing + @{text "eqs_subst ES X xrhs"} substitute @{text "xrhs"} into every equation + of the equational system @{text "ES"}. + *} + +definition + "eqs_subst ES X xrhs \ {(Y, rhs_subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \ ES}" + +text {* + The computation of regular expressions for equivalent classes is accomplished + using a iteration principle given by the following lemma. + *} + +lemma wf_iter [rule_format]: + fixes f + assumes step: "\ e. \P e; \ Q e\ \ (\ e'. P e' \ (f(e'), f(e)) \ less_than)" + shows pe: "P e \ (\ e'. P e' \ Q e')" +proof(induct e rule: wf_induct + [OF wf_inv_image[OF wf_less_than, where f = "f"]], clarify) + fix x + assume h [rule_format]: + "\y. (y, x) \ inv_image less_than f \ P y \ (\e'. P e' \ Q e')" + and px: "P x" + show "\e'. P e' \ Q e'" + proof(cases "Q x") + assume "Q x" with px show ?thesis by blast + next + assume nq: "\ Q x" + from step [OF px nq] + obtain e' where pe': "P e'" and ltf: "(f e', f x) \ less_than" by auto + show ?thesis + proof(rule h) + from ltf show "(e', x) \ inv_image less_than f" + by (simp add:inv_image_def) + next + from pe' show "P e'" . + qed + qed +qed + +text {* + The @{text "P"} in lemma @{text "wf_iter"} is an invaiant kept throughout the iteration procedure. + The particular invariant used to solve our problem is defined by function @{text "Inv(ES)"}, + an invariant over equal system @{text "ES"}. + Every definition starting next till @{text "Inv"} stipulates a property to be satisfied by @{text "ES"}. +*} + +text {* + Every variable is defined at most onece in @{text "ES"}. + *} +definition + "distinct_equas ES \ + \ X rhs rhs'. (X, rhs) \ ES \ (X, rhs') \ ES \ rhs = rhs'" +text {* + Every equation in @{text "ES"} (represented by @{text "(X, rhs)"}) is valid, i.e. @{text "(X = L rhs)"}. + *} +definition + "valid_eqns ES \ \ X rhs. (X, rhs) \ ES \ (X = L rhs)" + +text {* + The following @{text "rhs_nonempty rhs"} requires regular expressions occuring in transitional + items of @{text "rhs"} does not contain empty string. This is necessary for + the application of Arden's transformation to @{text "rhs"}. + *} +definition + "rhs_nonempty rhs \ (\ Y r. Trn Y r \ rhs \ [] \ L r)" + +text {* + The following @{text "ardenable ES"} requires that Arden's transformation is applicable + to every equation of equational system @{text "ES"}. + *} +definition + "ardenable ES \ \ X rhs. (X, rhs) \ ES \ rhs_nonempty rhs" + +(* The following non_empty seems useless. *) +definition + "non_empty ES \ \ X rhs. (X, rhs) \ ES \ X \ {}" + +text {* + The following @{text "finite_rhs ES"} requires every equation in @{text "rhs"} be finite. + *} +definition + "finite_rhs ES \ \ X rhs. (X, rhs) \ ES \ finite rhs" + +text {* + The following @{text "classes_of rhs"} returns all variables (or equivalent classes) + occuring in @{text "rhs"}. + *} +definition + "classes_of rhs \ {X. \ r. Trn X r \ rhs}" + +text {* + The following @{text "lefts_of ES"} returns all variables + defined by equational system @{text "ES"}. + *} +definition + "lefts_of ES \ {Y | Y yrhs. (Y, yrhs) \ ES}" + +text {* + The following @{text "self_contained ES"} requires that every + variable occuring on the right hand side of equations is already defined by some + equation in @{text "ES"}. + *} +definition + "self_contained ES \ \ (X, xrhs) \ ES. classes_of xrhs \ lefts_of ES" + + +text {* + The invariant @{text "Inv(ES)"} is a conjunction of all the previously defined constaints. + *} +definition + "Inv ES \ valid_eqns ES \ finite ES \ distinct_equas ES \ ardenable ES \ + non_empty ES \ finite_rhs ES \ self_contained ES" + +subsection {* The proof of this direction *} + +subsubsection {* Basic properties *} + +text {* + The following are some basic properties of the above definitions. +*} + +lemma L_rhs_union_distrib: + " L (A::rhs_item set) \ L B = L (A \ B)" +by simp + +lemma finite_snd_Trn: + assumes finite:"finite rhs" + shows "finite {r\<^isub>2. Trn Y r\<^isub>2 \ rhs}" (is "finite ?B") +proof- + def rhs' \ "{e \ rhs. \ r. e = Trn Y r}" + have "?B = (snd o the_Trn) ` rhs'" using rhs'_def by (auto simp:image_def) + moreover have "finite rhs'" using finite rhs'_def by auto + ultimately show ?thesis by simp +qed + +lemma rexp_of_empty: + assumes finite:"finite rhs" + and nonempty:"rhs_nonempty rhs" + shows "[] \ L (rexp_of rhs X)" +using finite nonempty rhs_nonempty_def +by (drule_tac finite_snd_Trn[where Y = X], auto simp:rexp_of_def items_of_def) + +lemma [intro!]: + "P (Trn X r) \ (\a. (\r. a = Trn X r \ P a))" by auto + +lemma finite_items_of: + "finite rhs \ finite (items_of rhs X)" +by (auto simp:items_of_def intro:finite_subset) + +lemma lang_of_rexp_of: + assumes finite:"finite rhs" + shows "L (items_of rhs X) = X ;; (L (rexp_of rhs X))" +proof - + have "finite ((snd \ the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto + thus ?thesis + apply (auto simp:rexp_of_def Seq_def items_of_def) + apply (rule_tac x = s1 in exI, rule_tac x = s2 in exI, auto) + by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def) +qed + +lemma rexp_of_lam_eq_lam_set: + assumes finite: "finite rhs" + shows "L (rexp_of_lam rhs) = L (lam_of rhs)" +proof - + have "finite (the_r ` {Lam r |r. Lam r \ rhs})" using finite + by (rule_tac finite_imageI, auto intro:finite_subset) + thus ?thesis by (auto simp:rexp_of_lam_def lam_of_def) +qed + +lemma [simp]: + " L (attach_rexp r xb) = L xb ;; L r" +apply (cases xb, auto simp:Seq_def) +by (rule_tac x = "s1 @ s1a" in exI, rule_tac x = s2a in exI,auto simp:Seq_def) + +lemma lang_of_append_rhs: + "L (append_rhs_rexp rhs r) = L rhs ;; L r" +apply (auto simp:append_rhs_rexp_def image_def) +apply (auto simp:Seq_def) +apply (rule_tac x = "L xb ;; L r" in exI, auto simp add:Seq_def) +by (rule_tac x = "attach_rexp r xb" in exI, auto simp:Seq_def) + +lemma classes_of_union_distrib: + "classes_of A \ classes_of B = classes_of (A \ B)" +by (auto simp add:classes_of_def) + +lemma lefts_of_union_distrib: + "lefts_of A \ lefts_of B = lefts_of (A \ B)" +by (auto simp:lefts_of_def) + + +subsubsection {* Intialization *} + +text {* + The following several lemmas until @{text "init_ES_satisfy_Inv"} shows that + the initial equational system satisfies invariant @{text "Inv"}. + *} + +lemma defined_by_str: + "\s \ X; X \ UNIV // (\Lang)\ \ X = (\Lang) `` {s}" +by (auto simp:quotient_def Image_def str_eq_rel_def) + +lemma every_eqclass_has_transition: + assumes has_str: "s @ [c] \ X" + and in_CS: "X \ UNIV // (\Lang)" + obtains Y where "Y \ UNIV // (\Lang)" and "Y ;; {[c]} \ X" and "s \ Y" +proof - + def Y \ "(\Lang) `` {s}" + have "Y \ UNIV // (\Lang)" + unfolding Y_def quotient_def by auto + moreover + have "X = (\Lang) `` {s @ [c]}" + using has_str in_CS defined_by_str by blast + then have "Y ;; {[c]} \ X" + unfolding Y_def Image_def Seq_def + unfolding str_eq_rel_def + by clarsimp + moreover + have "s \ Y" unfolding Y_def + unfolding Image_def str_eq_rel_def by simp + ultimately show thesis by (blast intro: that) +qed + +lemma l_eq_r_in_eqs: + assumes X_in_eqs: "(X, xrhs) \ (eqs (UNIV // (\Lang)))" + shows "X = L xrhs" +proof + show "X \ L xrhs" + proof + fix x + assume "(1)": "x \ X" + show "x \ L xrhs" + proof (cases "x = []") + assume empty: "x = []" + thus ?thesis using X_in_eqs "(1)" + by (auto simp:eqs_def init_rhs_def) + next + assume not_empty: "x \ []" + then obtain clist c where decom: "x = clist @ [c]" + by (case_tac x rule:rev_cases, auto) + have "X \ UNIV // (\Lang)" using X_in_eqs by (auto simp:eqs_def) + then obtain Y + where "Y \ UNIV // (\Lang)" + and "Y ;; {[c]} \ X" + and "clist \ Y" + using decom "(1)" every_eqclass_has_transition by blast + hence + "x \ L {Trn Y (CHAR c)| Y c. Y \ UNIV // (\Lang) \ Y ;; {[c]} \ X}" + using "(1)" decom + by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def) + thus ?thesis using X_in_eqs "(1)" + by (simp add:eqs_def init_rhs_def) + qed + qed +next + show "L xrhs \ X" using X_in_eqs + by (auto simp:eqs_def init_rhs_def) +qed + +lemma finite_init_rhs: + assumes finite: "finite CS" + shows "finite (init_rhs CS X)" +proof- + have "finite {Trn Y (CHAR c) |Y c. Y \ CS \ Y ;; {[c]} \ X}" (is "finite ?A") + proof - + def S \ "{(Y, c)| Y c. Y \ CS \ Y ;; {[c]} \ X}" + def h \ "\ (Y, c). Trn Y (CHAR c)" + have "finite (CS \ (UNIV::char set))" using finite by auto + hence "finite S" using S_def + by (rule_tac B = "CS \ UNIV" in finite_subset, auto) + moreover have "?A = h ` S" by (auto simp: S_def h_def image_def) + ultimately show ?thesis + by auto + qed + thus ?thesis by (simp add:init_rhs_def) +qed + +lemma init_ES_satisfy_Inv: + assumes finite_CS: "finite (UNIV // (\Lang))" + shows "Inv (eqs (UNIV // (\Lang)))" +proof - + have "finite (eqs (UNIV // (\Lang)))" using finite_CS + by (simp add:eqs_def) + moreover have "distinct_equas (eqs (UNIV // (\Lang)))" + by (simp add:distinct_equas_def eqs_def) + moreover have "ardenable (eqs (UNIV // (\Lang)))" + by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps) + moreover have "valid_eqns (eqs (UNIV // (\Lang)))" + using l_eq_r_in_eqs by (simp add:valid_eqns_def) + moreover have "non_empty (eqs (UNIV // (\Lang)))" + by (auto simp:non_empty_def eqs_def quotient_def Image_def str_eq_rel_def) + moreover have "finite_rhs (eqs (UNIV // (\Lang)))" + using finite_init_rhs[OF finite_CS] + by (auto simp:finite_rhs_def eqs_def) + moreover have "self_contained (eqs (UNIV // (\Lang)))" + by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def) + ultimately show ?thesis by (simp add:Inv_def) +qed + +subsubsection {* + Interation step + *} + +text {* + From this point until @{text "iteration_step"}, it is proved + that there exists iteration steps which keep @{text "Inv(ES)"} while + decreasing the size of @{text "ES"}. + *} +lemma arden_variate_keeps_eq: + assumes l_eq_r: "X = L rhs" + and not_empty: "[] \ L (rexp_of rhs X)" + and finite: "finite rhs" + shows "X = L (arden_variate X rhs)" +proof - + def A \ "L (rexp_of rhs X)" + def b \ "rhs - items_of rhs X" + def B \ "L b" + have "X = B ;; A\" + proof- + have "rhs = items_of rhs X \ b" by (auto simp:b_def items_of_def) + hence "L rhs = L(items_of rhs X \ b)" by simp + hence "L rhs = L(items_of rhs X) \ B" by (simp only:L_rhs_union_distrib B_def) + with lang_of_rexp_of + have "L rhs = X ;; A \ B " using finite by (simp only:B_def b_def A_def) + thus ?thesis + using l_eq_r not_empty + apply (drule_tac B = B and X = X in ardens_revised) + by (auto simp:A_def simp del:L_rhs.simps) + qed + moreover have "L (arden_variate X rhs) = (B ;; A\)" (is "?L = ?R") + by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs + B_def A_def b_def L_rexp.simps seq_union_distrib) + ultimately show ?thesis by simp +qed + +lemma append_keeps_finite: + "finite rhs \ finite (append_rhs_rexp rhs r)" +by (auto simp:append_rhs_rexp_def) + +lemma arden_variate_keeps_finite: + "finite rhs \ finite (arden_variate X rhs)" +by (auto simp:arden_variate_def append_keeps_finite) + +lemma append_keeps_nonempty: + "rhs_nonempty rhs \ rhs_nonempty (append_rhs_rexp rhs r)" +apply (auto simp:rhs_nonempty_def append_rhs_rexp_def) +by (case_tac x, auto simp:Seq_def) + +lemma nonempty_set_sub: + "rhs_nonempty rhs \ rhs_nonempty (rhs - A)" +by (auto simp:rhs_nonempty_def) + +lemma nonempty_set_union: + "\rhs_nonempty rhs; rhs_nonempty rhs'\ \ rhs_nonempty (rhs \ rhs')" +by (auto simp:rhs_nonempty_def) + +lemma arden_variate_keeps_nonempty: + "rhs_nonempty rhs \ rhs_nonempty (arden_variate X rhs)" +by (simp only:arden_variate_def append_keeps_nonempty nonempty_set_sub) + + +lemma rhs_subst_keeps_nonempty: + "\rhs_nonempty rhs; rhs_nonempty xrhs\ \ rhs_nonempty (rhs_subst rhs X xrhs)" +by (simp only:rhs_subst_def append_keeps_nonempty nonempty_set_union nonempty_set_sub) + +lemma rhs_subst_keeps_eq: + assumes substor: "X = L xrhs" + and finite: "finite rhs" + shows "L (rhs_subst rhs X xrhs) = L rhs" (is "?Left = ?Right") +proof- + def A \ "L (rhs - items_of rhs X)" + have "?Left = A \ L (append_rhs_rexp xrhs (rexp_of rhs X))" + by (simp only:rhs_subst_def L_rhs_union_distrib A_def) + moreover have "?Right = A \ L (items_of rhs X)" + proof- + have "rhs = (rhs - items_of rhs X) \ (items_of rhs X)" by (auto simp:items_of_def) + thus ?thesis by (simp only:L_rhs_union_distrib A_def) + qed + moreover have "L (append_rhs_rexp xrhs (rexp_of rhs X)) = L (items_of rhs X)" + using finite substor by (simp only:lang_of_append_rhs lang_of_rexp_of) + ultimately show ?thesis by simp +qed + +lemma rhs_subst_keeps_finite_rhs: + "\finite rhs; finite yrhs\ \ finite (rhs_subst rhs Y yrhs)" +by (auto simp:rhs_subst_def append_keeps_finite) + +lemma eqs_subst_keeps_finite: + assumes finite:"finite (ES:: (string set \ rhs_item set) set)" + shows "finite (eqs_subst ES Y yrhs)" +proof - + have "finite {(Ya, rhs_subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \ ES}" + (is "finite ?A") + proof- + def eqns' \ "{((Ya::string set), yrhsa)| Ya yrhsa. (Ya, yrhsa) \ ES}" + def h \ "\ ((Ya::string set), yrhsa). (Ya, rhs_subst yrhsa Y yrhs)" + have "finite (h ` eqns')" using finite h_def eqns'_def by auto + moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def) + ultimately show ?thesis by auto + qed + thus ?thesis by (simp add:eqs_subst_def) +qed + +lemma eqs_subst_keeps_finite_rhs: + "\finite_rhs ES; finite yrhs\ \ finite_rhs (eqs_subst ES Y yrhs)" +by (auto intro:rhs_subst_keeps_finite_rhs simp add:eqs_subst_def finite_rhs_def) + +lemma append_rhs_keeps_cls: + "classes_of (append_rhs_rexp rhs r) = classes_of rhs" +apply (auto simp:classes_of_def append_rhs_rexp_def) +apply (case_tac xa, auto simp:image_def) +by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+) + +lemma arden_variate_removes_cl: + "classes_of (arden_variate Y yrhs) = classes_of yrhs - {Y}" +apply (simp add:arden_variate_def append_rhs_keeps_cls items_of_def) +by (auto simp:classes_of_def) + +lemma lefts_of_keeps_cls: + "lefts_of (eqs_subst ES Y yrhs) = lefts_of ES" +by (auto simp:lefts_of_def eqs_subst_def) + +lemma rhs_subst_updates_cls: + "X \ classes_of xrhs \ + classes_of (rhs_subst rhs X xrhs) = classes_of rhs \ classes_of xrhs - {X}" +apply (simp only:rhs_subst_def append_rhs_keeps_cls + classes_of_union_distrib[THEN sym]) +by (auto simp:classes_of_def items_of_def) + +lemma eqs_subst_keeps_self_contained: + fixes Y + assumes sc: "self_contained (ES \ {(Y, yrhs)})" (is "self_contained ?A") + shows "self_contained (eqs_subst ES Y (arden_variate Y yrhs))" + (is "self_contained ?B") +proof- + { fix X xrhs' + assume "(X, xrhs') \ ?B" + then obtain xrhs + where xrhs_xrhs': "xrhs' = rhs_subst xrhs Y (arden_variate Y yrhs)" + and X_in: "(X, xrhs) \ ES" by (simp add:eqs_subst_def, blast) + have "classes_of xrhs' \ lefts_of ?B" + proof- + have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def eqs_subst_def) + moreover have "classes_of xrhs' \ lefts_of ES" + proof- + have "classes_of xrhs' \ + classes_of xrhs \ classes_of (arden_variate Y yrhs) - {Y}" + proof- + have "Y \ classes_of (arden_variate Y yrhs)" + using arden_variate_removes_cl by simp + thus ?thesis using xrhs_xrhs' by (auto simp:rhs_subst_updates_cls) + qed + moreover have "classes_of xrhs \ lefts_of ES \ {Y}" using X_in sc + apply (simp only:self_contained_def lefts_of_union_distrib[THEN sym]) + by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def) + moreover have "classes_of (arden_variate Y yrhs) \ lefts_of ES \ {Y}" + using sc + by (auto simp add:arden_variate_removes_cl self_contained_def lefts_of_def) + ultimately show ?thesis by auto + qed + ultimately show ?thesis by simp + qed + } thus ?thesis by (auto simp only:eqs_subst_def self_contained_def) +qed + +lemma eqs_subst_satisfy_Inv: + assumes Inv_ES: "Inv (ES \ {(Y, yrhs)})" + shows "Inv (eqs_subst ES Y (arden_variate Y yrhs))" +proof - + have finite_yrhs: "finite yrhs" + using Inv_ES by (auto simp:Inv_def finite_rhs_def) + have nonempty_yrhs: "rhs_nonempty yrhs" + using Inv_ES by (auto simp:Inv_def ardenable_def) + have Y_eq_yrhs: "Y = L yrhs" + using Inv_ES by (simp only:Inv_def valid_eqns_def, blast) + have "distinct_equas (eqs_subst ES Y (arden_variate Y yrhs))" + using Inv_ES + by (auto simp:distinct_equas_def eqs_subst_def Inv_def) + moreover have "finite (eqs_subst ES Y (arden_variate Y yrhs))" + using Inv_ES by (simp add:Inv_def eqs_subst_keeps_finite) + moreover have "finite_rhs (eqs_subst ES Y (arden_variate Y yrhs))" + proof- + have "finite_rhs ES" using Inv_ES + by (simp add:Inv_def finite_rhs_def) + moreover have "finite (arden_variate Y yrhs)" + proof - + have "finite yrhs" using Inv_ES + by (auto simp:Inv_def finite_rhs_def) + thus ?thesis using arden_variate_keeps_finite by simp + qed + ultimately show ?thesis + by (simp add:eqs_subst_keeps_finite_rhs) + qed + moreover have "ardenable (eqs_subst ES Y (arden_variate Y yrhs))" + proof - + { fix X rhs + assume "(X, rhs) \ ES" + hence "rhs_nonempty rhs" using prems Inv_ES + by (simp add:Inv_def ardenable_def) + with nonempty_yrhs + have "rhs_nonempty (rhs_subst rhs Y (arden_variate Y yrhs))" + by (simp add:nonempty_yrhs + rhs_subst_keeps_nonempty arden_variate_keeps_nonempty) + } thus ?thesis by (auto simp add:ardenable_def eqs_subst_def) + qed + moreover have "valid_eqns (eqs_subst ES Y (arden_variate Y yrhs))" + proof- + have "Y = L (arden_variate Y yrhs)" + using Y_eq_yrhs Inv_ES finite_yrhs nonempty_yrhs + by (rule_tac arden_variate_keeps_eq, (simp add:rexp_of_empty)+) + thus ?thesis using Inv_ES + by (clarsimp simp add:valid_eqns_def + eqs_subst_def rhs_subst_keeps_eq Inv_def finite_rhs_def + simp del:L_rhs.simps) + qed + moreover have + non_empty_subst: "non_empty (eqs_subst ES Y (arden_variate Y yrhs))" + using Inv_ES by (auto simp:Inv_def non_empty_def eqs_subst_def) + moreover + have self_subst: "self_contained (eqs_subst ES Y (arden_variate Y yrhs))" + using Inv_ES eqs_subst_keeps_self_contained by (simp add:Inv_def) + ultimately show ?thesis using Inv_ES by (simp add:Inv_def) +qed + +lemma eqs_subst_card_le: + assumes finite: "finite (ES::(string set \ rhs_item set) set)" + shows "card (eqs_subst ES Y yrhs) <= card ES" +proof- + def f \ "\ x. ((fst x)::string set, rhs_subst (snd x) Y yrhs)" + have "eqs_subst ES Y yrhs = f ` ES" + apply (auto simp:eqs_subst_def f_def image_def) + by (rule_tac x = "(Ya, yrhsa)" in bexI, simp+) + thus ?thesis using finite by (auto intro:card_image_le) +qed + +lemma eqs_subst_cls_remains: + "(X, xrhs) \ ES \ \ xrhs'. (X, xrhs') \ (eqs_subst ES Y yrhs)" +by (auto simp:eqs_subst_def) + +lemma card_noteq_1_has_more: + assumes card:"card S \ 1" + and e_in: "e \ S" + and finite: "finite S" + obtains e' where "e' \ S \ e \ e'" +proof- + have "card (S - {e}) > 0" + proof - + have "card S > 1" using card e_in finite + by (case_tac "card S", auto) + thus ?thesis using finite e_in by auto + qed + hence "S - {e} \ {}" using finite by (rule_tac notI, simp) + thus "(\e'. e' \ S \ e \ e' \ thesis) \ thesis" by auto +qed + +lemma iteration_step: + assumes Inv_ES: "Inv ES" + and X_in_ES: "(X, xrhs) \ ES" + and not_T: "card ES \ 1" + shows "\ ES'. (Inv ES' \ (\ xrhs'.(X, xrhs') \ ES')) \ + (card ES', card ES) \ less_than" (is "\ ES'. ?P ES'") +proof - + have finite_ES: "finite ES" using Inv_ES by (simp add:Inv_def) + then obtain Y yrhs + where Y_in_ES: "(Y, yrhs) \ ES" and not_eq: "(X, xrhs) \ (Y, yrhs)" + using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto) + def ES' == "ES - {(Y, yrhs)}" + let ?ES'' = "eqs_subst ES' Y (arden_variate Y yrhs)" + have "?P ?ES''" + proof - + have "Inv ?ES''" using Y_in_ES Inv_ES + by (rule_tac eqs_subst_satisfy_Inv, simp add:ES'_def insert_absorb) + moreover have "\xrhs'. (X, xrhs') \ ?ES''" using not_eq X_in_ES + by (rule_tac ES = ES' in eqs_subst_cls_remains, auto simp add:ES'_def) + moreover have "(card ?ES'', card ES) \ less_than" + proof - + have "finite ES'" using finite_ES ES'_def by auto + moreover have "card ES' < card ES" using finite_ES Y_in_ES + by (auto simp:ES'_def card_gt_0_iff intro:diff_Suc_less) + ultimately show ?thesis + by (auto dest:eqs_subst_card_le elim:le_less_trans) + qed + ultimately show ?thesis by simp + qed + thus ?thesis by blast +qed + +subsubsection {* + Conclusion of the proof + *} + +text {* + From this point until @{text "hard_direction"}, the hard direction is proved + through a simple application of the iteration principle. +*} + +lemma iteration_conc: + assumes history: "Inv ES" + and X_in_ES: "\ xrhs. (X, xrhs) \ ES" + shows + "\ ES'. (Inv ES' \ (\ xrhs'. (X, xrhs') \ ES')) \ card ES' = 1" + (is "\ ES'. ?P ES'") +proof (cases "card ES = 1") + case True + thus ?thesis using history X_in_ES + by blast +next + case False + thus ?thesis using history iteration_step X_in_ES + by (rule_tac f = card in wf_iter, auto) +qed + +lemma last_cl_exists_rexp: + assumes ES_single: "ES = {(X, xrhs)}" + and Inv_ES: "Inv ES" + shows "\ (r::rexp). L r = X" (is "\ r. ?P r") +proof- + let ?A = "arden_variate X xrhs" + have "?P (rexp_of_lam ?A)" + proof - + have "L (rexp_of_lam ?A) = L (lam_of ?A)" + proof(rule rexp_of_lam_eq_lam_set) + show "finite (arden_variate X xrhs)" using Inv_ES ES_single + by (rule_tac arden_variate_keeps_finite, + auto simp add:Inv_def finite_rhs_def) + qed + also have "\ = L ?A" + proof- + have "lam_of ?A = ?A" + proof- + have "classes_of ?A = {}" using Inv_ES ES_single + by (simp add:arden_variate_removes_cl + self_contained_def Inv_def lefts_of_def) + thus ?thesis + by (auto simp only:lam_of_def classes_of_def, case_tac x, auto) + qed + thus ?thesis by simp + qed + also have "\ = X" + proof(rule arden_variate_keeps_eq [THEN sym]) + show "X = L xrhs" using Inv_ES ES_single + by (auto simp only:Inv_def valid_eqns_def) + next + from Inv_ES ES_single show "[] \ L (rexp_of xrhs X)" + by(simp add:Inv_def ardenable_def rexp_of_empty finite_rhs_def) + next + from Inv_ES ES_single show "finite xrhs" + by (simp add:Inv_def finite_rhs_def) + qed + finally show ?thesis by simp + qed + thus ?thesis by auto +qed + +lemma every_eqcl_has_reg: + assumes finite_CS: "finite (UNIV // (\Lang))" + and X_in_CS: "X \ (UNIV // (\Lang))" + shows "\ (reg::rexp). L reg = X" (is "\ r. ?E r") +proof - + from X_in_CS have "\ xrhs. (X, xrhs) \ (eqs (UNIV // (\Lang)))" + by (auto simp:eqs_def init_rhs_def) + then obtain ES xrhs where Inv_ES: "Inv ES" + and X_in_ES: "(X, xrhs) \ ES" + and card_ES: "card ES = 1" + using finite_CS X_in_CS init_ES_satisfy_Inv iteration_conc + by blast + hence ES_single_equa: "ES = {(X, xrhs)}" + by (auto simp:Inv_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) + thus ?thesis using Inv_ES + by (rule last_cl_exists_rexp) +qed + +lemma finals_in_partitions: + "finals Lang \ (UNIV // (\Lang))" + by (auto simp:finals_def quotient_def) + +theorem hard_direction: + assumes finite_CS: "finite (UNIV // (\Lang))" + shows "\ (reg::rexp). Lang = L reg" +proof - + have "\ X \ (UNIV // (\Lang)). \ (reg::rexp). X = L reg" + using finite_CS every_eqcl_has_reg by blast + then obtain f + where f_prop: "\ X \ (UNIV // (\Lang)). X = L ((f X)::rexp)" + by (auto dest:bchoice) + def rs \ "f ` (finals Lang)" + have "Lang = \ (finals Lang)" using lang_is_union_of_finals by auto + also have "\ = L (folds ALT NULL rs)" + proof - + have "finite rs" + proof - + have "finite (finals Lang)" + using finite_CS finals_in_partitions[of "Lang"] + by (erule_tac finite_subset, simp) + thus ?thesis using rs_def by auto + qed + thus ?thesis + using f_prop rs_def finals_in_partitions[of "Lang"] by auto + qed + finally show ?thesis by blast +qed + +section {* Direction: @{text "regular language \finite partition"} *} + +subsection {* The scheme for this direction *} + +text {* + The following convenient notation @{text "x \Lang y"} means: + string @{text "x"} and @{text "y"} are equivalent with respect to + language @{text "Lang"}. + *} + +definition + str_eq ("_ \_ _") +where + "x \Lang y \ (x, y) \ (\Lang)" + +text {* + The very basic scheme to show the finiteness of the partion generated by a language @{text "Lang"} + is by attaching tags to every string. The set of tags are carfully choosen to make it finite. + If it can be proved that strings with the same tag are equivlent with respect @{text "Lang"}, + then the partition given rise by @{text "Lang"} must be finite. The reason for this is a lemma + in standard library (@{text "finite_imageD"}), which says: if the image of an injective + function on a set @{text "A"} is finite, then @{text "A"} is finite. It can be shown that + the function obtained by llifting @{text "tag"} + to the level of equalent classes (i.e. @{text "((op `) tag)"}) is injective + (by lemma @{text "tag_image_injI"}) and the image of this function is finite + (with the help of lemma @{text "finite_tag_imageI"}). This argument is formalized + by the following lemma @{text "tag_finite_imageD"}. + *} + +lemma tag_finite_imageD: + assumes str_inj: "\ m n. tag m = tag (n::string) \ m \lang n" + and range: "finite (range tag)" + shows "finite (UNIV // (\lang))" +proof (rule_tac f = "(op `) tag" in finite_imageD) + show "finite (op ` tag ` UNIV // \lang)" using range + apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset) + by (auto simp add:image_def Pow_def) +next + show "inj_on (op ` tag) (UNIV // \lang)" + proof- + { fix X Y + assume X_in: "X \ UNIV // \lang" + and Y_in: "Y \ UNIV // \lang" + and tag_eq: "tag ` X = tag ` Y" + then obtain x y where "x \ X" and "y \ Y" and "tag x = tag y" + unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def + apply simp by blast + with X_in Y_in str_inj[of x y] + have "X = Y" by (auto simp:quotient_def str_eq_rel_def str_eq_def) + } thus ?thesis unfolding inj_on_def by auto + qed +qed + +subsection {* Lemmas for basic cases *} + +text {* + The the final result of this direction is in @{text "easier_direction"}, which + is an induction on the structure of regular expressions. There is one case + for each regular expression operator. For basic operators such as @{text "NULL, EMPTY, CHAR c"}, + the finiteness of their language partition can be established directly with no need + of taggiing. This section contains several technical lemma for these base cases. + + The inductive cases involve operators @{text "ALT, SEQ"} and @{text "STAR"}. + Tagging functions need to be defined individually for each of them. There will be one + dedicated section for each of these cases, and each section goes virtually the same way: + gives definition of the tagging function and prove that strings + with the same tag are equivalent. + *} + +lemma quot_empty_subset: + "UNIV // (\{[]}) \ {{[]}, UNIV - {[]}}" +proof + fix x + assume "x \ UNIV // \{[]}" + then obtain y where h: "x = {z. (y, z) \ \{[]}}" + unfolding quotient_def Image_def by blast + show "x \ {{[]}, UNIV - {[]}}" + proof (cases "y = []") + case True with h + have "x = {[]}" by (auto simp:str_eq_rel_def) + thus ?thesis by simp + next + case False with h + have "x = UNIV - {[]}" by (auto simp:str_eq_rel_def) + thus ?thesis by simp + qed +qed + +lemma quot_char_subset: + "UNIV // (\{[c]}) \ {{[]},{[c]}, UNIV - {[], [c]}}" +proof + fix x + assume "x \ UNIV // \{[c]}" + then obtain y where h: "x = {z. (y, z) \ \{[c]}}" + unfolding quotient_def Image_def by blast + show "x \ {{[]},{[c]}, UNIV - {[], [c]}}" + proof - + { assume "y = []" hence "x = {[]}" using h + by (auto simp:str_eq_rel_def) + } moreover { + assume "y = [c]" hence "x = {[c]}" using h + by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_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) + } ultimately show ?thesis by blast + qed +qed + +subsection {* The case for @{text "SEQ"}*} + +definition + "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \ + ((\L\<^isub>1) `` {x}, {(\L\<^isub>2) `` {x - xa}| xa. xa \ x \ xa \ L\<^isub>1})" + +lemma tag_str_seq_range_finite: + "\finite (UNIV // \L\<^isub>1); finite (UNIV // \L\<^isub>2)\ + \ finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))" +apply (rule_tac B = "(UNIV // \L\<^isub>1) \ (Pow (UNIV // \L\<^isub>2))" in finite_subset) +by (auto simp:tag_str_SEQ_def Image_def quotient_def split:if_splits) + +lemma append_seq_elim: + assumes "x @ y \ L\<^isub>1 ;; L\<^isub>2" + shows "(\ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ y \ L\<^isub>2) \ + (\ ya \ y. (x @ ya) \ L\<^isub>1 \ (y - ya) \ L\<^isub>2)" +proof- + from assms obtain s\<^isub>1 s\<^isub>2 + where "x @ y = s\<^isub>1 @ s\<^isub>2" + and in_seq: "s\<^isub>1 \ L\<^isub>1 \ s\<^isub>2 \ L\<^isub>2" + by (auto simp:Seq_def) + hence "(x \ s\<^isub>1 \ (s\<^isub>1 - x) @ s\<^isub>2 = y) \ (s\<^isub>1 \ x \ (x - s\<^isub>1) @ y = s\<^isub>2)" + using app_eq_dest by auto + moreover have "\x \ s\<^isub>1; (s\<^isub>1 - x) @ s\<^isub>2 = y\ \ + \ ya \ y. (x @ ya) \ L\<^isub>1 \ (y - ya) \ L\<^isub>2" + using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE) + moreover have "\s\<^isub>1 \ x; (x - s\<^isub>1) @ y = s\<^isub>2\ \ + \ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ y \ L\<^isub>2" + using in_seq by (rule_tac x = s\<^isub>1 in exI, auto) + ultimately show ?thesis by blast +qed + +lemma tag_str_SEQ_injI: + "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \ m \(L\<^isub>1 ;; L\<^isub>2) n" +proof- + { fix x y z + assume xz_in_seq: "x @ z \ L\<^isub>1 ;; L\<^isub>2" + and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y" + have"y @ z \ L\<^isub>1 ;; L\<^isub>2" + proof- + have "(\ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ z \ L\<^isub>2) \ + (\ za \ z. (x @ za) \ L\<^isub>1 \ (z - za) \ L\<^isub>2)" + using xz_in_seq append_seq_elim by simp + moreover { + fix xa + assume h1: "xa \ x" and h2: "xa \ L\<^isub>1" and h3: "(x - xa) @ z \ L\<^isub>2" + obtain ya where "ya \ y" and "ya \ L\<^isub>1" and "(y - ya) @ z \ L\<^isub>2" + proof - + have "\ ya. ya \ y \ ya \ L\<^isub>1 \ (x - xa) \L\<^isub>2 (y - ya)" + proof - + have "{\L\<^isub>2 `` {x - xa} |xa. xa \ x \ xa \ L\<^isub>1} = + {\L\<^isub>2 `` {y - xa} |xa. xa \ y \ xa \ L\<^isub>1}" + (is "?Left = ?Right") + using h1 tag_xy by (auto simp:tag_str_SEQ_def) + moreover have "\L\<^isub>2 `` {x - xa} \ ?Left" using h1 h2 by auto + ultimately have "\L\<^isub>2 `` {x - xa} \ ?Right" by simp + thus ?thesis by (auto simp:Image_def str_eq_rel_def str_eq_def) + qed + with prems show ?thesis by (auto simp:str_eq_rel_def str_eq_def) + qed + hence "y @ z \ L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def) + } moreover { + fix za + assume h1: "za \ z" and h2: "(x @ za) \ L\<^isub>1" and h3: "z - za \ L\<^isub>2" + hence "y @ za \ L\<^isub>1" + proof- + have "\L\<^isub>1 `` {x} = \L\<^isub>1 `` {y}" + using h1 tag_xy by (auto simp:tag_str_SEQ_def) + with h2 show ?thesis + by (auto simp:Image_def str_eq_rel_def str_eq_def) + qed + with h1 h3 have "y @ z \ L\<^isub>1 ;; L\<^isub>2" + by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE) + } + ultimately show ?thesis by blast + qed + } thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \ m \(L\<^isub>1 ;; L\<^isub>2) n" + by (auto simp add: str_eq_def str_eq_rel_def) +qed + +lemma quot_seq_finiteI: + "\finite (UNIV // \L\<^isub>1); finite (UNIV // \L\<^isub>2)\ + \ finite (UNIV // \(L\<^isub>1 ;; L\<^isub>2))" + apply (rule_tac tag = "tag_str_SEQ L\<^isub>1 L\<^isub>2" in tag_finite_imageD) + by (auto intro:tag_str_SEQ_injI elim:tag_str_seq_range_finite) + +subsection {* The case for @{text "ALT"} *} + +definition + "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \ ((\L\<^isub>1) `` {x}, (\L\<^isub>2) `` {x})" + +lemma quot_union_finiteI: + assumes finite1: "finite (UNIV // \(L\<^isub>1::string set))" + and finite2: "finite (UNIV // \L\<^isub>2)" + shows "finite (UNIV // \(L\<^isub>1 \ L\<^isub>2))" +proof (rule_tac tag = "tag_str_ALT L\<^isub>1 L\<^isub>2" in tag_finite_imageD) + show "\m n. tag_str_ALT L\<^isub>1 L\<^isub>2 m = tag_str_ALT L\<^isub>1 L\<^isub>2 n \ m \(L\<^isub>1 \ L\<^isub>2) n" + unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by auto +next + show "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" using finite1 finite2 + apply (rule_tac B = "(UNIV // \L\<^isub>1) \ (UNIV // \L\<^isub>2)" in finite_subset) + by (auto simp:tag_str_ALT_def Image_def quotient_def) +qed + +subsection {* + The case for @{text "STAR"} + *} + +text {* + This turned out to be the trickiest case. + *} (* I will make some illustrations for it. *) + +definition + "tag_str_STAR L\<^isub>1 x \ {(\L\<^isub>1) `` {x - xa} | xa. xa < x \ xa \ L\<^isub>1\}" + +lemma finite_set_has_max: "\finite A; A \ {}\ \ + (\ max \ A. \ a \ A. f a <= (f max :: nat))" +proof (induct rule:finite.induct) + case emptyI thus ?case by simp +next + case (insertI A a) + show ?case + proof (cases "A = {}") + case True thus ?thesis by (rule_tac x = a in bexI, auto) + next + case False + with prems obtain max + where h1: "max \ A" + and h2: "\a\A. f a \ f max" by blast + show ?thesis + proof (cases "f a \ f max") + assume "f a \ f max" + with h1 h2 show ?thesis by (rule_tac x = max in bexI, auto) + next + assume "\ (f a \ f max)" + thus ?thesis using h2 by (rule_tac x = a in bexI, auto) + qed + qed +qed + +lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}" +apply (induct x rule:rev_induct, simp) +apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \ {xs}") +by (auto simp:strict_prefix_def) + + +lemma tag_str_star_range_finite: + "finite (UNIV // \L\<^isub>1) \ finite (range (tag_str_STAR L\<^isub>1))" +apply (rule_tac B = "Pow (UNIV // \L\<^isub>1)" in finite_subset) +by (auto simp:tag_str_STAR_def Image_def + quotient_def split:if_splits) + +lemma tag_str_STAR_injI: + "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \ m \(L\<^isub>1\) n" +proof- + { fix x y z + assume xz_in_star: "x @ z \ L\<^isub>1\" + and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y" + have "y @ z \ L\<^isub>1\" + proof(cases "x = []") + case True + with tag_xy have "y = []" + by (auto simp:tag_str_STAR_def strict_prefix_def) + thus ?thesis using xz_in_star True by simp + next + case False + obtain x_max + where h1: "x_max < x" + and h2: "x_max \ L\<^isub>1\" + and h3: "(x - x_max) @ z \ L\<^isub>1\" + and h4:"\ xa < x. xa \ L\<^isub>1\ \ (x - xa) @ z \ L\<^isub>1\ + \ length xa \ length x_max" + proof- + let ?S = "{xa. xa < x \ xa \ L\<^isub>1\ \ (x - xa) @ z \ L\<^isub>1\}" + have "finite ?S" + by (rule_tac B = "{xa. xa < x}" in finite_subset, + auto simp:finite_strict_prefix_set) + moreover have "?S \ {}" using False xz_in_star + by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def) + ultimately have "\ max \ ?S. \ a \ ?S. length a \ length max" + using finite_set_has_max by blast + with prems show ?thesis by blast + qed + obtain ya + where h5: "ya < y" and h6: "ya \ L\<^isub>1\" and h7: "(x - x_max) \L\<^isub>1 (y - ya)" + proof- + from tag_xy have "{\L\<^isub>1 `` {x - xa} |xa. xa < x \ xa \ L\<^isub>1\} = + {\L\<^isub>1 `` {y - xa} |xa. xa < y \ xa \ L\<^isub>1\}" (is "?left = ?right") + by (auto simp:tag_str_STAR_def) + moreover have "\L\<^isub>1 `` {x - x_max} \ ?left" using h1 h2 by auto + ultimately have "\L\<^isub>1 `` {x - x_max} \ ?right" by simp + with prems show ?thesis apply + (simp add:Image_def str_eq_rel_def str_eq_def) by blast + qed + have "(y - ya) @ z \ L\<^isub>1\" + proof- + from h3 h1 obtain a b where a_in: "a \ L\<^isub>1" + and a_neq: "a \ []" and b_in: "b \ L\<^isub>1\" + and ab_max: "(x - x_max) @ z = a @ b" + by (drule_tac star_decom, auto simp:strict_prefix_def elim:prefixE) + have "(x - x_max) \ a \ (a - (x - x_max)) @ b = z" + proof - + have "((x - x_max) \ a \ (a - (x - x_max)) @ b = z) \ + (a < (x - x_max) \ ((x - x_max) - a) @ z = b)" + using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def) + moreover { + assume np: "a < (x - x_max)" and b_eqs: " ((x - x_max) - a) @ z = b" + have "False" + proof - + let ?x_max' = "x_max @ a" + have "?x_max' < x" + using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) + moreover have "?x_max' \ L\<^isub>1\" + using a_in h2 by (simp add:star_intro3) + moreover have "(x - ?x_max') @ z \ L\<^isub>1\" + using b_eqs b_in np h1 by (simp add:diff_diff_appd) + moreover have "\ (length ?x_max' \ length x_max)" + using a_neq by simp + ultimately show ?thesis using h4 by blast + qed + } ultimately show ?thesis by blast + qed + then obtain za where z_decom: "z = za @ b" + and x_za: "(x - x_max) @ za \ L\<^isub>1" + using a_in by (auto elim:prefixE) + from x_za h7 have "(y - ya) @ za \ L\<^isub>1" + by (auto simp:str_eq_def str_eq_rel_def) + with z_decom b_in show ?thesis by (auto dest!:step[of "(y - ya) @ za"]) + qed + with h5 h6 show ?thesis + by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) + qed + } thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \ m \(L\<^isub>1\) n" + by (auto simp add:str_eq_def str_eq_rel_def) +qed + +lemma quot_star_finiteI: + "finite (UNIV // \L\<^isub>1) \ finite (UNIV // \(L\<^isub>1\))" + apply (rule_tac tag = "tag_str_STAR L\<^isub>1" in tag_finite_imageD) + by (auto intro:tag_str_STAR_injI elim:tag_str_star_range_finite) + +subsection {* + The main lemma + *} + +lemma easier_directio\: + "Lang = L (r::rexp) \ finite (UNIV // (\Lang))" +proof (induct arbitrary:Lang rule:rexp.induct) + case NULL + have "UNIV // (\{}) \ {UNIV} " + by (auto simp:quotient_def str_eq_rel_def str_eq_def) + with prems show "?case" by (auto intro:finite_subset) +next + case EMPTY + have "UNIV // (\{[]}) \ {{[]}, UNIV - {[]}}" + by (rule quot_empty_subset) + with prems show ?case by (auto intro:finite_subset) +next + case (CHAR c) + have "UNIV // (\{[c]}) \ {{[]},{[c]}, UNIV - {[], [c]}}" + by (rule quot_char_subset) + with prems show ?case by (auto intro:finite_subset) +next + case (SEQ r\<^isub>1 r\<^isub>2) + have "\finite (UNIV // \(L r\<^isub>1)); finite (UNIV // \(L r\<^isub>2))\ + \ finite (UNIV // \(L r\<^isub>1 ;; L r\<^isub>2))" + by (erule quot_seq_finiteI, simp) + with prems show ?case by simp +next + case (ALT r\<^isub>1 r\<^isub>2) + have "\finite (UNIV // \(L r\<^isub>1)); finite (UNIV // \(L r\<^isub>2))\ + \ finite (UNIV // \(L r\<^isub>1 \ L r\<^isub>2))" + by (erule quot_union_finiteI, simp) + with prems show ?case by simp +next + case (STAR r) + have "finite (UNIV // \(L r)) + \ finite (UNIV // \((L r)\))" + by (erule quot_star_finiteI) + with prems show ?case by simp +qed + +end + diff -r f5db9e08effc -r b6815473ee2e Prefix_subtract.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Prefix_subtract.thy Tue Jan 25 12:14:31 2011 +0000 @@ -0,0 +1,58 @@ +theory Prefix_subtract + imports Main List_Prefix +begin + +section {* A small theory of prefix subtraction *} + +text {* + The notion of @{text "prefix_subtract"} is need to make proofs more readable. + *} + +fun prefix_subtract :: "'a list \ 'a list \ 'a list" (infix "-" 51) +where + "prefix_subtract [] xs = []" +| "prefix_subtract (x#xs) [] = x#xs" +| "prefix_subtract (x#xs) (y#ys) = (if x = y then prefix_subtract xs ys else (x#xs))" + +lemma [simp]: "(x @ y) - x = y" +apply (induct x) +by (case_tac y, simp+) + +lemma [simp]: "x - x = []" +by (induct x, auto) + +lemma [simp]: "x = xa @ y \ x - xa = y " +by (induct x, auto) + +lemma [simp]: "x - [] = x" +by (induct x, auto) + +lemma [simp]: "(x - y = []) \ (x \ y)" +proof- + have "\xa. x = xa @ (x - y) \ xa \ y" + apply (rule prefix_subtract.induct[of _ x y], simp+) + by (clarsimp, rule_tac x = "y # xa" in exI, simp+) + thus "(x - y = []) \ (x \ y)" by simp +qed + +lemma diff_prefix: + "\c \ a - b; b \ a\ \ b @ c \ a" +by (auto elim:prefixE) + +lemma diff_diff_appd: + "\c < a - b; b < a\ \ (a - b) - c = a - (b @ c)" +apply (clarsimp simp:strict_prefix_def) +by (drule diff_prefix, auto elim:prefixE) + +lemma app_eq_cases[rule_format]: + "\ x . x @ y = m @ n \ (x \ m \ m \ x)" +apply (induct y, simp) +apply (clarify, drule_tac x = "x @ [a]" in spec) +by (clarsimp, auto simp:prefix_def) + +lemma app_eq_dest: + "x @ y = m @ n \ + (x \ m \ (m - x) @ n = y) \ (m \ x \ (x - m) @ y = n)" +by (frule_tac app_eq_cases, auto elim:prefixE) + +end diff -r f5db9e08effc -r b6815473ee2e tphols-2011/ROOT.ML --- a/tphols-2011/ROOT.ML Mon Jan 24 11:29:55 2011 +0000 +++ b/tphols-2011/ROOT.ML Tue Jan 25 12:14:31 2011 +0000 @@ -2,4 +2,4 @@ no_document use_thys ["This_Theory1", "This_Theory2"]; use_thys ["That_Theory1", "That_Theory2", "That_Theory3"]; *) -use_thys ["../Myhill"];; + use_thys ["../Prefix_subtract", "../Myhill"];