lexing: comparison thys/Paper/Paper.thy

equal deleted inserted replaced

-:91647a8d84a3
+:cdc0bdcfba3f
 ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)
 definition
 "match r s \<equiv> nullable (ders s r)"
+(*
+comments not implemented
+p9. "None is returned, indicating an error is raised" : there is no error
+p9. The condtion "not exists s3 s4..." appears often enough (in particular in
+the proof of Lemma 3) to warrant a definition.
+p9. "The POSIX value v" : at this point the existence of a POSIX value is yet
+to be shown
+p10. (proof Lemma 3) : separating the cases with description/itemize would greatly
+improve readability
+p11. Theorem 2(2) : Stressing the uniqueness is strange, given that it follows
+trivially from the fact that "lexer" is a function. Maybe state the existence of
+a unique POSIX value as corollary.
+p14. Proposition 3 is evidently false and Proposition 4 is a conjecture.
+I find it confusing that Propositions 1 and 2, which are proven facts, are also called propositions.
+*)
 (*>*)
 section {* Introduction *}
 @{term b} and @{term c}). We then use @{const nullable} to find out
 whether the resulting derivative regular expression @{term "r\<^sub>4"}
 can match the empty string. If yes, we call the function @{const mkeps}
 that produces a value @{term "v\<^sub>4"} for how @{term "r\<^sub>4"} can
 match the empty string (taking into account the POSIX constraints in case
-there are several ways). This functions is defined by the clauses:
+there are several ways). This function is defined by the clauses:
 \begin{figure}[t]
 \begin{center}
 \begin{tikzpicture}[scale=2,node distance=1.3cm,
 every node/.style={minimum size=7mm}]
 @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} $\dn$ @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}
 \end{center}
 \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 the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the left-hand
+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
 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
 \end{tabular}
 \end{lemma}
 \begin{proof}
 Both properties are by routine inductions: the first one can, for example,
-be proved by an induction over the definition of @{term derivatives}; the second by
+be proved by induction over the definition of @{term derivatives}; the second by
 an induction on @{term r}. There are no interesting cases.\qed
 \end{proof}
 Having defined the @{const mkeps} and @{text inj} function we can extend
 \Brz's matcher so that a [lexical] value is constructed (assuming the
 \noindent
 The central lemma for our POSIX relation is that the @{text inj}-function
 preserves POSIX values.
 \begin{lemma}\label{Posix2}
-@{thm[mode=IfThen] Posix2_roy_version}
+@{thm[mode=IfThen] Posix_injval}
 \end{lemma}
 \begin{proof}
 By induction on @{text r}. Suppose @{term "r = ALT r\<^sub>1 r\<^sub>2"}. There are
 \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> (c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\]
 \noindent We can use the induction hypothesis for @{text "r\<^sub>1"} to obtain
 @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}. Putting this all together allows us to infer
 @{term "((c # s\<^sub>1) @ s\<^sub>2) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (injval r\<^sub>1 c v\<^sub>1) v\<^sub>2"}. The case @{text "(c)"}
-is similarly.
+is similar.
 For @{text "(b)"} we know @{term "s \<in> der c r\<^sub>2 \<rightarrow> v\<^sub>1"} and
 @{term "s\<^sub>1 @ s\<^sub>2 \<notin> L (SEQ (der c r\<^sub>1) r\<^sub>2)"}. From the former
 we have @{term "(c # s) \<in> r\<^sub>2 \<rightarrow> (injval r\<^sub>2 c v\<^sub>1)"} by induction hypothesis
 for @{term "r\<^sub>2"}. From the latter we can infer
 \begin{proof}
 By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{Posix2}.\qed
 \end{proof}
 \noindent This concludes our correctness proof. Note that we have not
-changed the algorithm of Sulzmann and Lu,\footnote{Any deviation we
+changed the algorithm of Sulzmann and Lu,\footnote{All deviations we
-introduced is harmless.} but introduced our own specification for what a
+introduced are harmless.} but introduced our own specification for what a
 correct result---a POSIX value---should be. A strong point in favour of
 Sulzmann and Lu's algorithm is that it can be extended in various ways.
 *}
 & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{text "Some (inj r c (f\<^sub>r v))"}
 \end{tabular}
 \end{center}
 \noindent
-In the second clause we first calculate the derivative @{text "r \\ c"}
+In the second clause we first calculate the derivative @{term "der c r"}
 and then simplify the result. This gives us a simplified derivative
 @{text "r\<^sub>s"} and a rectification function @{text "f\<^sub>r"}. The lexer
 is then recursively called with the simplified derivative, but before
-we inject the character @{term c} into value, we need to rectify
+we inject the character @{term c} into the value, we need to rectify
 it (that is construct @{term "f\<^sub>r v"}). We can prove that
-\begin{lemma}
+\begin{theorem}
 @{thm slexer_correctness}
-\end{lemma}
+\end{theorem}
 \noindent
 holds but for lack of space refer the reader to our mechanisation for details.
 *}
-section {* The Correctness Argument by Sulzmmann and Lu\label{argu} *}
+section {* The Correctness Argument by Sulzmann and Lu\label{argu} *}
 text {*
 %  \newcommand{\greedy}{\succcurlyeq_{gr}}
 \newcommand{\posix}{>}

changeset 172	cdc0bdcfba3f
parent 171	91647a8d84a3
child 173	80fe81a28a52