# HG changeset patch # User urbanc # Date 1312522451 0 # Node ID 9f46a9571e376944881cc0fc7aeb6fc485a7989e # Parent 07a269d9642bdc14e4a8bb7842667922c0cf21ec more on the derivatives section diff -r 07a269d9642b -r 9f46a9571e37 Closures.thy --- a/Closures.thy Wed Aug 03 17:08:31 2011 +0000 +++ b/Closures.thy Fri Aug 05 05:34:11 2011 +0000 @@ -142,6 +142,9 @@ subsection {* Closure under left-quotients *} +abbreviation + "Ders_set A B \ \s \ A. Ders s B" + lemma closure_left_quotient: assumes "regular A" shows "regular (Ders_set B A)" @@ -150,7 +153,7 @@ have fin: "finite (pders_set B r)" by (rule finite_pders_set) have "Ders_set B (lang r) = (\ lang ` (pders_set B r))" - by (simp add: Ders_set_pders_set) + by (simp add: Ders_pders) also have "\ = lang (\(pders_set B r))" using fin by simp finally have "Ders_set B A = lang (\(pders_set B r))" using eq by simp diff -r 07a269d9642b -r 9f46a9571e37 Derivatives.thy --- a/Derivatives.thy Wed Aug 03 17:08:31 2011 +0000 +++ b/Derivatives.thy Fri Aug 05 05:34:11 2011 +0000 @@ -21,35 +21,15 @@ where "Ders s A \ {s'. s @ s' \ A}" -definition - Ders_set :: "'a lang \ 'a lang \ 'a lang" -where - "Ders_set A B \ {s' | s s'. s @ s' \ B \ s \ A}" - -lemma Ders_set_Ders: - shows "Ders_set A B = (\s \ A. Ders s B)" -unfolding Ders_set_def Ders_def -by auto - -lemma Der_zero [simp]: - shows "Der c {} = {}" -unfolding Der_def -by auto +abbreviation + "Derss s A \ \ (Ders s) ` A" -lemma Der_one [simp]: - shows "Der c {[]} = {}" -unfolding Der_def -by auto - -lemma Der_atom [simp]: - shows "Der c {[d]} = (if c = d then {[]} else {})" -unfolding Der_def -by auto - -lemma Der_union [simp]: - shows "Der c (A \ B) = Der c A \ Der c B" -unfolding Der_def -by auto +lemma Der_simps [simp]: + shows "Der c {} = {}" + and "Der c {[]} = {}" + and "Der c {[d]} = (if c = d then {[]} else {})" + and "Der c (A \ B) = Der c A \ Der c B" +unfolding Der_def by auto lemma Der_conc [simp]: shows "Der c (A \ B) = (Der c A) \ B \ (Delta A \ Der c B)" @@ -60,7 +40,7 @@ shows "Der c (A\) = (Der c A) \ A\" proof - have incl: "Delta A \ Der c (A\) \ (Der c A) \ A\" - unfolding Der_def Delta_def + unfolding Der_def Delta_def conc_def apply(auto) apply(drule star_decom) apply(auto simp add: Cons_eq_append_conv) @@ -69,7 +49,7 @@ have "Der c (A\) = Der c (A \ A\ \ {[]})" by (simp only: star_unfold_left[symmetric]) also have "... = Der c (A \ A\)" - by (simp only: Der_union Der_one) (simp) + by (simp only: Der_simps) (simp) also have "... = (Der c A) \ A\ \ (Delta A \ Der c (A\))" by simp also have "... = (Der c A) \ A\" @@ -77,19 +57,12 @@ finally show "Der c (A\) = (Der c A) \ A\" . qed -lemma Ders_nil [simp]: +lemma Ders_simps [simp]: shows "Ders [] A = A" -unfolding Ders_def by simp - -lemma Ders_cons [simp]: - shows "Ders (c # s) A = Ders s (Der c A)" + and "Ders (c # s) A = Ders s (Der c A)" + and "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)" unfolding Ders_def Der_def by auto -lemma Ders_append [simp]: - shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)" -unfolding Ders_def by simp - - subsection {* Brozowsky's derivatives of regular expressions *} fun @@ -137,7 +110,7 @@ subsection {* Antimirov's Partial Derivatives *} abbreviation - "Times_set rs r \ {Times r' r | r'. r' \ rs}" + "Timess rs r \ {Times r' r | r'. r' \ rs}" fun pder :: "'a \ 'a rexp \ ('a rexp) set" @@ -147,11 +120,11 @@ | "pder c (Atom c') = (if c = c' then {One} else {Zero})" | "pder c (Plus r1 r2) = (pder c r1) \ (pder c r2)" | "pder c (Times r1 r2) = - (if nullable r1 then Times_set (pder c r1) r2 \ pder c r2 else Times_set (pder c r1) r2)" -| "pder c (Star r) = Times_set (pder c r) (Star r)" + (if nullable r1 then Timess (pder c r1) r2 \ pder c r2 else Timess (pder c r1) r2)" +| "pder c (Star r) = Timess (pder c r) (Star r)" abbreviation - "pder_set c rs \ \r \ rs. pder c r" + "pder_set c rs \ \ pder c ` rs" fun pders :: "'a list \ 'a rexp \ ('a rexp) set" @@ -160,7 +133,7 @@ | "pders (c # s) r = \ (pders s) ` (pder c r)" abbreviation - "pders_set A r \ \s \ A. pders s r" + "pderss s A \ \ (pders s) ` A" lemma pders_append: "pders (s1 @ s2) r = \ (pders s2) ` (pders s1 r)" @@ -170,85 +143,113 @@ shows "pders (s @ [c]) r = pder_set c (pders s r)" by (simp add: pders_append) -lemma pders_set_lang: - shows "(\ (lang ` pder_set c rs)) = (\r \ rs. (\lang ` (pder c r)))" -unfolding image_def -by auto - -lemma pders_Zero [simp]: +lemma pders_simps [simp]: shows "pders s Zero = {Zero}" -by (induct s) (simp_all) - -lemma pders_One [simp]: - shows "pders s One = (if s = [] then {One} else {Zero})" + and "pders s One = (if s = [] then {One} else {Zero})" + and "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))" + and "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \ (pders s r2))" by (induct s) (auto) -lemma pders_Atom [simp]: - shows "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))" -by (induct s) (auto) +subsection {* Relating left-quotients and partial derivatives *} + +lemma Der_pder: + shows "Der c (lang r) = \ lang ` (pder c r)" +by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib) -lemma pders_Plus [simp]: - shows "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \ (pders s r2))" -by (induct s) (auto) +lemma Ders_pders: + shows "Ders s (lang r) = \ lang ` (pders s r)" +proof (induct s arbitrary: r) + case (Cons c s) + have ih: "\r. Ders s (lang r) = \ lang ` (pders s r)" by fact + have "Ders (c # s) (lang r) = Ders s (Der c (lang r))" by simp + also have "\ = Ders s (\ lang ` (pder c r))" by (simp add: Der_pder) + also have "\ = Derss s (lang ` (pder c r))" + by (auto simp add: Ders_def) + also have "\ = \ lang ` (pderss s (pder c r))" + using ih by auto + also have "\ = \ lang ` (pders (c # s) r)" by simp + finally show "Ders (c # s) (lang r) = \ lang ` pders (c # s) r" . +qed (simp add: Ders_def) + +subsection {* Relating derivatives and partial derivatives *} + +lemma + shows "(\ lang ` (pder c r)) = lang (der c r)" +unfolding Der_der[symmetric] Der_pder by simp + +lemma + shows "(\ lang ` (pders s r)) = lang (ders s r)" +unfolding Ders_ders[symmetric] Ders_pders by simp + + +subsection {* There are only finitely many partial derivatives for a language *} + +abbreviation + "pders_set A r \ \s \ A. pders s r" text {* Non-empty suffixes of a string *} definition "Suf s \ {v. v \ [] \ (\u. u @ v = s)}" -lemma Suf: +lemma Suf_snoc: shows "Suf (s @ [c]) = (Suf s) \ {[c]} \ {[c]}" unfolding Suf_def conc_def by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv) lemma Suf_Union: - shows "(\v \ Suf s \ {[c]}. P v) = (\v \ Suf s. P (v @ [c]))" + shows "(\v \ Suf s \ {[c]}. f v) = (\v \ Suf s. f (v @ [c]))" by (auto simp add: conc_def) +lemma pders_set_snoc: + shows "pders_set (Suf s \ {[c]}) r = (pder_set c (pders_set (Suf s) r))" +by (simp add: Suf_Union pders_snoc) + lemma pders_Times: - shows "pders s (Times r1 r2) \ Times_set (pders s r1) r2 \ (\v \ Suf s. pders v r2)" + shows "pders s (Times r1 r2) \ Timess (pders s r1) r2 \ (pders_set (Suf s) r2)" proof (induct s rule: rev_induct) case (snoc c s) - have ih: "pders s (Times r1 r2) \ Times_set (pders s r1) r2 \ (\v \ Suf s. pders v r2)" + have ih: "pders s (Times r1 r2) \ Timess (pders s r1) r2 \ (pders_set (Suf s) r2)" by fact have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" by (simp add: pders_snoc) - also have "\ \ pder_set c (Times_set (pders s r1) r2 \ (\v \ Suf s. pders v r2))" + also have "\ \ pder_set c (Timess (pders s r1) r2 \ (pders_set (Suf s) r2))" using ih by (auto) (blast) - also have "\ = pder_set c (Times_set (pders s r1) r2) \ pder_set c (\v \ Suf s. pders v r2)" - by (simp) - also have "\ = pder_set c (Times_set (pders s r1) r2) \ (\v \ Suf s. pder_set c (pders v r2))" + also have "\ = pder_set c (Timess (pders s r1) r2) \ pder_set c (pders_set (Suf s) r2)" by (simp) - also have "\ \ pder_set c (Times_set (pders s r1) r2) \ (pder c r2) \ (\v \ Suf s. pders (v @ [c]) r2)" - by (auto simp add: pders_snoc) - also have "\ \ Times_set (pder_set c (pders s r1)) r2 \ (pder c r2) \ (\v \ Suf s. pders (v @ [c]) r2)" - by (auto simp add: if_splits) (blast) - also have "\ = Times_set (pders (s @ [c]) r1) r2 \ (\v \ Suf (s @ [c]). pders v r2)" - by (auto simp add: pders_snoc Suf Suf_Union) + also have "\ = pder_set c (Timess (pders s r1) r2) \ pders_set (Suf s \ {[c]}) r2" + by (simp add: pders_set_snoc) + also have "\ \ pder_set c (Timess (pders s r1) r2) \ pder c r2 \ pders_set (Suf s \ {[c]}) r2" + by auto + also have "\ \ Timess (pders (s @ [c]) r1) r2 \ pder c r2 \ pders_set (Suf s \ {[c]}) r2" + by (auto simp add: if_splits pders_snoc) (blast) + also have "\ = Timess (pders (s @ [c]) r1) r2 \ pders_set (Suf (s @ [c])) r2" + by (auto simp add: Suf_snoc) finally show ?case . -qed (simp) +qed (simp) + lemma pders_Star: assumes a: "s \ []" - shows "pders s (Star r) \ (\v \ Suf s. Times_set (pders v r) (Star r))" + shows "pders s (Star r) \ (\v \ Suf s. Timess (pders v r) (Star r))" using a proof (induct s rule: rev_induct) case (snoc c s) - have ih: "s \ [] \ pders s (Star r) \ (\v\Suf s. Times_set (pders v r) (Star r))" by fact + have ih: "s \ [] \ pders s (Star r) \ (\v\Suf s. Timess (pders v r) (Star r))" by fact { assume asm: "s \ []" have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc) - also have "\ \ (pder_set c (\v\Suf s. Times_set (pders v r) (Star r)))" - using ih[OF asm] by blast - also have "\ = (\v\Suf s. pder_set c (Times_set (pders v r) (Star r)))" + also have "\ \ (pder_set c (\v\Suf s. Timess (pders v r) (Star r)))" + using ih[OF asm] by (auto) (blast) + also have "\ = (\v\Suf s. pder_set c (Timess (pders v r) (Star r)))" by simp - also have "\ \ (\v\Suf s. (Times_set (pder_set c (pders v r)) (Star r) \ pder c (Star r)))" + also have "\ \ (\v\Suf s. (Timess (pder_set c (pders v r)) (Star r) \ pder c (Star r)))" by (auto split: if_splits) - also have "\ = (\v\Suf s. (Times_set (pder_set c (pders v r)) (Star r))) \ pder c (Star r)" + also have "\ = (\v\Suf s. (Timess (pder_set c (pders v r)) (Star r))) \ pder c (Star r)" using asm by (auto simp add: Suf_def) - also have "\ = (\v\Suf s. (Times_set (pders (v @ [c]) r) (Star r))) \ (Times_set (pder c r) (Star r))" + also have "\ = (\v\Suf s. (Timess (pders (v @ [c]) r) (Star r))) \ (Timess (pder c r) (Star r))" by (simp add: pders_snoc) - also have "\ = (\v\Suf (s @ [c]). (Times_set (pders v r) (Star r)))" - by (auto simp add: Suf Suf_Union pders_snoc) + also have "\ = (\v\Suf (s @ [c]). (Timess (pders v r) (Star r)))" + by (auto simp add: Suf_snoc Suf_Union pders_snoc) finally have ?case . } moreover @@ -284,7 +285,7 @@ using a unfolding UNIV1_def Suf_def by (auto) lemma pders_set_Times: - shows "pders_set UNIV1 (Times r1 r2) \ Times_set (pders_set UNIV1 r1) r2 \ pders_set UNIV1 r2" + shows "pders_set UNIV1 (Times r1 r2) \ Timess (pders_set UNIV1 r1) r2 \ pders_set UNIV1 r2" unfolding UNIV1_def apply(rule UN_least) apply(rule subset_trans) @@ -298,7 +299,7 @@ done lemma pders_set_Star: - shows "pders_set UNIV1 (Star r) \ Times_set (pders_set UNIV1 r) (Star r)" + shows "pders_set UNIV1 (Star r) \ Timess (pders_set UNIV1 r) (Star r)" unfolding UNIV1_def apply(rule UN_least) apply(rule subset_trans) @@ -308,9 +309,9 @@ apply(auto) done -lemma finite_Times_set: +lemma finite_Timess: assumes a: "finite A" - shows "finite (Times_set A r)" + shows "finite (Timess A r)" using a by (auto) lemma finite_pders_set_UNIV1: @@ -326,11 +327,11 @@ apply(simp) apply(rule finite_subset) apply(rule pders_set_Times) -apply(simp only: finite_Times_set finite_Un) +apply(simp only: finite_Timess finite_Un) apply(simp) apply(rule finite_subset) apply(rule pders_set_Star) -apply(simp only: finite_Times_set) +apply(simp only: finite_Timess) done lemma pders_set_UNIV_UNIV1: @@ -371,48 +372,6 @@ qed -subsection {* Relating left-quotients and partial derivatives *} - -lemma Der_pder: - shows "Der c (lang r) = \ lang ` (pder c r)" -by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib) - -lemma Ders_pders: - shows "Ders s (lang r) = \ lang ` (pders s r)" -proof (induct s rule: rev_induct) - case (snoc c s) - have ih: "Ders s (lang r) = \ lang ` (pders s r)" by fact - have "Ders (s @ [c]) (lang r) = Ders [c] (Ders s (lang r))" - by (simp add: Ders_append) - also have "\ = Der c (\ lang ` (pders s r))" using ih - by (simp) - also have "\ = (\r\pders s r. Der c (lang r))" - unfolding Der_def image_def by auto - also have "\ = (\r\pders s r. (\ lang ` (pder c r)))" - by (simp add: Der_pder) - also have "\ = (\lang ` (pder_set c (pders s r)))" - by (simp add: pders_set_lang) - also have "\ = (\lang ` (pders (s @ [c]) r))" - by (simp add: pders_snoc) - finally show "Ders (s @ [c]) (lang r) = \ lang ` pders (s @ [c]) r" . -qed (simp add: Ders_def) - -lemma Ders_set_pders_set: - shows "Ders_set A (lang r) = (\ lang ` (pders_set A r))" -by (simp add: Ders_set_Ders Ders_pders) - - -subsection {* Relating derivatives and partial derivatives *} - -lemma - shows "(\ lang ` (pder c r)) = lang (der c r)" -unfolding Der_der[symmetric] Der_pder by simp - -lemma - shows "(\ lang ` (pders s r)) = lang (ders s r)" -unfolding Ders_ders[symmetric] Ders_pders by simp - - text {* Relating the Myhill-Nerode relation with left-quotients. *} lemma MN_Rel_Ders: diff -r 07a269d9642b -r 9f46a9571e37 Journal/Paper.thy --- a/Journal/Paper.thy Wed Aug 03 17:08:31 2011 +0000 +++ b/Journal/Paper.thy Fri Aug 05 05:34:11 2011 +0000 @@ -34,7 +34,7 @@ abbreviation "ATOM \ Atom" abbreviation "PLUS \ Plus" abbreviation "TIMES \ Times" -abbreviation "TIMESS \ Times_set" +abbreviation "TIMESS \ Timess" abbreviation "STAR \ Star" @@ -143,19 +143,18 @@ wide range of textbooks on this subject, many of which are aimed at students and contain very detailed `pencil-and-paper' proofs (e.g.~\cite{Kozen97, HopcroftUllman69}). It seems natural to exercise theorem provers by - formalising the theorems and by verifying formally the algorithms. 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 + formalising the theorems and by verifying formally the algorithms. + + 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 latter. HOL is a predicate calculus that allows quantification over predicate variables. Its type system is - based on Church's Simple Theory of Types \cite{Church40}. Although - many mathematical concepts can be conveniently expressed in HOL, there are some + based on Church's Simple Theory of Types \cite{Church40}. Although many + mathematical concepts can be conveniently expressed in HOL, there are some limitations that hurt badly, if one attempts a simple-minded formalisation - of regular languages in it. - - The typical approach to regular languages is to introduce finite automata - and then define everything in terms of them \cite{Kozen97}. For example, - a regular language is normally defined as: + of regular languages in it. The typical approach to regular languages is to + introduce finite automata and then define everything in terms of them + \cite{Kozen97}. For example, a regular language is normally defined as: \begin{dfntn}\label{baddef} A language @{text A} is \emph{regular}, provided there is a @@ -252,7 +251,8 @@ language as one for which there exists an automaton that recognises all its strings. This is because we cannot make a definition in HOL that is polymorphic in the state type and there is no type quantification available in HOL (unlike - in Coq, for example). + in Coq, for example).\footnote{Slind already pointed out this problem in an email + to the HOL4 mailing list on 21st April 2005.} An alternative, which provides us with a single type for automata, is to give every state node an identity, for example a natural @@ -266,8 +266,8 @@ problems as with graphs. Composing, for example, two non-deterministic automata in parallel requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98} dismisses for this the option of using identities, because it leads according to - him to ``messy proofs''. Since he does not need to define what a regular - language is, Nipkow opts for a variant of \eqref{disjointunion} using bit lists, but writes + him to ``messy proofs''. Since he does not need to define what regular + languages are, Nipkow opts for a variant of \eqref{disjointunion} using bit lists, but writes \begin{quote} \it% @@ -317,7 +317,7 @@ of automata \cite{Brzozowski10}). Such side-conditions mean that if we define a regular language as one for which there exists \emph{a} finite automaton that recognises all its strings (see Def.~\ref{baddef}), then we need a lemma which - ensures that another equivalent can be found satisfying the + ensures that another equivalent one can be found satisfying the side-condition. Unfortunately, such `little' and `obvious' lemmas make a formalisation of automata theory a hair-pulling experience. @@ -360,11 +360,12 @@ certain tagging-functions, and another indirect proof using Antimirov's partial derivatives \cite{Antimirov95}. Again to our best knowledge, the tagging-functions have not been used before to establish the Myhill-Nerode - theorem. Derivatives of regular expressions have been recently used quite - widely in the literature about regular expressions. However, partial - derivatives are more suitable in the context of the Myhill-Nerode theorem, - since it is easier to establish formally their finiteness result. - + theorem. Derivatives of regular expressions have been used recently quite + widely in the literature; partial derivatives, in contrast, attracted 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 have not found any proof that uses + either of them in order to prove the Myhill-Nerode theorem. *} section {* Preliminaries *} @@ -398,10 +399,13 @@ we will make use of the following properties of these constructions. \begin{prpstn}\label{langprops}\mbox{}\\ - \begin{tabular}{@ {}ll} + \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\"}. \end{tabular} \end{prpstn} @@ -1167,8 +1171,8 @@ \noindent that means we take the image of @{text f} w.r.t.~all elements in the domain. With this we will be able to infer that the tagging-functions, seen - as relations, give rise to finitely many equivalence classes of @{const - UNIV}. Finally we will show that the tagging-relations are more refined than + as relations, give rise to finitely many equivalence classes. + Finally we will show that the tagging-relations are more refined than @{term "\(lang r)"}, which implies that @{term "UNIV // \(lang r)"} must also be finite. We formally define the notion of a \emph{tagging-relation} as follows. @@ -1249,7 +1253,7 @@ is that we need to establish that @{term "=(tag_Plus A B)="} refines @{term "\(A \ B)"}. This amounts to showing @{term "x \A y"} or @{term "x \B y"} under the assumption @{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. As we shall see, this definition will - provide us just the right assumptions in order to get the proof through. + provide us with just the right assumptions in order to get the proof through. \begin{proof}[@{const "PLUS"}-Case] We can show in general, if @{term "finite (UNIV // \A)"} and @{term "finite @@ -1264,7 +1268,7 @@ \noindent The @{const TIMES}-case is slightly more complicated. We first prove the - following lemma, which will aid the refinement-proofs. + following lemma, which will aid the proof about refinement. \begin{lmm}\label{refinement} The relation @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} refines @{term "\A"}, provided for @@ -1274,15 +1278,21 @@ \noindent - We therefore can clean information from how the strings @{text "x @ z"} are in @{text A} - and construct appropriate tagging-functions to infer that @{term "y @ z \ A"}. - For the @{const Times}-case we additionally need the notion of the set of all - possible partitions of a string + We therefore can analyse how the strings @{text "x @ z"} are in the language + @{text A} and then construct an appropriate tagging-function to infer that + @{term "y @ z"} are also in @{text A}. For this we sill need the notion of + the set of all possible \emph{partitions} of a string \begin{equation} @{thm Partitions_def} \end{equation} + \noindent + If we know that @{text "(x\<^isub>p, x\<^isub>s) \ Partitions x"}, we will + refer to @{text "x\<^isub>p"} as the \emph{prefix} of the string @{text x}, + respectively to @{text "x\<^isub>s"} as the \emph{suffix}. + + 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"}: % @@ -1350,12 +1360,13 @@ (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 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 a possible partition - of the string @{text x}. So we have to know that both @{text "x\<^isub>p"} and the + 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"}. + This will solve the second case. Taking the two requirements, @{text "(*)"} and @{text "(**)"}, together we define the - tagging-function as: + tagging-function in the @{const Times}-case as: \begin{center} @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}~@{text "\"}~ @@ -1363,27 +1374,32 @@ \end{center} \noindent - With this definition in place, we can discharge the @{const "Times"}-case as follows. + We have to make the assumption for all suffixes @{text "x\<^isub>s"}, since we do + 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 @{term "tag_Times A B"} is a subset of this product set, and therefore finite. - By Lemma \ref{refinement} we know + For the refinement of @{term "\(A \ B)"} and @{text "\<^raw:$\threesim$>\<^bsub>\tag A B\<^esub>"}, + we have by Lemma \ref{refinement} \begin{center} @{term "tag_Times A B x = tag_Times A B y"} \end{center} \noindent - and @{term "x @ z \ A \ B"}, and have to establish @{term "y @ z \ A \ B"}. As shown - above, there are two cases to be considered (see pictures above). First, - there exists a @{text "z\<^isub>p"} and @{text "z\<^isub>s"} such that @{term "x @ z\<^isub>p \ A"} and @{text "z\<^isub>s \ B"}. - By the assumption about @{term "tag_Times A B"} we have - @{term "\A `` {x} = \A `` {y}"} and thus @{term "x \A y"}. Which means by the Myhill-Nerode - relation that @{term "y @ z\<^isub>p \ A"} holds. Using @{text "z\<^isub>s \ B"}, we can conclude in this case - with @{term "y @ z \ A \ B"}. + and @{term "x @ z \ A \ B"}, and have to establish @{term "y @ z \ A \ + B"}. As shown in the pictures above, there are two cases to be + considered. First, there exists a @{text "z\<^isub>p"} and @{text + "z\<^isub>s"} such that @{term "x @ z\<^isub>p \ A"} and @{text "z\<^isub>s + \ B"}. By the assumption about @{term "tag_Times A B"} we have @{term "\A + `` {x} = \A `` {y}"} and thus @{term "x \A y"}. Hence by the Myhill-Nerode + relation @{term "y @ z\<^isub>p \ A"} holds. Using @{text "z\<^isub>s \ B"}, + we can conclude in this case with @{term "y @ z \ A \ B"} (recall @{text + "z\<^isub>p @ z\<^isub>s = z"}). Second there exists a partition @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{text "x\<^isub>p \ A"} and @{text "x\<^isub>s @ z \ B"}. We therefore have @@ -1403,7 +1419,7 @@ This means there must be a partition @{text "y\<^isub>p"} and @{text "y\<^isub>s"} such that @{term "y\<^isub>p \ A"} and @{term "\B `` {x\<^isub>s} = \B `` {y\<^isub>s}"}. Unfolding the Myhill-Nerode relation and together with the - facts that @{text "x\<^isub>p \ A"} and @{text "x\<^isub>s @ z \ B"}, we + facts that @{text "x\<^isub>p \ A"} and \mbox{@{text "x\<^isub>s @ z \ B"}}, we obtain @{term "y\<^isub>p \ A"} and @{text "y\<^isub>s @ z \ B"}, as needed in this case. We again can complete the @{const TIMES}-case by setting @{text A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}. @@ -1411,7 +1427,7 @@ \noindent The case for @{const Star} is similar to @{const TIMES}, but poses a few - extra challenges. To deal with them we define first the notion of a \emph{string + extra challenges. To deal with them, we define first the notion of a \emph{string prefix} and a \emph{strict string prefix}: \begin{center} @@ -1421,8 +1437,7 @@ \end{tabular} \end{center} - \noindent - When we analyse the case of @{text "x @ z"} being an element in @{term "A\"} + When analysing the case of @{text "x @ z"} being an element in @{term "A\"} and @{text x} is not the empty string, we have the following picture: \begin{center} @@ -1466,13 +1481,13 @@ \noindent We can find a strict prefix @{text "x\<^isub>p"} of @{text x} such that @{term "x\<^isub>p \ A\"}, @{text "x\<^isub>p < x"} and the rest @{term "x\<^isub>s @ z \ A\"}. For example the empty string - @{text "[]"} would do. + @{text "[]"} would do (recall @{term "x \ []"}). There are potentially many such prefixes, but there can only be finitely many of them (the string @{text x} is finite). Let us therefore choose the longest one and call it @{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we - know it is in @{term "A\"} and it is not the empty string. By Prop.~\ref{langprops}@{text "(i)"}, + know it is in @{term "A\"} and cannot be the empty string. By Prop.~\ref{langprops}@{text "(iv)"}, we can separate - this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \ A"} + this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \ []"}, @{text "a \ A"} and @{term "b \ A\"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"}, otherwise @{text "x\<^bsub>pmax\<^esub>"} is not the longest prefix. That means @{text a} `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and @@ -1497,8 +1512,9 @@ that @{term "x @ z \ A\"} implies @{term "y @ z \ A\"}. We first need to consider the case that @{text x} is the empty string. - From the assumption we can infer @{text y} is the empty string and - clearly have @{term "y @ z \ A\"}. In case @{text x} is not the empty + From the assumption about strict prefixes in @{text "\<^raw:$\threesim$>\<^bsub>\tag A\<^esub>"}, we + can infer @{text y} is the empty string and + then clearly have @{term "y @ z \ A\"}. In case @{text x} is not the empty string, we can divide the string @{text "x @ z"} as shown in the picture above. By the tagging-function and the facts @{text "x\<^bsub>pmax\<^esub> \ A\<^isup>\"} and @{text "x\<^bsub>pmax\<^esub> < x"}, we have @@ -1515,17 +1531,17 @@ \end{center} \noindent - and we know there exist partitions @{text "y\<^isub>p"} and @{text + From this we know there exist partitions @{text "y\<^isub>p"} and @{text "y\<^isub>s"} with @{term "y\<^isub>p \ A\"} and also @{term "x\<^isub>s \A y\<^isub>s"}. Unfolding the Myhill-Nerode relation we know @{term "y\<^isub>s @ z\<^isub>a \ A"}. We also know that @{term "z\<^isub>b \ A\"}. Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \ A\"}, which means @{term "y @ z \ A\"}. As the last step we have to set - @{text "A"} to @{term "lang r"} and complete the proof. + @{text "A"} to @{term "lang r"} and thus complete the proof. \end{proof} *} -section {* Second Part based on Partial Derivatives *} +section {* Second Part proved using Partial Derivatives *} text {* \noindent @@ -1534,10 +1550,12 @@ a more refined relation than @{term "\(lang r)"} for which we can show that there are only finitely many equivalence classes. So far we showed this by induction on @{text "r"}. However, there is also - an indirect method to come up with such a refined relation. Assume - the following two definitions for a left-quotient of a language, which - we write as @{term "Der c A"} and @{term "Ders s A"} where - @{text c} is a character and @{text s} a string: + an indirect method to come up with such a refined relation based on + derivatives of regular expressions \cite{Brzozowski64}. + + Assume the following two definitions for a \emph{left-quotient} of a language, + which we write as @{term "Der c A"} and @{term "Ders s A"} where @{text c} + is a character and @{text s} a string: \begin{center} \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{2mm}}l} @@ -1547,6 +1565,14 @@ \end{center} \noindent + In order to aid readability, we shall also make use of the following abbreviation: + + \begin{center} + @{abbrev "Derss s A"} + \end{center} + + + \noindent Clearly we have the following relation between the Myhill-Nerode relation (Def.~\ref{myhillneroderel}) and left-quotients @@ -1555,20 +1581,20 @@ \end{equation} \noindent - It is realtively easy to establish the following properties for left-quotients: + It is straightforward to establish the following properties for left-quotients: \begin{equation} \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l} - @{thm (lhs) Der_zero} & $=$ & @{thm (rhs) Der_zero}\\ - @{thm (lhs) Der_one} & $=$ & @{thm (rhs) Der_one}\\ - @{thm (lhs) Der_atom} & $=$ & @{thm (rhs) Der_atom}\\ - @{thm (lhs) Der_union} & $=$ & @{thm (rhs) Der_union}\\ + @{thm (lhs) Der_simps(1)} & $=$ & @{thm (rhs) Der_simps(1)}\\ + @{thm (lhs) Der_simps(2)} & $=$ & @{thm (rhs) Der_simps(2)}\\ + @{thm (lhs) Der_simps(3)} & $=$ & @{thm (rhs) Der_simps(3)}\\ + @{thm (lhs) Der_simps(4)} & $=$ & @{thm (rhs) Der_simps(4)}\\ @{thm (lhs) Der_conc} & $=$ & @{thm (rhs) Der_conc}\\ @{thm (lhs) Der_star} & $=$ & @{thm (rhs) Der_star}\\ - @{thm (lhs) Ders_nil} & $=$ & @{thm (rhs) Ders_nil}\\ - @{thm (lhs) Ders_cons} & $=$ & @{thm (rhs) Ders_cons}\\ - %@{thm (lhs) Ders_append[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$ - % & @{thm (rhs) Ders_append[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\ + @{thm (lhs) Ders_simps(1)} & $=$ & @{thm (rhs) Ders_simps(1)}\\ + @{thm (lhs) Ders_simps(2)} & $=$ & @{thm (rhs) Ders_simps(2)}\\ + %@{thm (lhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$ + % & @{thm (rhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\ \end{tabular}} \end{equation} @@ -1603,10 +1629,10 @@ \end{center} \noindent - The last two lines extend @{const der} to strings (list of characters) where - list-cons is written \mbox{@{text "_ :: _"}}. The function @{term "nullable r"} needed - in the @{const Times}-case tests whether a regular expression can recognise - the empty string: + The last two clauses extend derivatives for characters to strings (list of + characters). The list-cons operator is written \mbox{@{text "_ :: _"}}. The + function @{term "nullable r"} needed in the @{const Times}-case tests + whether a regular expression can recognise the empty string: \begin{center} \begin{tabular}{c@ {\hspace{10mm}}c} @@ -1639,8 +1665,8 @@ \noindent The importance in the context of the Myhill-Nerode theorem is that - we can use \eqref{mhders} and the equations above in order to - establish that @{term "x \(lang r) y"} if and only if + we can use \eqref{mhders} and \eqref{Dersders} in order to + establish that @{term "x \(lang r) y"} is equivalent to @{term "lang (ders x r) = lang (ders y r)"}. From this we obtain \begin{equation} @@ -1649,29 +1675,35 @@ \noindent - Consequently, we can use as the tagging relation @{text - "\<^raw:$\threesim$>\<^bsub>(\x. ders x r)\<^esub>"}, since it refines - @{term "\(lang r)"}. However, in order to be useful in the Myhill-Nerode - theorem, we have to show that for a language there are only finitely many - derivatives. Unfortunately, this is not true in general: Sakarovitch gives - an example with infinitely many derivatives - \cite[Page~141]{Sakarovitch09}. What Brzozowski \cite{Brzozowski64} proved is - that for every language there \emph{are} finitely `dissimilar' derivatives for a - regular expression. Two regular expressions are said to be \emph{similar} - provided they can be identified using the using the @{text "ACI"}-identities: + which means the right-hand side (seen as relation) refines the + Myhill-Nerode relation. Consequently, we can use + @{text "\<^raw:$\threesim$>\<^bsub>(\x. ders x r)\<^esub>"} as a potential tagging-relation + for the regular expression @{text r}. However, in + order to be useful in the Myhill-Nerode theorem, we also have to show that + for the corresponding language there are only finitely many derivatives---ensuring + that there are only finitely many equivalence classes. Unfortunately, this + is not true in general. Sakarovitch gives an example where a regular + expression has infinitely many derivatives w.r.t.~a language + \cite[Page~141]{Sakarovitch09}. What Brzozowski \cite{Brzozowski64} proved + is that for every language there \emph{are} only finitely `dissimilar' + derivatives for a regular expression. Two regular expressions are said to be + \emph{similar} provided they can be identified using the using the @{text + "ACI"}-identities: - \begin{center} - \begin{tabular}{cl} + \begin{equation}\label{ACI} + \mbox{\begin{tabular}{cl} (@{text A}) & @{term "Plus (Plus r\<^isub>1 r\<^isub>2) r\<^isub>3"} $\equiv$ @{term "Plus r\<^isub>1 (Plus r\<^isub>2 r\<^isub>3)"}\\ (@{text C}) & @{term "Plus r\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\ (@{text I}) & @{term "Plus r r"} $\equiv$ @{term "r"}\\ - \end{tabular} - \end{center} + \end{tabular}} + \end{equation} \noindent - Carrying this idea through menas we now have to reasoning modulo @{text "ACI"}. - This can be done, but it is very painful in a theorem prover (since there is - no direct characterisation of the set of dissimlar derivatives). + Carrying this idea through, we must not consider the set of all derivatives, + but the ones modulo @{text "ACI"}. In principle, this can be formally + defined, but it is very painful in a theorem prover (since there is no + direct characterisation of the set of dissimlar derivatives). + Fortunately, there is a much simpler approach using \emph{partial derivatives}. They were introduced by Antimirov \cite{Antimirov95} and can be defined @@ -1686,49 +1718,97 @@ & @{text "\"} & @{thm (rhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\ @{thm (lhs) pder.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~% - @{term "(Times_set (pder c r\<^isub>1) r\<^isub>2) \ (pder c r\<^isub>2)"}\\ + @{term "(Timess (pder c r\<^isub>1) r\<^isub>2) \ (pder c r\<^isub>2)"}\\ & & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~% - @{term "Times_set (pder c r\<^isub>1) r\<^isub>2"}\\ + @{term "Timess (pder c r\<^isub>1) r\<^isub>2"}\\ @{thm (lhs) pder.simps(6)} & @{text "\"} & @{thm (rhs) pder.simps(6)}\smallskip\\ @{thm (lhs) pders.simps(1)} & @{text "\"} & @{thm (rhs) pders.simps(1)}\\ - @{thm (lhs) pders.simps(2)} & @{text "\"} & @{thm (rhs) pders.simps(2)}\\ + @{thm (lhs) pders.simps(2)} & @{text "\"} & @{text "\ (pders s) ` (pder c r)"}\\ \end{tabular} \end{center} \noindent - Unlike `simple' derivatives, these functions return a set of regular - expressions. In the @{const Times} and @{const Star} cases we use + Again the last two clauses extend partial derivatives from characters to strings. + Unlike `simple' derivatives, the functions for partial derivatives return sets of regular + expressions. In the @{const Times} and @{const Star} cases we therefore use the + auxiliary definition \begin{center} @{text "TIMESS rs r \ {TIMES r' r | r' \ rs}"} \end{center} \noindent - in order to `sequence' a regular expressions with respect to a set of regular - expresions. Note that in the last case we first build the set of partial derivatives - w.r.t~@{text c}, then build the image of this set under the function @{term "pders s"} - and finally `union up' all resulting sets. Note also that in some sense, partial - derivatives have the @{text "ACI"}-identities already build in. Antimirov - \cite{Antimirov95} - showed + in order to `sequence' a regular expression with a set of regular + expressions. Note that in the last clause we first build the set of partial + derivatives w.r.t~the character @{text c}, then build the image of this set under the + function @{term "pders s"} and finally `union up' all resulting sets. It will be + convenient to introduce the following abbreviation + + \begin{center} + @{abbrev "pderss s A"} + \end{center} + + \noindent + which simplifies the last clause of @{const "pders"} to + + \begin{center} + \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}} + @{thm (lhs) pders.simps(2)} & @{text "\"} & @{thm (rhs) pders.simps(2)}\\ + \end{tabular} + \end{center} + + Partial derivatives can be seen as having the @{text "ACI"}-identities already built in: + taking the partial derivatives of the + regular expressions in \eqref{ACI} gives us in each case + equal sets. Antimirov \cite{Antimirov95} showed a similar result to + \eqref{Dersders} for partial derivatives: \begin{equation} - \mbox{\begin{tabular}{c} - @{thm Der_pder}\\ - @{thm Ders_pders} + \mbox{\begin{tabular}{lc} + @{text "(i)"} & @{thm Der_pder}\\ + @{text "(ii)"} & @{thm Ders_pders} \end{tabular}} - \end{equation} + \end{equation} + + \begin{proof} + The first fact is by a simple induction on @{text r}. For the second we slightly + modify Antimirov's proof by performing an induction on @{text s} where we + genaralise over all @{text r}. That means in the @{text "cons"}-case the + induction hypothesis is + + \begin{center} + @{text "(IH)"}\hspace{3mm}@{term "\r. Ders s (lang r) = \ lang ` (pders s r)"} + \end{center} \noindent - and proved that for every language and regular expression there are only finitely + With this we can establish + + \begin{center} + \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}ll} + @{term "Ders (c # s) (lang r)"} + & @{text "="} & @{term "Ders s (Der c (lang r))"} & by def.\\ + & @{text "="} & @{term "Ders s (\ lang ` (pder c r))"} & by @{text "(i)"}\\ + & @{text "="} & @{term "\ (Ders s) ` (lang ` (pder c r))"} & by def.~of @{text "Ders"}\\ + & @{text "="} & @{term "\ lang ` (\ pders s ` (pder c r))"} & by IH\\ + & @{text "="} & @{term "\ lang ` (pders (c # s) r)"} & by def.\\ + \end{tabular} + \end{center} + + \noindent + In order to apply the induction hypothesis in the fourth step, we need the generalisation + over all regular expressions @{text r}. The case for the empty string is routine and omitted. + \end{proof} + + Antimirov also proved that for every language and regular expression there are only finitely many partial derivatives. *} section {* Closure Properties *} text {* - The beautiful characteristics of regular languages is that they are closed - under many operations. Closure under union, sequencencing and Kleene-star + \noindent + The real beauty of regular languages is that they are closed + under almost all set operations. Closure under union, concatenation and Kleene-star are trivial to establish given our definition of regularity (Def.~\ref{regular}). More interesting is the closure under complement, because it seems difficult to construct a regular expression for the complement diff -r 07a269d9642b -r 9f46a9571e37 Journal/document/root.bib --- a/Journal/document/root.bib Wed Aug 03 17:08:31 2011 +0000 +++ b/Journal/document/root.bib Fri Aug 05 05:34:11 2011 +0000 @@ -1,3 +1,5 @@ + + @article{OwensReppyTuron09, author = {S.~Owens and J.~Reppy and A.~Turon}, title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined}, diff -r 07a269d9642b -r 9f46a9571e37 Journal/document/root.tex --- a/Journal/document/root.tex Wed Aug 03 17:08:31 2011 +0000 +++ b/Journal/document/root.tex Fri Aug 05 05:34:11 2011 +0000 @@ -54,7 +54,7 @@ to formalise in HOL-based theorem provers. The reason is that they need to be represented as graphs, matrices or functions, none of which are inductive datatypes. Also convenient operations for disjoint unions of -graphs and functions are not easily formalisiable in HOL. In contrast, regular +graphs, matrices and functions are not easily formalisiable in HOL. In contrast, regular expressions can be defined conveniently as a datatype and a corresponding reasoning infrastructure comes for free. We show in this paper that a central result from formal language theory---the Myhill-Nerode theorem---can be diff -r 07a269d9642b -r 9f46a9571e37 Myhill_2.thy --- a/Myhill_2.thy Wed Aug 03 17:08:31 2011 +0000 +++ b/Myhill_2.thy Fri Aug 05 05:34:11 2011 +0000 @@ -101,21 +101,17 @@ lemma tag_finite_imageD: assumes rng_fnt: "finite (range tag)" - and same_tag_eqvt: "=tag= \ \A" + and refined: "=tag= \ \A" shows "finite (UNIV // \A)" proof (rule_tac refined_partition_finite [of "=tag="]) show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt]) next - from same_tag_eqvt - show "=tag= \ \A" . + show "=tag= \ \A" using refined . next show "equiv UNIV =tag=" - unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def + and "equiv UNIV (\A)" + unfolding equiv_def str_eq_def tag_eq_def refl_on_def sym_def trans_def by auto -next - show "equiv UNIV (\A)" - unfolding equiv_def str_eq_def sym_def refl_on_def trans_def - by blast qed @@ -139,18 +135,16 @@ proof fix x assume "x \ UNIV // \{[]}" - then obtain y where h: "x = {z. (y, z) \ \{[]}}" + 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_def) - thus ?thesis by simp - next - case False with h - have "x = UNIV - {[]}" by (auto simp: str_eq_def) - thus ?thesis by simp - qed + { assume "y = []" + with h have "x = {[]}" by (auto simp: str_eq_def) + then have "x \ {{[]}, UNIV - {[]}}" by simp } + moreover + { assume "y \ []" + with h have "x = UNIV - {[]}" by (auto simp: str_eq_def) + then have "x \ {{[]}, UNIV - {[]}}" by simp } + ultimately show "x \ {{[]}, UNIV - {[]}}" by blast qed lemma quot_one_finiteI [intro]: @@ -408,7 +402,7 @@ definition tag_Star :: "'a lang \ 'a list \ ('a lang) set" where - "tag_Star A \ (\x. {\A `` {v} | u v. u < x \ u \ A\ \ (u, v) \ Partitions x})" + "tag_Star A \ \x. {\A `` {v} | u v. u < x \ u \ A\ \ (u, v) \ Partitions x}" lemma tag_Star_non_empty_injI: assumes a: "tag_Star A x = tag_Star A y" @@ -444,11 +438,13 @@ and c: "x @ z \ A\" and d: "x = []" shows "y @ z \ A\" -using assms -apply(simp) -apply(simp add: tag_Star_def strict_prefix_def) -apply(auto simp add: prefix_def Partitions_def) -by (metis Nil_in_star append_self_conv2) +proof - + from a have "{} = tag_Star A y" unfolding tag_Star_def using d by auto + then have "y = []" + unfolding tag_Star_def Partitions_def strict_prefix_def prefix_def + by (auto) (metis Nil_in_star append_self_conv2) + then show "y @ z \ A\" using c d by simp +qed lemma quot_star_finiteI [intro]: assumes finite1: "finite (UNIV // \A)"