# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1455328809 0
# Node ID 7f589bfecffadb1ef359a3efae9d5bc941a6a9e8
# Parent  7f4f8c34da958d7e24a388ac24dad49d08952116
updated

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 {*
diff -r 7f4f8c34da95 -r 7f589bfecffa thys/ReStar.thy
--- a/thys/ReStar.thy	Wed Feb 10 17:38:29 2016 +0000
+++ b/thys/ReStar.thy	Sat Feb 13 02:00:09 2016 +0000
@@ -1165,6 +1165,21 @@
     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
 | "[] \<in> STAR r \<rightarrow> Stars []"
 
+inductive 
+  PMatchX :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("\<turnstile> _ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
+where
+  "\<turnstile> s \<in> EMPTY \<rightarrow> Void"
+| "\<turnstile> (c # s) \<in> (CHAR c) \<rightarrow> (Char c)"
+| "\<turnstile> s \<in> r1 \<rightarrow> v \<Longrightarrow> \<turnstile> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
+| "\<lbrakk>\<turnstile> s \<in> r2 \<rightarrow> v; \<not>(\<exists>s'. s' \<sqsubseteq> s \<and> flat v \<sqsubseteq> s' \<and> s' \<in> L(r1))\<rbrakk> \<Longrightarrow> \<turnstile> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
+| "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; \<turnstile> s2 \<in> r2 \<rightarrow> v2;
+    \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> (s3 @ s4) \<sqsubseteq> s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
+    \<turnstile> (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
+| "\<lbrakk>s1 \<in> r \<rightarrow> v; \<turnstile> s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
+    \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> (s\<^sub>3 @ s\<^sub>4) \<sqsubseteq> s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
+    \<Longrightarrow> \<turnstile> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
+| "\<turnstile> s \<in> STAR r \<rightarrow> Stars []"
+
 lemma PMatch1:
   assumes "s \<in> r \<rightarrow> v"
   shows "\<turnstile> v : r" "flat v = s"
@@ -1180,6 +1195,53 @@
 by (metis Prf.intros(6))
 
 
+lemma PMatchX1:
+  assumes "\<turnstile> s \<in> r \<rightarrow> v"
+  shows "\<turnstile> v : r"
+using assms
+apply(induct s r v rule: PMatchX.induct)
+apply(auto simp add: prefix_def intro: Prf.intros)
+apply (metis PMatch1(1) Prf.intros(1))
+by (metis PMatch1(1) Prf.intros(7))
+
+
+lemma PMatchX:
+  assumes "\<turnstile> s \<in> r \<rightarrow> v"
+  shows "flat v \<sqsubseteq> s"
+using assms
+apply(induct s r v rule: PMatchX.induct)
+apply(auto simp add: prefix_def PMatch1)
+done
+
+lemma PMatchX_PMatch:
+  assumes "\<turnstile> s \<in> r \<rightarrow> v" "flat v = s"
+  shows "s \<in> r \<rightarrow> v"
+using assms
+apply(induct s r v rule: PMatchX.induct)
+apply(auto intro: PMatch.intros)
+apply(rule PMatch.intros)
+apply(simp)
+apply (metis PMatchX Prefixes_def mem_Collect_eq)
+apply (smt2 PMatch.intros(5) PMatch1(2) PMatchX append_Nil2 append_assoc append_self_conv prefix_def)
+by (metis L.simps(6) PMatch.intros(6) PMatch1(2) append_Nil2 append_eq_conv_conj prefix_def)
+
+lemma PMatch_PMatchX:
+  assumes "s \<in> r \<rightarrow> v" 
+  shows "\<turnstile> s \<in> r \<rightarrow> v"
+using assms
+apply(induct s r v arbitrary: s' rule: PMatch.induct)
+apply(auto intro: PMatchX.intros)
+apply(rule PMatchX.intros)
+apply(simp)
+apply(rule notI)
+apply(auto)[1]
+apply (metis PMatch1(2) append_eq_conv_conj length_sprefix less_imp_le_nat prefix_def sprefix_def take_all)
+apply(rule PMatchX.intros)
+apply(simp)
+apply(simp)
+apply(auto)[1]
+oops
+
 lemma 
   assumes "\<rhd> v : r"
   shows "(flat v) \<in> r \<rightarrow> v"
@@ -1410,23 +1472,28 @@
 apply(simp_all)[7]
 apply(clarify)
 apply(erule PMatch.cases)
-apply(simp_all)[7]
+apply(simp_all)[4]
 apply(clarify)
+apply(simp (no_asm))
 apply(subst append.simps(2)[symmetric])
 apply(rule PMatch.intros)
 apply metis
 apply metis
+apply(erule contrapos_nn)
+apply(erule exE)+
 apply(auto)[1]
 apply(simp add: L_flat_NPrf)
 apply(auto)[1]
+thm v3_proj
 apply(frule_tac c="c" in v3_proj)
 apply metis
-apply(drule_tac x="s\<^sub>3" in spec)
-apply(drule mp)
+apply(rule_tac x="s\<^sub>3" in exI)
+apply(simp)
 apply (metis NPrf_imp_Prf v4_proj2)
 apply(simp)
 (* interesting case *)
 apply(clarify)
+apply(clarify)
 apply(simp)
 apply(subst (asm) L.simps(4)[symmetric])
 apply(simp only: L_flat_Prf)
@@ -1692,6 +1759,21 @@
 | "(Stars vs1) 2\<succ>s (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) 2\<succ>(flat v @ s) (Stars (v # vs2))"
 | "(Stars []) 2\<succ>[] (Stars [])"
 
+lemma admissibility:
+  assumes "\<turnstile> s \<in> r \<rightarrow> v" "\<turnstile> v' : r" 
+  shows "v \<succ>r v'"
+using assms
+apply(induct arbitrary: v')
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis ValOrd.intros(7))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis ValOrd.intros(8))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis ValOrd.intros(6))
+oops
 
 lemma admissibility:
   assumes "2\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
diff -r 7f4f8c34da95 -r 7f589bfecffa thys/paper.pdf
Binary file thys/paper.pdf has changed