diff -r 7f4f8c34da95 -r 7f589bfecffa thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Wed Feb 10 17:38:29 2016 +0000
+++ b/thys/Paper/Paper.thy	Sat Feb 13 02:00:09 2016 +0000
@@ -15,6 +15,7 @@
   flat ("|_|" [70] 73) and
   Sequ ("_ @ _" [78,77] 63) and
   injval ("inj _ _ _" [1000,77,1000] 77) and 
+  projval ("proj _ _ _" [1000,77,1000] 77) and 
   length ("len _" [78] 73) and
   ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73)
 (*>*)
@@ -257,6 +258,75 @@
   @{thm[mode=IfThen] PMatch2}
 
   \mbox{}\bigskip
+  
+  \noindent {\bf Proof} The proof is by induction on the definition of
+  @{const der}. Other inductions would go through as well. The
+  interesting case is for @{term "SEQ r\<^sub>1 r\<^sub>2"}. First we analyse the
+  case where @{term "nullable r\<^sub>1"}. We have by induction hypothesis
+
+  \[
+  \begin{array}{l}
+  (IH1)\quad @{text "\<forall>s v."} \text{\;if\;} @{term "s \<in> der c r\<^sub>1 \<rightarrow> v"} 
+  \text{\;then\;} @{term "(c # s) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v"}\\
+  (IH2)\quad @{text "\<forall>s v."} \text{\;if\;} @{term "s \<in> der c r\<^sub>2 \<rightarrow> v"} 
+  \text{\;then\;} @{term "(c # s) \<in> r\<^sub>2 \<rightarrow> injval r\<^sub>2 c v"}
+  \end{array}
+  \]
+  
+  \noindent
+  and have 
+
+  \[
+  @{term "s \<in> ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2) \<rightarrow> v"}
+  \]
+  
+  \noindent
+  There are two cases what @{term v} can be: (1) @{term "Left v'"} and (2) @{term "Right v'"}.
+
+  \begin{itemize}
+  \item[(1)] We know @{term "s \<in> SEQ (der c r\<^sub>1) r\<^sub>2 \<rightarrow> v'"} holds, from which we
+  can infer that there are @{text "s\<^sub>1"}, @{term "s\<^sub>2"}, @{text "v\<^sub>1"}, @{term "v\<^sub>2"}
+  with
+
+  \[
+  @{term "s\<^sub>1 \<in> der c r\<^sub>1 \<rightarrow> v\<^sub>1"} \qquad\text{and}\qquad @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"}
+  \]
+
+  and also
+
+  \[
+  @{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) \<and> s\<^sub>4 \<in> L r\<^sub>2)"}
+  \]
+
+  \noindent
+  and have to prove
+  
+  \[
+  @{term "((c # s\<^sub>1) @ s\<^sub>2) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (injval r\<^sub>1 c v\<^sub>1) v\<^sub>2"}
+  \]
+
+  \noindent
+  The two requirements @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"} and 
+  @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} can be proved by the induction hypothese (IH1) and the
+  fact above.
+
+  \noindent
+  This leaves to prove
+  
+  \[
+  @{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> (c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}
+  \]
+  
+  \noindent
+  which holds because @{term "(c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 "} implies @{term "s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) "}
+
+  \item[(2)] This case is similar except that in the last step we have to
+  instantiate the existential quantifier with @{term "Seq (projval r\<^sub>1 c v) v'"}
+  \end{itemize}
+
+  \noindent 
+  The final case is that @{term " \<not> nullable r\<^sub>1"} holds. This case again similar
+  to the cases above.
 *}
 
 text {*