--- a/thys/Paper/Paper.thy Mon May 09 12:53:12 2016 +0100
+++ b/thys/Paper/Paper.thy Mon May 09 15:00:28 2016 +0100
@@ -65,14 +65,9 @@
(*
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
@@ -80,9 +75,6 @@
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.
-
*)
(*>*)
@@ -602,7 +594,7 @@
\end{center}
\noindent If the regular expression does not match the string, @{const None} is
- returned, indicating an error is raised. If the regular expression \emph{does}
+ returned. If the regular expression \emph{does}
match the string, then @{const Some} value is returned. One important
virtue of this algorithm is that it can be implemented with ease in any
functional programming language and also in Isabelle/HOL. In the remaining
@@ -644,7 +636,22 @@
\end{tabular}
\end{center}
- \noindent We claim that this relation captures the idea behind the two
+ \noindent
+ We can prove that given a string @{term s} and regular expression @{term
+ r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow> v"}.
+
+ \begin{theorem}
+ @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}
+ \end{theorem}
+
+ \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and
+ a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the
+ auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl)
+ Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily
+ established by inductions.\qed \end{proof}
+
+
+ We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the two
informal POSIX rules shown in the Introduction: Consider for example the
rules @{text "P+L"} and @{text "P+R"} where the POSIX value for a string
and an alternative regular expression, that is @{term "(s, ALT r\<^sub>1 r\<^sub>2)"},
@@ -677,21 +684,6 @@
be ``chipped'' away; only in case of the empty string we accept @{term
"Stars []"} as the POSIX value.
- We can prove that given a string @{term s} and regular expression @{term
- r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow>
- v"}.
-
- \begin{theorem}
- @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}
- \end{theorem}
-
- \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and
- a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the
- auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl)
- Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily
- established by inductions.\qed \end{proof}
-
- \noindent
Next is the lemma that shows the function @{term "mkeps"} calculates
the POSIX value for the empty string and a nullable regular expression.
@@ -994,11 +986,11 @@
(v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''
formulation, for example:
- \begin{proposition}
+ \begin{falsehood}
Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}.
If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}
then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.
- \end{proposition}
+ \end{falsehood}
\noindent If formulated in this way, then there are various counter
examples: For example let @{term r} be @{text "a + ((a + a)\<cdot>(a + \<zero>))"}
@@ -1027,12 +1019,12 @@
counter-example we were able to find (by hand and by machine). Thus the
transitivity lemma should be formulated as:
- \begin{proposition}
+ \begin{conject}
Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"},
and also @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}.\\
If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}
then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.
- \end{proposition}
+ \end{conject}
\noindent While we agree with Sulzmann and Lu that this property
probably(!) holds, proving it seems not so straightforward: although one