--- a/thys/Journal/Paper.thy Fri Aug 25 15:05:20 2017 +0200
+++ b/thys/Journal/Paper.thy Fri Aug 25 23:52:49 2017 +0200
@@ -1152,56 +1152,130 @@
@{thm [mode=IfThen] Posix_PosOrd[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
\end{theorem}
- \begin{proof} By induction on our POSIX rules. It is clear that
- @{text "v\<^sub>1"} and @{text "v\<^sub>2"} have the same underlying
- string.
+ \begin{proof} By induction on our POSIX rules. By
+ Thm~\ref{posixdeterm} and the definition of @{const LV}, it is clear
+ that @{text "v\<^sub>1"} and @{text "v\<^sub>2"} have the same
+ underlying string @{term s}. The three base cases are
+ straightforward: for example for @{term "v\<^sub>1 = Void"}, we have
+ that @{term "v\<^sub>2 \<in> LV ONE []"} must also be of the form
+ \mbox{@{term "v\<^sub>2 = Void"}}. Therefore we have @{term
+ "v\<^sub>1 :\<sqsubseteq>val v\<^sub>2"}. The inductive cases for
+ @{term "ALT r\<^sub>1 r\<^sub>2"} and @{term "SEQ r\<^sub>1
+ r\<^sub>2"} are as follows:
- The two base cases are straightforward: for example for @{term
- "v\<^sub>1 = Void"}, we have that @{term "v\<^sub>2 \<in> LV ONE
- []"} must also be of the form \mbox{@{term "v\<^sub>2 =
- Void"}}. Therefore we have @{term "v\<^sub>1 :\<sqsubseteq>val
- v\<^sub>2"}. The inductive cases are as follows:
+
+ \begin{itemize}
- \begin{itemize} \item[$\bullet$] Case @{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 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 same underlying string @{text s} is always
- smaller or equal than a @{text Right}-value. 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"}.\smallskip
+ \item[$\bullet$] Case @{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
+ 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
+ same underlying string @{text s} is always smaller or equal than a
+ @{text Right}-value. 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
\item[$\bullet$] Case @{term "s \<in> (ALT r\<^sub>1 r\<^sub>2)
\<rightarrow> (Right w\<^sub>1)"}: This case similar as the previous
case, except that we know that @{term "s \<notin> L
- r\<^sub>1"}. This is needed when @{term "v\<^sub>2 = 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 using Prop.~\ref{inhabs}. So also in this
- case \mbox{@{term "v\<^sub>1 :\<sqsubseteq>val v\<^sub>2"}}.\smallskip
+ 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
+ w\<^sub>2"} @{text "= s"}} and @{term "\<Turnstile> w\<^sub>2 :
+ r\<^sub>1"}, we can derive a contradiction using
+ Prop.~\ref{inhabs}. So also in this case \mbox{@{term "v\<^sub>1
+ :\<sqsubseteq>val v\<^sub>2"}}.\smallskip
- \item[$\bullet$] Case @{term "(s\<^sub>1 @ s\<^sub>2) \<in> (SEQ r\<^sub>1 r\<^sub>2)
- \<rightarrow> (Seq w\<^sub>1 w\<^sub>2)"}: 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
-
+ \item[$\bullet$] Case @{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 on out @{text PS}-rule we know that either @{term
+ "s\<^sub>1 = flat u\<^sub>1"} or @{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"} and are done.
+
\end{itemize}
+
+ \noindent The case for @{text "P\<star>"} is similar to the @{text PS}-case.\qed
\end{proof}
- Given a lexical value @{text "v\<^sub>1"}, say, in @{term "LV r s"} for which there does
- not exists any smaller value in @{term "LV r s"}, then this value is our POSIX value:
+ \noindent This theorem shows that our posix value @{text
+ "v\<^sub>1"} with @{term "s \<in> r \<rightarrow> v\<^sub>1"} is a
+ minimal element for 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 must be a @{text
+ POSIX}-value. Given a lexical value @{text "v\<^sub>1"}, say, in
+ @{term "LV r s"}, for which there does not exists any smaller value
+ in @{term "LV r s"}, then this value is our @{text POSIX}-value:
\begin{theorem}
@{thm [mode=IfThen] PosOrd_Posix[where ?v1.0="v\<^sub>1"]}
\end{theorem}
- \begin{proof}
- By induction on @{text r}.
+ \begin{proof} By induction on @{text r}. The tree base cases are
+ again straightforward. For example if @{term "v\<^sub>1 \<in> LV
+ ONE s"} then @{term "v\<^sub>1 = Void"} and @{term "s = []"}. We
+ know that @{term "[] \<in> ONE \<rightarrow> Void"} holds. In the
+ cases for @{term "ALT r\<^sub>1 r\<^sub>2"} and @{term "SEQ
+ r\<^sub>1 r\<^sub>2"} we reason as follows:
+
+ \begin{itemize}
+
+ \item[$\bullet$] Case @{term "v\<^sub>1 \<in> LV (ALT r\<^sub>1
+ r\<^sub>2) s"} with @{term "v\<^sub>1 = Left w\<^sub>1"} and @{term
+ "w\<^sub>1 \<in> LV r\<^sub>1 s"}: In order to use the induction
+ hypothesis we need to infer
+
+ \begin{center}
+ @{term "\<forall>v'
+ \<in> LV (ALT r\<^sub>1 r\<^sub>2) s. \<not> (v' :\<sqsubset>val
+ Left w\<^sub>1)"}
+ implies
+ @{term "\<forall>v' \<in> LV r\<^sub>1
+ s. \<not> (v' :\<sqsubset>val w\<^sub>1)"}
+ \end{center}
+
+ \noindent This can be done because of ?? we can infer that for every
+ @{text v'} in @{term "LV r\<^sub>1 s"} and @{term "v'
+ :\<sqsubset>val w\<^sub>1"} also @{term "Left v' :\<sqsubset>val
+ Left w\<^sub>1"} holds. This gives a contradiction. Consequently, we
+ can use the induction hypothesis to obtain @{term "s \<in> r\<^sub>1
+ \<rightarrow> w\<^sub>1"} and then conclude this case with @{term "s
+ \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> v\<^sub>1"}.\smallskip
+
+ \item[$\bullet$] Case @{term "v\<^sub>1 \<in> LV (ALT r\<^sub>1
+ r\<^sub>2) s"} with @{term "v\<^sub>1 = Right w\<^sub>1"} and @{term
+ "w\<^sub>1 \<in> LV r\<^sub>2 s"}: Like above we can use the
+ induction hypothesis in order to infer @{term "s \<in> r\<^sub>2
+ \<rightarrow> w\<^sub>1"}. In order to conclude we still need to
+ obtain @{term "s \<notin> L r\<^sub>1"}. Let us suppose the opposite.
+ Then there is a @{term v'} such that @{term "v' \<in> LV r\<^sub>1 s"}
+ by Prop ??? and hence @{term "Left v' \<in> LV (ALT r\<^sub>1 r\<^sub>2) s"}.
+ But then we can use the second assumption of the theorem to infer that
+ @{term "\<not>(Left v' :\<sqsubset>val Right w\<^sub>1)"}, which cannot be the case.
+ Therefore @{term "s \<notin> L r\<^sub>1"} must hold and we can also conclude in this
+ case.
+
+
+
+
+ \end{itemize}
+
\end{proof}
*}