diff -r 12772d537b71 -r 462d893ecb3d thys/Journal/Paper.thy
--- 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}
 *}