# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1500399560 -3600
# Node ID d36be1e356c0ee01b9885e6fbf5f394af9c1e101
# Parent  e2828c4a1e2318e76d8966d3bdc2d64cf2fdff5a
changed definitions of PRF

diff -r e2828c4a1e23 -r d36be1e356c0 Literature/alternative-posix-conf.pdf
Binary file Literature/alternative-posix-conf.pdf has changed
diff -r e2828c4a1e23 -r d36be1e356c0 thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Thu Jul 06 16:05:33 2017 +0100
+++ b/thys/Journal/Paper.thy	Tue Jul 18 18:39:20 2017 +0100
@@ -3,17 +3,28 @@
 imports 
    "../Lexer"
    "../Simplifying" 
-   "../Sulzmann" 
+   "../Positions" 
    "~~/src/HOL/Library/LaTeXsugar"
 begin
 
+lemma Suc_0_fold:
+  "Suc 0 = 1"
+by simp
+
+
+
 declare [[show_question_marks = false]]
 
 abbreviation 
- "der_syn r c \<equiv> der c r"
+  "der_syn r c \<equiv> der c r"
 
 abbreviation 
- "ders_syn r s \<equiv> ders s r"
+  "ders_syn r s \<equiv> ders s r"
+
+
+abbreviation
+  "nprec v1 v2 \<equiv> \<not>(v1 :\<sqsubset>val v2)"
+
 
 notation (latex output)
   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
@@ -26,7 +37,7 @@
   SEQ ("_ \<cdot> _" [77,77] 78) and
   STAR ("_\<^sup>\<star>" [1000] 78) and
   
-  val.Void ("'(')" 1000) and
+  val.Void ("Empty" 78) and
   val.Char ("Char _" [1000] 78) and
   val.Left ("Left _" [79] 78) and
   val.Right ("Right _" [1000] 78) and
@@ -56,8 +67,18 @@
   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
   slexer ("lexer\<^sup>+" 1000) and
 
+  at ("_\<^raw:\mbox{$\downharpoonleft$}>\<^bsub>_\<^esub>") and
+  lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and
+  PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and
+  PosOrd_ex ("_ \<prec> _" [77,77] 77) and
+  PosOrd_ex1 ("_ \<^raw:\mbox{$\preccurlyeq$}> _" [77,77] 77) and
+  pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and
+  nprec ("_ \<^raw:\mbox{$\not\prec$}> _" [77,77] 77) 
+
+  (*
   ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and
   ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)
+  *)
 
 definition 
   "match r s \<equiv> nullable (ders s r)"
@@ -99,7 +120,7 @@
 one way of how the string is matched. There are two commonly used
 disambiguation strategies to generate a unique answer: one is called GREEDY
 matching \cite{Frisch2004} and the other is POSIX
-matching~\cite{Kuklewicz,Sulzmann2014,Vansummeren2006}. For example consider
+matching~\cite{POSIX,Kuklewicz,OkuiSuzuki2013,Sulzmann2014,Vansummeren2006}. For example consider
 the string @{term xy} and the regular expression \mbox{@{term "STAR (ALT
 (ALT x y) xy)"}}. Either the string can be matched in two `iterations' by
 the single letter-regular expressions @{term x} and @{term y}, or directly
@@ -114,18 +135,24 @@
 what programmers consider basic syntactic building blocks in their programs.
 These building blocks are often specified by some regular expressions, say
 @{text "r\<^bsub>key\<^esub>"} and @{text "r\<^bsub>id\<^esub>"} for recognising keywords and
-identifiers, respectively. There are two underlying (informal) rules behind
-tokenising a string in a POSIX fashion according to a collection of regular
+identifiers, respectively. There are a few underlying (informal) rules behind
+tokenising a string in a POSIX \cite{POSIX} fashion according to a collection of regular
 expressions:
 
 \begin{itemize} 
-\item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``maximal munch rule''}):
+\item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``{M}aximal {M}unch {R}ule''}):
 The longest initial substring matched by any regular expression is taken as
 next token.\smallskip
 
 \item[$\bullet$] \emph{Priority Rule:}
-For a particular longest initial substring, the first regular expression
-that can match determines the token.
+For a particular longest initial substring, the first (leftmost) regular expression
+that can match determines the token.\smallskip
+
+\item[$\bullet$] \emph{Star Rule:} A subexpression repeated by ${}^\star$ shall 
+not match an empty string unless this is the only match for the repetition.\smallskip
+
+\item[$\bullet$] \emph{Empty String Rule:} An empty string shall be considered to 
+be longer than no match at all.
 \end{itemize}
 
 \noindent Consider for example a regular expression @{text "r\<^bsub>key\<^esub>"} for recognising keywords
@@ -157,7 +184,7 @@
 algorithm. This proof idea is inspired by work of Frisch and Cardelli
 \cite{Frisch2004} on a GREEDY regular expression matching
 algorithm. However, we were not able to establish transitivity and
-totality for the ``order relation'' by Sulzmann and Lu. In Section
+totality for the ``order relation'' by Sulzmann and Lu. ??In Section
 \ref{argu} we identify some inherent problems with their approach (of
 which some of the proofs are not published in \cite{Sulzmann2014});
 perhaps more importantly, we give a simple inductive (and
@@ -1008,6 +1035,104 @@
   \end{proof} 
 *}
 
+section {* Ordering of Values according to Okui and Suzuki*}
+
+text {*
+
+ Positions are lists of natural numbers.
+
+ The subvalue at position @{text p}, written @{term "at v p"}, is defined 
+  
+
+ \begin{center}
+ \begin{tabular}{r@ {\hspace{0mm}}lcl}
+ @{term v} &  @{text "\<downharpoonleft>\<^bsub>[]\<^esub>"} & @{text "\<equiv>"}& @{thm (rhs) at.simps(1)}\\
+ @{term "Left v"} & @{text "\<downharpoonleft>\<^bsub>0::ps\<^esub>"} & @{text "\<equiv>"}& @{thm (rhs) at.simps(2)}\\
+ @{term "Right v"} & @{text "\<downharpoonleft>\<^bsub>1::ps\<^esub>"} & @{text "\<equiv>"} & 
+ @{thm (rhs) at.simps(3)[simplified Suc_0_fold]}\\
+ @{term "Seq v\<^sub>1 v\<^sub>2"} & @{text "\<downharpoonleft>\<^bsub>0::ps\<^esub>"} & @{text "\<equiv>"} & 
+ @{thm (rhs) at.simps(4)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} \\
+ @{term "Seq v\<^sub>1 v\<^sub>2"} & @{text "\<downharpoonleft>\<^bsub>1::ps\<^esub>"}
+ & @{text "\<equiv>"} & 
+ @{thm (rhs) at.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2", simplified Suc_0_fold]} \\
+ @{term "Stars vs"} & @{text "\<downharpoonleft>\<^bsub>n::ps\<^esub>"} & @{text "\<equiv>"}& @{thm (rhs) at.simps(6)}\\
+ \end{tabular} 
+ \end{center}
+
+ \begin{center}
+ \begin{tabular}{lcl}
+ @{thm (lhs) Pos.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(1)}\\
+ @{thm (lhs) Pos.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(2)}\\
+ @{thm (lhs) Pos.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(3)}\\
+ @{thm (lhs) Pos.simps(4)} & @{text "\<equiv>"} & @{thm (rhs) Pos.simps(4)}\\
+ @{thm (lhs) Pos.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+  & @{text "\<equiv>"} 
+  & @{thm (rhs) Pos.simps(5)[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}\\
+ @{thm (lhs) Pos_stars} & @{text "\<equiv>"} & @{thm (rhs) Pos_stars}\\
+ \end{tabular}
+ \end{center}
+
+ @{thm pflat_len_def}
+
+
+ \begin{center}
+ \begin{tabular}{ccc}
+ @{thm [mode=Axiom] lex_list.intros(1)}\hspace{1cm} &
+ @{thm [mode=Rule] lex_list.intros(2)[where ?ps1.0="ps\<^sub>1" and ?ps2.0="ps\<^sub>2"]}\hspace{1cm} &
+ @{thm [mode=Rule] lex_list.intros(3)[where ?p1.0="p\<^sub>1" and ?p2.0="p\<^sub>2" and
+                                            ?ps1.0="ps\<^sub>1" and ?ps2.0="ps\<^sub>2"]}
+ \end{tabular}
+ \end{center}
+
+
+ Main definition by Okui and Suzuki.
+
+ \begin{center}
+ \begin{tabular}{ccl}
+ @{thm (lhs) PosOrd_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} &
+ @{text "\<equiv>"} &
+ @{term "pflat_len v\<^sub>1 p > pflat_len v\<^sub>2 p"}   and\\
+ & & @{term "(\<forall>q \<in> Pos v\<^sub>1 \<union> Pos v\<^sub>2. q \<sqsubset>lex p --> pflat_len v\<^sub>1 q = pflat_len v\<^sub>2 q)"}
+ \end{tabular}
+ \end{center}
+
+ @{thm PosOrd_ex_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ @{thm PosOrd_ex1_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ Lemma 1
+
+ @{thm [mode=IfThen] PosOrd_shorterE[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ but in the other direction only
+
+ @{thm [mode=IfThen] PosOrd_shorterI[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} 
+
+ Lemma Transitivity:
+
+ @{thm [mode=IfThen] PosOrd_trans[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2" and ?v3.0="v\<^sub>3"]} 
+
+
+*}
+
+text {*
+
+ Theorems:
+
+ @{thm [mode=IfThen] Posix_CPT}
+
+ @{thm [mode=IfThen] Posix_PosOrd[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ Corrollary from the last one
+
+ @{thm [mode=IfThen] Posix_PosOrd_stronger[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+
+ Theorem
+
+ @{thm [mode=IfThen] PosOrd_Posix[where ?v1.0="v\<^sub>1"]}
+*}
+
+
 section {* The Correctness Argument by Sulzmann and Lu\label{argu} *}
 
 text {*
@@ -1022,24 +1147,7 @@
   Their central definition is an ``ordering relation'' defined by the
   rules (slightly adapted to fit our notation):
 
-\begin{center}  
-\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}	
-@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) &
-@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\
-
-@{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\,(A1) &
-@{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\,(A2)\smallskip\\
-
-@{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}\,(A3) &
-@{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\,(A4)\smallskip\\
-
-@{thm[mode=Rule] K1[of "v" "vs" "r"]}\,(K1) &
-@{thm[mode=Rule] K2[of "v" "vs" "r"]}\,(K2)\smallskip\\
-
-@{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\,(K3) &
-@{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\,(K4)
-\end{tabular}
-\end{center}
+  ??
 
   \noindent The idea behind the rules (A1) and (A2), for example, is that a
   @{text Left}-value is bigger than a @{text Right}-value, if the underlying
@@ -1062,143 +1170,8 @@
   What is interesting for our purposes is that the properties reflexivity,
   totality and transitivity for this GREEDY ordering can be proved
   relatively easily by induction.
-
-  These properties of GREEDY, however, do not transfer to the POSIX
-  ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. 
-  To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is
-  not defined inductively, but as $($@{term "v\<^sub>1 = v\<^sub>2"}$)$ $\vee$ $($@{term "(v\<^sub>1 >r
-  v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}$)$. This means that @{term "v\<^sub>1
-  >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp)
-  (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''
-  formulation, for example:
-
-  \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{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>))"}
-  then the @{term "v\<^sub>1"}, @{term "v\<^sub>2"} and @{term "v\<^sub>3"} below are values
-  of @{term r}:
-
-  \begin{center}
-  \begin{tabular}{lcl}
-  @{term "v\<^sub>1"} & $=$ & @{term "Left(Char a)"}\\
-  @{term "v\<^sub>2"} & $=$ & @{term "Right(Seq (Left(Char a)) (Right Void))"}\\
-  @{term "v\<^sub>3"} & $=$ & @{term "Right(Seq (Right(Char a)) (Left(Char a)))"}
-  \end{tabular}
-  \end{center}
-
-  \noindent Moreover @{term "v\<^sub>1 >(r::rexp) v\<^sub>2"} and @{term "v\<^sub>2 >(r::rexp)
-  v\<^sub>3"}, but \emph{not} @{term "v\<^sub>1 >(r::rexp) v\<^sub>3"}! The reason is that
-  although @{term "v\<^sub>3"} is a @{text "Right"}-value, it can match a longer
-  string, namely @{term "flat v\<^sub>3 = [a,a]"}, while @{term "flat v\<^sub>1"} (and
-  @{term "flat v\<^sub>2"}) matches only @{term "[a]"}. So transitivity in this
-  formulation does not hold---in this example actually @{term "v\<^sub>3
-  >(r::rexp) v\<^sub>1"}!
-
-  Sulzmann and Lu ``fix'' this problem by weakening the transitivity
-  property. They require in addition that the underlying strings are of the
-  same length. This excludes the counter example above and any
-  counter-example we were able to find (by hand and by machine). Thus the
-  transitivity lemma should be formulated as:
-
-  \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{conject}
-
-  \noindent While we agree with Sulzmann and Lu that this property
-  probably(!) holds, proving it seems not so straightforward: although one
-  begins with the assumption that the values have the same flattening, this
-  cannot be maintained as one descends into the induction. This is a problem
-  that occurs in a number of places in the proofs by Sulzmann and Lu.
-
-  Although they do not give an explicit proof of the transitivity property,
-  they give a closely related property about the existence of maximal
-  elements. They state that this can be verified by an induction on @{term r}. We
-  disagree with this as we shall show next in case of transitivity. The case
-  where the reasoning breaks down is the sequence case, say @{term "SEQ r\<^sub>1 r\<^sub>2"}.
-  The induction hypotheses in this case are
+*}
 
-\begin{center}
-\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
-\begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}}
-IH @{term "r\<^sub>1"}:\\
-@{text "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."} \\
-  & @{term "\<turnstile> v\<^sub>1 : r\<^sub>1"}\;@{text "\<and>"}
-    @{term "\<turnstile> v\<^sub>2 : r\<^sub>1"}\;@{text "\<and>"}
-    @{term "\<turnstile> v\<^sub>3 : r\<^sub>1"}\\
-  & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\
-  & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>2 \<and> v\<^sub>2 >(r\<^sub>1::rexp) v\<^sub>3"}\medskip\\
-  & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>3"}
-\end{tabular} &
-\begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}}
-IH @{term "r\<^sub>2"}:\\
-@{text "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."}\\ 
-  & @{term "\<turnstile> v\<^sub>1 : r\<^sub>2"}\;@{text "\<and>"}
-    @{term "\<turnstile> v\<^sub>2 : r\<^sub>2"}\;@{text "\<and>"}
-    @{term "\<turnstile> v\<^sub>3 : r\<^sub>2"}\\
-  & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\
-  & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>2 \<and> v\<^sub>2 >(r\<^sub>2::rexp) v\<^sub>3"}\medskip\\
-  & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>3"}
-\end{tabular}
-\end{tabular}
-\end{center} 
-
-  \noindent We can assume that
-  %
-  \begin{equation}
-  @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"}
-  \qquad\textrm{and}\qquad
-  @{term "(Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"}
-  \label{assms}
-  \end{equation}
-
-  \noindent hold, and furthermore that the values have equal length, namely:
-  %
-  \begin{equation}
-  @{term "flat (Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) = flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"}
-  \qquad\textrm{and}\qquad
-  @{term "flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) = flat (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"}
-  \label{lens}
-  \end{equation} 
-
-  \noindent We need to show that @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2)
-  (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"} holds. We can proceed by analysing how the
-  assumptions in \eqref{assms} have arisen. There are four cases. Let us
-  assume we are in the case where we know
-
-  \[
-  @{term "v\<^sub>1\<^sub>l >(r\<^sub>1::rexp) v\<^sub>2\<^sub>l"}
-  \qquad\textrm{and}\qquad
-  @{term "v\<^sub>2\<^sub>l >(r\<^sub>1::rexp) v\<^sub>3\<^sub>l"}
-  \]
-
-  \noindent and also know the corresponding inhabitation judgements. This is
-  exactly a case where we would like to apply the induction hypothesis
-  IH~$r_1$. But we cannot! We still need to show that @{term "flat (v\<^sub>1\<^sub>l) =
-  flat(v\<^sub>2\<^sub>l)"} and @{term "flat(v\<^sub>2\<^sub>l) = flat(v\<^sub>3\<^sub>l)"}. We know from
-  \eqref{lens} that the lengths of the sequence values are equal, but from
-  this we cannot infer anything about the lengths of the component values.
-  Indeed in general they will be unequal, that is
-
-  \[
-  @{term "flat(v\<^sub>1\<^sub>l) \<noteq> flat(v\<^sub>2\<^sub>l)"}  
-  \qquad\textrm{and}\qquad
-  @{term "flat(v\<^sub>1\<^sub>r) \<noteq> flat(v\<^sub>2\<^sub>r)"}
-  \]
-
-  \noindent but still \eqref{lens} will hold. Now we are stuck, since the IH
-  does not apply. As said, this problem where the induction hypothesis does
-  not apply arises in several places in the proof of Sulzmann and Lu, not
-  just for proving transitivity.
-
-*}
 
 section {* Conclusion *}
 
diff -r e2828c4a1e23 -r d36be1e356c0 thys/Journal/document/root.bib
--- a/thys/Journal/document/root.bib	Thu Jul 06 16:05:33 2017 +0100
+++ b/thys/Journal/document/root.bib	Tue Jul 18 18:39:20 2017 +0100
@@ -1,5 +1,25 @@
+
+
+
+@Misc{POSIX,
+  title =     {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition},
+  year =      {2004},
+  note =    {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}}
+}
+
+
+@InProceedings{AusafDyckhoffUrban2016,
+  author =   {F.~Ausaf and R.~Dyckhoff and C.~Urban},
+  title = 	 {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)},
+  year = 	 {2016},
+  booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)},
+  volume = 	 {9807},
+  series = 	 {LNCS},
+  pages =        {69--86}
+}
+
 @article{aduAFP16,
-  author =   {Fahad Ausaf and Roy Dyckhoff and Christian Urban},
+  author =   {F.~Ausaf and R.~Dyckhoff and C.~Urban},
   title =    {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions},
   journal =  {Archive of Formal Proofs},
   year =     2016,
@@ -255,13 +275,6 @@
   series =       {LNCS}
 }
 
-@book{Michaelson,
-  title={An introduction to functional programming through lambda calculus},
-  author={Michaelson, Greg},
-  year={2011},
-  publisher={Courier Corporation}
-}
-
 @article{Owens2008,
   author    = {S.~Owens and K.~Slind},
   title     = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},
@@ -273,92 +286,8 @@
 }
 
 
-@book{Velleman,
-  title={How to prove it: a structured approach},
-  author={Velleman, Daniel J},
-  year={2006},
-  publisher={Cambridge University Press}
-}
-
-@book{Jones,
-  title={Implementing functional languages:[a tutorial]},
-  author={Jones, Simon L Peyton and Lester, David R},
-  volume={124},
-  year={1992},
-  publisher={Prentice Hall Reading}
-}
-
-@article{Cardelli,
-  title={Type systems},
-  author={Cardelli, Luca},
-  journal={ACM Computing Surveys},
-  volume={28},
-  number={1},
-  pages={263--264},
-  year={1996}
-}
-
-@article{Morrisett,
-  author    = {J. Gregory Morrisett and
-               Karl Crary and
-               Neal Glew and
-               David Walker},
-  title     = {Stack-based typed assembly language},
-  journal   = {J. Funct. Program.},
-  volume    = {13},
-  number    = {5},
-  pages     = {957--959},
-  year      = {2003},
-  url       = {http://dx.doi.org/10.1017/S0956796802004446},
-  doi       = {10.1017/S0956796802004446},
-  timestamp = {Fri, 19 Mar 2004 13:48:27 +0100},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jfp/MorrisettCGW03},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
-@book{Nipkow,
-  title={Concrete Semantics: With Isabelle/HOL},
-  author={Nipkow, Tobias and Klein, Gerwin},
-  year={2014},
-  publisher={Springer}
-}
-
-@article{Dube,
-  author    = {Danny Dub{\'{e}} and
-               Marc Feeley},
-  title     = {Efficiently building a parse tree from a regular expression},
-  journal   = {Acta Inf.},
-  volume    = {37},
-  number    = {2},
-  pages     = {121--144},
-  year      = {2000},
-  url       = {http://link.springer.de/link/service/journals/00236/bibs/0037002/00370121.htm},
-  timestamp = {Tue, 25 Nov 2003 14:51:21 +0100},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/acta/DubeF00},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
-@article{Morrisett2,
-  author    = {J. Gregory Morrisett and
-               David Walker and
-               Karl Crary and
-               Neal Glew},
-  title     = {From system {F} to typed assembly language},
-  journal   = {{ACM} Trans. Program. Lang. Syst.},
-  volume    = {21},
-  number    = {3},
-  pages     = {527--568},
-  year      = {1999},
-  url       = {http://doi.acm.org/10.1145/319301.319345},
-  doi       = {10.1145/319301.319345},
-  timestamp = {Wed, 26 Nov 2003 14:26:46 +0100},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/toplas/MorrisettWCG99},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
 @article{Owens2,
-  author    = {Scott Owens and
-               Konrad Slind},
+  author    = {S.~Owens and K.~Slind},
   title     = {Adapting functional programs to higher order logic},
   journal   = {Higher-Order and Symbolic Computation},
   volume    = {21},
@@ -379,3 +308,15 @@
 
 
 
+@InProceedings{OkuiSuzuki2013,
+  author =       {S.~Okui and T.~Suzuki},
+  title =        {{D}isambiguation in {R}egular {E}xpression {M}atching via
+                  {P}osition {A}utomata with {A}ugmented {T}ransitions},
+  booktitle = {Proc.~of the 15th International Conference on Implementation
+                  and Application of Automata (CIAA)},
+  year =      {2010},
+  volume =    {6482},
+  series =    {LNCS},
+  pages =     {231--240}
+}
+
diff -r e2828c4a1e23 -r d36be1e356c0 thys/Journal/document/root.tex
--- a/thys/Journal/document/root.tex	Thu Jul 06 16:05:33 2017 +0100
+++ b/thys/Journal/document/root.tex	Tue Jul 18 18:39:20 2017 +0100
@@ -33,8 +33,17 @@
 \newtheorem{conject}{Conjecture}
 
 \begin{document}
+\renewcommand{\thefootnote}{$\star$} \footnotetext[1]{This paper is a
+  revised and expanded version of \cite{AusafDyckhoffUrban2016}.
+  Compared with that paper we give a second definition for POSIX
+  values and prove that it is equivalent to the original one. This
+  definition is based on an ordering of values and very similar to the
+  definition given by Sulzmann and Lu~\cite{Sulzmann2014}. We also
+  extend our results to additional constructors of regular
+  expressions.}  \renewcommand{\thefootnote}{\arabic{footnote}}
 
-\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)}
+
+\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions}
 \author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{3}}
 \institute{King's College London\\
 		\email{fahad.ausaf@icloud.com}
@@ -50,20 +59,19 @@
 expressions. They can be used for a very simple regular expression
 matching algorithm.  Sulzmann and Lu cleverly extended this algorithm
 in order to deal with POSIX matching, which is the underlying
-disambiguation strategy for regular expressions needed in lexers.
-Sulzmann and Lu have made available on-line what they call a
-``rigorous proof'' of the correctness of their algorithm w.r.t.\ their
-specification; regrettably, it appears to us to have unfillable gaps.
-In the first part of this paper we give our inductive definition of
-what a POSIX value is and show $(i)$ that such a value is unique (for
-given regular expression and string being matched) and $(ii)$ that
-Sulzmann and Lu's algorithm always generates such a value (provided
-that the regular expression matches the string).  We also prove the
-correctness of an optimised version of the POSIX matching
-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 the gaps in this argument cannot be filled easily.\smallskip
+disambiguation strategy for regular expressions needed in lexers.  In
+the first part of this paper we give our inductive definition of what
+a POSIX value is and show $(i)$ that such a value is unique (for given
+regular expression and string being matched) and $(ii)$ that Sulzmann
+and Lu's algorithm always generates such a value (provided that the
+regular expression matches the string). We also prove the correctness
+of an optimised version of the POSIX matching algorithm.  In the
+second part we show that $(iii)$ our inductive definition of a POSIX
+value is equivalent to an alternative definition by Okui and Suzuki
+which identifies a POSIX value as least element according to an
+ordering of values. The advantage of the definition based on the
+ordering is that it implements more directly the POSIX
+longest-leftmost matching semantics.\smallskip
 
 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
 Isabelle/HOL
diff -r e2828c4a1e23 -r d36be1e356c0 thys/Lexer.thy
--- a/thys/Lexer.thy	Thu Jul 06 16:05:33 2017 +0100
+++ b/thys/Lexer.thy	Tue Jul 18 18:39:20 2017 +0100
@@ -79,17 +79,20 @@
 by (auto) (metis Star.simps)
 
 lemma Star_decomp: 
-  assumes a: "c # x \<in> A\<star>" 
-  shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
-using a
+  assumes "c # x \<in> A\<star>" 
+  shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>"
+using assms
 by (induct x\<equiv>"c # x" rule: Star.induct) 
    (auto simp add: append_eq_Cons_conv)
 
 lemma Star_Der_Sequ: 
   shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"
 unfolding Der_def
-by(auto simp add: Der_def Sequ_def Star_decomp)
-
+apply(rule subsetI)
+apply(simp)
+unfolding Sequ_def
+apply(simp)
+by(auto simp add: Sequ_def Star_decomp)
 
 
 lemma Der_star [simp]:
@@ -245,8 +248,7 @@
 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 | "\<turnstile> Void : ONE"
 | "\<turnstile> Char c : CHAR c"
-| "\<turnstile> Stars [] : STAR r"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
+| "\<forall>v \<in> set vs. \<turnstile> v : r \<Longrightarrow> \<turnstile> Stars vs : STAR r"
 
 inductive_cases Prf_elims:
   "\<turnstile> v : ZERO"
@@ -254,31 +256,25 @@
   "\<turnstile> v : ALT r1 r2"
   "\<turnstile> v : ONE"
   "\<turnstile> v : CHAR c"
-(*  "\<turnstile> vs : STAR r"*)
+  "\<turnstile> vs : STAR r"
+
+lemma Star_concat:
+  assumes "\<forall>s \<in> set ss. s \<in> A"  
+  shows "concat ss \<in> A\<star>"
+using assms by (induct ss) (auto)
+
 
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
-by(induct v r rule: Prf.induct)
-  (auto simp add: Sequ_def)
-
-lemma Prf_Stars:
-  assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
-  shows "\<turnstile> Stars vs : STAR r"
-using assms
-by(induct vs) (auto intro: Prf.intros)
+by (induct v r rule: Prf.induct)
+   (auto simp add: Sequ_def Star_concat)
 
 lemma Prf_Stars_append:
   assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"
   shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"
 using assms
-apply(induct vs1 arbitrary: vs2)
-apply(auto intro: Prf.intros)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto intro: Prf.intros)
-done
-
+by (auto intro!: Prf.intros elim!: Prf_elims)
 
 lemma Star_string:
   assumes "s \<in> A\<star>"
@@ -306,40 +302,45 @@
   assumes "\<turnstile> v : r" 
   shows "flat v \<in> L r"
 using assms
-by (induct)(auto simp add: Sequ_def)
+by (induct) (auto simp add: Sequ_def Star_concat)
 
 lemma L_flat_Prf2:
   assumes "s \<in> L r" 
   shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
 using assms
-apply(induct r arbitrary: s)
-apply(auto simp add: Sequ_def intro: Prf.intros)
-using Prf.intros(1) flat.simps(5) apply blast
-using Prf.intros(2) flat.simps(3) apply blast
-using Prf.intros(3) flat.simps(4) apply blast
-apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
-apply(auto)[1]
-apply(rule_tac x="Stars vs" in exI)
-apply(simp)
-apply (simp add: Prf_Stars)
-apply(drule Star_string)
-apply(auto)
-apply(rule Star_val)
-apply(auto)
-done
+proof(induct r arbitrary: s)
+  case (STAR r s)
+  have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> flat v = s" by fact
+  have "s \<in> L (STAR r)" by fact
+  then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r"
+  using Star_string by auto
+  then obtain vs where "concat (map flat vs) = s" "\<forall>v\<in>set vs. \<turnstile> v : r"
+  using IH Star_val by blast
+  then show "\<exists>v. \<turnstile> v : STAR r \<and> flat v = s"
+  using Prf.intros(6) flat_Stars by blast
+next 
+  case (SEQ r1 r2 s)
+  then show "\<exists>v. \<turnstile> v : SEQ r1 r2 \<and> flat v = s"
+  unfolding Sequ_def L.simps by (fastforce intro: Prf.intros)
+next
+  case (ALT r1 r2 s)
+  then show "\<exists>v. \<turnstile> v : ALT r1 r2 \<and> flat v = s"
+  unfolding L.simps by (fastforce intro: Prf.intros)
+qed (auto intro: Prf.intros)
 
 lemma L_flat_Prf:
   "L(r) = {flat v | v. \<turnstile> v : r}"
 using L_flat_Prf1 L_flat_Prf2 by blast
 
+(*
 lemma Star_values_exists:
   assumes "s \<in> (L r)\<star>"
   shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r"
 using assms
 apply(drule_tac Star_string)
 apply(auto)
-by (metis L_flat_Prf2 Prf_Stars Star_val)
-
+by (metis L_flat_Prf2 Prf.intros(6) Star_val)
+*)
 
 
 section {* Sulzmann and Lu functions *}
@@ -385,24 +386,14 @@
 using assms
 apply(induct r arbitrary: c v rule: rexp.induct)
 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
-(* STAR *)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)
-apply (metis Prf.intros(6) Prf.intros(7))
-by (metis Prf.intros(7))
+done
 
 lemma Prf_injval_flat:
   assumes "\<turnstile> v : der c r" 
   shows "flat (injval r c v) = c # (flat v)"
 using assms
 apply(induct arbitrary: v rule: der.induct)
-apply(auto elim!: Prf_elims split: if_splits)
-apply(metis mkeps_flat)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)[7]
+apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
 done
 
 
@@ -444,7 +435,9 @@
   assumes "s \<in> r \<rightarrow> v"
   shows "\<turnstile> v : r"
 using assms
-by (induct s r v rule: Posix.induct)(auto intro: Prf.intros)
+apply(induct s r v rule: Posix.induct)
+apply(auto intro!: Prf.intros elim!: Prf_elims)
+done
 
 
 lemma Posix_mkeps:
diff -r e2828c4a1e23 -r d36be1e356c0 thys/Positions.thy
--- a/thys/Positions.thy	Thu Jul 06 16:05:33 2017 +0100
+++ b/thys/Positions.thy	Tue Jul 18 18:39:20 2017 +0100
@@ -3,8 +3,7 @@
   imports "Lexer" 
 begin
 
-
-section {* Position in values *}
+section {* Positions in Values *}
 
 fun 
   at :: "val \<Rightarrow> nat list \<Rightarrow> val"
@@ -16,6 +15,8 @@
 | "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
 | "at (Stars vs) (n#ps)= at (nth vs n) ps"
 
+
+
 fun Pos :: "val \<Rightarrow> (nat list) set"
 where
   "Pos (Void) = {[]}"
@@ -26,15 +27,13 @@
 | "Pos (Stars []) = {[]}"
 | "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
 
+
 lemma Pos_stars:
   "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
 apply(induct vs)
 apply(simp) 
-apply(simp)
 apply(simp add: insert_ident)
 apply(rule subset_antisym)
-apply(auto)
-apply(auto)[1]
 using less_Suc_eq_0_disj by auto
 
 lemma Pos_empty:
@@ -44,7 +43,7 @@
 fun intlen :: "'a list \<Rightarrow> int"
 where
   "intlen [] = 0"
-| "intlen (x#xs) = 1 + intlen xs"
+| "intlen (x # xs) = 1 + intlen xs"
 
 lemma intlen_bigger:
   shows "0 \<le> intlen xs"
@@ -62,6 +61,15 @@
 apply (smt Suc_lessI intlen.simps(2) length_Suc_conv nat_neq_iff)
 by (smt Suc_lessE intlen.simps(2) length_Suc_conv)
 
+lemma intlen_length_eq:
+  shows "intlen xs = intlen ys \<longleftrightarrow> length xs = length ys"
+apply(induct xs arbitrary: ys)
+apply (auto simp add: intlen_bigger not_less)
+apply(case_tac ys)
+apply(simp_all)
+apply (smt intlen_bigger)
+apply (smt intlen.elims intlen_bigger length_Suc_conv)
+by (metis intlen.simps(2) length_Suc_conv)
 
 definition pflat_len :: "val \<Rightarrow> nat list => int"
 where
@@ -87,9 +95,9 @@
 apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
 done
 
-lemma outside_lemma:
-  assumes "p \<notin> Pos v1 \<union> Pos v2"
-  shows "pflat_len v1 p = pflat_len v2 p"
+lemma pflat_len_outside:
+  assumes "p \<notin> Pos v1"
+  shows "pflat_len v1 p = -1 "
 using assms by (auto simp add: pflat_len_def)
 
 
@@ -121,10 +129,8 @@
   fixes xs ys :: "nat list"
   shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
   and   "xs \<sqsubset>lex [] \<longleftrightarrow> False"
-  and   "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))"
-apply(auto elim: lex_list.cases intro: lex_list.intros)
-apply(auto simp add: neq_Nil_conv not_less_iff_gr_or_eq intro: lex_list.intros)
-done
+  and   "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (x = y \<and> xs \<sqsubset>lex ys))"
+by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros)
 
 lemma lex_trans:
   fixes ps1 ps2 ps3 :: "nat list"
@@ -139,7 +145,7 @@
   fixes p q :: "nat list"
   shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
 apply(induct p arbitrary: q)
-apply(auto)
+apply(auto elim: lex_list.cases)
 apply(case_tac q)
 apply(auto)
 done
@@ -147,7 +153,7 @@
 
 
 
-section {* Ordering of values according to Okui & Suzuki *}
+section {* POSIX Ordering of Values According to Okui & Suzuki *}
 
 
 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
@@ -155,111 +161,95 @@
   "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and>
                    (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
 
-definition PosOrd2:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val2 _ _" [60, 60, 59] 60)
-where
-  "v1 \<sqsubset>val2 p v2 \<equiv> p \<in> Pos v1 \<and> 
-                   pflat_len v1 p > pflat_len v2 p \<and>
-                   (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
+
 
-lemma XXX:
-  "v1 \<sqsubset>val p v2 \<longleftrightarrow> v1 \<sqsubset>val2 p v2"
-apply(auto simp add: PosOrd_def PosOrd2_def)
-apply(auto simp add: pflat_len_def split: if_splits)
-by (smt intlen_bigger)
+definition pflat_len2 :: "val \<Rightarrow> nat list => (bool * nat)"
+where
+  "pflat_len2 v p \<equiv> (if p \<in> Pos v then (True, length (flat (at v p))) else (False, 0))"
+
+instance prod :: (ord, ord) ord
+  by (rule Orderings.class.Orderings.ord.of_class.intro)
 
 
-(* some tests *)
+lemma "(0, 0) < (3::nat, 2::nat)"
 
-definition ValFlat_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>fval _ _")
-where
-  "v1 \<sqsubset>fval p v2 \<equiv> p \<in> Pos v1 \<and> 
-                    (p \<notin> Pos v2 \<or> flat (at v2 p) \<sqsubset>spre flat (at v1 p)) \<and>
-                    (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> (pflat_len v1 q = pflat_len v2 q))"
+
+
 
-lemma 
-  assumes "v1 \<sqsubset>fval p v2" 
-  shows "v1 \<sqsubset>val p v2"
-using assms
-unfolding ValFlat_ord_def PosOrd_def
-apply(clarify)
-apply(simp add: pflat_len_def)
-apply(auto)[1]
-apply(smt intlen_bigger)
-apply(simp add: sprefix_list_def prefix_list_def)
-apply(auto)[1]
-apply(drule sym)
-apply(simp add: intlen_append)
-apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3))
-apply(smt intlen_bigger)
-done
-
-lemma 
-  assumes "v1 \<sqsubset>val p v2" "flat (at v2 p) \<sqsubset>spre flat (at v1 p)"
-  shows "v1 \<sqsubset>fval p v2"
-using assms
-unfolding ValFlat_ord_def PosOrd_def
-apply(clarify)
-oops
+definition PosOrd2:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val2 _ _" [60, 60, 59] 60)
+where
+  "v1 \<sqsubset>val2 p v2 \<equiv> (fst (pflat_len2 v1 p) > fst (pflat_len2 v2 p) \<or>
+                     snd (pflat_len2 v1 p) > fst (pflat_len2 v2 p)) \<and>
+                    (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
 
 
 definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
 where
-  "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)"
+  "v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2"
 
-definition PosOrd_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
+definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
 where
   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
 
+
 lemma PosOrd_shorterE:
   assumes "v1 :\<sqsubset>val v2" 
   shows "length (flat v2) \<le> length (flat v1)"
 using assms
-apply(auto simp add: PosOrd_ex_def PosOrd_def)
+apply(auto simp add: pflat_len_simps PosOrd_ex_def PosOrd_def)
 apply(case_tac p)
-apply(simp add: pflat_len_simps)
-apply(simp add: intlen_length)
+apply(simp add: pflat_len_simps intlen_length)
 apply(simp)
 apply(drule_tac x="[]" in bspec)
 apply(simp add: Pos_empty)
-apply(simp add: pflat_len_simps)
-by (metis intlen_length le_less less_irrefl linear)
-
+apply(simp add: pflat_len_simps le_less intlen_length_eq)
+done
 
 lemma PosOrd_shorterI:
-  assumes "length (flat v') < length (flat v)"
-  shows "v :\<sqsubset>val v'" 
+  assumes "length (flat v2) < length (flat v1)"
+  shows "v1 :\<sqsubset>val v2" 
 using assms
 unfolding PosOrd_ex_def
 by (metis intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def)
 
 lemma PosOrd_spreI:
-  assumes "(flat v') \<sqsubset>spre (flat v)"
+  assumes "flat v' \<sqsubset>spre flat v"
   shows "v :\<sqsubset>val v'" 
 using assms
 apply(rule_tac PosOrd_shorterI)
 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
 
+
 lemma PosOrd_Left_Right:
   assumes "flat v1 = flat v2"
   shows "Left v1 :\<sqsubset>val Right v2" 
 unfolding PosOrd_ex_def
 apply(rule_tac x="[0]" in exI)
-using assms
+using assms 
 apply(auto simp add: PosOrd_def pflat_len_simps)
 apply(smt intlen_bigger)
 done
 
-lemma PosOrd_LeftI:
-  assumes "v :\<sqsubset>val v'" "flat v = flat v'"
-  shows "(Left v) :\<sqsubset>val (Left v')" 
-using assms(1)
+lemma PosOrd_Left_eq:
+  assumes "flat v = flat v'"
+  shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'" 
+using assms
 unfolding PosOrd_ex_def
 apply(auto)
+apply(case_tac p)
+apply(simp add: PosOrd_def pflat_len_simps)
+apply(case_tac a)
+apply(simp add: PosOrd_def pflat_len_simps)
+apply(rule_tac x="list" in exI)
+apply(auto simp add: PosOrd_def pflat_len_simps)[1]
+apply (smt Un_def lex_list.intros(2) mem_Collect_eq pflat_len_simps(3))
+apply (smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(3))
+apply(auto simp add: PosOrd_def pflat_len_outside)[1]
 apply(rule_tac x="0#p" in exI)
-using assms(2)
 apply(auto simp add: PosOrd_def pflat_len_simps)
 done
 
+
 lemma PosOrd_RightI:
   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
   shows "(Right v) :\<sqsubset>val (Right v')" 
@@ -271,31 +261,6 @@
 apply(auto simp add: PosOrd_def pflat_len_simps)
 done
 
-lemma PosOrd_LeftE:
-  assumes "(Left v1) :\<sqsubset>val (Left v2)"
-  shows "v1 :\<sqsubset>val v2"
-using assms
-apply(simp add: PosOrd_ex_def)
-apply(erule exE)
-apply(case_tac p)
-apply(simp add: PosOrd_def)
-apply(auto simp add: pflat_len_simps)
-apply(rule_tac x="[]" in exI)
-apply(simp add: Pos_empty pflat_len_simps)
-apply(auto simp add: pflat_len_simps PosOrd_def)
-apply(case_tac a)
-apply(auto simp add: pflat_len_simps)[1]
-apply(rule_tac x="list" in exI)
-apply(auto)
-apply(drule_tac x="0#q" in bspec)
-apply(simp)
-apply(simp add: pflat_len_simps)
-apply(drule_tac x="0#q" in bspec)
-apply(simp)
-apply(simp add: pflat_len_simps)
-apply(simp add: pflat_len_def)
-done
-
 lemma PosOrd_RightE:
   assumes "(Right v1) :\<sqsubset>val (Right v2)"
   shows "v1 :\<sqsubset>val v2"
@@ -517,14 +482,14 @@
     by (rule lex_trichotomous)
   moreover
     { assume "p = p'"
-      with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def
-      by (smt outside_lemma)
+      with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
+      by fastforce
       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
     }   
   moreover
     { assume "p \<sqsubset>lex p'"
-      with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def
-      by (metis lex_trans outside_lemma)
+      with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
+      by (smt Un_iff lex_trans)
       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
     }
   moreover
@@ -560,26 +525,47 @@
 apply(auto simp add: PosOrd_ex_def PosOrd_def)
 using assms PosOrd_irrefl PosOrd_trans by blast
 
-lemma WW2:
-  assumes "\<not>(v1 :\<sqsubset>val v2)" 
-  shows "v1 = v2 \<or> v2 :\<sqsubset>val v1"
-using assms
-oops
-
 lemma PosOrd_SeqE2:
-  assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
-  shows "v1 :\<sqsubset>val v1' \<or> (v1 = v1' \<and> v2 :\<sqsubset>val v2')"
+  assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
+  shows "v1 :\<sqsubset>val v1' \<or> (intlen (flat v1) = intlen (flat v1') \<and> v2 :\<sqsubset>val v2')"
 using assms 
 apply(frule_tac PosOrd_SeqE)
 apply(erule disjE)
 apply(simp)
-apply(auto)
 apply(case_tac "v1 :\<sqsubset>val v1'")
 apply(simp)
+apply(rule disjI2)
+apply(rule conjI)
+prefer 2
+apply(simp)
+apply(auto)
 apply(auto simp add: PosOrd_ex_def)
-apply(case_tac "v1 = v1'")
+apply(auto simp add: PosOrd_def pflat_len_simps)
+apply(case_tac p)
+apply(auto simp add: PosOrd_def pflat_len_simps)
+apply(case_tac a)
+apply(auto simp add: PosOrd_def pflat_len_simps)
+apply (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
+by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
+
+lemma PosOrd_SeqE4:
+  assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
+  shows "v1 :\<sqsubset>val v1' \<or> (flat v1 = flat v1' \<and> v2 :\<sqsubset>val v2')"
+using assms 
+apply(frule_tac PosOrd_SeqE)
+apply(erule disjE)
 apply(simp)
-oops
+apply(case_tac "v1 :\<sqsubset>val v1'")
+apply(simp)
+apply(rule disjI2)
+apply(rule conjI)
+prefer 2
+apply(simp)
+apply(auto)
+apply(case_tac "length (flat v1') < length (flat v1)")
+using PosOrd_shorterI apply blast
+by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2))
+
 
 section {* CPT and CPTpre *}
 
@@ -592,84 +578,19 @@
 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 | "\<Turnstile> Void : ONE"
 | "\<Turnstile> Char c : CHAR c"
-| "\<Turnstile> Stars [] : STAR r"
-| "\<lbrakk>\<Turnstile> v : r; flat v \<noteq> []; \<Turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
+| "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
 
 lemma Prf_CPrf:
   assumes "\<Turnstile> v : r"
   shows "\<turnstile> v : r"
 using assms
-by (induct) (auto intro: Prf.intros)
-
-lemma pflat_len_equal_iff:
-  assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
-  and "\<forall>p. pflat_len v1 p = pflat_len v2 p"
-  shows "v1 = v2"
-using assms
-apply(induct v1 r arbitrary: v2 rule: CPrf.induct)
-apply(rotate_tac 4)
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply (metis pflat_len_simps(1) pflat_len_simps(2))
-apply(rotate_tac 2)
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply (metis pflat_len_simps(3))
-apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9))
-apply(rotate_tac 2)
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9))
-apply (metis pflat_len_simps(5))
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv neq_Nil_conv not_less_iff_gr_or_eq pflat_len_simps(9))
-apply(rotate_tac 5)
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv list.distinct(1) list.exhaust not_less_iff_gr_or_eq pflat_len_simps(9))
-apply(auto)
-apply (metis pflat_len_simps(8))
-apply(subgoal_tac "v = va")
-prefer 2
-apply (metis pflat_len_simps(8))
-apply(simp)
-apply(rotate_tac 3)
-apply(drule_tac x="Stars vsa" in meta_spec)
-apply(simp)
-apply(drule_tac meta_mp)
-apply(rule allI)
-apply(case_tac p)
-apply(simp add: pflat_len_simps)
-apply(drule_tac x="[]" in spec)
-apply(simp add: pflat_len_simps intlen_append)
-apply(drule_tac x="Suc a#list" in spec)
-apply(simp add: pflat_len_simps intlen_append)
-apply(simp)
-done
-
-lemma PosOrd_trichotomous_stronger:
-  assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
-  shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (v1 = v2)"
-oops
+by (induct)(auto intro: Prf.intros)
 
 lemma CPrf_stars:
   assumes "\<Turnstile> Stars vs : STAR r"
   shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
 using assms
-apply(induct vs)
-apply(auto)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
+apply(erule_tac CPrf.cases)
 apply(simp_all)
 done
 
@@ -677,11 +598,8 @@
   assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
   shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
 using assms
-apply(induct vs1 arbitrary: vs2)
-apply(auto intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(auto intro: CPrf.intros)
+apply(erule_tac CPrf.cases)
+apply(auto intro: CPrf.intros elim: Prf.cases)
 done
 
 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
@@ -697,6 +615,74 @@
   shows "CPT r s \<subseteq> CPTpre r s"
 by(auto simp add: CPT_def CPTpre_def)
 
+lemma CPT_simps:
+  shows "CPT ZERO s = {}"
+  and   "CPT ONE s = (if s = [] then {Void} else {})"
+  and   "CPT (CHAR c) s = (if s = [c] then {Char c} else {})"
+  and   "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"
+  and   "CPT (SEQ r1 r2) s = 
+          {Seq v1 v2 | v1 v2. flat v1 @ flat v2 = s \<and> v1 \<in> CPT r1 (flat v1) \<and> v2 \<in> CPT r2 (flat v2)}"
+  and   "CPT (STAR r) s = 
+          Stars ` {vs. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. v \<in> CPT r (flat v) \<and> flat v \<noteq> [])}"
+apply -
+apply(auto simp add: CPT_def intro: CPrf.intros)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[6]
+apply(auto simp add: CPT_def intro: CPrf.intros)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[6]
+apply(erule CPrf.cases)
+apply(simp_all)[6]
+apply(auto simp add: CPT_def intro: CPrf.intros)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[6]
+apply(erule CPrf.cases)
+apply(simp_all)[6]
+apply(auto simp add: CPT_def intro: CPrf.intros)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[6]
+apply(auto simp add: CPT_def intro: CPrf.intros)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[6]
+(* STAR case *)
+apply(auto simp add: CPT_def intro: CPrf.intros)[1]
+apply(erule CPrf.cases)
+apply(simp_all)[6]
+done
+
+(*
+lemma CPTpre_STAR_finite:
+  assumes "\<And>s. finite (CPT r s)"
+  shows "finite (CPT (STAR r) s)"
+apply(induct s rule: length_induct)
+apply(case_tac xs)
+apply(simp)
+apply(simp add: CPT_simps)
+apply(auto)
+apply(rule finite_imageI)
+using assms
+thm finite_Un
+prefer 2
+apply(simp add: CPT_simps)
+apply(rule finite_imageI)
+apply(rule finite_subset)
+apply(rule CPTpre_subsets)
+apply(simp)
+apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)
+apply(auto)[1]
+apply(rule finite_imageI)
+apply(simp add: Collect_case_prod_Sigma)
+apply(rule finite_SigmaI)
+apply(rule assms)
+apply(case_tac "flat v = []")
+apply(simp)
+apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)
+apply(simp)
+apply(auto)[1]
+apply(rule test)
+apply(simp)
+done
+
 lemma CPTpre_subsets:
   "CPTpre ZERO s = {}"
   "CPTpre ONE s \<subseteq> {Void}"
@@ -717,6 +703,7 @@
 apply(simp_all)
 apply(erule CPrf.cases)
 apply(simp_all)
+
 apply(erule CPrf.cases)
 apply(simp_all)
 apply(erule CPrf.cases)
@@ -845,13 +832,21 @@
 apply(rule CPT_CPTpre_subset)
 apply(rule CPTpre_finite)
 done
+*)
 
 lemma Posix_CPT:
   assumes "s \<in> r \<rightarrow> v"
   shows "v \<in> CPT r s"
 using assms
-by (induct rule: Posix.induct)
-   (auto simp add: CPT_def intro: CPrf.intros)
+apply(induct rule: Posix.induct)
+apply(auto simp add: CPT_def intro: CPrf.intros elim: CPrf.cases)
+apply(rotate_tac 5)
+apply(erule CPrf.cases)
+apply(simp_all)
+apply(rule CPrf.intros)
+apply(simp_all)
+done
+
 
 section {* The Posix Value is smaller than any other Value *}
 
@@ -866,14 +861,14 @@
   then have "v = Void"
     by (simp add: CPT_simps)
   then show "Void :\<sqsubseteq>val v"
-    by (simp add: PosOrd_ex1_def)
+    by (simp add: PosOrd_ex_eq_def)
 next
   case (Posix_CHAR c v)
   have "v \<in> CPT (CHAR c) [c]" by fact
   then have "v = Char c"
     by (simp add: CPT_simps)
   then show "Char c :\<sqsubseteq>val v"
-    by (simp add: PosOrd_ex1_def)
+    by (simp add: PosOrd_ex_eq_def)
 next
   case (Posix_ALT1 s r1 v r2 v2)
   have as1: "s \<in> r1 \<rightarrow> v" by fact
@@ -895,14 +890,14 @@
      have "flat v3 = flat v" using as1 Left(3)
        by (simp add: Posix1(2)) 
      ultimately have "Left v :\<sqsubseteq>val Left v3"
-       by (auto simp add: PosOrd_ex1_def PosOrd_LeftI)
+       by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq)
      then show "Left v :\<sqsubseteq>val v2" unfolding Left .
   next
      case (Right v3)
      have "flat v3 = flat v" using as1 Right(3)
        by (simp add: Posix1(2)) 
      then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1 
-       by (auto simp add: PosOrd_ex1_def PosOrd_Left_Right)
+       by (auto simp add: PosOrd_ex_eq_def PosOrd_Left_Right)
      then show "Left v :\<sqsubseteq>val v2" unfolding Right .
   qed
 next
@@ -927,7 +922,7 @@
      have "flat v3 = flat v" using as1 Right(3)
        by (simp add: Posix1(2)) 
      ultimately have "Right v :\<sqsubseteq>val Right v3" 
-        by (auto simp add: PosOrd_ex1_def PosOrd_RightI)
+        by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
      then show "Right v :\<sqsubseteq>val v2" unfolding Right .
   next
      case (Left v3)
@@ -961,7 +956,7 @@
     by (auto simp add: CPT_def)
   then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
   then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
-    unfolding  PosOrd_ex1_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) 
+    unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) 
   then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
 next 
   case (Posix_STAR1 s1 r v s2 vs v3) 
@@ -972,13 +967,20 @@
   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
   have cond2: "flat v \<noteq> []" by fact
   have "v3 \<in> CPT (STAR r) (s1 @ s2)" by fact
-  then consider
-    (NonEmpty) v3a vs3 where
-    "v3 = Stars (v3a # vs3)" "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
+  then consider 
+    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
+    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
     "flat (Stars (v3a # vs3)) = s1 @ s2"
   | (Empty) "v3 = Stars []"
-  by (force simp add: CPT_def elim: CPrf.cases)
-  then show "Stars (v # vs) :\<sqsubseteq>val v3"
+  unfolding CPT_def
+  apply(auto)
+  apply(erule CPrf.cases)
+  apply(simp_all)
+  apply(auto)[1]
+  apply(case_tac vs)
+  apply(auto)
+  using CPrf.intros(6) by blast
+  then show "Stars (v # vs) :\<sqsubseteq>val v3" (* HERE *)
     proof (cases)
       case (NonEmpty v3a vs3)
       have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
@@ -993,16 +995,16 @@
         using NonEmpty(2,3) by (auto simp add: CPT_def)
       then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
       then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
-         unfolding PosOrd_ex1_def by auto     
+         unfolding PosOrd_ex_eq_def by auto     
       then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
-        unfolding  PosOrd_ex1_def
+        unfolding  PosOrd_ex_eq_def
         by (metis PosOrd_StarsI PosOrd_StarsI2 flat.simps(7) val.inject(5))
       then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
     next 
       case Empty
       have "v3 = Stars []" by fact
       then show "Stars (v # vs) :\<sqsubseteq>val v3"
-      unfolding PosOrd_ex1_def using cond2
+      unfolding PosOrd_ex_eq_def using cond2
       by (simp add: PosOrd_shorterI)
     qed      
 next 
@@ -1011,7 +1013,7 @@
   then have "v2 = Stars []" 
     unfolding CPT_def by (auto elim: CPrf.cases) 
   then show "Stars [] :\<sqsubseteq>val v2"
-  by (simp add: PosOrd_ex1_def)
+  by (simp add: PosOrd_ex_eq_def)
 qed
 
 lemma Posix_PosOrd_stronger:
@@ -1030,7 +1032,7 @@
       then have "flat v2 \<sqsubset>spre flat v1" using assms(1)
         using Posix1(2) by blast
       then have "v1 :\<sqsubseteq>val v2"
-        by (simp add: PosOrd_ex1_def PosOrd_spreI) 
+        by (simp add: PosOrd_ex_eq_def PosOrd_spreI) 
     }
   ultimately show "v1 :\<sqsubseteq>val v2" by blast
 qed
@@ -1040,9 +1042,9 @@
   shows "\<not>(\<exists>v2 \<in> CPTpre r s. v2 :\<sqsubset>val v1)"
 using assms
 by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def 
-    PosOrd_ex1_def PosOrd_ex_def PosOrd_trans)
+    PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
 
-
+(*
 lemma PosOrd_Posix_Stars:
   assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v"
   and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
@@ -1115,12 +1117,93 @@
 apply(simp)
 apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def)
 by (metis PosOrd_StarsI PosOrd_ex_def PosOrd_spreI append_assoc append_self_conv flat.simps(7) flat_Stars prefix_list_def sprefix_list_def)
+*)
+
+
+lemma test2: 
+  assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
+  shows "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" 
+using assms
+apply(induct vs)
+apply(auto simp add: CPT_def)
+apply(rule CPrf.intros)
+apply(simp)
+apply(rule CPrf.intros)
+apply(simp_all)
+by (metis (no_types, lifting) CPT_def Posix_CPT mem_Collect_eq)
+
+
+lemma PosOrd_Posix_Stars:
+  assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
+  and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
+  shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" 
+using assms
+proof(induct vs)
+  case Nil
+  show "flat (Stars []) \<in> STAR r \<rightarrow> Stars []"
+    by(simp add: Posix.intros)
+next
+  case (Cons v vs)
+  have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []; 
+             \<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
+             \<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact
+  have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact
+  have as3: "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
+  have "flat v \<in> r \<rightarrow> v" using as2 by simp
+  moreover
+  have  "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
+    proof (rule IH)
+      show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp
+    next 
+      show "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3
+        apply(auto)
+        apply(subst (asm) (2) PT_def)
+        apply(auto)
+        apply(erule Prf.cases)
+        apply(simp_all)
+        apply(drule_tac x="Stars (v # vs)" in bspec)
+        apply(simp add: PT_def CPT_def)
+        using Posix1a Prf.intros(6) calculation
+        apply(rule_tac Prf.intros)
+        apply(simp add:)
+        apply (simp add: PosOrd_StarsI2)
+        done
+    qed
+  moreover
+  have "flat v \<noteq> []" using as2 by simp
+  moreover
+  have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" 
+   using as3
+   apply(auto)
+   apply(drule L_flat_Prf2)
+   apply(erule exE)
+   apply(simp only: L.simps[symmetric])
+   apply(drule L_flat_Prf2)
+   apply(erule exE)
+   apply(clarify)
+   apply(rotate_tac 5)
+   apply(erule Prf.cases)
+   apply(simp_all)
+   apply(clarify)
+   apply(drule_tac x="Stars (va#vs)" in bspec)
+   apply(auto simp add: PT_def)[1]   
+   apply(rule Prf.intros)
+   apply(simp)
+   by (simp add: PosOrd_StarsI PosOrd_shorterI)
+  ultimately show "flat (Stars (v # vs)) \<in> STAR r \<rightarrow> Stars (v # vs)"
+  by (simp add: Posix.intros)
+qed
+
 
 
 section {* The Smallest Value is indeed the Posix Value *}
 
+text {*
+  The next lemma seems to require PT instead of CPT in the Star-case.
+*}
+
 lemma PosOrd_Posix:
-  assumes "v1 \<in> CPT r s" "\<forall>v2 \<in> PT r s. \<not> v2 :\<sqsubset>val v1"
+  assumes "v1 \<in> CPT r s" "\<forall>v\<^sub>2 \<in> PT r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
   shows "s \<in> r \<rightarrow> v1" 
 using assms
 proof(induct r arbitrary: s v1)
@@ -1159,7 +1242,7 @@
        unfolding CPT_def Left by (auto elim: CPrf.cases)
      moreover
      have "\<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
-       unfolding PT_def Left using Prf.intros(2) PosOrd_LeftI by force  
+       unfolding PT_def Left using Prf.intros(2) PosOrd_Left_eq by force  
      ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
      then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
      then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
@@ -1248,10 +1331,7 @@
         "v1 = Stars vs" "s = flat (Stars vs)"
         "\<forall>v \<in> set vs. v \<in> CPT r (flat v)"
         unfolding CPT_def by (auto elim: CPrf.cases dest!: CPrf_stars)
-   have "Stars vs \<in> CPT (STAR r) (flat (Stars vs))" 
-     using as2 unfolding eqs .
-   moreover
-   have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v" 
+   have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" 
      proof 
         fix v
         assume a: "v \<in> set vs"
@@ -1266,7 +1346,7 @@
              assume "v2 \<in> PT r (flat v)"
              then have "Stars (pre @ [v2] @ post) \<in> PT (STAR r) s" 
                  using as2 unfolding e eqs
-                 apply(auto simp add: CPT_def PT_def intro!: Prf_Stars)[1]
+                 apply(auto simp add: CPT_def PT_def intro!: Prf.intros)[1]
                  using CPrf_Stars_appendE CPrf_stars Prf_CPrf apply blast
                  by (meson CPrf_Stars_appendE CPrf_stars Prf_CPrf list.set_intros(2))
              then have  "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
@@ -1276,8 +1356,8 @@
                 PosOrd_StarsI PosOrd_Stars_appendI by auto
           qed     
         with IH
-        show "flat v \<in> r \<rightarrow> v" using a as2 unfolding eqs
-          using eqs(3) by blast
+        show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs
+          using eqs(3) by (smt CPT_def CPrf_stars mem_Collect_eq) 
      qed
    moreover
    have "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" 
@@ -1289,12 +1369,6 @@
          apply(auto elim: Prf.cases)
          apply(erule Prf.cases)
          apply(auto intro: Prf.intros)
-         apply(drule_tac x="[]" in meta_spec) 
-         apply(simp)
-         apply(drule meta_mp)
-         apply(auto intro: Prf.intros)
-         apply(drule_tac x="(v#vsa)" in meta_spec)
-         apply(auto intro: Prf.intros)
          done
        then show "False" using as1 unfolding eqs
          apply -
@@ -1302,7 +1376,8 @@
          apply(auto simp add: PT_def)
          done
      qed
-   ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
+   ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
+     thm PosOrd_Posix_Stars
      by (rule PosOrd_Posix_Stars)
    then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
 qed
diff -r e2828c4a1e23 -r d36be1e356c0 thys/README
--- a/thys/README	Thu Jul 06 16:05:33 2017 +0100
+++ b/thys/README	Tue Jul 18 18:39:20 2017 +0100
@@ -12,10 +12,11 @@
 
   isabelle build -c -v -d . Journal
 
-Othe directories are:
+Other directories are:
 =====================
 
   Paper
+  Journal
   Literature