# HG changeset patch # User Christian Urban # Date 1462792196 -3600 # Node ID cdc0bdcfba3ff67cc8af2b8377a09168609549ae # Parent 91647a8d84a30a96511fa61612b8e6be59bf2335 updated diff -r 91647a8d84a3 -r cdc0bdcfba3f thys/Paper/Paper.thy --- a/thys/Paper/Paper.thy Sun May 08 09:49:21 2016 +0100 +++ b/thys/Paper/Paper.thy Mon May 09 12:09:56 2016 +0100 @@ -62,6 +62,29 @@ definition "match r s \ 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 *} @@ -414,7 +437,7 @@ 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} @@ -519,7 +542,7 @@ \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 @@ -559,7 +582,7 @@ \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} @@ -684,7 +707,7 @@ preserves POSIX values. \begin{lemma}\label{Posix2} - @{thm[mode=IfThen] Posix2_roy_version} + @{thm[mode=IfThen] Posix_injval} \end{lemma} \begin{proof} @@ -722,7 +745,7 @@ \noindent We can use the induction hypothesis for @{text "r\<^sub>1"} to obtain @{term "(c # s\<^sub>1) \ r\<^sub>1 \ injval r\<^sub>1 c v\<^sub>1"}. Putting this all together allows us to infer @{term "((c # s\<^sub>1) @ s\<^sub>2) \ SEQ r\<^sub>1 r\<^sub>2 \ 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 \ der c r\<^sub>2 \ v\<^sub>1"} and @{term "s\<^sub>1 @ s\<^sub>2 \ L (SEQ (der c r\<^sub>1) r\<^sub>2)"}. From the former @@ -760,8 +783,8 @@ \end{proof} \noindent This concludes our correctness proof. Note that we have not - changed the algorithm of Sulzmann and Lu,\footnote{Any deviation we - introduced is harmless.} but introduced our own specification for what a + changed the algorithm of Sulzmann and Lu,\footnote{All deviations we + 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. @@ -891,23 +914,23 @@ \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}} diff -r 91647a8d84a3 -r cdc0bdcfba3f thys/Paper/document/root.bib --- a/thys/Paper/document/root.bib Sun May 08 09:49:21 2016 +0100 +++ b/thys/Paper/document/root.bib Mon May 09 12:09:56 2016 +0100 @@ -219,7 +219,7 @@ @InProceedings{Coquand2012, author = {T.~Coquand and V.~Siles}, title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory}, - booktitle = {Proc.~of the 1st Conference on Certified Programs and Proofs (CPP)}, + booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)}, pages = {119--134}, year = {2011}, volume = {7086}, diff -r 91647a8d84a3 -r cdc0bdcfba3f thys/Paper/document/root.tex --- a/thys/Paper/document/root.tex Sun May 08 09:49:21 2016 +0100 +++ b/thys/Paper/document/root.tex Mon May 09 12:09:56 2016 +0100 @@ -68,8 +68,7 @@ algorithm. Our definitions and proof are much simpler than those by Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the second part we analyse the correctness argument by Sulzmann and Lu and -explain why it seems hard to turn it into a proof rigorous enough to -be accepted by a system such as Isabelle/HOL.\smallskip +explain why the gaps in this argument cannot be filled easily.\smallskip {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions, Isabelle/HOL diff -r 91647a8d84a3 -r cdc0bdcfba3f thys/ReStar.thy --- a/thys/ReStar.thy Sun May 08 09:49:21 2016 +0100 +++ b/thys/ReStar.thy Mon May 09 12:09:56 2016 +0100 @@ -170,8 +170,6 @@ | Left val | Stars "val list" -datatype_compat val - section {* The string behind a value *} @@ -215,9 +213,8 @@ lemma Prf_flat_L: assumes "\ v : r" shows "flat v \ L r" using assms -apply(induct v r rule: Prf.induct) -apply(auto simp add: Sequ_def) -done +by(induct v r rule: Prf.induct) + (auto simp add: Sequ_def) lemma Prf_Stars: assumes "\v \ set vs. \ v : r" @@ -457,8 +454,7 @@ qed -(* a proof that does not need proj *) -lemma Posix2_roy_version: +lemma Posix_injval: assumes "s \ (der c r) \ v" shows "(c # s) \ r \ (injval r c v)" using assms @@ -636,7 +632,7 @@ apply(drule_tac x="der a r" in meta_spec) apply(simp add: der_correctness Der_def) apply(rule iffI) -apply(auto intro: Posix2_roy_version simp add: Posix1(1)) +apply(auto intro: Posix_injval simp add: Posix1(1)) done diff -r 91647a8d84a3 -r cdc0bdcfba3f thys/paper.pdf Binary file thys/paper.pdf has changed