| author | Christian Urban <urbanc@in.tum.de> |
| Wed, 06 Sep 2017 00:52:08 +0100 | |
| changeset 273 | e85099ac4c6c |
| parent 272 | f16019b11179 |
| child 274 | 692b62426677 |
| thys/Journal/Paper.thy | file | annotate | diff | comparison | revisions | |
| thys/Positions.thy | file | annotate | diff | comparison | revisions | |
| thys/SpecExt.thy | file | annotate | diff | comparison | revisions |
--- a/thys/Journal/Paper.thy Sun Aug 27 00:03:31 2017 +0300 +++ b/thys/Journal/Paper.thy Wed Sep 06 00:52:08 2017 +0100 @@ -19,6 +19,10 @@ "_Collect" :: "pttrn => bool => 'a set" ("(1{_ \<^raw:\mbox{\boldmath$\mid$}> _})") "_CollectIn" :: "pttrn => 'a set => bool => 'a set" ("(1{_ \<in> _ |e _})") +syntax + "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>_.a./ _)" [0, 10] 10) + "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>!_.a./ _)" [0, 10] 10) + abbreviation "der_syn r c \<equiv> der c r" @@ -37,12 +41,12 @@ If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and - ZERO ("\<^bold>0" 78) and - ONE ("\<^bold>1" 1000) and + ZERO ("\<^bold>0" 81) and + ONE ("\<^bold>1" 81) and CHAR ("_" [1000] 80) and ALT ("_ + _" [77,77] 78) and SEQ ("_ \<cdot> _" [77,77] 78) and - STAR ("_\<^sup>\<star>" [1000] 78) and + STAR ("_\<^sup>\<star>" [78] 78) and val.Void ("Empty" 78) and val.Char ("Char _" [1000] 78) and @@ -56,6 +60,7 @@ der_syn ("_\\_" [79, 1000] 76) and ders_syn ("_\\_" [79, 1000] 76) and flat ("|_|" [75] 74) and + flats ("|_|" [72] 74) and Sequ ("_ @ _" [78,77] 63) and injval ("inj _ _ _" [79,77,79] 76) and mkeps ("mkeps _" [79] 76) and @@ -106,6 +111,7 @@ *) + (*>*) @@ -187,8 +193,8 @@ matches also. By the Star Rule we know @{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} matches @{text "iffoo"}, respectively @{text "if"}, in exactly one `iteration' of the star. The -Empty String Rule is for cases where, for example, @{text -"(a\<^sup>\<star>)\<^sup>\<star>"} matches against the +Empty String Rule is for cases where, for example, the regular expression +@{text "(a\<^sup>\<star>)\<^sup>\<star>"} matches against the string @{text "bc"}. Then the longest initial matched substring is the empty string, which is matched by both the whole regular expression and the parenthesised subexpression. @@ -202,13 +208,34 @@ expression matches a string, values encode the information of \emph{how} the string is matched by the regular expression---that is, which part of the string is matched by which part of the regular -expression. For this consider again the the string @{text "xy"} and -the regular expression \mbox{@{text "(x + (y + -xy))\<^sup>\<star>"}}. The POSIX value, which corresponds to using the -star in only one repetition, +expression. For this consider again the string @{text "xy"} and +the regular expression \mbox{@{text "(x + (y + xy))\<^sup>\<star>"}} +(this time fully parenthesised). We can view this regular expression +as tree and if the string @{text xy} is matched by two Star +`iterations', then the @{text x} is matched by the left-most +alternative in this tree and the @{text y} by the right-left alternative. This +suggests to record this matching as + +\begin{center} +@{term "Stars [Left(Char x), Right(Left(Char y))]"} +\end{center} +\noindent where @{const Stars}, @{text Left}, @{text Right} and @{text +Char} are constructors for values. @{text Stars} records how many +iterations were used; @{text Left}, respectively @{text Right}, which +alternative is used. This `tree view' leads naturally to the +idea that regular expressions act as types and values as inhabiting +those types. This view was first put forward by ???. The value for the +single `iteration', i.e.~the POSIX value, would look as follows -\marginpar{explain values; who introduced them} +\begin{center} +@{term "Stars [Seq (Char x) (Char y)]"} +\end{center} + +\noindent where @{const Stars} has only a single-element list for the +single iteration and @{const Seq} indicates that @{term xy} is matched +by a sequence regular expression, which we will in what follows +write more formally as @{term "SEQ x y"}. Sulzmann and Lu give a simple algorithm to calculate a value that @@ -280,15 +307,17 @@ section {* Preliminaries *} -text {* \noindent Strings in Isabelle/HOL are lists of characters with the -empty string being represented by the empty list, written @{term "[]"}, and -list-cons being written as @{term "DUMMY # DUMMY"}. Often we use the usual -bracket notation for lists also for strings; for example a string consisting -of just a single character @{term c} is written @{term "[c]"}. By using the +text {* \noindent Strings in Isabelle/HOL are lists of characters with +the empty string being represented by the empty list, written @{term +"[]"}, and list-cons being written as @{term "DUMMY # DUMMY"}. Often +we use the usual bracket notation for lists also for strings; for +example a string consisting of just a single character @{term c} is +written @{term "[c]"}. We use the usual definitions for +\emph{prefixes} and \emph{strict prefixes} of strings. By using the type @{type char} for characters we have a supply of finitely many characters roughly corresponding to the ASCII character set. Regular -expressions are defined as usual as the elements of the following inductive -datatype: +expressions are defined as usual as the elements of the following +inductive datatype: \begin{center} @{text "r :="} @@ -308,16 +337,18 @@ \begin{center} \begin{tabular}{l@ {\hspace{4mm}}rcl} - (1) & @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\ - (2) & @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\ - (3) & @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\ - (4) & @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ - (5) & @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ - (6) & @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\ + \textit{(1)} & @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\ + \textit{(2)} & @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\ + \textit{(3)} & @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\ + \textit{(4)} & @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & + @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ + \textit{(5)} & @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & + @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ + \textit{(6)} & @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\ \end{tabular} \end{center} - \noindent In clause (4) we use the operation @{term "DUMMY ;; + \noindent In clause \textit{(4)} we use the operation @{term "DUMMY ;; DUMMY"} for the concatenation of two languages (it is also list-append for strings). We use the star-notation for regular expressions and for languages (in the last clause above). The star for languages is defined @@ -362,12 +393,14 @@ @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\ @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}%\medskip\\ - \end{tabular} - \end{center} + @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\medskip\\ - \begin{center} - \begin{tabular}{lcl} +% \end{tabular} +% \end{center} + +% \begin{center} +% \begin{tabular}{lcl} + @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\ @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\ @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\ @@ -392,9 +425,9 @@ \begin{proposition}\label{derprop}\mbox{}\\ \begin{tabular}{ll} - @{text "(1)"} & @{thm (lhs) nullable_correctness} if and only if + \textit{(1)} & @{thm (lhs) nullable_correctness} if and only if @{thm (rhs) nullable_correctness}, and \\ - @{text "(2)"} & @{thm[mode=IfThen] der_correctness}. + \textit{(2)} & @{thm[mode=IfThen] der_correctness}. \end{tabular} \end{proposition} @@ -457,15 +490,21 @@ \end{tabular} \end{center} - \noindent Sulzmann and Lu also define inductively an inhabitation relation - that associates values to regular expressions. We define this relation as - follows:\footnote{Note that the rule for @{term Stars} differs from our - earlier paper \cite{AusafDyckhoffUrban2016}. There we used the original - definition by Sulzmann and Lu which does not require that the values @{term "v \<in> set vs"} - flatten to a non-empty string. The reason for introducing the - more restricted version of lexical values is convenience later - on when reasoning about - an ordering relation for values.} + \noindent We will sometimes refer to the underlying string of a + value as \emph{flattened value}. We will also overload our notation and + use @{term "flats vs"} for flattening a list of values and concatenating + the resulting strings. + + Sulzmann and Lu define + inductively an \emph{inhabitation relation} that associates values to + regular expressions. We define this relation as + follows:\footnote{Note that the rule for @{term Stars} differs from + our earlier paper \cite{AusafDyckhoffUrban2016}. There we used the + original definition by Sulzmann and Lu which does not require that + the values @{term "v \<in> set vs"} flatten to a non-empty + string. The reason for introducing the more restricted version of + lexical values is convenience later on when reasoning about an + ordering relation for values.} \begin{center} \begin{tabular}{c@ {\hspace{12mm}}c} @@ -501,7 +540,7 @@ set of all \emph{Lexical Values} inhabited by @{text r} with the underlying string being @{text s}:\footnote{Okui and Suzuki refer to our lexical values as \emph{canonical values} in \cite{OkuiSuzuki2010}. The notion of \emph{non-problematic - values} by Cardelli and Frisch \cite{Frisch2004} is similar, but not identical + values} by Cardelli and Frisch \cite{Frisch2004} is related, but not identical to our lexical values.} \begin{center} @@ -519,7 +558,7 @@ @{term Stars}-rule above. For example using Sulzmann and Lu's less restrictive definition, @{term "LV (STAR ONE) []"} would contain infinitely many values, but according to our more restricted - definition @{thm LV_STAR_ONE_empty}. + definition only a single value, namely @{thm LV_STAR_ONE_empty}. If a regular expression @{text r} matches a string @{text s}, then generally the set @{term "LV r s"} is not just a singleton set. In @@ -618,25 +657,25 @@ % \begin{center} \begin{tabular}{l@ {\hspace{5mm}}lcl} - (1) & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ - (2) & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & + \textit{(1)} & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ + \textit{(2)} & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ - (3) & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & + \textit{(3)} & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ - (4) & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ + \textit{(4)} & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ - (5) & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ + \textit{(5)} & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ - (6) & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ + \textit{(6)} & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ - (7) & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ + \textit{(7)} & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\ \end{tabular} \end{center} \noindent To better understand what is going on in this definition it might be instructive to look first at the three sequence cases (clauses - (4)--(6)). In each case we need to construct an ``injected value'' for + \textit{(4)} -- \textit{(6)}). In each case we need to construct an ``injected value'' for @{term "SEQ r\<^sub>1 r\<^sub>2"}. This must be a value of the form @{term "Seq DUMMY DUMMY"}\,. Recall the clause of the @{text derivative}-function for sequence regular expressions: @@ -648,22 +687,22 @@ \noindent Consider first the @{text "else"}-branch where the derivative is @{term "SEQ (der c r\<^sub>1) r\<^sub>2"}. The corresponding value must therefore be of the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the left-hand - side in clause~(4) of @{term inj}. In the @{text "if"}-branch the derivative is an + side in clause~\textit{(4)} of @{term inj}. In the @{text "if"}-branch the derivative is an alternative, namely @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}. This means we either have to consider a @{text Left}- or @{text Right}-value. In case of the @{text Left}-value we know further it must be a value for a sequence regular expression. Therefore the pattern - we match in the clause (5) is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, - while in (6) it is just @{term "Right v\<^sub>2"}. One more interesting - point is in the right-hand side of clause (6): since in this case the + we match in the clause \textit{(5)} is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, + while in \textit{(6)} it is just @{term "Right v\<^sub>2"}. One more interesting + point is in the right-hand side of clause \textit{(6)}: since in this case the regular expression @{text "r\<^sub>1"} does not ``contribute'' to matching the string, that means it only matches the empty string, we need to call @{const mkeps} in order to construct a value for how @{term "r\<^sub>1"} can match this empty string. A similar argument applies for why we can - expect in the left-hand side of clause (7) that the value is of the form + expect in the left-hand side of clause \textit{(7)} that the value is of the form @{term "Seq v (Stars vs)"}---the derivative of a star is @{term "SEQ (der c r) (STAR r)"}. Finally, the reason for why we can ignore the second argument - in clause (1) of @{term inj} is that it will only ever be called in cases + in clause \textit{(1)} of @{term inj} is that it will only ever be called in cases where @{term "c=d"}, but the usual linearity restrictions in patterns do not allow us to build this constraint explicitly into our function definition.\footnote{Sulzmann and Lu state this clause as @{thm (lhs) @@ -712,7 +751,7 @@ part of this section we prove that this algorithm is correct. The well-known idea of POSIX matching is informally defined by some - rules such as the longest match and priority rule (see + rules such as the Longest Match and Priority Rules (see Introduction); as correctly argued in \cite{Sulzmann2014}, this needs formal specification. Sulzmann and Lu define an ``ordering relation'' between values and argue that there is a maximum value, @@ -720,8 +759,8 @@ introduce a simple inductive definition that specifies directly what a \emph{POSIX value} is, incorporating the POSIX-specific choices into the side-conditions of our rules. Our definition is inspired by - the matching relation given by Vansummeren - \cite{Vansummeren2006}. The relation we define is ternary and + the matching relation given by Vansummeren~\cite{Vansummeren2006}. + The relation we define is ternary and written as \mbox{@{term "s \<in> r \<rightarrow> v"}}, relating strings, regular expressions and values; the inductive rules are given in Figure~\ref{POSIXrules}. @@ -802,8 +841,8 @@ @{term v} cannot be flattened to the empty string. In effect, we require that in each ``iteration'' of the star, some non-empty substring needs to be ``chipped'' away; only in case of the empty string we accept @{term - "Stars []"} as the POSIX value. Indeed we can show that our POSIX value - is a lexical value which excludes those @{text Stars} containing subvalues + "Stars []"} as the POSIX value. Indeed we can show that our POSIX values + are lexical values which exclude those @{text Stars} that contain subvalues that flatten to the empty string. \begin{lemma}\label{LVposix} @@ -909,7 +948,7 @@ By induction on @{term s} using Lemma~\ref{lemmkeps} and \ref{Posix2}.\qed \end{proof} - \noindent In (2) we further know by Theorem~\ref{posixdeterm} that the + \noindent In \textit{(2)} we further know by Theorem~\ref{posixdeterm} that the value returned by the lexer must be unique. A simple corollary of our two theorems is: @@ -942,20 +981,20 @@ details of their proofs, but which are evidently not in final form yet. Unfortunately, we were not able to verify claims that their ordering has properties such as being transitive or having maximal - elements. + elements. Okui and Suzuki \cite{OkuiSuzuki2010,OkuiSuzukiTech} described another ordering of values, which they use to establish the correctness of their automata-based algorithm for POSIX matching. Their ordering resembles some aspects of the one given by Sulzmann - and Lu, but is quite different. To begin with, Okui and Suzuki - identify POSIX values as minimal, rather than maximal, elements in - their ordering. A more substantial difference is that the ordering - by Okui and Suzuki uses \emph{positions} in order to identify and - compare subvalues. Positions are lists of natural numbers. This - allows them to quite naturally formalise the Longest Match and - Priority rules of the informal POSIX standard. Consider for example - the value @{term v} + and Lu, but overall is quite different. To begin with, Okui and + Suzuki identify POSIX values as minimal, rather than maximal, + elements in their ordering. A more substantial difference is that + the ordering by Okui and Suzuki uses \emph{positions} in order to + identify and compare subvalues. Positions are lists of natural + numbers. This allows them to quite naturally formalise the Longest + Match and Priority rules of the informal POSIX standard. Consider + for example the value @{term v} \begin{center} @{term "v == Stars [Seq (Char x) (Char y), Char z]"} @@ -965,8 +1004,8 @@ At position @{text "[0,1]"} of this value is the subvalue @{text "Char y"} and at position @{text "[1]"} the subvalue @{term "Char z"}. At the `root' position, or empty list - @{term "[]"}, is the whole value @{term v}. The positions @{text - "[0,1,0]"} and @{text "[2]"}, for example, are outside of @{text + @{term "[]"}, is the whole value @{term v}. Positions such as @{text + "[0,1,0]"} or @{text "[2]"} are outside of @{text v}. If it exists, the subvalue of @{term v} at a position @{text p}, written @{term "at v p"}, can be recursively defined by @@ -987,7 +1026,7 @@ \noindent In the last clause we use Isabelle's notation @{term "vs ! n"} for the @{text n}th element in a list. The set of positions inside a value @{text v}, - written @{term "Pos v"}, is given by the clauses + written @{term "Pos v"}, is given by \begin{center} \begin{tabular}{lcl} @@ -1003,7 +1042,7 @@ \end{center} \noindent - whereby @{text len} stands for the length of a list. Clearly + whereby @{text len} in the last clause stands for the length of a list. Clearly for every position inside a value there exists a subvalue at that position. @@ -1019,7 +1058,7 @@ \end{center} \noindent Both values match the string @{text "xyz"}, that means if - we flatten the values at their respective root position, we obtain + we flatten these values at their respective root position, we obtain @{text "xyz"}. However, at position @{text "[0]"}, @{text v} matches @{text xy} whereas @{text w} matches only the shorter @{text x}. So according to the Longest Match Rule, we should prefer @{text v}, @@ -1046,7 +1085,7 @@ @{term "v == Left (Char x)"} \qquad and \qquad @{term "w == Right (Char x)"} \end{center} - \noindent Both values match @{text x}, but at position @{text "[0]"} + \noindent Both values match @{text x}. At position @{text "[0]"} the norm of @{term v} is @{text 1} (the subvalue matches @{text x}), but the norm of @{text w} is @{text "-1"} (the position is outside @{text w} according to how we defined the `inside' positions of @@ -1055,7 +1094,8 @@ "pflat_len w [1]"} are reversed, but the point is that subvalues will be analysed according to lexicographically ordered positions. According to this ordering, the position @{text "[0]"} - takes precedence. The lexicographic ordering of positions, written + takes precedence over @{text "[1]"} and thus also @{text v} will be + preferred over @{text w}. The lexicographic ordering of positions, written @{term "DUMMY \<sqsubset>lex DUMMY"}, can be conveniently formalised by three inference rules @@ -1070,8 +1110,9 @@ With the norm and lexicographic order in place, we can state the key definition of Okui and Suzuki - \cite{OkuiSuzuki2010}: a value @{term "v\<^sub>1"} is \emph{smaller} than - @{term "v\<^sub>2"} if and only if $(i)$ the norm at position @{text p} is + \cite{OkuiSuzuki2010}: a value @{term "v\<^sub>1"} is \emph{smaller at position @{text p}} than + @{term "v\<^sub>2"}, written @{term "v\<^sub>1 \<sqsubset>val p v\<^sub>2"}, + if and only if $(i)$ the norm at position @{text p} is greater in @{term "v\<^sub>1"} (that is the string @{term "flat (at v\<^sub>1 p)"} is longer than @{term "flat (at v\<^sub>2 p)"}) and $(ii)$ all subvalues at positions that are inside @{term "v\<^sub>1"} or @{term "v\<^sub>2"} and that are @@ -1106,7 +1147,9 @@ While we encountered a number of obstacles for establishing properties like transitivity for the ordering of Sulzmann and Lu (and which we failed to overcome), it is relatively straightforward to establish this - property for the ordering by Okui and Suzuki. + property for the orderings + @{term "DUMMY :\<sqsubset>val DUMMY"} and @{term "DUMMY :\<sqsubseteq>val DUMMY"} + by Okui and Suzuki. \begin{lemma}[Transitivity]\label{transitivity} @{thm [mode=IfThen] PosOrd_trans[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2" and ?v3.0="v\<^sub>3"]} @@ -1118,42 +1161,103 @@ "v\<^sub>3"}) are `distinct'. Since @{text "\<prec>\<^bsub>lex\<^esub>"} is trichotomous, we need to consider three cases, namely @{term "p = q"}, @{term "p \<sqsubset>lex q"} and - @{term "q \<sqsubset>lex p"}. Let us look at the first case. - Clearly @{term "pflat_len v\<^sub>2 p < pflat_len v\<^sub>1 p"} - and @{term "pflat_len v\<^sub>3 p < pflat_len v\<^sub>2 p"} - imply @{term "pflat_len v\<^sub>3 p < pflat_len v\<^sub>1 p"}. - It remains to show for a @{term "p' \<in> Pos v\<^sub>1 \<union> Pos v\<^sub>3"} - with @{term "p' \<sqsubset>lex p"} that - @{term "pflat_len v\<^sub>1 p' = pflat_len v\<^sub>3 p'"} holds. - Suppose @{term "p' \<in> Pos v\<^sub>1"}, then we can infer from the - first assumption that @{term "pflat_len v\<^sub>1 p' = pflat_len v\<^sub>2 p'"}. - But this means that @{term "p'"} must be in @{term "Pos v\<^sub>2"} too. - Hence we can use the second assumption and infer @{term "pflat_len v\<^sub>2 p' = pflat_len v\<^sub>3 p'"}, which concludes - this case with @{term "v\<^sub>1 :\<sqsubset>val v\<^sub>3"}. - The reasoning in the other cases is similar.\qed + @{term "q \<sqsubset>lex p"}. Let us look at the first case. Clearly + @{term "pflat_len v\<^sub>2 p < pflat_len v\<^sub>1 p"} and @{term + "pflat_len v\<^sub>3 p < pflat_len v\<^sub>2 p"} imply @{term + "pflat_len v\<^sub>3 p < pflat_len v\<^sub>1 p"}. It remains to show + that for a @{term "p' \<in> Pos v\<^sub>1 \<union> Pos v\<^sub>3"} + with @{term "p' \<sqsubset>lex p"} that @{term "pflat_len v\<^sub>1 + p' = pflat_len v\<^sub>3 p'"} holds. Suppose @{term "p' \<in> Pos + v\<^sub>1"}, then we can infer from the first assumption that @{term + "pflat_len v\<^sub>1 p' = pflat_len v\<^sub>2 p'"}. But this means + that @{term "p'"} must be in @{term "Pos v\<^sub>2"} too (the norm + cannot be @{text "-1"} given @{term "p' \<in> Pos v\<^sub>1"}). + Hence we can use the second assumption and + infer @{term "pflat_len v\<^sub>2 p' = pflat_len v\<^sub>3 p'"}, + which concludes this case with @{term "v\<^sub>1 :\<sqsubset>val + v\<^sub>3"}. The reasoning in the other cases is similar.\qed \end{proof} - \noindent It is straightforward to show that @{text "\<prec>"} and - $\preccurlyeq$ are partial orders. Okui and Suzuki also show that it - is a linear order for lexical values \cite{OkuiSuzuki2010} of a given - regular expression and given string, but we have not done this. It is + \noindent + The proof for $\preccurlyeq$ is similar and omitted. + It is also straightforward to show that @{text "\<prec>"} and + $\preccurlyeq$ are partial orders. Okui and Suzuki furthermore show that they + are linear orderings for lexical values \cite{OkuiSuzuki2010} of a given + regular expression and given string, but we have not formalised this in Isabelle. It is not essential for our results. What we are going to show below is - that for a given @{text r} and @{text s}, the ordering has a unique + that for a given @{text r} and @{text s}, the orderings have a unique minimal element on the set @{term "LV r s"}, which is the POSIX value - we defined in the previous section. + we defined in the previous section. We start with two properties that + show how the length of a flattened value relates to the @{text "\<prec>"}-ordering. + + \begin{proposition}\mbox{}\smallskip\\\label{ordlen} + \begin{tabular}{@ {}ll} + (1) & + @{thm [mode=IfThen] PosOrd_shorterE[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}\\ + (2) & + @{thm [mode=IfThen] PosOrd_shorterI[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} + \end{tabular} + \end{proposition} + + \noindent Both properties follow from the definition of the ordering. Note that + \textit{(2)} entails that a value, say @{term "v\<^sub>2"}, whose underlying + string is a strict prefix of another flattened value, say @{term "v\<^sub>1"}, then + @{term "v\<^sub>1"} must be smaller than @{term "v\<^sub>2"}. For our proofs it + will be useful to have the following properties---in each case the underlying strings + of the compared values are the same: - - Lemma 1 - - @{thm [mode=IfThen] PosOrd_shorterE[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} + \begin{proposition}\mbox{}\smallskip\\\label{ordintros} + \begin{tabular}{ll} + \textit{(1)} & + @{thm [mode=IfThen] PosOrd_Left_Right[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}\\ + \textit{(2)} & If + @{thm (prem 1) PosOrd_Left_eq[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} \;then\; + @{thm (lhs) PosOrd_Left_eq[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} \;iff\; + @{thm (rhs) PosOrd_Left_eq[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}\\ + \textit{(3)} & If + @{thm (prem 1) PosOrd_Right_eq[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} \;then\; + @{thm (lhs) PosOrd_Right_eq[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} \;iff\; + @{thm (rhs) PosOrd_Right_eq[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}\\ + \textit{(4)} & If + @{thm (prem 1) PosOrd_Seq_eq[where ?v2.0="v\<^sub>2" and ?w2.0="w\<^sub>2"]} \;then\; + @{thm (lhs) PosOrd_Seq_eq[where ?v2.0="v\<^sub>2" and ?w2.0="w\<^sub>2"]} \;iff\; + @{thm (rhs) PosOrd_Seq_eq[where ?v2.0="v\<^sub>2" and ?w2.0="w\<^sub>2"]}\\ + \textit{(5)} & If + @{thm (prem 2) PosOrd_SeqI1[simplified, where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2" and + ?w1.0="w\<^sub>1" and ?w2.0="w\<^sub>2"]} \;and\; + @{thm (prem 1) PosOrd_SeqI1[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2" and + ?w1.0="w\<^sub>1" and ?w2.0="w\<^sub>2"]} \;then\; + @{thm (concl) PosOrd_SeqI1[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2" and + ?w1.0="w\<^sub>1" and ?w2.0="w\<^sub>2"]}\\ + \textit{(6)} & If + @{thm (prem 1) PosOrd_Stars_append_eq[where ?vs1.0="vs\<^sub>1" and ?vs2.0="vs\<^sub>2"]} \;then\; + @{thm (lhs) PosOrd_Stars_append_eq[where ?vs1.0="vs\<^sub>1" and ?vs2.0="vs\<^sub>2"]} \;iff\; + @{thm (rhs) PosOrd_Stars_append_eq[where ?vs1.0="vs\<^sub>1" and ?vs2.0="vs\<^sub>2"]}\\ + + \textit{(7)} & If + @{thm (prem 2) PosOrd_StarsI[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2" and + ?vs1.0="vs\<^sub>1" and ?vs2.0="vs\<^sub>2"]} \;and\; + @{thm (prem 1) PosOrd_StarsI[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2" and + ?vs1.0="vs\<^sub>1" and ?vs2.0="vs\<^sub>2"]} \;then\; + @{thm (concl) PosOrd_StarsI[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2" and + ?vs1.0="vs\<^sub>1" and ?vs2.0="vs\<^sub>2"]}\\ + \end{tabular} + \end{proposition} - but in the other direction only - - @{thm [mode=IfThen] PosOrd_shorterI[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} - + \noindent One might prefer that statements \textit{(4)} and \textit{(5)} + (respectively \textit{(6)} and \textit{(7)}) + are combined into a single \textit{iff}-statement (like the ones for @{text + Left} and @{text Right}). Unfortunately this cannot be done easily: such + a single statement would require an additional assumption about the + two values @{term "Seq v\<^sub>1 v\<^sub>2"} and @{term "Seq w\<^sub>1 w\<^sub>2"} + being inhabited by the same regular expression. The + complexity of the proofs involved seems to not justify such a + `cleaner' single statement. The statements given are just the properties that + allow us to establish our theorems. The proofs for Proposition~\ref{ordintros} + are routine. - Next we establish how Okui and Suzuki's ordering relates to our + Next we establish how Okui and Suzuki's orderings relate to our definition of POSIX values. Given a @{text POSIX} value @{text "v\<^sub>1"} for @{text r} and @{text s}, then any other lexical value @{text "v\<^sub>2"} in @{term "LV r s"} is greater or equal than @{text @@ -1179,47 +1283,55 @@ \begin{itemize} \item[$\bullet$] Case @{text "P+L"} with @{term "s \<in> (ALT r\<^sub>1 r\<^sub>2) - \<rightarrow> (Left w\<^sub>1)"}: In this case @{term "v\<^sub>1 = - Left w\<^sub>1"} and the value @{term "v\<^sub>2"} is either of the + \<rightarrow> (Left w\<^sub>1)"}: In this case the value + @{term "v\<^sub>2"} is either of the form @{term "Left w\<^sub>2"} or @{term "Right w\<^sub>2"}. In the - latter case we can immediately conclude with @{term "v\<^sub>1 - :\<sqsubseteq>val v\<^sub>2"} since a @{text Left}-value with the + latter case we can immediately conclude with \mbox{@{term "v\<^sub>1 + :\<sqsubseteq>val v\<^sub>2"}} since a @{text Left}-value with the same underlying string @{text s} is always smaller than a - @{text Right}-value. In the former case we have @{term "w\<^sub>2 + @{text Right}-value by Proposition~\ref{ordintros}\textit{(1)}. + In the former case we have @{term "w\<^sub>2 \<in> LV r\<^sub>1 s"} and can use the induction hypothesis to infer @{term "w\<^sub>1 :\<sqsubseteq>val w\<^sub>2"}. Because @{term "w\<^sub>1"} and @{term "w\<^sub>2"} have the same underlying string @{text s}, we can conclude with @{term "Left w\<^sub>1 - :\<sqsubseteq>val Left w\<^sub>2"} by Prop ???.\smallskip + :\<sqsubseteq>val Left w\<^sub>2"} using + Proposition~\ref{ordintros}\textit{(2)}.\smallskip \item[$\bullet$] Case @{text "P+R"} with @{term "s \<in> (ALT r\<^sub>1 r\<^sub>2) \<rightarrow> (Right w\<^sub>1)"}: This case similar to the previous case, except that we additionally know @{term "s \<notin> L r\<^sub>1"}. This is needed when @{term "v\<^sub>2"} is of the form - @{term "Left w\<^sub>2"}. Since \mbox{@{term "flat v\<^sub>2 = flat + \mbox{@{term "Left w\<^sub>2"}}. Since \mbox{@{term "flat v\<^sub>2 = flat w\<^sub>2"} @{text "= s"}} and @{term "\<Turnstile> w\<^sub>2 : r\<^sub>1"}, we can derive a contradiction for \mbox{@{term "s \<notin> L r\<^sub>1"}} using Proposition~\ref{inhabs}. So also in this case \mbox{@{term "v\<^sub>1 :\<sqsubseteq>val v\<^sub>2"}}.\smallskip - \item[$\bullet$] Case @{text "PS"} with @{term "(s\<^sub>1 @ s\<^sub>2) \<in> (SEQ - r\<^sub>1 r\<^sub>2) \<rightarrow> (Seq w\<^sub>1 w\<^sub>2)"}: We - can assume @{term "v\<^sub>2 = Seq (u\<^sub>1) (u\<^sub>2)"} with - @{term "\<Turnstile> u\<^sub>1 : r\<^sub>1"} and \mbox{@{term - "\<Turnstile> u\<^sub>2 : r\<^sub>2"}}. We have @{term "s\<^sub>1 @ - s\<^sub>2 = (flat u\<^sub>1) @ (flat u\<^sub>2)"}. By the - side-condition of the @{text PS}-rule we know that either @{term - "s\<^sub>1 = flat u\<^sub>1"} or that @{term "flat u\<^sub>1"} is a - strict prefix ??? of @{term "s\<^sub>1"}. In the latter case we can - infer @{term "w\<^sub>1 :\<sqsubset>val u\<^sub>1"} by ??? and from - this @{term "v\<^sub>1 :\<sqsubseteq>val v\<^sub>2"} by ???. In the - former case we know @{term "u\<^sub>1 \<in> LV r\<^sub>1 s\<^sub>1"} - and @{term "u\<^sub>2 \<in> LV r\<^sub>2 s\<^sub>2"}. With this we - can use the induction hypotheses to infer @{term "w\<^sub>1 - :\<sqsubseteq>val u\<^sub>1"} and @{term "w\<^sub>2 - :\<sqsubseteq>val u\<^sub>2"}. By ??? we can again infer @{term - "v\<^sub>1 :\<sqsubseteq>val v\<^sub>2"}. + \item[$\bullet$] Case @{text "PS"} with @{term "(s\<^sub>1 @ + s\<^sub>2) \<in> (SEQ r\<^sub>1 r\<^sub>2) \<rightarrow> (Seq + w\<^sub>1 w\<^sub>2)"}: We can assume @{term "v\<^sub>2 = Seq + (u\<^sub>1) (u\<^sub>2)"} with @{term "\<Turnstile> u\<^sub>1 : + r\<^sub>1"} and \mbox{@{term "\<Turnstile> u\<^sub>2 : + r\<^sub>2"}}. We have @{term "s\<^sub>1 @ s\<^sub>2 = (flat + u\<^sub>1) @ (flat u\<^sub>2)"}. By the side-condition of the + @{text PS}-rule we know that either @{term "s\<^sub>1 = flat + u\<^sub>1"} or that @{term "flat u\<^sub>1"} is a strict prefix of + @{term "s\<^sub>1"}. In the latter case we can infer @{term + "w\<^sub>1 :\<sqsubset>val u\<^sub>1"} by + Proposition~\ref{ordlen}\textit{(2)} and from this @{term "v\<^sub>1 + :\<sqsubseteq>val v\<^sub>2"} by Proposition~\ref{ordintros}\textit{(5)} + (as noted above @{term "v\<^sub>1"} and @{term "v\<^sub>2"} must have the + same underlying string). + In the former case we know + @{term "u\<^sub>1 \<in> LV r\<^sub>1 s\<^sub>1"} and @{term + "u\<^sub>2 \<in> LV r\<^sub>2 s\<^sub>2"}. With this we can use the + induction hypotheses to infer @{term "w\<^sub>1 :\<sqsubseteq>val + u\<^sub>1"} and @{term "w\<^sub>2 :\<sqsubseteq>val u\<^sub>2"}. By + Proposition~\ref{ordintros}\textit{(4,5)} we can again infer + @{term "v\<^sub>1 :\<sqsubseteq>val + v\<^sub>2"}. \end{itemize} @@ -1228,14 +1340,16 @@ \noindent This theorem shows that our @{text POSIX} value for a regular expression @{text r} and string @{term s} is in fact a - minimal element of the values in @{text "LV r s"}. By ??? we also - know that any value in @{text "LV s' r"}, with @{term "s'"} being a - prefix, cannot be smaller than @{text "v\<^sub>1"}. The next theorem - shows the opposite---namely any minimal element in @{term "LV r s"} - must be a @{text POSIX} value. For this it helps that we proved in - the previous section that whenever a string @{term "s \<in> L r"} then - a corresponding @{text POSIX} value exists and is a lexical value, - see Theorem ??? and Lemma ???. + minimal element of the values in @{text "LV r s"}. By + Proposition~\ref{ordlen}\textit{(2)} we also know that any value in + @{text "LV s' r"}, with @{term "s'"} being a strict prefix, cannot be + smaller than @{text "v\<^sub>1"}. The next theorem shows the + opposite---namely any minimal element in @{term "LV r s"} must be a + @{text POSIX} value. This can be established by induction on @{text + r}, but the proof can be drastically simplified by using the fact + from the previous section about the existence of a @{text POSIX} value + whenever a string @{term "s \<in> L r"}. + \begin{theorem} @{thm [mode=IfThen] PosOrd_Posix[where ?v1.0="v\<^sub>1"]} @@ -1246,23 +1360,31 @@ @{term "s \<in> L r"} by Proposition~\ref{inhabs}. Hence by Theorem~\ref{lexercorrect}(2) there exists a @{text POSIX} value @{term "v\<^sub>P"} with @{term "s \<in> r \<rightarrow> v\<^sub>P"} - and by Lemma~\ref{LVposix} we also have @{term "v\<^sub>P \<in> LV r s"}. + and by Lemma~\ref{LVposix} we also have \mbox{@{term "v\<^sub>P \<in> LV r s"}}. By Theorem~\ref{orderone} we therefore have @{term "v\<^sub>P :\<sqsubseteq>val v\<^sub>1"}. If @{term "v\<^sub>P = v\<^sub>1"} then - we are done. Otherwise we have @{term "v\<^sub>P :\<sqsubset>val v\<^sub>1"} which - however contradicts the second assumption and we are done too.\qed + we are done. Otherwise we have @{term "v\<^sub>P :\<sqsubset>val v\<^sub>1"}, which + however contradicts the second assumption about @{term "v\<^sub>1"} being the smallest + element in @{term "LV r s"}. So we are done in this case too.\qed \end{proof} + \noindent + From this we can also show + that if @{term "LV r s"} is non-empty (or equivalently @{term "s \<in> L r"}) then + it has a unique minimal element: + \begin{corollary} @{thm [mode=IfThen] Least_existence1} \end{corollary} - \noindent To sum up, we have shown that minimal elements according - to the ordering by Okui and Suzuki are exactly the @{text POSIX} - values we defined inductively in Section~\ref{posixsec} - IS THE minimal element unique? We have not shown totality. + \noindent To sum up, we have shown that the (unique) minimal elements + of the ordering by Okui and Suzuki are exactly the @{text POSIX} + values we defined inductively in Section~\ref{posixsec}. This provides + an independent confirmation that our ternary relation formalise the + informal POSIX rules. + *} section {* Optimisations *} @@ -1436,9 +1558,7 @@ A strong point in favour of Sulzmann and Lu's algorithm is that it can be extended in various - ways. - - If we are interested in tokenising a string, then we need to not just + ways. If we are interested in tokenising a string, then we need to not just split up the string into tokens, but also ``classify'' the tokens (for example whether it is a keyword or an identifier). This can be done with only minor modifications to the algorithm by introducing \emph{record
--- a/thys/Positions.thy Sun Aug 27 00:03:31 2017 +0300 +++ b/thys/Positions.thy Wed Sep 06 00:52:08 2017 +0100 @@ -134,7 +134,7 @@ "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" -lemma test: +lemma PosOrd_def2: shows "v1 \<sqsubset>val p v2 \<longleftrightarrow> pflat_len v1 p > pflat_len v2 p \<and> (\<forall>q \<in> Pos v1. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q) \<and> @@ -246,9 +246,13 @@ assumes "v1 :\<sqsubset>val v2" shows "length (flat v2) \<le> length (flat v1)" using assms unfolding PosOrd_ex_def PosOrd_def -apply(auto simp add: pflat_len_def split: if_splits) -apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le) -by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear) +apply(auto) +apply(case_tac p) +apply(simp add: pflat_len_simps) +apply(drule_tac x="[]" in bspec) +apply(simp add: Pos_empty) +apply(simp add: pflat_len_simps) +done lemma PosOrd_shorterI: assumes "length (flat v2) < length (flat v1)" @@ -271,6 +275,7 @@ unfolding pflat_len_def by (auto split: if_splits) + lemma PosOrd_Left_Right: assumes "flat v1 = flat v2" shows "Left v1 :\<sqsubset>val Right v2" @@ -283,7 +288,7 @@ assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2" shows "v1 :\<sqsubset>val v2" using assms -unfolding PosOrd_ex_def test +unfolding PosOrd_ex_def PosOrd_def2 apply(auto simp add: pflat_len_simps) apply(frule pflat_len_inside) apply(auto simp add: pflat_len_simps) @@ -293,7 +298,7 @@ assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2" shows "Left v1 :\<sqsubset>val Left v2" using assms -unfolding PosOrd_ex_def test +unfolding PosOrd_ex_def PosOrd_def2 apply(auto simp add: pflat_len_simps) by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3)) @@ -308,7 +313,7 @@ assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2" shows "v1 :\<sqsubset>val v2" using assms -unfolding PosOrd_ex_def test +unfolding PosOrd_ex_def PosOrd_def2 apply(auto simp add: pflat_len_simps) apply(frule pflat_len_inside) apply(auto simp add: pflat_len_simps) @@ -318,7 +323,7 @@ assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2" shows "Right v1 :\<sqsubset>val Right v2" using assms -unfolding PosOrd_ex_def test +unfolding PosOrd_ex_def PosOrd_def2 apply(auto simp add: pflat_len_simps) by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5)) @@ -331,8 +336,8 @@ lemma PosOrd_SeqI1: - assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" - shows "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" + assumes "v1 :\<sqsubset>val w1" "flat (Seq v1 v2) = flat (Seq w1 w2)" + shows "Seq v1 v2 :\<sqsubset>val Seq w1 w2" using assms(1) apply(subst (asm) PosOrd_ex_def) apply(subst (asm) PosOrd_def) @@ -347,14 +352,15 @@ apply(simp only: Pos.simps) apply(auto)[1] apply(simp add: pflat_len_simps) +apply(auto simp add: pflat_len_simps) using assms(2) apply(simp) -apply(auto simp add: pflat_len_simps) -by (metis length_append of_nat_add) +apply(metis length_append of_nat_add) +done lemma PosOrd_SeqI2: - assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'" - shows "Seq v v2 :\<sqsubset>val Seq v v2'" + assumes "v2 :\<sqsubset>val w2" "flat v2 = flat w2" + shows "Seq v v2 :\<sqsubset>val Seq v w2" using assms(1) apply(subst (asm) PosOrd_ex_def) apply(subst (asm) PosOrd_def) @@ -374,47 +380,31 @@ apply(auto simp add: pflat_len_simps) done -lemma PosOrd_SeqE: - assumes "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" - shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'" -using assms +lemma PosOrd_Seq_eq: + assumes "flat v2 = flat w2" + shows "(Seq v v2) :\<sqsubset>val (Seq v w2) \<longleftrightarrow> v2 :\<sqsubset>val w2" +using assms +apply(auto) +prefer 2 +apply(simp add: PosOrd_SeqI2) apply(simp add: PosOrd_ex_def) -apply(erule exE) +apply(auto) apply(case_tac p) -apply(simp add: PosOrd_def) -apply(auto simp add: pflat_len_simps)[1] -apply(rule_tac x="[]" in exI) -apply(drule_tac x="[]" in spec) -apply(simp add: Pos_empty pflat_len_simps) +apply(simp add: PosOrd_def pflat_len_simps) apply(case_tac a) -apply(rule disjI1) -apply(simp add: PosOrd_def) -apply(auto simp add: pflat_len_simps)[1] +apply(simp add: PosOrd_def pflat_len_simps) +apply(clarify) +apply(case_tac nat) +prefer 2 +apply(simp add: PosOrd_def pflat_len_simps pflat_len_outside) apply(rule_tac x="list" in exI) -apply(simp) -apply(rule ballI) -apply(rule impI) -apply(drule_tac x="0#q" in bspec) -apply(simp) -apply(simp add: pflat_len_simps) -apply(case_tac nat) -apply(rule disjI2) -apply(simp add: PosOrd_def) -apply(auto simp add: pflat_len_simps) -apply(rule_tac x="list" in exI) -apply(simp add: Pos_empty) -apply(rule ballI) -apply(rule impI) -apply(auto)[1] -apply(drule_tac x="Suc 0#q" in bspec) -apply(simp) -apply(simp add: pflat_len_simps) -apply(drule_tac x="Suc 0#q" in bspec) -apply(simp) -apply(simp add: pflat_len_simps) -apply(simp add: PosOrd_def pflat_len_def) +apply(auto simp add: PosOrd_def2 pflat_len_simps) +apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2)) +apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2)) done + + lemma PosOrd_StarsI: assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)" shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)" @@ -499,17 +489,17 @@ done lemma PosOrd_Stars_append_eq: - assumes "flat (Stars vs1) = flat (Stars vs2)" + assumes "flats vs1 = flats vs2" shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" using assms apply(rule_tac iffI) apply(erule PosOrd_Stars_appendE) apply(rule PosOrd_Stars_appendI) apply(auto) -done +done lemma PosOrd_almost_trichotomous: - shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))" + shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (length (flat v1) = length (flat v2))" apply(auto simp add: PosOrd_ex_def) apply(auto simp add: PosOrd_def) apply(rule_tac x="[]" in exI) @@ -519,48 +509,6 @@ done -lemma PosOrd_SeqE2: - assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')" - shows "v1 :\<sqsubset>val v1' \<or> (intlen (flat v1) = intlen (flat v1') \<and> v2 :\<sqsubset>val v2')" -using assms -apply(frule_tac PosOrd_SeqE) -apply(erule disjE) -apply(simp) -apply(case_tac "v1 :\<sqsubset>val v1'") -apply(simp) -apply(rule disjI2) -apply(rule conjI) -prefer 2 -apply(simp) -apply(auto) -apply(auto simp add: PosOrd_ex_def) -apply(auto simp add: PosOrd_def pflat_len_simps) -apply(case_tac p) -apply(auto simp add: PosOrd_def pflat_len_simps) -apply(case_tac a) -apply(auto simp add: PosOrd_def pflat_len_simps) -apply (metis PosOrd_SeqI1 PosOrd_def PosOrd_ex_def PosOrd_shorterI PosOrd_assym assms less_linear) -by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def PosOrd_assym assms of_nat_eq_iff) - -lemma PosOrd_SeqE4: - assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')" - shows "v1 :\<sqsubset>val v1' \<or> (flat v1 = flat v1' \<and> v2 :\<sqsubset>val v2')" -using assms -apply(frule_tac PosOrd_SeqE) -apply(erule disjE) -apply(simp) -apply(case_tac "v1 :\<sqsubset>val v1'") -apply(simp) -apply(rule disjI2) -apply(rule conjI) -prefer 2 -apply(simp) -apply(auto) -apply(case_tac "length (flat v1') < length (flat v1)") -using PosOrd_shorterI apply blast -by (metis PosOrd_SeqI1 PosOrd_shorterI PosOrd_assym antisym_conv3 append_eq_append_conv assms(2)) - - section {* The Posix Value is smaller than any other Value *} @@ -671,8 +619,7 @@ by (auto simp add: LV_def) then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 - thm PosOrd_SeqI1 PosOrd_SeqI2 - unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) + unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_Seq_eq) then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast next case (Posix_STAR1 s1 r v s2 vs v3) @@ -775,6 +722,16 @@ lemma Least_existence1: assumes "LV r s \<noteq> {}" + shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" +using Least_existence[OF assms] assms +using PosOrdeq_antisym by blast + + + + + +lemma Least_existence1_pre: + assumes "LV r s \<noteq> {}" shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v" using Least_existence[OF assms] assms apply -
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/thys/SpecExt.thy Wed Sep 06 00:52:08 2017 +0100 @@ -0,0 +1,978 @@ + +theory SpecExt + imports Main "~~/src/HOL/Library/Sublist" +begin + +section {* Sequential Composition of Languages *} + +definition + Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) +where + "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" + +text {* Two Simple Properties about Sequential Composition *} + +lemma Sequ_empty_string [simp]: + shows "A ;; {[]} = A" + and "{[]} ;; A = A" +by (simp_all add: Sequ_def) + +lemma Sequ_empty [simp]: + shows "A ;; {} = {}" + and "{} ;; A = {}" +by (simp_all add: Sequ_def) + +lemma Sequ_assoc: + shows "(A ;; B) ;; C = A ;; (B ;; C)" +apply(auto simp add: Sequ_def) +apply blast +by (metis append_assoc) + +lemma Sequ_Union_in: + shows "(A ;; (\<Union>x\<in> B. C x)) = (\<Union>x\<in> B. A ;; C x)" +by (auto simp add: Sequ_def) + +section {* Semantic Derivative (Left Quotient) of Languages *} + +definition + Der :: "char \<Rightarrow> string set \<Rightarrow> string set" +where + "Der c A \<equiv> {s. c # s \<in> A}" + +definition + Ders :: "string \<Rightarrow> string set \<Rightarrow> string set" +where + "Ders s A \<equiv> {s'. s @ s' \<in> A}" + +lemma Der_null [simp]: + shows "Der c {} = {}" +unfolding Der_def +by auto + +lemma Der_empty [simp]: + shows "Der c {[]} = {}" +unfolding Der_def +by auto + +lemma Der_char [simp]: + shows "Der c {[d]} = (if c = d then {[]} else {})" +unfolding Der_def +by auto + +lemma Der_union [simp]: + shows "Der c (A \<union> B) = Der c A \<union> Der c B" +unfolding Der_def +by auto + +lemma Der_UNION [simp]: + shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" +by (auto simp add: Der_def) + +lemma Der_Sequ [simp]: + shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" +unfolding Der_def Sequ_def +by (auto simp add: Cons_eq_append_conv) + + +section {* Kleene Star for Languages *} + +inductive_set + Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) + for A :: "string set" +where + start[intro]: "[] \<in> A\<star>" +| step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" + +(* Arden's lemma *) + +lemma Star_cases: + shows "A\<star> = {[]} \<union> A ;; A\<star>" +unfolding Sequ_def +by (auto) (metis Star.simps) + +lemma Star_decomp: + assumes "c # x \<in> A\<star>" + shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>" +using assms +by (induct x\<equiv>"c # x" rule: Star.induct) + (auto simp add: append_eq_Cons_conv) + +lemma Star_Der_Sequ: + shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>" +unfolding Der_def Sequ_def +by(auto simp add: Star_decomp) + + +lemma Der_star [simp]: + shows "Der c (A\<star>) = (Der c A) ;; A\<star>" +proof - + have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" + by (simp only: Star_cases[symmetric]) + also have "... = Der c (A ;; A\<star>)" + by (simp only: Der_union Der_empty) (simp) + also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" + by simp + also have "... = (Der c A) ;; A\<star>" + using Star_Der_Sequ by auto + finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . +qed + +section {* Power operation for Sets *} + +fun + Pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101) +where + "A \<up> 0 = {[]}" +| "A \<up> (Suc n) = A ;; (A \<up> n)" + +lemma Pow_empty [simp]: + shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)" +by(induct n) (auto simp add: Sequ_def) + +lemma Pow_Suc_rev: + "A \<up> (Suc n) = (A \<up> n) ;; A" +apply(induct n arbitrary: A) +apply(simp_all) +by (metis Sequ_assoc) + + +lemma Pow_decomp: + assumes "c # x \<in> A \<up> n" + shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A \<up> (n - 1)" +using assms +apply(induct n) +apply(auto simp add: Cons_eq_append_conv Sequ_def) +apply(case_tac n) +apply(auto simp add: Sequ_def) +apply(blast) +done + +lemma Star_Pow: + assumes "s \<in> A\<star>" + shows "\<exists>n. s \<in> A \<up> n" +using assms +apply(induct) +apply(auto) +apply(rule_tac x="Suc n" in exI) +apply(auto simp add: Sequ_def) +done + +lemma Pow_Star: + assumes "s \<in> A \<up> n" + shows "s \<in> A\<star>" +using assms +apply(induct n arbitrary: s) +apply(auto simp add: Sequ_def) +done + +lemma Der_Pow_0: + shows "Der c (A \<up> 0) = {}" +by(simp add: Der_def) + +lemma Der_Pow_Suc: + shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" +unfolding Der_def Sequ_def +apply(auto simp add: Cons_eq_append_conv Sequ_def dest!: Pow_decomp) +apply(case_tac n) +apply(force simp add: Sequ_def)+ +done + +lemma Der_Pow [simp]: + shows "Der c (A \<up> n) = (if n = 0 then {} else (Der c A) ;; (A \<up> (n - 1)))" +apply(case_tac n) +apply(simp_all del: Pow.simps add: Der_Pow_0 Der_Pow_Suc) +done + +lemma Der_Pow_Sequ [simp]: + shows "Der c (A ;; A \<up> n) = (Der c A) ;; (A \<up> n)" +by (simp only: Pow.simps[symmetric] Der_Pow) (simp) + + +lemma Pow_Sequ_Un: + assumes "0 < x" + shows "(\<Union>n \<in> {..x}. (A \<up> n)) = ({[]} \<union> (\<Union>n \<in> {..x - Suc 0}. A ;; (A \<up> n)))" +using assms +apply(auto simp add: Sequ_def) +apply(smt Pow.elims Sequ_def Suc_le_mono Suc_pred atMost_iff empty_iff insert_iff mem_Collect_eq) +apply(rule_tac x="Suc xa" in bexI) +apply(auto simp add: Sequ_def) +done + +lemma Pow_Sequ_Un2: + assumes "0 < x" + shows "(\<Union>n \<in> {x..}. (A \<up> n)) = (\<Union>n \<in> {x - Suc 0..}. A ;; (A \<up> n))" +using assms +apply(auto simp add: Sequ_def) +apply(case_tac n) +apply(auto simp add: Sequ_def) +apply fastforce +apply(case_tac x) +apply(auto) +apply(rule_tac x="Suc xa" in bexI) +apply(auto simp add: Sequ_def) +done + +section {* Regular Expressions *} + +datatype rexp = + ZERO +| ONE +| CHAR char +| SEQ rexp rexp +| ALT rexp rexp +| STAR rexp +| UPNTIMES rexp nat +| NTIMES rexp nat +| FROMNTIMES rexp nat +| NMTIMES rexp nat nat + +section {* Semantics of Regular Expressions *} + +fun + L :: "rexp \<Rightarrow> string set" +where + "L (ZERO) = {}" +| "L (ONE) = {[]}" +| "L (CHAR c) = {[c]}" +| "L (SEQ r1 r2) = (L r1) ;; (L r2)" +| "L (ALT r1 r2) = (L r1) \<union> (L r2)" +| "L (STAR r) = (L r)\<star>" +| "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)" +| "L (NTIMES r n) = (L r) \<up> n" +| "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)" +| "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" + +section {* Nullable, Derivatives *} + +fun + nullable :: "rexp \<Rightarrow> bool" +where + "nullable (ZERO) = False" +| "nullable (ONE) = True" +| "nullable (CHAR c) = False" +| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" +| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" +| "nullable (STAR r) = True" +| "nullable (UPNTIMES r n) = True" +| "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" +| "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" +| "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" + +fun + der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" +where + "der c (ZERO) = ZERO" +| "der c (ONE) = ZERO" +| "der c (CHAR d) = (if c = d then ONE else ZERO)" +| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" +| "der c (SEQ r1 r2) = + (if nullable r1 + then ALT (SEQ (der c r1) r2) (der c r2) + else SEQ (der c r1) r2)" +| "der c (STAR r) = SEQ (der c r) (STAR r)" +| "der c (UPNTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (UPNTIMES r (n - 1)))" +| "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))" +| "der c (FROMNTIMES r n) = SEQ (der c r) (FROMNTIMES r (n - 1))" +| "der c (NMTIMES r n m) = + (if m < n then ZERO + else (if n = 0 then (if m = 0 then ZERO else + SEQ (der c r) (UPNTIMES r (m - 1))) else + SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" + +fun + ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" +where + "ders [] r = r" +| "ders (c # s) r = ders s (der c r)" + + +lemma nullable_correctness: + shows "nullable r \<longleftrightarrow> [] \<in> (L r)" +by(induct r) (auto simp add: Sequ_def) + + +lemma der_correctness: + shows "L (der c r) = Der c (L r)" +apply(induct r) +apply(simp add: nullable_correctness del: Der_UNION) +apply(simp add: nullable_correctness del: Der_UNION) +apply(simp add: nullable_correctness del: Der_UNION) +apply(simp add: nullable_correctness del: Der_UNION) +apply(simp add: nullable_correctness del: Der_UNION) +apply(simp add: nullable_correctness del: Der_UNION) +prefer 2 +apply(simp add: nullable_correctness del: Der_UNION) +apply(simp add: nullable_correctness del: Der_UNION) +apply(rule impI) +apply(subst Sequ_Union_in) +apply(subst Der_Pow_Sequ[symmetric]) +apply(subst Pow.simps[symmetric]) +apply(subst Der_UNION[symmetric]) +apply(subst Pow_Sequ_Un) +apply(simp) +apply(simp only: Der_union Der_empty) +apply(simp) +apply(simp add: nullable_correctness del: Der_UNION) +apply(subst Sequ_Union_in) +apply(subst Der_Pow_Sequ[symmetric]) +apply(subst Pow.simps[symmetric]) +apply(case_tac x2) +prefer 2 +apply(subst Pow_Sequ_Un2) +apply(simp) +apply(simp) +apply(auto simp add: Sequ_def Der_def)[1] +apply(rule_tac x="Suc xa" in exI) +apply(auto simp add: Sequ_def)[1] +apply(drule Pow_decomp) +apply(auto)[1] +apply (metis append_Cons) +apply(simp add: nullable_correctness del: Der_UNION) +apply(rule impI) +apply(rule conjI) +apply(rule impI) +apply(subst Sequ_Union_in) +apply(subst Der_Pow_Sequ[symmetric]) +apply(subst Pow.simps[symmetric]) +apply(subst Der_UNION[symmetric]) +apply(case_tac x3a) +apply(simp) +apply(clarify) +apply(auto simp add: Sequ_def Der_def Cons_eq_append_conv)[1] +apply(rule_tac x="Suc xa" in bexI) +apply(auto simp add: Sequ_def)[2] +apply (metis append_Cons) +apply (metis (no_types, hide_lams) Pow_decomp atMost_iff diff_Suc_eq_diff_pred diff_is_0_eq) +apply(rule impI)+ +apply(subst Sequ_Union_in) +apply(subst Der_Pow_Sequ[symmetric]) +apply(subst Pow.simps[symmetric]) +apply(subst Der_UNION[symmetric]) +apply(case_tac x2) +apply(simp) +apply(simp del: Pow.simps) +apply(auto simp add: Sequ_def Der_def) +apply (metis One_nat_def Suc_le_D Suc_le_mono atLeastAtMost_iff diff_Suc_1 not_le) +by fastforce + + + +lemma ders_correctness: + shows "L (ders s r) = Ders s (L r)" +by (induct s arbitrary: r) + (simp_all add: Ders_def der_correctness Der_def) + + + +section {* Values *} + +datatype val = + Void +| Char char +| Seq val val +| Right val +| Left val +| Stars "val list" + + +section {* The string behind a value *} + +fun + flat :: "val \<Rightarrow> string" +where + "flat (Void) = []" +| "flat (Char c) = [c]" +| "flat (Left v) = flat v" +| "flat (Right v) = flat v" +| "flat (Seq v1 v2) = (flat v1) @ (flat v2)" +| "flat (Stars []) = []" +| "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" + +abbreviation + "flats vs \<equiv> concat (map flat vs)" + +lemma flat_Stars [simp]: + "flat (Stars vs) = flats vs" +by (induct vs) (auto) + +lemma Star_concat: + assumes "\<forall>s \<in> set ss. s \<in> A" + shows "concat ss \<in> A\<star>" +using assms by (induct ss) (auto) + +lemma Star_cstring: + assumes "s \<in> A\<star>" + shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])" +using assms +apply(induct rule: Star.induct) +apply(auto)[1] +apply(rule_tac x="[]" in exI) +apply(simp) +apply(erule exE) +apply(clarify) +apply(case_tac "s1 = []") +apply(rule_tac x="ss" in exI) +apply(simp) +apply(rule_tac x="s1#ss" in exI) +apply(simp) +done + +lemma Aux: + assumes "\<forall>s\<in>set ss. s = []" + shows "concat ss = []" +using assms +by (induct ss) (auto) + +lemma Pow_cstring_nonempty: + assumes "s \<in> A \<up> n" + shows "\<exists>ss. concat ss = s \<and> length ss \<le> n \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])" +using assms +apply(induct n arbitrary: s) +apply(auto) +apply(simp add: Sequ_def) +apply(erule exE)+ +apply(clarify) +apply(drule_tac x="s2" in meta_spec) +apply(simp) +apply(clarify) +apply(case_tac "s1 = []") +apply(simp) +apply(rule_tac x="ss" in exI) +apply(simp) +apply(rule_tac x="s1 # ss" in exI) +apply(simp) +done + +lemma Pow_cstring: + assumes "s \<in> A \<up> n" + shows "\<exists>ss1 ss2. concat (ss1 @ ss2) = s \<and> length (ss1 @ ss2) = n \<and> + (\<forall>s \<in> set ss1. s \<in> A \<and> s \<noteq> []) \<and> (\<forall>s \<in> set ss2. s \<in> A \<and> s = [])" +using assms +apply(induct n arbitrary: s) +apply(auto)[1] +apply(simp only: Pow_Suc_rev) +apply(simp add: Sequ_def) +apply(erule exE)+ +apply(clarify) +apply(drule_tac x="s1" in meta_spec) +apply(simp) +apply(erule exE)+ +apply(clarify) +apply(case_tac "s2 = []") +apply(simp) +apply(rule_tac x="ss1" in exI) +apply(rule_tac x="s2#ss2" in exI) +apply(simp) +apply(rule_tac x="ss1 @ [s2]" in exI) +apply(rule_tac x="ss2" in exI) +apply(simp) +apply(subst Aux) +apply(auto)[1] +apply(subst Aux) +apply(auto)[1] +apply(simp) +done + + +section {* Lexical Values *} + + + +inductive + Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100) +where + "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2" +| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" +| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" +| "\<Turnstile> Void : ONE" +| "\<Turnstile> Char c : CHAR c" +| "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : STAR r" +| "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; length vs \<le> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : UPNTIMES r n" +| "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; + \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; + length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n" +| "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; + \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; + length (vs1 @ vs2) \<ge> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : FROMNTIMES r n" +| "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; + \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; + length (vs1 @ vs2) \<ge> n; length (vs1 @ vs2) \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NMTIMES r n m" + +inductive_cases Prf_elims: + "\<Turnstile> v : ZERO" + "\<Turnstile> v : SEQ r1 r2" + "\<Turnstile> v : ALT r1 r2" + "\<Turnstile> v : ONE" + "\<Turnstile> v : CHAR c" + "\<Turnstile> vs : STAR r" + "\<Turnstile> vs : UPNTIMES r n" + "\<Turnstile> vs : NTIMES r n" + "\<Turnstile> vs : FROMNTIMES r n" + "\<Turnstile> vs : NMTIMES r n m" + +lemma Prf_Stars_appendE: + assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" + shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" +using assms +by (auto intro: Prf.intros elim!: Prf_elims) + +lemma flats_empty: + assumes "(\<forall>v\<in>set vs. flat v = [])" + shows "flats vs = []" +using assms +by(induct vs) (simp_all) + +lemma Star_cval: + assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" + shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])" +using assms +apply(induct ss) +apply(auto) +apply(rule_tac x="[]" in exI) +apply(simp) +apply(case_tac "flat v = []") +apply(rule_tac x="vs" in exI) +apply(simp) +apply(rule_tac x="v#vs" in exI) +apply(simp) +done + + +lemma flats_cval: + assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" + shows "\<exists>vs1 vs2. flats (vs1 @ vs2) = concat ss \<and> length (vs1 @ vs2) = length ss \<and> + (\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []) \<and> + (\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = [])" +using assms +apply(induct ss rule: rev_induct) +apply(rule_tac x="[]" in exI)+ +apply(simp) +apply(simp) +apply(clarify) +apply(case_tac "flat v = []") +apply(rule_tac x="vs1" in exI) +apply(rule_tac x="v#vs2" in exI) +apply(simp) +apply(rule_tac x="vs1 @ [v]" in exI) +apply(rule_tac x="vs2" in exI) +apply(simp) +apply(subst (asm) (2) flats_empty) +apply(simp) +apply(simp) +done + +lemma flats_cval_nonempty: + assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" + shows "\<exists>vs. flats vs = concat ss \<and> length vs \<le> length ss \<and> + (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])" +using assms +apply(induct ss) +apply(rule_tac x="[]" in exI) +apply(simp) +apply(simp) +apply(clarify) +apply(case_tac "flat v = []") +apply(rule_tac x="vs" in exI) +apply(simp) +apply(rule_tac x="v # vs" in exI) +apply(simp) +done + +lemma Pow_flats: + assumes "\<forall>v \<in> set vs. flat v \<in> A" + shows "flats vs \<in> A \<up> length vs" +using assms +by(induct vs)(auto simp add: Sequ_def) + +lemma Pow_flats_appends: + assumes "\<forall>v \<in> set vs1. flat v \<in> A" "\<forall>v \<in> set vs2. flat v \<in> A" + shows "flats vs1 @ flats vs2 \<in> A \<up> (length vs1 + length vs2)" +using assms +apply(induct vs1) +apply(auto simp add: Sequ_def Pow_flats) +done + +lemma L_flat_Prf1: + assumes "\<Turnstile> v : r" + shows "flat v \<in> L r" +using assms +apply(induct) +apply(auto simp add: Sequ_def Star_concat Pow_flats) +apply(meson Pow_flats atMost_iff) +using Pow_flats_appends apply blast +apply(meson Pow_flats_appends atLeast_iff) +apply(meson Pow_flats_appends atLeastAtMost_iff) +done + +lemma L_flat_Prf2: + assumes "s \<in> L r" + shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" +using assms +proof(induct r arbitrary: s) + case (STAR r s) + have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact + have "s \<in> L (STAR r)" by fact + then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" + using Star_cstring by auto + then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" + using IH Star_cval by metis + then show "\<exists>v. \<Turnstile> v : STAR r \<and> flat v = s" + using Prf.intros(6) flat_Stars by blast +next + case (SEQ r1 r2 s) + then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s" + unfolding Sequ_def L.simps by (fastforce intro: Prf.intros) +next + case (ALT r1 r2 s) + then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s" + unfolding L.simps by (fastforce intro: Prf.intros) +next + case (NTIMES r n) + have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact + have "s \<in> L (NTIMES r n)" by fact + then obtain ss1 ss2 where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = n" + "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" + using Pow_cstring by force + then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = n" + "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" + using IH flats_cval + apply - + apply(drule_tac x="ss1 @ ss2" in meta_spec) + apply(drule_tac x="r" in meta_spec) + apply(drule meta_mp) + apply(simp) + apply (metis Un_iff) + apply(clarify) + apply(drule_tac x="vs1" in meta_spec) + apply(drule_tac x="vs2" in meta_spec) + apply(simp) + done + then show "\<exists>v. \<Turnstile> v : NTIMES r n \<and> flat v = s" + using Prf.intros(8) flat_Stars by blast +next + case (FROMNTIMES r n) + have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact + have "s \<in> L (FROMNTIMES r n)" by fact + then obtain ss1 ss2 m where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = m" "n \<le> m" + "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" + using Pow_cstring by auto blast + then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = m" "n \<le> m" + "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" + using IH flats_cval + apply - + apply(drule_tac x="ss1 @ ss2" in meta_spec) + apply(drule_tac x="r" in meta_spec) + apply(drule meta_mp) + apply(simp) + apply (metis Un_iff) + apply(clarify) + apply(drule_tac x="vs1" in meta_spec) + apply(drule_tac x="vs2" in meta_spec) + apply(simp) + done + then show "\<exists>v. \<Turnstile> v : FROMNTIMES r n \<and> flat v = s" + using Prf.intros(9) flat_Stars by blast +next + case (NMTIMES r n m) + have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact + have "s \<in> L (NMTIMES r n m)" by fact + then obtain ss1 ss2 k where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = k" "n \<le> k" "k \<le> m" + "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" + using Pow_cstring by (auto, blast) + then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = k" "n \<le> k" "k \<le> m" + "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" + using IH flats_cval + apply - + apply(drule_tac x="ss1 @ ss2" in meta_spec) + apply(drule_tac x="r" in meta_spec) + apply(drule meta_mp) + apply(simp) + apply (metis Un_iff) + apply(clarify) + apply(drule_tac x="vs1" in meta_spec) + apply(drule_tac x="vs2" in meta_spec) + apply(simp) + done + then show "\<exists>v. \<Turnstile> v : NMTIMES r n m \<and> flat v = s" + apply(rule_tac x="Stars (vs1 @ vs2)" in exI) + apply(simp) + apply(rule Prf.intros) + apply(auto) + done +next + case (UPNTIMES r n s) + have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact + have "s \<in> L (UPNTIMES r n)" by fact + then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" "length ss \<le> n" + using Pow_cstring_nonempty by force + then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" "length vs \<le> n" + using IH flats_cval_nonempty by (smt order.trans) + then show "\<exists>v. \<Turnstile> v : UPNTIMES r n \<and> flat v = s" + using Prf.intros(7) flat_Stars by blast +qed (auto intro: Prf.intros) + + +lemma L_flat_Prf: + shows "L(r) = {flat v | v. \<Turnstile> v : r}" +using L_flat_Prf1 L_flat_Prf2 by blast + + + +section {* Sets of Lexical Values *} + +text {* + Shows that lexical values are finite for a given regex and string. +*} + +definition + LV :: "rexp \<Rightarrow> string \<Rightarrow> val set" +where "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}" + +lemma LV_simps: + shows "LV ZERO s = {}" + and "LV ONE s = (if s = [] then {Void} else {})" + and "LV (CHAR c) s = (if s = [c] then {Char c} else {})" + and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s" +unfolding LV_def +by (auto intro: Prf.intros elim: Prf.cases) + + +abbreviation + "Prefixes s \<equiv> {s'. prefixeq s' s}" + +abbreviation + "Suffixes s \<equiv> {s'. suffixeq s' s}" + +abbreviation + "SSuffixes s \<equiv> {s'. suffix s' s}" + +lemma Suffixes_cons [simp]: + shows "Suffixes (c # s) = Suffixes s \<union> {c # s}" +by (auto simp add: suffixeq_def Cons_eq_append_conv) + + +lemma finite_Suffixes: + shows "finite (Suffixes s)" +by (induct s) (simp_all) + +lemma finite_SSuffixes: + shows "finite (SSuffixes s)" +proof - + have "SSuffixes s \<subseteq> Suffixes s" + unfolding suffix_def suffixeq_def by auto + then show "finite (SSuffixes s)" + using finite_Suffixes finite_subset by blast +qed + +lemma finite_Prefixes: + shows "finite (Prefixes s)" +proof - + have "finite (Suffixes (rev s))" + by (rule finite_Suffixes) + then have "finite (rev ` Suffixes (rev s))" by simp + moreover + have "rev ` (Suffixes (rev s)) = Prefixes s" + unfolding suffixeq_def prefixeq_def image_def + by (auto)(metis rev_append rev_rev_ident)+ + ultimately show "finite (Prefixes s)" by simp +qed + +lemma LV_STAR_finite: + assumes "\<forall>s. finite (LV r s)" + shows "finite (LV (STAR r) s)" +proof(induct s rule: length_induct) + fix s::"char list" + assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" + then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" + by (auto simp add: suffix_def) + def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)" + def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r s'" + def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)" + have "finite S1" using assms + unfolding S1_def by (simp_all add: finite_Prefixes) + moreover + with IH have "finite S2" unfolding S2_def + by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) + ultimately + have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp + moreover + have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" + unfolding S1_def S2_def f_def + unfolding LV_def image_def prefixeq_def suffix_def + apply(auto elim: Prf_elims) + apply(erule Prf_elims) + apply(auto) + apply(case_tac vs) + apply(auto intro: Prf.intros) + done + ultimately + show "finite (LV (STAR r) s)" by (simp add: finite_subset) +qed + +lemma LV_UPNTIMES_STAR: + "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s" +by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims) + +lemma LV_FROMNTIMES_STAR: + "LV (FROMNTIMES r n) s \<subseteq> LV (STAR r) s" +apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims) +oops + +lemma LV_finite: + shows "finite (LV r s)" +proof(induct r arbitrary: s) + case (ZERO s) + show "finite (LV ZERO s)" by (simp add: LV_simps) +next + case (ONE s) + show "finite (LV ONE s)" by (simp add: LV_simps) +next + case (CHAR c s) + show "finite (LV (CHAR c) s)" by (simp add: LV_simps) +next + case (ALT r1 r2 s) + then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps) +next + case (SEQ r1 r2 s) + def f \<equiv> "\<lambda>(v1, v2). Seq v1 v2" + def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r1 s'" + def S2 \<equiv> "\<Union>s' \<in> Suffixes s. LV r2 s'" + have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+ + then have "finite S1" "finite S2" unfolding S1_def S2_def + by (simp_all add: finite_Prefixes finite_Suffixes) + moreover + have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)" + unfolding f_def S1_def S2_def + unfolding LV_def image_def prefixeq_def suffixeq_def + by (auto elim: Prf.cases) + ultimately + show "finite (LV (SEQ r1 r2) s)" + by (simp add: finite_subset) +next + case (STAR r s) + then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite) +next + case (NTIMES r n s) + have "\<And>s. finite (LV r s)" by fact + then show "finite (LV (NTIMES r n) s)" + apply(simp add: LV_def) +qed + + + +section {* Our POSIX Definition *} + +inductive + Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) +where + Posix_ONE: "[] \<in> ONE \<rightarrow> Void" +| Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)" +| Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" +| Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" +| Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; + \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> + (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" +| Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; + \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> + \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" +| Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" + +inductive_cases Posix_elims: + "s \<in> ZERO \<rightarrow> v" + "s \<in> ONE \<rightarrow> v" + "s \<in> CHAR c \<rightarrow> v" + "s \<in> ALT r1 r2 \<rightarrow> v" + "s \<in> SEQ r1 r2 \<rightarrow> v" + "s \<in> STAR r \<rightarrow> v" + +lemma Posix1: + assumes "s \<in> r \<rightarrow> v" + shows "s \<in> L r" "flat v = s" +using assms +by (induct s r v rule: Posix.induct) + (auto simp add: Sequ_def) + +text {* + Our Posix definition determines a unique value. +*} + +lemma Posix_determ: + assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" + shows "v1 = v2" +using assms +proof (induct s r v1 arbitrary: v2 rule: Posix.induct) + case (Posix_ONE v2) + have "[] \<in> ONE \<rightarrow> v2" by fact + then show "Void = v2" by cases auto +next + case (Posix_CHAR c v2) + have "[c] \<in> CHAR c \<rightarrow> v2" by fact + then show "Char c = v2" by cases auto +next + case (Posix_ALT1 s r1 v r2 v2) + have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact + moreover + have "s \<in> r1 \<rightarrow> v" by fact + then have "s \<in> L r1" by (simp add: Posix1) + ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto + moreover + have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact + ultimately have "v = v'" by simp + then show "Left v = v2" using eq by simp +next + case (Posix_ALT2 s r2 v r1 v2) + have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact + moreover + have "s \<notin> L r1" by fact + ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" + by cases (auto simp add: Posix1) + moreover + have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact + ultimately have "v = v'" by simp + then show "Right v = v2" using eq by simp +next + case (Posix_SEQ s1 r1 v1 s2 r2 v2 v') + have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'" + "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" + "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact+ + then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'" + apply(cases) apply (auto simp add: append_eq_append_conv2) + using Posix1(1) by fastforce+ + moreover + have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'" + "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+ + ultimately show "Seq v1 v2 = v'" by simp +next + case (Posix_STAR1 s1 r v s2 vs v2) + have "(s1 @ s2) \<in> STAR r \<rightarrow> v2" + "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []" + "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact+ + then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" + apply(cases) apply (auto simp add: append_eq_append_conv2) + using Posix1(1) apply fastforce + apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2) + using Posix1(2) by blast + moreover + have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" + "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ + ultimately show "Stars (v # vs) = v2" by auto +next + case (Posix_STAR2 r v2) + have "[] \<in> STAR r \<rightarrow> v2" by fact + then show "Stars [] = v2" by cases (auto simp add: Posix1) +qed + + +text {* + Our POSIX value is a lexical value. +*} + +lemma Posix_LV: + assumes "s \<in> r \<rightarrow> v" + shows "v \<in> LV r s" +using assms unfolding LV_def +apply(induct rule: Posix.induct) +apply(auto simp add: intro!: Prf.intros elim!: Prf_elims) +done + +end \ No newline at end of file