# HG changeset patch # User Christian Urban # Date 1373041157 -3600 # Node ID 8c4b6fb43ebee0033a7e95ce85482cf5aa1ef0eb # Parent a0bcf886b8efce482faa9b5a1cdde7c086f83819 polished more and updated to new isabelle diff -r a0bcf886b8ef -r 8c4b6fb43ebe Closures.thy --- a/Closures.thy Fri Jul 05 12:07:48 2013 +0100 +++ b/Closures.thy Fri Jul 05 17:19:17 2013 +0100 @@ -156,7 +156,7 @@ from assms obtain r::"'a rexp" where eq: "lang r = A" by auto have fin: "finite (pderivs_lang B r)" by (rule finite_pderivs_lang) - have "Deriv_lang B (lang r) = (\ lang ` (pderivs_lang B r))" + have "Deriv_lang B (lang r) = (\ (lang ` (pderivs_lang B r)))" by (simp add: Derivs_pderivs pderivs_lang_def) also have "\ = lang (\(pderivs_lang B r))" using fin by simp finally have "Deriv_lang B A = lang (\(pderivs_lang B r))" using eq diff -r a0bcf886b8ef -r 8c4b6fb43ebe Derivatives.thy --- a/Derivatives.thy Fri Jul 05 12:07:48 2013 +0100 +++ b/Derivatives.thy Fri Jul 05 17:19:17 2013 +0100 @@ -8,83 +8,9 @@ text{* This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}. *} -subsection {* Left-Quotients of languages *} - -definition Deriv :: "'a \ 'a lang \ 'a lang" -where "Deriv x A = { xs. x#xs \ A }" - -definition Derivs :: "'a list \ 'a lang \ 'a lang" -where "Derivs xs A = { ys. xs @ ys \ A }" - -abbreviation - Derivss :: "'a list \ 'a lang set \ 'a lang" -where - "Derivss s As \ \ (Derivs s) ` As" - - -lemma Deriv_empty[simp]: "Deriv a {} = {}" - and Deriv_epsilon[simp]: "Deriv a {[]} = {}" - and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})" - and Deriv_union[simp]: "Deriv a (A \ B) = Deriv a A \ Deriv a B" -by (auto simp: Deriv_def) - -lemma Deriv_conc_subset: -"Deriv a A @@ B \ Deriv a (A @@ B)" (is "?L \ ?R") -proof - fix w assume "w \ ?L" - then obtain u v where "w = u @ v" "a # u \ A" "v \ B" - by (auto simp: Deriv_def) - then have "a # w \ A @@ B" - by (auto intro: concI[of "a # u", simplified]) - thus "w \ ?R" by (auto simp: Deriv_def) -qed - -lemma Der_conc [simp]: - shows "Deriv c (A @@ B) = (Deriv c A) @@ B \ (if [] \ A then Deriv c B else {})" -unfolding Deriv_def conc_def -by (auto simp add: Cons_eq_append_conv) - -lemma Deriv_star [simp]: - shows "Deriv c (star A) = (Deriv c A) @@ star A" -proof - - have incl: "[] \ A \ Deriv c (star A) \ (Deriv c A) @@ star A" - unfolding Deriv_def conc_def - apply(auto simp add: Cons_eq_append_conv) - apply(drule star_decom) - apply(auto simp add: Cons_eq_append_conv) - done - - have "Deriv c (star A) = Deriv c (A @@ star A \ {[]})" - by (simp only: star_unfold_left[symmetric]) - also have "... = Deriv c (A @@ star A)" - by (simp only: Deriv_union) (simp) - also have "... = (Deriv c A) @@ (star A) \ (if [] \ A then Deriv c (star A) else {})" - by simp - also have "... = (Deriv c A) @@ star A" - using incl by auto - finally show "Deriv c (star A) = (Deriv c A) @@ star A" . -qed - -lemma Derivs_simps [simp]: - shows "Derivs [] A = A" - and "Derivs (c # s) A = Derivs s (Deriv c A)" - and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)" -unfolding Derivs_def Deriv_def by auto - - subsection {* Brozowski's derivatives of regular expressions *} fun - nullable :: "'a rexp \ bool" -where - "nullable (Zero) = False" -| "nullable (One) = True" -| "nullable (Atom c) = False" -| "nullable (Plus r1 r2) = (nullable r1 \ nullable r2)" -| "nullable (Times r1 r2) = (nullable r1 \ nullable r2)" -| "nullable (Star r) = True" - -fun deriv :: "'a \ 'a rexp \ 'a rexp" where "deriv c (Zero) = Zero" @@ -102,23 +28,26 @@ | "derivs (c # s) r = derivs s (deriv c r)" -lemma nullable_iff: - shows "nullable r \ [] \ lang r" -by (induct r) (auto simp add: conc_def split: if_splits) - -lemma Deriv_deriv: - shows "Deriv c (lang r) = lang (deriv c r)" +lemma lang_deriv: "lang (deriv c r) = Deriv c (lang r)" by (induct r) (simp_all add: nullable_iff) -lemma Derivs_derivs: - shows "Derivs s (lang r) = lang (derivs s r)" -by (induct s arbitrary: r) (simp_all add: Deriv_deriv) +lemma lang_derivs: "lang (derivs s r) = Derivs s (lang r)" +by (induct s arbitrary: r) (simp_all add: lang_deriv) + +text {* A regular expression matcher: *} + +definition matcher :: "'a rexp \ 'a list \ bool" where +"matcher r s = nullable (derivs s r)" + +lemma matcher_correctness: "matcher r s \ s \ lang r" +by (induct s arbitrary: r) + (simp_all add: nullable_iff lang_deriv matcher_def Deriv_def) subsection {* Antimirov's partial derivatives *} abbreviation - "Timess rs r \ {Times r' r | r'. r' \ rs}" + "Timess rs r \ (\r' \ rs. {Times r' r})" fun pderiv :: "'a \ 'a rexp \ 'a rexp set" @@ -135,20 +64,20 @@ pderivs :: "'a list \ 'a rexp \ ('a rexp) set" where "pderivs [] r = {r}" -| "pderivs (c # s) r = \ (pderivs s) ` (pderiv c r)" +| "pderivs (c # s) r = \ (pderivs s ` pderiv c r)" abbreviation pderiv_set :: "'a \ 'a rexp set \ 'a rexp set" where - "pderiv_set c rs \ \ pderiv c ` rs" + "pderiv_set c rs \ \ (pderiv c ` rs)" abbreviation pderivs_set :: "'a list \ 'a rexp set \ 'a rexp set" where - "pderivs_set s rs \ \ (pderivs s) ` rs" + "pderivs_set s rs \ \ (pderivs s ` rs)" lemma pderivs_append: - "pderivs (s1 @ s2) r = \ (pderivs s2) ` (pderivs s1 r)" + "pderivs (s1 @ s2) r = \ (pderivs s2 ` pderivs s1 r)" by (induct s1 arbitrary: r) (simp_all) lemma pderivs_snoc: @@ -168,33 +97,33 @@ subsection {* Relating left-quotients and partial derivatives *} lemma Deriv_pderiv: - shows "Deriv c (lang r) = \ lang ` (pderiv c r)" + shows "Deriv c (lang r) = \ (lang ` pderiv c r)" by (induct r) (auto simp add: nullable_iff conc_UNION_distrib) lemma Derivs_pderivs: - shows "Derivs s (lang r) = \ lang ` (pderivs s r)" + shows "Derivs s (lang r) = \ (lang ` pderivs s r)" proof (induct s arbitrary: r) case (Cons c s) - have ih: "\r. Derivs s (lang r) = \ lang ` (pderivs s r)" by fact + have ih: "\r. Derivs s (lang r) = \ (lang ` pderivs s r)" by fact have "Derivs (c # s) (lang r) = Derivs s (Deriv c (lang r))" by simp - also have "\ = Derivs s (\ lang ` (pderiv c r))" by (simp add: Deriv_pderiv) + also have "\ = Derivs s (\ (lang ` pderiv c r))" by (simp add: Deriv_pderiv) also have "\ = Derivss s (lang ` (pderiv c r))" by (auto simp add: Derivs_def) - also have "\ = \ lang ` (pderivs_set s (pderiv c r))" + also have "\ = \ (lang ` (pderivs_set s (pderiv c r)))" using ih by auto - also have "\ = \ lang ` (pderivs (c # s) r)" by simp - finally show "Derivs (c # s) (lang r) = \ lang ` pderivs (c # s) r" . + also have "\ = \ (lang ` (pderivs (c # s) r))" by simp + finally show "Derivs (c # s) (lang r) = \ (lang ` pderivs (c # s) r)" . qed (simp add: Derivs_def) subsection {* Relating derivatives and partial derivatives *} lemma deriv_pderiv: - shows "(\ lang ` (pderiv c r)) = lang (deriv c r)" -unfolding Deriv_deriv[symmetric] Deriv_pderiv by simp + shows "\ (lang ` (pderiv c r)) = lang (deriv c r)" +unfolding lang_deriv Deriv_pderiv by simp lemma derivs_pderivs: - shows "(\ lang ` (pderivs s r)) = lang (derivs s r)" -unfolding Derivs_derivs[symmetric] Derivs_pderivs by simp + shows "\ (lang ` (pderivs s r)) = lang (derivs s r)" +unfolding lang_derivs Derivs_pderivs by simp subsection {* Finiteness property of partial derivatives *} @@ -272,7 +201,7 @@ have "pderivs (s @ [c]) (Times r1 r2) = pderiv_set c (pderivs s (Times r1 r2))" by (simp add: pderivs_snoc) also have "\ \ pderiv_set c (Timess (pderivs s r1) r2 \ (pderivs_lang (PSuf s) r2))" - using ih by (auto) (blast) + using ih by fast also have "\ = pderiv_set c (Timess (pderivs s r1) r2) \ pderiv_set c (pderivs_lang (PSuf s) r2)" by (simp) also have "\ = pderiv_set c (Timess (pderivs s r1) r2) \ pderivs_lang (PSuf s @@ {[c]}) r2" @@ -282,7 +211,7 @@ by auto also have "\ \ Timess (pderiv_set c (pderivs s r1)) r2 \ pderiv c r2 \ pderivs_lang (PSuf s @@ {[c]}) r2" - by (auto simp add: if_splits) (blast) + by (auto simp add: if_splits) also have "\ = Timess (pderivs (s @ [c]) r1) r2 \ pderiv c r2 \ pderivs_lang (PSuf s @@ {[c]}) r2" by (simp add: pderivs_snoc) also have "\ \ Timess (pderivs (s @ [c]) r1) r2 \ pderivs_lang (PSuf (s @ [c])) r2" @@ -319,9 +248,9 @@ { assume asm: "s \ []" have "pderivs (s @ [c]) (Star r) = pderiv_set c (pderivs s (Star r))" by (simp add: pderivs_snoc) also have "\ \ pderiv_set c (Timess (pderivs_lang (PSuf s) r) (Star r))" - using ih[OF asm] by (auto) (blast) + using ih[OF asm] by fast also have "\ \ Timess (pderiv_set c (pderivs_lang (PSuf s) r)) (Star r) \ pderiv c (Star r)" - by (auto split: if_splits) (blast)+ + by (auto split: if_splits) also have "\ \ Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r) \ (Timess (pderiv c r) (Star r))" by (simp only: PSuf_snoc pderivs_lang_snoc pderivs_lang_union) (auto simp add: pderivs_lang_def) @@ -331,11 +260,7 @@ } moreover { assume asm: "s = []" - then have ?case - apply (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def) - apply(rule_tac x = "[c]" in exI) - apply(auto) - done + then have ?case by (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def) } ultimately show ?case by blast qed (simp) @@ -377,18 +302,4 @@ shows "finite (pderivs_lang A r)" by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV) - -subsection {* A regular expression matcher based on Brozowski's derivatives *} - -fun - matcher :: "'a rexp \ 'a list \ bool" -where - "matcher r s = nullable (derivs s r)" - -lemma matcher_correctness: - shows "matcher r s \ s \ lang r" -by (induct s arbitrary: r) - (simp_all add: nullable_iff Deriv_deriv[symmetric] Deriv_def) - - end \ No newline at end of file diff -r a0bcf886b8ef -r 8c4b6fb43ebe Journal/Paper.thy --- a/Journal/Paper.thy Fri Jul 05 12:07:48 2013 +0100 +++ b/Journal/Paper.thy Fri Jul 05 17:19:17 2013 +0100 @@ -3,6 +3,18 @@ imports "../Closures2" "../Attic/Prefix_subtract" begin +lemma nullable_iff: + shows "nullable r \ [] \ lang r" +by (induct r) (auto simp add: conc_def split: if_splits) + +lemma Deriv_deriv: + shows "Deriv c (lang r) = lang (deriv c r)" +by (induct r) (simp_all add: nullable_iff) + +lemma Derivs_derivs: + shows "Derivs s (lang r) = lang (derivs s r)" +by (induct s arbitrary: r) (simp_all add: Deriv_deriv) + declare [[show_question_marks = false]] consts @@ -218,7 +230,7 @@ A popular choice for a theorem prover would be one based on Higher-Order Logic (HOL), for example HOL4, HOLlight or Isabelle/HOL. For the development - presented in this paper we will use the Isabelle/HOL. HOL is a predicate calculus + presented in this paper we will use the Isabelle/HOL system. HOL is a predicate calculus that allows quantification over predicate variables. Its type system is based on the Simple Theory of Types by \citeN{Church40}. Although many mathematical concepts can be conveniently expressed in HOL, there are some @@ -231,10 +243,10 @@ define most notions in terms of them. For example, a regular language is normally defined as: - \begin{dfntn}\label{baddef} + \begin{definition}\label{baddef} A language @{text A} is \emph{regular}, provided there is a finite deterministic automaton that recognises all strings of @{text "A"}. - \end{dfntn} + \end{definition} \noindent This approach has many benefits. Among them is the fact that it is easy to @@ -388,9 +400,9 @@ the link between regular expressions and automata in the context of lexing. \citeN{BerghoferReiter09} use functions as well for formalising automata working over bit strings in the context of Presburger arithmetic. - A Larger formalisation of automata theory, including the Myhill-Nerode theorem, + A larger formalisation of automata theory, including the Myhill-Nerode theorem, was carried out in Nuprl by \citeN{Constable00} which also uses functions. - Other large formailsations of automata theory in Coq are by + Other large formalisations of automata theory in Coq are by \citeN{Filliatre97} who essentially uses graphs and by \citeN{Almeidaetal10} and \citeN{Braibant12}, who both use matrices. Many of these works, like \citeN{Nipkow98} or \citeN{Braibant12}, mention intrinsic problems with @@ -423,24 +435,45 @@ exists an automaton that recognises all its strings, we define a regular language as: - \begin{dfntn}\label{regular} + \begin{definition}\label{regular} A language @{text A} is \emph{regular}, provided there is a regular expression that matches all strings of @{text "A"}. - \end{dfntn} + \end{definition} \noindent - And then `forget' automata completely. - The reason is that regular expressions %, unlike graphs, matrices and - %functions, - can be defined as an inductive datatype and a reasoning - infrastructure for them (like induction and recursion) comes for free in - HOL. %Moreover, no side-conditions will be needed for regular expressions, + We then want to `forget' automata completely and see how far we come + with formalising results from regular language theory. The reason + is that regular expressions, unlike graphs, matrices and + functions, can be defined as an inductive datatype and a reasoning + infrastructure for them (like induction and recursion) comes for + free in HOL. But this question whether formal language theory can be + done without automata crops up also in non-theorem prover + contexts. For example, Gasarch asked in the Computational Complexity + blog by \citeN{GasarchBlog} whether the complementation of + regular-expression languages can be proved without using + automata. He concluded + + \begin{quote} + ``{\it \ldots it can't be done}'' + \end{quote} + + \noindent + and even pondered + + \begin{quote} + ``{\it \ldots [b]ut is there a rigorous way to even state that?}'' + \end{quote} + + %Moreover, no side-conditions will be needed for regular expressions, %like we need for automata. - This convenience of regular expressions has + \noindent + We will give an answer to these questions in this paper. + + The convenience of regular expressions has recently been exploited in HOL4 with a formalisation of regular expression matching based on derivatives by \citeN{OwensSlind08}, and with an equivalence checker for regular expressions in Isabelle/HOL by \citeN{KraussNipkow11} - and in Matida by \citeN{Asperti12} and in Coq by \citeN{CoquandSiles12}. The + and in Matita by \citeN{Asperti12} and in Coq by \citeN{CoquandSiles12}. The main purpose of this paper is to show that a central result about regular languages---the Myhill-Nerode Theorem---can be recreated by only using regular expressions. This theorem gives necessary and sufficient conditions @@ -458,13 +491,13 @@ an argument about solving equational systems. This argument appears to be folklore. For the other part, we give two proofs: one direct proof using certain tagging-functions, and another indirect proof using Antimirov's - partial derivatives \citeyear{Antimirov95}. Again to our best knowledge, the + partial derivatives (\citeyear{Antimirov95}). Again to our best knowledge, the tagging-functions have not been used before for establishing the Myhill-Nerode Theorem. Derivatives of regular expressions have been used recently quite widely in the literature; partial derivatives, in contrast, attract much less attention. However, partial derivatives are more suitable in the - context of the Myhill-Nerode Theorem, since it is easier to establish - formally their finiteness result. We are not aware of any proof that uses + context of the Myhill-Nerode Theorem, since it is easier to + formally establish their finiteness result. We are not aware of any proof that uses either of them for proving the Myhill-Nerode Theorem. *} @@ -499,16 +532,16 @@ In the paper we will make use of the following properties of these constructions. - \begin{prpstn}\label{langprops}\mbox{}\\ + \begin{proposition}\label{langprops}\mbox{}\\ \begin{tabular}{@ {}lp{10cm}} (i) & @{thm star_unfold_left} \\ (ii) & @{thm[mode=IfThen] pow_length}\\ (iii) & @{thm conc_Union_left} \\ (iv) & If @{thm (prem 1) star_decom} and @{thm (prem 2) star_decom} then there exists an @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{text "x = x\<^isub>p @ x\<^isub>s"} - and @{term "x\<^isub>p \ []"} such that @{term "x\<^isub>p \ A"} and @{term "x\<^isub>s \ A\"}. + and \mbox{@{term "x\<^isub>p \ []"}} such that @{term "x\<^isub>p \ A"} and @{term "x\<^isub>s \ A\"}. \end{tabular} - \end{prpstn} + \end{proposition} \noindent In @{text "(ii)"} we use the notation @{term "length s"} for the length of a @@ -534,16 +567,19 @@ which solves equations of the form @{term "X = A \ X \ B"} provided @{term "[] \ A"}. However we will need the following `reversed' version of Arden's Lemma (`reversed' in the sense of changing the order of @{term "A \ X"} to - \mbox{@{term "X \ A"}}).\footnote{The details of the proof for the reversed Arden's Lemma - are given in the Appendix.} + \mbox{@{term "X \ A"}}). + %\footnote{The details of the proof for the reversed Arden's Lemma + %are given in the Appendix.} - \begin{lmm}[Reversed Arden's Lemma]\label{arden}\mbox{}\\ + \begin{lemma}[Reversed Arden's Lemma]\label{arden}\mbox{}\\ If @{thm (prem 1) reversed_Arden} then @{thm (lhs) reversed_Arden} if and only if @{thm (rhs) reversed_Arden}. - \end{lmm} + \end{lemma} \noindent + The proof of this reversed version of Arden's lemma follows the proof of the + original version. Regular expressions are defined as the inductive datatype \begin{center} @@ -576,7 +612,7 @@ Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating a regular expression that matches the union of all languages of @{text rs}. - This definion is not trivial in a theorem prover, because @{text rs} (being a set) is unordered, + This definition is not trivial in a theorem prover, because @{text rs} (being a set) is unordered, but the regular expression needs an order. Since we only need to know the existence @@ -607,17 +643,17 @@ text {* \noindent The key definition in the Myhill-Nerode Theorem is the - \emph{Myhill-Nerode Relation}, which states that w.r.t.~a language two - strings are related, provided there is no distinguishing extension in this + \emph{Myhill-Nerode Relation}, which states that two + strings are related w.r.t.~a language, provided there is no distinguishing extension in this language. This can be defined as a ternary relation. - \begin{dfntn}[Myhill-Nerode Relation]\label{myhillneroderel} + \begin{definition}[Myhill-Nerode Relation]\label{myhillneroderel} Given a language @{text A}, two strings @{text x} and @{text y} are Myhill-Nerode related provided \begin{center} @{thm str_eq_def'} \end{center} - \end{dfntn} + \end{definition} \noindent It is easy to see that @{term "\A"} is an equivalence relation, which @@ -640,13 +676,13 @@ that if there are finitely many equivalence classes, like in the example above, then the language is regular. In our setting we therefore have to show: - \begin{thrm}\label{myhillnerodeone} + \begin{theorem}\label{myhillnerodeone} @{thm[mode=IfThen] Myhill_Nerode1} - \end{thrm} + \end{theorem} \noindent To prove this theorem, we first define the set @{term "finals A"} as those equivalence - classes from @{term "UNIV // \A"} that contain strings of @{text A}, namely + classes from \mbox{@{term "UNIV // \A"}} that contain strings of @{text A}, namely % \begin{equation} @{thm finals_def} @@ -683,8 +719,11 @@ \noindent which means that if we append the character @{text c} to the end of all strings in the equivalence class @{text Y}, we obtain a subset of - @{text X}. Note that we do not define an automaton here, we merely relate two sets - (with the help of a character). In our concrete example we have + @{text X}. + %Note that we do not define formally an automaton here, + %we merely relate two sets + %(with the help of a character). + In our concrete example we have @{term "X\<^isub>1 \c\ X\<^isub>2"}, @{term "X\<^isub>1 \d\<^isub>i\ X\<^isub>3"} with @{text "d\<^isub>i"} being any other character than @{text c}, and @{term "X\<^isub>3 \c\<^isub>j\ X\<^isub>3"} for any character @{text "c\<^isub>j"}. @@ -706,7 +745,7 @@ \end{center} \noindent - where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} are pairs consiting of an equivalence class and + where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} are pairs consisting of an equivalence class and a regular expression. In the initial equational system, they stand for all transitions @{term "Y\<^isub>i\<^isub>j \c\<^isub>i\<^isub>j\ X\<^isub>i"}. @@ -796,9 +835,9 @@ for representing the right-hand sides of equations, we can prove \eqref{inv1} and \eqref{inv2} more concisely as % - \begin{lmm}\label{inv} + \begin{lemma}\label{inv} If @{thm (prem 1) test} then @{text "X = \ \ ` rhs"}. - \end{lmm} + \end{lemma} \noindent Our proof of Theorem~\ref{myhillnerodeone} will proceed by transforming the @@ -876,13 +915,13 @@ \noindent This allows us to prove a version of Arden's Lemma on the level of equations. - \begin{lmm}\label{ardenable} + \begin{lemma}\label{ardenable} Given an equation @{text "X = rhs"}. If @{text "X = \\ ` rhs"}, @{thm (prem 2) Arden_preserves_soundness}, and @{thm (prem 3) Arden_preserves_soundness}, then @{text "X = \\ ` (Arden X rhs)"}. - \end{lmm} + \end{lemma} \noindent Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma, @@ -1027,9 +1066,9 @@ It is straightforward to prove that the initial equational system satisfies the invariant. - \begin{lmm}\label{invzero} + \begin{lemma}\label{invzero} @{thm[mode=IfThen] Init_ES_satisfies_invariant} - \end{lmm} + \end{lemma} \begin{proof} Finiteness is given by the assumption and the way how we set up the @@ -1042,12 +1081,12 @@ \noindent Next we show that @{text Iter} preserves the invariant. - \begin{lmm}\label{iterone} If + \begin{lemma}\label{iterone} If @{thm (prem 1) iteration_step_invariant[where xrhs="rhs"]}, @{thm (prem 2) iteration_step_invariant[where xrhs="rhs"]} and @{thm (prem 3) iteration_step_invariant[where xrhs="rhs"]}, then @{thm (concl) iteration_step_invariant[where xrhs="rhs"]}. - \end{lmm} + \end{lemma} \begin{proof} The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated @@ -1079,12 +1118,12 @@ \noindent We also need the fact that @{text Iter} decreases the termination measure. - \begin{lmm}\label{itertwo} If + \begin{lemma}\label{itertwo} If @{thm (prem 1) iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}, @{thm (prem 2) iteration_step_measure[simplified (no_asm), where xrhs="rhs"]} and @{thm (prem 3) iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}, then\\ \mbox{@{thm (concl) iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}}. - \end{lmm} + \end{lemma} \begin{proof} By assumption we know that @{text "ES"} is finite and has more than one element. @@ -1099,11 +1138,11 @@ This brings us to our property we want to establish for @{text Solve}. - \begin{lmm} + \begin{lemma} If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists a @{text rhs} such that @{term "Solve X (Init (UNIV // \A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"}. - \end{lmm} + \end{lemma} \begin{proof} In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly @@ -1119,7 +1158,7 @@ Premise 3 of~\eqref{whileprinciple} is by Lemma~\ref{itertwo}. Now in premise 4 we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"} and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"} - does not holds. By the stronger invariant we know there exists such a @{text "rhs"} + does not hold. By the stronger invariant we know there exists such a @{text "rhs"} with @{term "(X, rhs) \ ES"}. Because @{text Cond} is not true, we know the cardinality of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the set @{text "{(X, rhs)}"}, for which the invariant holds. This allows us to conclude that @@ -1131,9 +1170,9 @@ With this lemma in place we can show that for every equivalence class in @{term "UNIV // \A"} there exists a regular expression. - \begin{lmm}\label{every_eqcl_has_reg} + \begin{lemma}\label{every_eqcl_has_reg} @{thm[mode=IfThen] every_eqcl_has_reg} - \end{lmm} + \end{lemma} \begin{proof} By the preceding lemma, we know that there exists a @{text "rhs"} such @@ -1181,9 +1220,9 @@ In this section we will give a proof for establishing the second part of the Myhill-Nerode Theorem. It can be formulated in our setting as follows: - \begin{thrm}\label{myhillnerodetwo} + \begin{theorem}\label{myhillnerodetwo} Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}. - \end{thrm} + \end{theorem} \noindent The proof will be by induction on the structure of @{text r}. It turns out @@ -1209,7 +1248,7 @@ \noindent Much more interesting, however, are the inductive cases. They seem hard to be solved directly. The reader is invited to try.\footnote{The induction hypothesis is not strong enough - to make any progress with the TIME and STAR cases.} + to make any progress with the @{text TIMES} and @{text STAR} cases.} In order to see how our proof proceeds consider the following suggestive picture given by \citeN{Constable00}: @@ -1250,10 +1289,10 @@ suffices to show in each induction step that another relation, say @{text R}, has finitely many equivalence classes and refines @{term "\(lang r)"}. - \begin{dfntn} + \begin{definition} A relation @{text "R\<^isub>1"} \emph{refines} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \ R\<^isub>2"}. - \end{dfntn} + \end{definition} \noindent For constructing @{text R}, we will rely on some \emph{tagging-functions} @@ -1275,12 +1314,12 @@ as follows. - \begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x} + \begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x} and @{text y} are \emph{tag-related} provided \begin{center} @{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y \ tag x = tag y"}\;. \end{center} - \end{dfntn} + \end{definition} In order to establish finiteness of a set @{text A}, we shall use the following powerful @@ -1295,9 +1334,9 @@ is finite, then the set @{text A} itself must be finite. We can use it to establish the following two lemmas. - \begin{lmm}\label{finone} + \begin{lemma}\label{finone} @{thm[mode=IfThen] finite_eq_tag_rel} - \end{lmm} + \end{lemma} \begin{proof} We set in \eqref{finiteimageD}, @{text f} to be @{text "X \ tag ` X"}. We have @@ -1312,12 +1351,12 @@ with @{thm (concl) finite_eq_tag_rel}. \end{proof} - \begin{lmm}\label{fintwo} + \begin{lemma}\label{fintwo} Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}. If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]} then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}. - \end{lmm} + \end{lemma} \begin{proof} We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to @@ -1368,11 +1407,11 @@ The @{const TIMES}-case is slightly more complicated. We first prove the following lemma, which will aid the proof about refinement. - \begin{lmm}\label{refinement} + \begin{lemma}\label{refinement} The relation @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} refines @{term "\A"}, provided for all strings @{text x}, @{text y} and @{text z} we have that \mbox{@{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y"}} and @{term "x @ z \ A"} imply @{text "y @ z \ A"}. - \end{lmm} + \end{lemma} \noindent @@ -1390,7 +1429,9 @@ refer to @{text "x\<^isub>p"} as the \emph{prefix} of the string @{text x}, and respectively to @{text "x\<^isub>s"} as the \emph{suffix}. +*} +text {* Now assuming @{term "x @ z \ A \ B"}, there are only two possible ways of how to `split' this string to be in @{term "A \ B"}: % @@ -1452,18 +1493,20 @@ \end{tabular} \end{center} % + \noindent Either @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (first picture) or there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (second picture). In both cases we have to show that @{term "y @ z \ A \ B"}. The first case - we will only go through if we know that @{term "x \A y"} holds @{text "(*)"}. Because then + we will only go through if we know that @{term "x \A y"} holds @{text "("}@{text "*"}@{text ")"}. + Because then we can infer from @{term "x @ z\<^isub>p \ A"} that @{term "y @ z\<^isub>p \ A"} holds for all @{text "z\<^isub>p"}. In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is one possible partition of the string @{text x}. We have to know that both @{text "x\<^isub>p"} and the corresponding partition @{text "y\<^isub>p"} are in @{text "A"}, and that @{text "x\<^isub>s"} is `@{text B}-related' - to @{text "y\<^isub>s"} @{text "(**)"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \ B"}. + to @{text "y\<^isub>s"} @{text "("}@{text "**"}@{text ")"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \ B"}. This will solve the second case. - Taking the two requirements, @{text "(*)"} and @{text "(**)"}, together we define the + Taking the two requirements, @{text "("}@{text "*"}@{text ")"} and @{text "(**)"}, together we define the tagging-function in the @{const Times}-case as: \begin{center} @@ -1476,7 +1519,6 @@ not know anything about how the string @{term x} is partitioned. With this definition in place, let us prove the @{const "Times"}-case. - \begin{proof}[@{const TIMES}-Case] If @{term "finite (UNIV // \A)"} and @{term "finite (UNIV // \B)"} then @{term "finite ((UNIV // \A) \ (Pow (UNIV // \B)))"} holds. The range of @@ -1884,7 +1926,7 @@ induction hypothesis is \begin{center} - @{text "(IH)"}\hspace{3mm}@{term "\r. Derivs s (lang r) = \ lang ` (pderivs s r)"} + @{text "(IH)"}\hspace{3mm}@{term "\r. Derivs s (lang r) = \ (lang ` (pderivs s r))"} \end{center} \noindent @@ -1894,10 +1936,10 @@ \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}ll} @{term "Derivs (c # s) (lang r)"} & @{text "="} & @{term "Derivs s (Deriv c (lang r))"} & by def.\\ - & @{text "="} & @{term "Derivs s (\ lang ` (pderiv c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\ - & @{text "="} & @{term "\ (Derivs s) ` (lang ` (pderiv c r))"} & by def.~of @{text "Ders"}\\ - & @{text "="} & @{term "\ lang ` (\ pderivs s ` (pderiv c r))"} & by IH\\ - & @{text "="} & @{term "\ lang ` (pderivs (c # s) r)"} & by def.\\ + & @{text "="} & @{term "Derivs s (\ (lang ` (pderiv c r)))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\ + & @{text "="} & @{term "\ ((Derivs s) ` (lang ` (pderiv c r)))"} & by def.~of @{text "Ders"}\\ + & @{text "="} & @{term "\ (lang ` (\ (pderivs s ` (pderiv c r))))"} & by IH\\ + & @{text "="} & @{term "\ (lang ` (pderivs (c # s) r))"} & by def.\\ \end{tabular} \end{center} @@ -1931,10 +1973,10 @@ @{thm pderivs_lang_def} \end{equation} - \begin{thrm}[\cite{Antimirov95}]\label{antimirov} + \begin{theorem}[\cite{Antimirov95}]\label{antimirov} For every language @{text A} and every regular expression @{text r}, \mbox{@{thm finite_pderivs_lang}}. - \end{thrm} + \end{theorem} \noindent Antimirov's proof first establishes this theorem for the language @{term UNIV1}, @@ -2101,7 +2143,7 @@ and \eqref{Derspders} we have % \begin{equation}\label{eqq} - @{term "Deriv_lang B (lang r) = (\ lang ` (pderivs_lang B r))"} + @{term "Deriv_lang B (lang r) = (\ (lang ` (pderivs_lang B r)))"} \end{equation} \noindent @@ -2145,11 +2187,11 @@ \noindent We like to establish - \begin{thrm}[\cite{Haines69}]\label{subseqreg} + \begin{theorem}[\cite{Haines69}]\label{subseqreg} For every language @{text A}, the languages @{text "(i)"} @{term "SUBSEQ A"} and @{text "(ii)"} @{term "SUPSEQ A"} are regular. - \end{thrm} + \end{theorem} \noindent Our proof follows the one given by \citeN[Pages 92--95]{Shallit08}, except that we use @@ -2182,9 +2224,9 @@ whereby the last equation follows from the fact that @{term "A\"} contains the empty string. With these properties at our disposal we can establish the lemma - \begin{lmm} + \begin{lemma} If @{text A} is regular, then also @{term "SUPSEQ A"}. - \end{lmm} + \end{lemma} \begin{proof} Since our alphabet is finite, we have a regular expression, written @{text ALL}, that @@ -2212,12 +2254,12 @@ \noindent Now we can prove the main lemma w.r.t.~@{const "SUPSEQ"}, namely - \begin{lmm}\label{mset} + \begin{lemma}\label{mset} For every language @{text A}, there exists a finite language @{text M} such that \begin{center} \mbox{@{term "SUPSEQ M = SUPSEQ A"}}\;. \end{center} - \end{lmm} + \end{lemma} \begin{proof} For @{text M} we take the set of all minimal elements of @{text A}. An element @{text x} @@ -2275,11 +2317,11 @@ the non-regularity of languages. For this we use the following version of the Continuation Lemma (see for example~\cite{Rosenberg06}). - \begin{lmm}[Continuation Lemma] + \begin{lemma}[Continuation Lemma] If a language @{text A} is regular and a set of strings @{text B} is infinite, then there exist two distinct strings @{text x} and @{text y} in @{text B} such that @{term "x \A y"}. - \end{lmm} + \end{lemma} \noindent This lemma can be easily deduced from the Myhill-Nerode Theorem and the Pigeonhole @@ -2293,9 +2335,9 @@ for the strings consisting of @{text n} times the character a; similarly for @{text "b\<^isup>n"}). For this consider the infinite set @{text "B \ \\<^isub>n a\<^sup>n"}. - \begin{lmm} + \begin{lemma} No two distinct strings in set @{text "B"} are Myhill-Nerode related by language @{text A}. - \end{lmm} + \end{lemma} \begin{proof} After unfolding the definition of @{text "B"}, we need to establish that given @{term "i \ j"}, @@ -2344,9 +2386,9 @@ We have established in Isabelle/HOL both directions of the Myhill-Nerode Theorem. % - \begin{thrm}[Myhill-Nerode Theorem]\mbox{}\\ + \begin{theorem}[Myhill-Nerode Theorem]\mbox{}\\ A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}. - \end{thrm} + \end{theorem} \noindent Having formalised this theorem means we pushed our point of view quite @@ -2452,8 +2494,8 @@ algorithm is still executable. Given the infrastructure for executable sets introduced by \citeN{Haftmann09} in Isabelle/HOL, it should. - We started out by claiming that in a theorem prover it is eaiser to - reason about regular expressions than about automta. Here are some + We started out by claiming that in a theorem prover it is easier to + reason about regular expressions than about automata. Here are some numbers: Our formalisation of the Myhill-Nerode Theorem consists of 780 lines of Isabelle/Isar code for the first direction and 460 for the second (the one based on tagging-functions), plus around 300 @@ -2536,50 +2578,50 @@ We are grateful for the comments we received from Larry Paulson. Tobias Nipkow made us aware of the properties in Theorem~\ref{subseqreg} and Tjark Weber helped us with proving them. Christian Sternagel provided us with a - version of Higman's Lemma that applies to arbtrary, but finite alphabets. + version of Higman's Lemma that applies to arbitrary, but finite alphabets. \bibliographystyle{acmtrans} \bibliography{root} - \newpage - \begin{appendix} - \section{Appendix$^\star$} + %\newpage + %\begin{appendix} + %\section{Appendix$^\star$} - \renewcommand{\thefootnote}{\mbox{$\star$}} - \footnotetext{If the reviewers deem more suitable, the authors are - prepared to drop material or move it to an electronic appendix.} + %\renewcommand{\thefootnote}{\mbox{$\star$}} + %\footnotetext{If the reviewers deem more suitable, the authors are + %prepared to drop material or move it to an electronic appendix.} - \begin{proof}[of Lemma~\ref{arden}] - For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show - that @{thm (lhs) reversed_Arden} holds. From Property~\ref{langprops}@{text "(i)"} - we have @{term "A\ = A \ A\ \ {[]}"}, - which is equal to @{term "A\ = A\ \ A \ {[]}"}. Adding @{text B} to both - sides gives @{term "B \ A\ = B \ (A\ \ A \ {[]})"}, whose right-hand side - is equal to @{term "(B \ A\) \ A \ B"}. Applying the assumed equation - completes this direction. + %\begin{proof}[of Lemma~\ref{arden}] + %For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show + %that @{thm (lhs) reversed_Arden} holds. From Property~\ref{langprops}@{text "(i)"} + %we have @{term "A\ = A \ A\ \ {[]}"}, + %which is equal to @{term "A\ = A\ \ A \ {[]}"}. Adding @{text B} to both + %sides gives @{term "B \ A\ = B \ (A\ \ A \ {[]})"}, whose right-hand side + %is equal to @{term "(B \ A\) \ A \ B"}. Applying the assumed equation + %completes this direction. - For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction - on @{text n}, we can establish the property + %For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction + %on @{text n}, we can establish the property - \begin{center} - @{text "(*)"}\hspace{5mm} @{thm (concl) reversed_arden_helper} - \end{center} + %\begin{center} + %@{text "("}@{text "*"}@{text ")"}\hspace{5mm} @{thm (concl) reversed_arden_helper} + %\end{center} - \noindent - Using this property we can show that @{term "B \ (A \ n) \ X"} holds for - all @{text n}. From this we can infer @{term "B \ A\ \ X"} using the definition - of @{text "\"}. - For the inclusion in the other direction we assume a string @{text s} - with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden} - we know by Property~\ref{langprops}@{text "(ii)"} that - @{term "s \ X \ (A \ Suc k)"} since its length is only @{text k} - (the strings in @{term "X \ (A \ Suc k)"} are all longer). - From @{text "(*)"} it follows then that - @{term s} must be an element in @{term "(\m\k. B \ (A \ m))"}. This in turn - implies that @{term s} is in @{term "(\n. B \ (A \ n))"}. Using Property~\ref{langprops}@{text "(iii)"} - this is equal to @{term "B \ A\"}, as we needed to show. - \end{proof} - \end{appendix} + %\noindent + %Using this property we can show that @{term "B \ (A \ n) \ X"} holds for + %all @{text n}. From this we can infer @{term "B \ A\ \ X"} using the definition + %of @{text "\"}. + %For the inclusion in the other direction we assume a string @{text s} + %with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden} + %we know by Property~\ref{langprops}@{text "(ii)"} that + %@{term "s \ X \ (A \ Suc k)"} since its length is only @{text k} + %(the strings in @{term "X \ (A \ Suc k)"} are all longer). + %From @{text "("}@{text "*"}@{text ")"} it follows then that + %@{term s} must be an element in @{term "(\m\k. B \ (A \ m))"}. This in turn + %implies that @{term s} is in @{term "(\n. B \ (A \ n))"}. Using Property~\ref{langprops}@{text "(iii)"} + %this is equal to @{term "B \ A\"}, as we needed to show. + %\end{proof} + % \end{appendix} *} diff -r a0bcf886b8ef -r 8c4b6fb43ebe Journal/document/root.tex --- a/Journal/document/root.tex Fri Jul 05 12:07:48 2013 +0100 +++ b/Journal/document/root.tex Fri Jul 05 17:19:17 2013 +0100 @@ -1,9 +1,10 @@ -\documentclass[final, natbib]{svjour3} +\documentclass[final,natbib]{svjour3} %\documentclass[acmtocl,final]{acmtrans2m} \usepackage{isabelle} \usepackage{isabellesym} \usepackage{amsmath} \usepackage{amssymb} +%%\usepackage{amsthm} \usepackage{tikz} \usepackage{pgf} \usetikzlibrary{arrows,automata,decorations,fit,calc} @@ -41,10 +42,10 @@ \newcommand{\bigplus}{\mbox{\Large\bf$+$}} -\newtheorem{thrm}{Theorem}[section] -\newtheorem{lmm}{Lemma}[section] -\newtheorem{dfntn}{Definition}[section] -\newtheorem{prpstn}{Proposition}[section] +%\spnewtheorem{thrm}{Theorem}[section]{\bf}{\it} +%\spnewtheorem{lmm}{Lemma}[section]{\bf}{\it} +%\spnewtheorem{dfntn}{Definition}[section]{\bf}{\it} +%\spnewtheorem{prpstn}{Proposition}[section]{\bf}{\it} \begin{document} @@ -58,7 +59,7 @@ \author{Chunhan Wu \and Xingyuan Zhang \and Christian Urban} \institute{Chunhan Wu \and Xingyuan Zhang \at PLA University of Science and Technology Nanjing, China \and -Christian Urban \at King's College London, United Kingdom} +Chunhan Wu \and Christian Urban \at King's College London, United Kingdom} \date{Received: date / Accepted: date} diff -r a0bcf886b8ef -r 8c4b6fb43ebe ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ROOT Fri Jul 05 17:19:17 2013 +0100 @@ -0,0 +1,20 @@ +session Myhill in "Journal" = HOL + + options [document = false] + theories + "../Folds" + "../Regular_Set" + "../Regular_Exp" + "../Derivatives" + "../Myhill_1" + "../Myhill_2" + "../Myhill" + "../Closures" + "../Closures2" + "../Attic/Prefix_subtract" + + +session Journal in "Journal" = Myhill + + options [document = pdf, document_output = "..", document_variants = "journal"] + theories + "Paper" + diff -r a0bcf886b8ef -r 8c4b6fb43ebe Regular_Exp.thy --- a/Regular_Exp.thy Fri Jul 05 12:07:48 2013 +0100 +++ b/Regular_Exp.thy Fri Jul 05 17:19:17 2013 +0100 @@ -24,8 +24,7 @@ "lang (Times r s) = conc (lang r) (lang s)" | "lang (Star r) = star(lang r)" -primrec atoms :: "'a rexp \ 'a set" -where +primrec atoms :: "'a rexp \ 'a set" where "atoms Zero = {}" | "atoms One = {}" | "atoms (Atom a) = {a}" | @@ -33,4 +32,15 @@ "atoms (Times r s) = atoms r \ atoms s" | "atoms (Star r) = atoms r" +primrec nullable :: "'a rexp \ bool" where +"nullable (Zero) = False" | +"nullable (One) = True" | +"nullable (Atom c) = False" | +"nullable (Plus r1 r2) = (nullable r1 \ nullable r2)" | +"nullable (Times r1 r2) = (nullable r1 \ nullable r2)" | +"nullable (Star r) = True" + +lemma nullable_iff: "nullable r \ [] \ lang r" +by (induct r) (auto simp add: conc_def split: if_splits) + end diff -r a0bcf886b8ef -r 8c4b6fb43ebe Regular_Set.thy --- a/Regular_Set.thy Fri Jul 05 12:07:48 2013 +0100 +++ b/Regular_Set.thy Fri Jul 05 17:19:17 2013 +0100 @@ -216,7 +216,7 @@ abbreviation Derivss :: "'a list \ 'a lang set \ 'a lang" where - "Derivss s As \ \ (Derivs s) ` As" + "Derivss s As \ \ (Derivs s ` As)" lemma Deriv_empty[simp]: "Deriv a {} = {}"