--- a/thys/Re.thy	Thu Sep 22 00:40:03 2016 +0100
+++ b/thys/Re.thy	Sat Oct 08 12:16:17 2016 +0100
@@ -5,7 +5,7 @@
 
 
 section {* Sequential Composition of Sets *}
-
+m
 definition
   Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 where 
@@ -1027,7 +1027,7 @@
 apply metis
 done
 
-section (* tryout with all-mkeps *)
+section {* tryout with all-mkeps *}
 
 fun 
   alleps :: "rexp \<Rightarrow> val set"
@@ -1038,12 +1038,21 @@
 | "alleps(SEQ r1 r2) = {Seq v1 v2 | v1 v2. v1 \<in> alleps r1 \<and> v2 \<in> alleps r2}"
 | "alleps(ALT r1 r2) = {Left v1 | v1. v1 \<in> alleps r1} \<union> {Right v2 | v2. v2 \<in> alleps r2}"
 
+fun injall :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val set"
+where
+  "injall (EMPTY) c Void = {}"
+| "injall (CHAR d) c Void = (if c = d then {Char d} else {})"
+| "injall (ALT r1 r2) c (Left v1) = {Left v | v. v \<in> injall r1 c v1}"
+| "injall (ALT r1 r2) c (Right v2) = {Right v | v. v \<in> injall r2 c v2}"
+| "injall (SEQ r1 r2) c (Seq v1 v2) = {Seq v v2 | v. v \<in> injall r1 c v1}"
+| "injall (SEQ r1 r2) c (Left (Seq v1 v2)) = {Seq v v2 | v. v \<in> injall r1 c v1}"
+| "injall (SEQ r1 r2) c (Right v2) = {Seq v v' | v v'. v \<in> alleps r1 \<and> v' \<in> injall r2 c v2}"
+
 fun 
   allvals :: "rexp \<Rightarrow> string \<Rightarrow> val set"
 where
   "allvals r [] = alleps r"
-| "allvals r (c#s) = {injval r c v | v. v \<in> allvals (der c r) s}"
-
+| "allvals r (c#s) = {v | v v'. v \<in> injall r c v' \<and> v' \<in> allvals (der c r) s}"
 
 lemma q1: 
   assumes "v \<in> alleps r"
@@ -1053,6 +1062,87 @@
 apply(auto intro: Prf.intros)
 done
 
+
+lemma allvals_NULL:
+  shows "allvals (NULL) s = {}"
+apply(induct_tac s)
+apply(simp)
+apply(simp)
+done
+
+lemma allvals_EMPTY:
+  shows "allvals (EMPTY) [] = {Void}"
+  and   "s \<noteq> [] \<Longrightarrow> allvals (EMPTY) s = {}"
+apply(simp)
+apply(case_tac s)
+apply(simp)
+apply(simp add: allvals_NULL)
+done
+
+lemma allvals_CHAR:
+  shows "allvals (CHAR c) [c] = {Char c}"
+  and   "s \<noteq> [c] \<Longrightarrow> allvals (CHAR c) s = {}"
+apply(simp)
+apply(case_tac s)
+apply(simp)
+apply(case_tac "c = a")
+apply(simp add: allvals_EMPTY)
+apply(simp add: allvals_NULL)
+done
+
+lemma allvals_ALT:
+  shows "allvals (ALT r1 r2) s = {Left v1 | v1. v1 \<in> allvals r1 s} \<union>
+                                 {Right v2 | v2. v2 \<in> allvals r2 s}"
+apply(induct s arbitrary: r1 r2)
+apply(simp)
+apply(simp)
+apply(auto)
+apply blast
+apply(rule_tac x="Left v'" in exI)
+apply(simp)
+apply(rule_tac x="Right v'" in exI)
+apply(simp)
+done
+
+lemma allvals_SEQ_Nil:
+  "allvals (SEQ r1 r2) [] = {Seq v1 v2 | v1 v2. v1 \<in> allvals r1 [] \<and> v2 \<in> allvals r2 []}"
+by simp
+
+lemma allvals_SEQ:
+  shows "allvals (SEQ r1 r2) s = {Seq v1 v2 | v1 v2 s1 s2. 
+      s = s1 @ s2 \<and> v1 \<in> allvals r1 s1 \<and> v2 \<in> allvals r2 s2}"
+using assms
+apply(induct s arbitrary: r1 r2)
+apply(simp)
+apply(simp)
+apply(auto)
+apply(simp_all add: allvals_ALT)
+apply(auto)
+apply (metis (mono_tags, lifting) allvals.simps(2) append_Cons mem_Collect_eq)
+apply fastforce
+prefer 2
+apply(rule_tac x="a#s1" in exI)
+apply(rule_tac x="s2" in exI)
+apply(simp)
+apply(fastforce)
+prefer 2
+apply(subst (asm) Cons_eq_append_conv)
+apply(auto)[1]
+using Prf_flat_L nullable_correctness q1 apply fastforce
+apply(rule_tac x="Seq v' v2" in exI)
+apply(simp)
+apply(rule_tac x="ys'" in exI)
+apply(rule_tac x="s2" in exI)
+apply(simp)
+apply(subst (asm) Cons_eq_append_conv)
+apply(auto)[1]
+apply(rule_tac x="Right v'" in exI)
+apply(simp)
+apply(rule_tac x="Left (Seq v' v2)" in exI)
+apply(simp)
+apply(auto)[1]
+done
+
 lemma q11:
   assumes "nullable r" "\<turnstile> v : r" "flat v = []"
   shows "v \<in> alleps r"
@@ -1081,10 +1171,81 @@
   assumes "nullable r"
   shows "alleps r = {v. \<turnstile> v : r \<and> flat v = []}"
 using assms
-apply(auto)
+apply(auto) 
 apply (simp_all add: q1)
 by (simp add: q11)
 
+
+lemma k0:
+  assumes "\<turnstile> v : der a r" "v' \<in> injall r a v"
+  shows "flat v' = a # flat v"
+using assms
+apply(induct a r arbitrary: v v' rule: der.induct)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(case_tac "c = c'")
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)[1]
+apply(auto)[1]
+apply(case_tac "nullable r1")
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+using q1 apply blast
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+done
+
+lemma k:
+  assumes "\<turnstile> v' : der a r" "v \<in> injall r a v'"
+  shows "\<turnstile> v : r"
+using assms
+apply(induct a r arbitrary: v v' rule: der.induct)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(case_tac "c = c'")
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto intro: Prf.intros)[1]
+apply(auto intro: Prf.intros)[1]
+apply(case_tac "nullable r1")
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+apply(auto intro: Prf.intros)[1]
+using Prf.intros(1) q1 apply blast
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+using Prf.intros(1) by auto
+
+
+
 lemma q22: 
   assumes "v \<in> allvals r s"
   shows "\<turnstile> v : r \<and> s \<in> L (r) \<and> flat v = s"
@@ -1093,154 +1254,213 @@
 apply(auto)
 apply(simp_all add: q1)
 using Prf_flat_L q1 apply fastforce
-apply (simp add: v3)
-apply (metis Prf_flat_L v3 v4)
-by (simp add: v4)
+apply(drule_tac x="v'" in meta_spec)
+apply(drule_tac x="der a r" in meta_spec)
+apply(simp)
+apply(clarify)
+apply(rule k)
+apply(assumption)
+apply(assumption)
+apply(drule_tac x="v'" in meta_spec)
+apply(drule_tac x="der a r" in meta_spec)
+apply(simp)
+apply(clarify)
+using Prf_flat_L v3 v4 apply fastforce
+apply(drule_tac x="v'" in meta_spec)
+apply(drule_tac x="der a r" in meta_spec)
+apply(simp)
+apply(clarify)
+using k0 by blast
 
-
-lemma qa_oops:
-  assumes "\<turnstile> v : r" "\<exists>s. flat v = a # s \<and> a # s \<in> L r" "\<turnstile> projval r a v : der a r"
-  shows "injval r a (projval r a v) = v"
+lemma ra:
+  assumes "v \<in> allvals r1 s"
+  shows "Left v \<in> allvals (ALT r1 r2) s"
 using assms
-apply(induct v r arbitrary: )
-defer
-defer
+apply(induct s arbitrary: r1 r2 v)
+apply(simp)
+apply(auto)
+apply(rule_tac x="Left v'" in exI)
 apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[4]
-apply(auto simp only:)
+done
+
+lemma rb:
+  assumes "v \<in> allvals r2 s"
+  shows "Right v \<in> allvals (ALT r1 r2) s"
+using assms
+apply(induct s arbitrary: r1 r2 v)
 apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-
+apply(auto)
+apply(rule_tac x="Right v'" in exI)
+apply(simp)
 done
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
+
+lemma r1:
+  assumes "v1 \<in> alleps r1" "v2 \<in> allvals r2 s2"
+  shows "Seq v1 v2 \<in> allvals (SEQ r1 r2) s2"
+using assms
+apply(induct s2 arbitrary: r1 r2 v1 v2)
+apply(simp)
+apply(simp)
+apply(auto)
+apply(rule_tac x="Right v'" in exI)
+apply(simp)
+apply(rule rb)
+apply(simp)
+using not_nullable_flat q1 by blast
+
+lemma r2:
+  assumes "v1 \<in> allvals r1 s1" "v2 \<in> allvals r2 s2"
+  shows "Seq v1 v2 \<in> allvals (SEQ r1 r2) (s1 @ s2)"
+using assms
+apply(induct s1 arbitrary: r1 r2 v1 v2 s2)
+apply(simp)
+apply(rule r1) 
+apply(simp)
+apply(simp)
+apply(simp)
 apply(auto)
-using Prf_flat_L apply fastforce
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-using Prf_flat_L apply force
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto)[1]
-apply(case_tac "nullable r1a")
+apply(drule_tac x="der a r1" in meta_spec)
+apply(drule_tac x="r2" in meta_spec)
+apply(drule_tac x="v'" in meta_spec)
+apply(drule_tac x="v2" in meta_spec)
+apply(drule_tac x="s2" in meta_spec)
+apply(simp)
+apply(rule_tac x="Left (Seq v' v2)" in exI)
+apply(simp)
+apply(rule ra)
+apply(simp)
+apply(drule_tac x="der a r1" in meta_spec)
+apply(drule_tac x="r2" in meta_spec)
+apply(drule_tac x="v'" in meta_spec)
+apply(drule_tac x="v2" in meta_spec)
+apply(drule_tac x="s2" in meta_spec)
+apply(simp)
+apply(rule_tac x="Seq v' v2" in exI)
 apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto simp add: Sequ_def)[1]
-apply(simp add: Cons_eq_append_conv)
-apply(auto)
+done
 
+lemma q22a: 
+  assumes " s \<in> L (r)"
+  shows "\<exists>v. v \<in> allvals r s \<and> flat v = s"
+using assms
+apply(induct r arbitrary: s)
+apply(auto)
+apply(simp add: Sequ_def)
+apply(auto)
+apply(drule_tac x="s1" in meta_spec) 
+apply(drule_tac x="s2" in meta_spec) 
+apply(auto)
+apply(rule_tac x="Seq v va" in exI)
+apply(simp)
+apply(rule r2)
+apply(simp)
+apply(simp)
+apply(drule_tac x="s" in meta_spec) 
+apply(simp)
+apply(auto)
+apply(rule_tac x="Left v" in exI)
+apply(simp)
+apply(rule ra)
+apply(simp)
+apply(drule_tac x="s" in meta_spec) 
+apply(drule_tac x="s" in meta_spec) 
+apply(simp)
+apply(auto)
+apply(rule_tac x="Right v" in exI)
+apply(simp)
+apply(rule rb)
+apply(simp)
+done
 
-using Prf_flat_L 
-apply(erule Prf.cases)
-apply(simp_all)
-using Prf_flat_L
+lemma q22b: 
+  assumes " s \<in> L (r)" "\<turnstile> v : r" "flat v = s"
+  shows "v \<in> allvals r s"
+using assms
+apply(induct r arbitrary: s v)
+apply(auto)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(simp add: Sequ_def)
-apply(auto)[1]
-apply(simp add: Cons_eq_append_conv)
-apply(auto)[1]
-sorry
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(simp add: append_eq_append_conv2)
+apply(auto)
+apply (metis Prf_flat_L append_assoc r2)
+apply (metis Prf_flat_L r2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto intro: ra rb)[2]
+apply(rule rb)
+apply (simp add: Prf_flat_L)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto intro: ra rb)[2]
+apply(rule ra)
+by (simp add: Prf_flat_L)
 
 
 lemma q2:
   assumes "s \<in> L(r)" 
   shows "allvals r s = {v. \<turnstile> v : r \<and> s \<in> L (r) \<and> flat v = s}"
 using assms
-apply(induct s arbitrary: r)
-apply(simp)
-apply(subst q33)
-using nullable_correctness apply blast
-apply(simp)
-apply(simp)
-apply(drule_tac x="der a r" in meta_spec)
-apply(drule meta_mp)
-using lex_correct1 lex_correct3 apply fastforce
-apply(simp)
 apply(auto)
-using v3 apply blast
-apply (simp add: v4)
-apply(rule_tac x="projval r a x" in exI)
+apply (simp add: q22)
+apply (simp add: q22)
+by (simp add: q22b)
+
+lemma r3a:
+  assumes "v' \<in> allvals (SEQ r1 r2) (s1 @ s2)" 
+          "(s1 @ s2) \<in> L (SEQ r1 r2)"
+  shows "\<exists>v1 v2. v' = Seq v1 v2 \<and> v1 \<in> allvals r1 s1 \<and> v2 \<in> allvals r2 s2" 
+using assms
+apply(subst (asm) q2)
+apply(auto)
+apply(erule_tac Prf.cases)
+apply(simp_all)
 apply(rule conjI)
-defer
-apply(rule conjI)
-apply (simp add: v3_proj)
-apply (simp add: v4_proj2)
-apply(subgoal_tac "projval r a x \<in>  allvals (der a r) s")
-apply(simp)
-apply(subst qa_oops)
-apply(simp)
-apply(blast)
-
-lemma q2: 
-  assumes "\<turnstile> v : r" "s \<in> L (r)" "flat v = s"
-  shows "v \<in> allvals r s"
-using assms
-apply(induct s arbitrary: r v)
+apply(simp add: append_eq_append_conv2)
 apply(auto)
-apply(subgoal_tac "nullable r")
-apply(simp add: q11)
-using not_nullable_flat apply fastforce
-apply(drule sym)
-apply(simp)
-apply(case_tac s)
-apply(simp)
+apply(subst q2)
+oops
 
-apply(drule_tac x="projval r a v" in meta_spec) 
-apply(drule_tac x="der a r" in meta_spec)
-apply(drule meta_mp)
-defer
-apply(drule meta_mp)
-using v3_proj apply blast
-apply(rule_tac x="projval r a v" in exI)
+lemma r3:
+  assumes "Seq v1 v2 \<in> allvals (SEQ r1 r2) (s1 @ s2)" 
+          "flat v1 = s1" "flat v2 = s2"
+          "(s1 @ s2) \<in> L (SEQ r1 r2)"
+  shows "v1 \<in> allvals r1 s1"  "v2 \<in> allvals r2 s2" 
+using assms
+apply(subst (asm) q2)
 apply(auto)
-defer
-apply(subst (asm) v4_proj2)
-apply(assumption)
-apply(assumption)
-apply(simp)
-apply(subst v4_proj2)
-apply(assumption)
-apply(assumption)
-apply(simp)
-apply(subst (asm) v4_proj2)
-apply(assumption)
-apply(assumption)
-sorry
-
-
-
-lemma
- "{v. \<turnstile> v : r \<and> flat v = s} = allvals r s"
+apply(erule_tac Prf.cases)
+apply(simp_all)
+apply(subst q2)
 apply(auto)
-apply(rule q2)
-apply(simp)
+using Prf_flat_L apply blast
+using Prf_flat_L apply blast
+using assms
+apply(subst (asm) q2)
+apply(auto)
+apply(erule_tac Prf.cases)
+apply(simp_all)
+apply(subst q2)
+apply(auto)
+using Prf_flat_L apply blast
+using Prf_flat_L apply blast
+done
 
 
 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> string \<Rightarrow> bool" 
 where
-  "POSIX2 v r s \<equiv> (\<turnstile> v : r \<and> (\<forall>v'\<in>allvals r s. v \<succ>r v'))"
+  "POSIX2 v r s \<equiv> (\<turnstile> v : r \<and> flat v = s \<and> (\<forall>v'\<in>allvals r s. v \<succ>r v'))"
+
+
+
 
 lemma k1:
+  assumes "nullable r"
   shows "POSIX2 v r [] \<Longrightarrow> \<forall>v' \<in> alleps r. v \<succ>r v'"
 using assms
 apply(induct r arbitrary: v)
@@ -1255,21 +1475,713 @@
 done
 
 lemma k2:
+  assumes "s \<in> L r"
   shows "POSIX2 v r s \<Longrightarrow> \<forall>v' \<in> allvals r s. v \<succ>r v'"
 using assms
 apply(induct s arbitrary: r v)
-apply(simp add: k1)
+apply(simp)
+apply(rule k1)
+apply (simp add: nullable_correctness)
+apply(simp)
+apply(simp)
 apply(auto)
 apply(simp only: POSIX2_def)
 apply(simp)
 apply(clarify)
-apply(drule_tac x="injval r a va" in spec)
+apply(drule_tac x="x" in spec)
 apply(drule mp)
-defer
+apply(auto)
+done
+
+lemma pos:
+  assumes "s \<in> r \<rightarrow> v" 
+  shows "v \<in> allvals r s"
+using assms
+apply(subst q2)
+using PMatch1(1) PMatch1(2) Prf_flat_L apply blast
+apply(simp)
+using PMatch1(1) PMatch1(2) Prf_flat_L by blast
+
+lemma mkeps_val:
+  assumes "nullable r"
+  shows "mkeps r \<in> alleps r"
+using assms
+apply(induct r)
+apply(auto)
+done
+
+lemma injval_injall:
+  assumes "\<turnstile> v : der a r"
+  shows "injval r a v \<in> injall r a v"
+using assms
+apply(induct a r arbitrary: v rule: der.induct)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)
+using mkeps_val apply blast
+apply(erule Prf.cases)
+apply(simp_all)
+done
+
+
+lemma mkeps_val1:
+  assumes "nullable r" "v \<succ>r mkeps r" "flat v = []" "\<turnstile> v : r"
+  shows "v = mkeps r"
+using assms
+apply(induct r arbitrary: v)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(auto)
+apply(erule Prf.cases)
+apply(auto)
+apply(erule Prf.cases)
+apply(auto)
+apply(erule Prf.cases)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(auto)
+apply(erule Prf.cases)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(auto)
+apply(erule Prf.cases)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(auto)
+apply (simp add: not_nullable_flat)
+apply(erule ValOrd.cases)
 apply(auto)
 done
+
+lemma sulzmann_our:
+  assumes "v \<in> alleps r" "nullable r"
+  shows "mkeps r \<succ>r v"
+using assms
+apply(induct r arbitrary: v)
+apply(simp_all)
+apply(rule ValOrd.intros)
+apply(auto)[1]
+apply(case_tac "mkeps r1 = v1")
+apply(simp)
+apply(rule ValOrd.intros)
+apply(blast)
+apply(rule ValOrd.intros)
+apply(blast)
+apply(simp)
+apply(auto)
+apply(rule ValOrd.intros)
+apply(blast)
+apply(rule ValOrd.intros)
+apply(blast)
+apply(rule ValOrd.intros)
+using not_nullable_flat q1 apply blast
+apply(rule ValOrd.intros)
+using q1 apply auto[1]
+apply(rule ValOrd.intros)
+apply (simp add: q1)
+apply(rule ValOrd.intros)
+apply(blast)
 done
 
+lemma destruct:
+  assumes "\<forall>s3. s1 @ s3 \<in> L r1 \<longrightarrow> s3 = [] \<or> (\<forall>s4. s3 @ s4 = s2 \<longrightarrow> s4 \<notin> L r2)"
+  and "s1 \<in> L r1" "s2 \<in> L r2" "(s1' @ s2') \<sqsubseteq> (s1 @ s2)"
+  and "s1'@ s2' \<in> L (SEQ r1 r2)"  "s1' \<in> L r1"
+  shows "s1' \<sqsubseteq> s1"
+using assms
+apply(simp add: prefix_def)
+apply(auto)
+apply(simp add: append_eq_append_conv2)
+apply(auto)
+apply(simp add: Sequ_def)
+apply(auto)
+apply(drule_tac x="us" in spec)
+apply(simp)
+apply(auto)
+apply(simp add: append_eq_append_conv2)
+apply(auto)
+oops
+
+lemma inj_ord:
+  assumes "v1 \<succ>(der a r) v2" "s \<in> (der a r) \<rightarrow> v1" "s' \<in> L (der a r)" 
+          "v1 \<in> allvals (der a r) s" "v2 \<in> allvals (der a r) s'" "s' \<sqsubseteq> s" 
+  shows "injval r a v1 \<succ>r injval r a v2"
+using assms
+apply(induct a r arbitrary: s s' v1 v2 rule: der.induct)
+apply(simp_all)
+(*apply(simp add: allvals_NULL)
+apply(simp add: allvals_NULL)*)
+apply(case_tac "c = c'")
+apply(simp)
+apply(case_tac "s = []")
+apply(subgoal_tac "s' = []")
+prefer 2
+using allvals_EMPTY(2) apply blast
+apply(simp add: allvals_EMPTY)
+apply(rule ValOrd.intros)
+apply(simp add: allvals_EMPTY)
+apply(simp)
+(*apply(simp add: allvals_NULL)*)
+(* ALT case *)
+apply(simp add: allvals_ALT)
+apply(auto)[1]
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(rule ValOrd.intros)
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(rule ValOrd.intros)
+apply(subst v4)
+apply(simp)
+apply (simp add: q22)
+apply(subst v4)
+apply(simp)
+apply (simp add: q22)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(rule ValOrd.intros)
+apply(subst v4)
+apply (simp add: q22)
+apply(subst v4)
+apply (simp add: q22)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(rule ValOrd.intros)
+apply(erule PMatch.cases)
+apply(simp_all)
+using q22 apply auto[1]
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(rule ValOrd.intros)
+using q22 apply auto[1]
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(rule ValOrd.intros)
+apply(subst v4)
+apply (simp add: q22)
+apply(subst v4)
+apply (simp add: q22)
+apply(simp)
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(rule ValOrd.intros)
+apply(subst v4)
+apply (simp add: q22)
+apply(subst v4)
+apply (simp add: q22)
+apply(simp)
+using q22 apply auto[1]
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(rule ValOrd.intros)
+using q22 apply auto[1]
+(* seq case *)
+apply(case_tac "nullable r1")
+apply(simp)
+prefer 2
+apply(simp)
+apply(simp add: allvals_SEQ)
+apply(auto)[1]
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(simp)
+apply(rule ValOrd.intros)
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(clarify)
+apply(rotate_tac 1)
+apply(drule_tac x="s1b" in meta_spec)
+apply(rotate_tac 13)
+apply(drule_tac x="s1a" in meta_spec)
+apply(drule_tac x="v1c" in meta_spec)
+apply(drule_tac x="v1'" in meta_spec)
+apply(simp)
+apply(subgoal_tac "s1 = s1b")
+prefer 2
+apply (metis PMatch1(2) q22)
+apply(simp)
+apply(clarify)
+apply(drule destruct)
+apply (metis PMatch1(2) q22)
+apply (metis PMatch1(2) q22)
+apply(assumption)
+apply (metis PMatch1(2) q22)
+apply (metis PMatch1(2) q22)
+apply(subgoal_tac "s2a = s2b")
+prefer 2
+apply (metis PMatch1(2) q22)
+apply(drule destruct)
+apply (metis PMatch1(2) q22)
+apply (metis PMatch1(2) q22)
+apply(assumption)
+back
+apply (metis PMatch1(2) q22)
+apply (metis PMatch1(2) q22)
+
+
+
+apply(simp add: allvals_ALT)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(blast)
+apply(rule ValOrd.intros)
+apply(clarify)
+apply(simp add: allvals_SEQ)
+apply(auto)[1]
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(auto)
+apply(drule_tac x="s1b" in meta_spec)
+apply(drule_tac x="v1" in meta_spec)
+apply(drule_tac x="v1'a" in meta_spec)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(subgoal_tac "s1 = s1b")
+apply(simp)
+apply (metis PMatch1(2) q22)
+apply(drule_tac meta_mp)
+apply(subgoal_tac "s1a = s1b")
+apply(simp)
+apply(simp add: append_eq_append_conv2)
+apply(auto)[1]
+apply(subgoal_tac "s2 = s2a")
+apply(simp)
+apply(clarify)
+prefer 2
+using q22 apply blast
+using q22 apply blast
+using q22 apply blast
+apply(subgoal_tac "usa = []")
+apply(simp)
+prefer 2
+using q22 apply blast
+prefer 3
+apply(simp)
+prefer 4
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(clarify)
+apply(simp)
+prefer 5
+apply(erule PMatch.cases)
+apply(simp_all)
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(clarify)
+apply(simp add: allvals_SEQ)
+apply(auto)[1]
+apply (simp add: q22)
+apply(simp add: allvals_SEQ)
+apply(auto)[1]
+apply(simp add: append_eq_append_conv2)
+apply(auto)[1]
+apply (simp add: q22)
+thm PMatch2
+apply(drule PMatch2)
+
+
+lemma sulzmann_our:
+  assumes "\<forall>v' \<in> allvals r s. v \<succ>r v'" "s \<in> L r" "\<turnstile> v : r" "flat v = s"
+  shows "s \<in> r \<rightarrow> v"
+using assms
+apply(induct s arbitrary: r v)
+apply(simp_all)
+apply(subst (asm) q33)
+apply (simp add: nullable_correctness)
+apply(simp)
+apply(drule_tac x="mkeps r" in spec)
+apply(drule mp)
+apply(rule conjI)
+using mkeps_val not_nullable_flat q1 apply blast
+using mkeps_flat not_nullable_flat apply blast
+apply(subgoal_tac "nullable r")
+apply(drule mkeps_val1)
+apply(assumption)
+apply(simp)
+apply(simp)
+apply(simp)
+using PMatch_mkeps not_nullable_flat apply blast
+using not_nullable_flat apply blast
+apply(drule_tac x="der a r" in meta_spec)
+apply(drule_tac x="projval r a v" in meta_spec)
+apply(drule meta_mp)
+defer
+apply(drule meta_mp)
+using Prf_flat_L v3_proj v4_proj2 apply blast
+apply(drule meta_mp)
+using v3_proj apply blast
+apply(drule meta_mp)
+apply (simp add: v4_proj2)
+defer
+apply(rule ballI)
+apply(drule_tac x="injval r a x" in spec)
+apply(auto)
+apply(drule_tac x="x" in spec)
+apply(drule mp)
+apply(rule injval_injall)
+using q22 apply blast
+apply(simp)
+(* HERE *)
+
+
+lemma our_sulzmann:
+  assumes "s \<in> r \<rightarrow> v" "v' \<in> allvals r s"
+  shows "v \<succ>r v'"
+using assms
+apply(induct r arbitrary: s v v')
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+(* SEQ - case *)
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(subst (asm) (3) q2)
+apply(simp add: Sequ_def)
+apply(rule_tac x="s1" in exI)
+apply(rule_tac x="s2" in exI)
+apply(simp)
+apply(rule conjI)
+using PMatch1(1) PMatch1(2) Prf_flat_L apply fastforce
+apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+apply(simp)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(case_tac "v1 = v1a")
+apply(simp)
+apply(rule ValOrd.intros)
+apply(rotate_tac 1)
+apply(drule_tac x="s2" in meta_spec)
+apply(drule_tac x="v2" in meta_spec)
+apply(drule_tac x="v2a" in meta_spec)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(subst q2)
+using PMatch1(1) PMatch1(2) Prf_flat_L apply fastforce
+apply(simp)
+apply(rule conjI)
+using PMatch1(1) PMatch1(2) Prf_flat_L apply fastforce
+apply (simp add: PMatch1(2))
+apply(simp)
+apply(rule ValOrd.intros)
+prefer 2
+apply(simp)
+apply(drule_tac x="s1" in meta_spec)
+apply(drule_tac x="v1" in meta_spec)
+apply(drule_tac x="v1a" in meta_spec)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(subst q2)
+apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+apply(simp)
+apply(rule conjI)
+apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+apply(subst (asm) append_eq_append_conv2)
+apply(auto)[1]
+using Prf_flat_L apply fastforce
+
+apply(drule_tac x="us" in spec)
+apply(auto)[1]
+
+using Prf_flat_L apply fastforce
+using Prf_flat_L apply blast
+apply(drule_tac meta_mp)
+apply(subst q2)
+using Prf_flat_L apply fastforce
+apply(simp)
+using Prf_flat_L apply fastforce
+apply(simp)
+apply(drule_tac x="flat v1a" in meta_spec)
+apply(drule_tac x="v1" in meta_spec)
+apply(drule_tac x="v1a" in meta_spec)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(drule meta_mp)
+apply(subst q2)
+apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+apply(simp)
+apply(rule conjI)
+apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+apply(drule_tac x="[]" in spec)
+apply(auto)[1]
+
+using Prf_flat_L apply fast
+apply(drule_tac x="us" in spec)
+apply(simp)
+
+apply (simp add: Prf_flat_L)
+apply(simp)
+thm PMatch1
+qed
+done
+using PMatch1(1) PMatch1(2) Prf_flat_L apply fastforce
+apply(simp)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule ValOrd.intros)
+apply(drule_tac x="v1" in meta_spec)
+apply(drule meta_mp)
+apply(subst q2)
+apply (simp add: Prf_flat_L)
+apply(simp)
+apply (simp add: Prf_flat_L)
+apply(simp)
+apply(rule ValOrd.intros)
+apply(auto)[1]
+apply (simp add: PMatch1(2))
+apply (simp add: PMatch1(2))
+apply(subst (asm) (2) q2)
+using PMatch1(1) PMatch1(2) Prf_flat_L apply fastforce
+apply(simp)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)
+prefer 2
+apply(rule ValOrd.intros)
+using q22b apply blast
+apply(rule ValOrd.intros)
+apply(auto)
+using Prf_flat_L apply blast
+apply(subst (asm) (3) q2)
+apply(simp add: Sequ_def)
+apply(rule_tac x="s1" in exI)
+apply(rule_tac x="s2" in exI)
+apply(simp)
+using PMatch1(1) PMatch1(2) Prf_flat_L apply fastforce
+apply(simp)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto simp add: Sequ_def)[1]
+apply(case_tac "v1 = v1a")
+apply(simp)
+apply(rule ValOrd.intros)
+apply(rotate_tac 3)
+apply(drule_tac x="v2a" in meta_spec)
+apply(drule_tac meta_mp)
+apply(subst q2)
+using PMatch1(1) PMatch1(2) Prf_flat_L apply fastforce
+apply(simp)
+apply(rule conjI)
+using PMatch1(1) PMatch1(2) Prf_flat_L apply fastforce
+apply (metis PMatch1(2) same_append_eq)
+apply(simp)
+apply(rule ValOrd.intros)
+apply(drule_tac x="v1a" in meta_spec)
+apply(drule_tac meta_mp)
+apply(subst q2)
+using PMatch1(1) PMatch1(2) Prf_flat_L apply fastforce
+apply(simp)
+apply(rule conjI)
+using PMatch1(1) PMatch1(2) Prf_flat_L apply fastforce
+prefer 2
+apply(simp)
+prefer 2
+apply(simp)
+apply(rotate_tac 7)
+apply(drule sym)
+apply(simp)
+apply(subst (asm) (2) append_eq_append_conv2)
+apply(auto)[1]
+apply(frule_tac x="us" in spec)
+apply(auto)[1]
+prefer 2
+apply(drule_tac x="flat v2a" in spec)
+apply(auto)[1]
+
+apply(subgoal_tac "flat v2a = s2")
+apply(simp)
+
+apply(simp add: append_eq_append_conv2)
+apply(auto)
+prefer 2
+apply blast
+prefer 2
+apply (metis Prf_flat_L append_self_conv2)
+prefer 4
+
+
+
+lemma our_sulzmann:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "POSIX2 v r s"
+using assms
+apply(induct s r v)
+apply(auto)
+apply(simp add: POSIX2_def)
+using Prf.intros(4) ValOrd.intros(7) apply blast
+apply(simp add: POSIX2_def)
+apply (simp add: Prf.intros(5) ValOrd.intros(8))
+apply(simp add: POSIX2_def)
+apply(auto)
+apply(rule Prf.intros)
+apply(simp)
+apply(subgoal_tac "(\<exists>x1. x = Left x1) \<or> (\<exists>x1. x = Right x1)")
+apply(auto)[1]
+apply(rule ValOrd.intros)
+apply(drule_tac x="x1" in bspec)
+apply(subst (asm) q2)
+apply (simp add: Prf_flat_L)
+apply(simp)
+apply(subst q2)
+apply (simp add: Prf_flat_L)
+apply(auto)[1]
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply (simp add: Prf_flat_L)
+apply(rule ValOrd.intros)
+apply(subst (asm) (2) q2)
+apply (simp add: Prf_flat_L)
+apply(auto)[1]
+defer
+apply(simp add: POSIX2_def)
+apply(auto)[1]
+apply(rule Prf.intros)
+apply (simp add: Prf_flat_L)
+apply(subgoal_tac "(\<exists>x1. x = Left x1) \<or> (\<exists>x1. x = Right x1)")
+apply(auto)[1]
+apply(rule ValOrd.intros)
+apply(subst (asm) (2) q2)
+apply (simp add: Prf_flat_L)
+apply(auto)[1]
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)[1]
+using Prf_flat_L apply force
+apply(rule ValOrd.intros)
+apply(drule_tac x="x1" in bspec)
+apply(subst (asm) q2)
+apply (simp add: Prf_flat_L)
+apply(auto)[1]
+apply(subst q2)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+defer
+apply(auto)[1]
+apply(simp add: POSIX2_def)
+apply(auto intro: Prf.intros)[1]
+apply(subgoal_tac "(\<exists>x1 x2. x = Seq x1 x2 \<and> flat v1 @ flat v2 = flat x1 @ flat x2)")
+apply(auto)[1]
+apply(case_tac "v1 = x1")
+apply(simp)
+apply(rule ValOrd.intros)
+apply(rotate_tac 6)
+apply(drule_tac x="x2" in bspec)
+apply(subst (asm) q2)
+apply (simp add: Sequ_def Prf_flat_L)
+
+using Prf_flat_L apply blast
+apply(auto)[1]
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(subst q2)
+apply (simp add: Prf_flat_L)
+apply(auto)[1]
+apply(auto simp add: Sequ_def)
+using Prf_flat_L apply blast
+apply(rule ValOrd.intros)
+apply(rotate_tac 5)
+apply(drule_tac x="x1" in bspec)
+apply(rotate_tac 1)
+apply(subst (asm) q2)
+apply (simp add: Sequ_def Prf_flat_L)
+using Prf_flat_L apply blast
+apply(auto)[1]
+apply(subst q2)
+apply (simp add: Sequ_def Prf_flat_L)
+apply(auto)[1]
+apply(rotate_tac 7)
+apply(erule Prf.cases)
+apply(simp_all)
+apply (simp add: Sequ_def Prf_flat_L)
+apply(rotate_tac 7)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)[1]
+apply(simp add: append_eq_append_conv2)
+apply(auto simp add: Sequ_def)[1]
+using Prf_flat_L apply fastforce
+apply(simp add: append_eq_append_conv2)
+apply(auto simp add: Sequ_def)[1]
+
+apply(auto)[1]
+
+apply(simp add: POSIX2_def)
+apply(simp add: POSIX2_def)
+apply(simp add: POSIX2_def)
+apply(simp add: POSIX2_def)
+apply(simp add: POSIX2_def)
+
 lemma "s \<in> L(r) \<Longrightarrow> \<exists>v. POSIX2 v r s"
 apply(induct r arbitrary: s)
 apply(auto)
@@ -1286,6 +2198,7 @@
 apply(simp add: POSIX2_def)
 apply(auto)[1]
 using Prf.intros(2) apply blast
+
 apply(case_tac s)
 apply(simp)
 apply(auto)[1]