--- 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"