diff -r 8b919b3d753e -r 7f4f8c34da95 thys/ReStar.thy
--- a/thys/ReStar.thy	Mon Feb 08 15:51:23 2016 +0000
+++ b/thys/ReStar.thy	Wed Feb 10 17:38:29 2016 +0000
@@ -32,6 +32,11 @@
 where
   "Der c A \<equiv> {s. [c] @ s \<in> A}"
 
+definition 
+  Ders :: "string \<Rightarrow> string set \<Rightarrow> string set"
+where  
+  "Ders s A \<equiv> {s' | s'. s @ s' \<in> A}"
+
 lemma Der_null [simp]:
   shows "Der c {} = {}"
 unfolding Der_def
@@ -809,13 +814,20 @@
 apply(simp_all add: nullable_correctness)
 done
 
+lemma ders_correctness:
+  shows "L (ders s r) = Ders s (L r)"
+apply(induct s arbitrary: r) 
+apply(simp add: Ders_def)
+apply(simp)
+apply(subst der_correctness)
+apply(simp add: Ders_def Der_def)
+done
+
 section {* Injection function *}
 
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 where
-  "injval (EMPTY) c Void = Char c"
-| "injval (CHAR d) c Void = Char d"
-| "injval (CHAR d) c (Char c') = Seq (Char d) (Char c')"
+  "injval (CHAR d) c Void = Char d"
 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
@@ -869,6 +881,7 @@
 apply(auto)
 done
 
+
 lemma v3:
   assumes "\<turnstile> v : der c r" 
   shows "\<turnstile> (injval r c v) : r"
@@ -1028,6 +1041,113 @@
 by (metis list.inject v4_proj)
 
 
+section {* Roy's Definition *}
+
+inductive 
+  Roy :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<rhd> _ : _" [100, 100] 100)
+where
+  "\<rhd> Void : EMPTY"
+| "\<rhd> Char c : CHAR c"
+| "\<rhd> v : r1 \<Longrightarrow> \<rhd> Left v : ALT r1 r2"
+| "\<lbrakk>\<rhd> v : r2; flat v \<notin> L r1\<rbrakk> \<Longrightarrow> \<rhd> Right v : ALT r1 r2"
+| "\<lbrakk>\<rhd> v1 : r1; \<rhd> v2 : r2; \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow>
+      \<rhd> Seq v1 v2 : SEQ r1 r2"
+| "\<lbrakk>\<rhd> v : r; \<rhd> Stars vs : STAR r; flat v \<noteq> []; 
+   \<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))\<rbrakk> \<Longrightarrow>
+      \<rhd> Stars (v#vs) : STAR r"
+| "\<rhd> Stars [] : STAR r"
+
+lemma drop_append:
+  assumes "s1 \<sqsubseteq> s2"
+  shows "s1 @ drop (length s1) s2 = s2"
+using assms
+apply(simp add: prefix_def)
+apply(auto)
+done
+
+lemma royA: 
+  assumes "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
+  shows "\<forall>s. (s \<in> L(ders (flat v1) r1) \<and> 
+              s \<sqsubseteq> (flat v2) \<and> drop (length s) (flat v2) \<in> L r2 \<longrightarrow> s = [])" 
+using assms
+apply -
+apply(rule allI)
+apply(rule impI)
+apply(simp add: ders_correctness)
+apply(simp add: Ders_def)
+thm rest_def
+apply(drule_tac x="s" in spec)
+apply(simp)
+apply(erule disjE)
+apply(simp)
+apply(drule_tac x="drop (length s) (flat v2)" in spec)
+apply(simp add: drop_append)
+done
+
+lemma royB:
+  assumes "\<forall>s. (s \<in> L(ders (flat v1) r1) \<and> 
+              s \<sqsubseteq> (flat v2) \<and> drop (length s) (flat v2) \<in> L r2 \<longrightarrow> s = [])"
+  shows "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" 
+using assms
+apply -
+apply(auto simp add: prefix_def ders_correctness Ders_def)
+by (metis append_eq_conv_conj)
+
+lemma royC: 
+  assumes "\<forall>s t. (s \<in> L(ders (flat v1) r1) \<and> 
+                s \<sqsubseteq> (flat v2 @ t) \<and> drop (length s) (flat v2 @ t) \<in> L r2 \<longrightarrow> s = [])" 
+  shows "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
+using assms
+apply -
+apply(rule royB)
+apply(rule allI)
+apply(drule_tac x="s" in spec)
+apply(drule_tac x="[]" in spec)
+apply(simp)
+done
+
+inductive 
+  Roy2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("2\<rhd> _ : _" [100, 100] 100)
+where
+  "2\<rhd> Void : EMPTY"
+| "2\<rhd> Char c : CHAR c"
+| "2\<rhd> v : r1 \<Longrightarrow> 2\<rhd> Left v : ALT r1 r2"
+| "\<lbrakk>2\<rhd> v : r2; flat v \<notin> L r1\<rbrakk> \<Longrightarrow> 2\<rhd> Right v : ALT r1 r2"
+| "\<lbrakk>2\<rhd> v1 : r1; 2\<rhd> v2 : r2;
+    \<forall>s t. (s \<in> L(ders (flat v1) r1) \<and> 
+                s \<sqsubseteq> (flat v2 @ t) \<and> drop (length s) (flat v2) \<in> (L r2 ;; {t}) \<longrightarrow> s = [])\<rbrakk> \<Longrightarrow>
+    2\<rhd> Seq v1 v2 : SEQ r1 r2"
+| "\<lbrakk>2\<rhd> v : r; 2\<rhd> Stars vs : STAR r; flat v \<noteq> []; 
+    \<forall>s t. (s \<in> L(ders (flat v) r) \<and> 
+              s \<sqsubseteq> (flat (Stars vs) @ t) \<and> drop (length s) (flat (Stars vs)) \<in> (L (STAR r) ;; {t}) \<longrightarrow> s = [])\<rbrakk>\<Longrightarrow>
+    2\<rhd> Stars (v#vs) : STAR r"
+| "2\<rhd> Stars [] : STAR r"
+
+lemma Roy2_props:
+  assumes "2\<rhd> v : r"
+  shows "\<turnstile> v : r"
+using assms
+apply(induct)
+apply(auto intro: Prf.intros)
+done
+
+lemma Roy_mkeps_nullable:
+  assumes "nullable(r)" 
+  shows "2\<rhd> (mkeps r) : r"
+using assms
+apply(induct rule: nullable.induct)
+apply(auto intro: Roy2.intros)
+apply (metis Roy2.intros(4) mkeps_flat nullable_correctness)
+apply(rule Roy2.intros)
+apply(simp_all)
+apply(rule allI)
+apply(rule impI)
+apply(simp add: ders_correctness Ders_def)
+apply(auto simp add: Sequ_def)
+apply(simp add: mkeps_flat)
+apply(auto simp add: prefix_def)
+done
+
 section {* Alternative Posix definition *}
 
 inductive 
@@ -1045,6 +1165,45 @@
     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
 | "[] \<in> STAR r \<rightarrow> Stars []"
 
+lemma PMatch1:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "\<turnstile> v : r" "flat v = s"
+using assms
+apply(induct s r v rule: PMatch.induct)
+apply(auto)
+apply (metis Prf.intros(4))
+apply (metis Prf.intros(5))
+apply (metis Prf.intros(2))
+apply (metis Prf.intros(3))
+apply (metis Prf.intros(1))
+apply (metis Prf.intros(7))
+by (metis Prf.intros(6))
+
+
+lemma 
+  assumes "\<rhd> v : r"
+  shows "(flat v) \<in> r \<rightarrow> v"
+using assms
+apply(induct)
+apply(auto intro: PMatch.intros)
+apply(rule PMatch.intros)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(auto)[1]
+done
+
+lemma 
+  assumes "s \<in> r \<rightarrow> v"
+  shows "\<rhd> v : r"
+using assms
+apply(induct)
+apply(auto intro: Roy.intros)
+apply (metis PMatch1(2) Roy.intros(4))
+apply (metis PMatch1(2) Roy.intros(5))
+by (metis L.simps(6) PMatch1(2) Roy.intros(6))
+
+
 lemma PMatch_mkeps:
   assumes "nullable r"
   shows "[] \<in> r \<rightarrow> mkeps r"
@@ -1067,19 +1226,6 @@
 apply(metis PMatch.intros(7))
 done
 
-lemma PMatch1:
-  assumes "s \<in> r \<rightarrow> v"
-  shows "\<turnstile> v : r" "flat v = s"
-using assms
-apply(induct s r v rule: PMatch.induct)
-apply(auto)
-apply (metis Prf.intros(4))
-apply (metis Prf.intros(5))
-apply (metis Prf.intros(2))
-apply (metis Prf.intros(3))
-apply (metis Prf.intros(1))
-apply (metis Prf.intros(7))
-by (metis Prf.intros(6))
 
 lemma PMatch1N:
   assumes "s \<in> r \<rightarrow> v"
@@ -1342,6 +1488,96 @@
 apply(simp add: Der_def)
 done
 
+lemma PMatch_Roy2:
+  assumes "2\<rhd> v : (der c r)"
+  shows "2\<rhd> (injval r c v) : r"
+using assms
+apply(induct c r arbitrary: v rule: der.induct)
+apply(auto)
+apply(erule Roy2.cases)
+apply(simp_all)
+apply(erule Roy2.cases)
+apply(simp_all)
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Roy2.cases)
+apply(simp_all)
+apply (metis Roy2.intros(2))
+apply(erule Roy2.cases)
+apply(simp_all)
+apply(erule Roy2.cases)
+apply(simp_all)
+apply(clarify)
+apply (metis Roy2.intros(3))
+apply(clarify)
+apply(rule Roy2.intros(4))
+apply(metis)
+apply(simp add: der_correctness Der_def)
+apply(subst v4)
+apply (metis Roy2_props)
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Roy2.cases)
+apply(simp_all)
+apply(clarify)
+apply(erule Roy2.cases)
+apply(simp_all)
+apply(clarify)
+apply(rule Roy2.intros)
+apply metis
+apply(simp)
+apply(auto)[1]
+apply(simp add: ders_correctness Ders_def)
+apply(simp add: der_correctness Der_def)
+apply(drule_tac x="s" in spec)
+apply(drule mp)
+apply(rule conjI)
+apply(subst (asm) v4)
+apply (metis Roy2_props)
+apply(simp)
+apply(rule_tac x="t" in exI)
+apply(simp)
+apply(simp)
+apply(rule Roy2.intros)
+apply (metis Roy_mkeps_nullable)
+apply metis
+apply(auto)[1]
+apply(simp add: ders_correctness Ders_def)
+apply(subst (asm) mkeps_flat)
+apply(simp)
+apply(simp)
+apply(subst (asm) v4)
+apply (metis Roy2_props)
+apply(subst (asm) v4)
+apply (metis Roy2_props)
+apply(simp add: Sequ_def prefix_def)
+apply(auto)[1]
+apply(simp add: append_eq_Cons_conv)
+apply(auto)
+apply(drule_tac x="ys'" in spec)
+apply(drule mp)
+apply(simp add: der_correctness Der_def)
+apply(simp add: append_eq_append_conv2)
+apply(auto)[1]
+prefer 2
+apply(erule Roy2.cases)
+apply(simp_all)
+apply(rule Roy2.intros)
+apply metis
+apply(simp)
+apply(auto)[1]
+apply(simp add: ders_correctness Ders_def)
+apply(subst (asm) v4)
+apply (metis Roy2_props)
+apply(drule_tac x="s" in spec)
+apply(drule mp)
+apply(rule conjI)
+apply(simp add: der_correctness Der_def)
+apply(auto)[1]
+oops
+
+
 lemma lex_correct1:
   assumes "s \<notin> L r"
   shows "lex r s = None"
@@ -1436,10 +1672,181 @@
 | "(Char c) \<succ>(CHAR c) (Char c)"
 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
-| "v1 \<succ>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
+| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
 | "(Stars []) \<succ>(STAR r) (Stars [])"
 
+inductive ValOrd2 :: "val \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ>_ _" [100, 100, 100] 100)
+where
+  "v2 2\<succ>s v2' \<Longrightarrow> (Seq v1 v2) 2\<succ>(flat v1 @ s) (Seq v1 v2')" 
+| "\<lbrakk>v1 2\<succ>s v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ>s (Seq v1' v2')" 
+| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ>(flat v1) (Right v2)"
+| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 2\<succ>(flat v2) (Left v1)"
+| "v2 2\<succ>s v2' \<Longrightarrow> (Right v2) 2\<succ>s (Right v2')"
+| "v1 2\<succ>s v1' \<Longrightarrow> (Left v1) 2\<succ>s (Left v1')"
+| "Void 2\<succ>[] Void"
+| "(Char c) 2\<succ>[c] (Char c)"
+| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) 2\<succ>[] (Stars (v # vs))"
+| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) 2\<succ>(flat (Stars (v # vs))) (Stars [])"
+| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) 2\<succ>(flat v1) (Stars (v2 # vs2))"
+| "(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 "2\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
+  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))
+apply (metis ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
+apply (metis ValOrd.intros(5))
+(* Seq case *)
+apply(erule Prf.cases)
+apply(clarify)+
+prefer 2
+apply(clarify)
+prefer 2
+apply(clarify)
+prefer 2
+apply(clarify)
+prefer 2
+apply(clarify)
+prefer 2
+apply(clarify)
+prefer 2
+apply(clarify)
+apply(subgoal_tac "flat v1 \<sqsubset> flat v1a \<or> flat v1a \<sqsubseteq> flat v1")
+prefer 2
+apply(simp add: prefix_def sprefix_def)
+apply (metis append_eq_append_conv2)
+apply(erule disjE)
+apply(subst (asm) sprefix_def)
+apply(subst (asm) (5) prefix_def)
+apply(clarify)
+apply(subgoal_tac "(s3 @ flat v2a) \<sqsubseteq> flat v2")
+prefer 2
+apply(simp)
+apply (metis append_assoc prefix_append)
+apply(subgoal_tac "s3 \<noteq> []")
+prefer 2
+apply (metis append_Nil2)
+apply(subst (asm) (5) prefix_def)
+apply(erule exE)
+apply(drule_tac x="s3" in spec)
+apply(drule_tac x="s3a" in spec)
+apply(drule mp)
+apply(rule conjI)
+apply(simp add: ders_correctness Ders_def)
+apply (metis Prf_flat_L)
+apply(rule conjI)
+apply(simp)
+apply (metis append_assoc prefix_def)
+apply(simp)
+apply(subgoal_tac "drop (length s3) (flat v2) = flat v2a @ s3a")
+apply(simp add: Sequ_def)
+apply (metis Prf_flat_L)
+thm drop_append
+apply (metis append_eq_conv_conj)
+apply(simp)
+apply (metis ValOrd.intros(1) ValOrd.intros(2) flat.simps(5) prefix_append)
+(* star cases *)
+oops
+
+
+lemma admisibility:
+  assumes "\<rhd> v : r" "\<turnstile> v' : r"
+  shows "v \<succ>r v'"
+using assms
+apply(induct arbitrary: v')
+prefer 5
+apply(drule royA)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(case_tac "v1 = v1a")
+apply(simp)
+apply(rule ValOrd.intros)
+apply metis
+apply (metis ValOrd.intros(2))
+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))
+apply(rule ValOrd.intros)
+defer
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(rule ValOrd.intros)
+(* seq case goes through *)
+oops
+
+
+lemma admisibility:
+  assumes "\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
+  shows "v \<succ>r v'"
+using assms
+apply(induct arbitrary: v')
+prefer 5
+apply(drule royA)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(case_tac "v1 = v1a")
+apply(simp)
+apply(rule ValOrd.intros)
+apply(subst (asm) (3) prefix_def)
+apply(erule exE)
+apply(simp)
+apply (metis prefix_def)
+(* the unequal case *)
+apply(subgoal_tac "flat v1 \<sqsubset> flat v1a \<or> flat v1a \<sqsubseteq> flat v1")
+prefer 2
+apply(simp add: prefix_def sprefix_def)
+apply (metis append_eq_append_conv2)
+apply(erule disjE)
+(* first case  flat v1 \<sqsubset> flat v1a *)
+apply(subst (asm) sprefix_def)
+apply(subst (asm) (5) prefix_def)
+apply(clarify)
+apply(subgoal_tac "(s3 @ flat v2a) \<sqsubseteq> flat v2")
+prefer 2
+apply(simp)
+apply (metis append_assoc prefix_append)
+apply(subgoal_tac "s3 \<noteq> []")
+prefer 2
+apply (metis append_Nil2)
+(* HERE *)
+apply(subst (asm) (5) prefix_def)
+apply(erule exE)
+apply(simp add: ders_correctness Ders_def)
+apply(simp add: prefix_def)
+apply(clarify)
+apply(subst (asm) append_eq_append_conv2)
+apply(erule exE)
+apply(erule disjE)
+apply(clarify)
+oops
+
+
+
 lemma ValOrd_refl:
   assumes "\<turnstile> v : r"
   shows "v \<succ>r v"
@@ -1509,7 +1916,77 @@
 apply(simp_all)[7]
 apply(auto)
 apply (metis ValOrd.intros(10) ValOrd.intros(9))
-by (metis ValOrd.intros(11))
+apply(case_tac "v = va")
+prefer 2
+apply (metis ValOrd.intros(11))
+apply(simp)
+apply(rule ValOrd.intros(12))
+apply(erule contrapos_np)
+apply(rule ValOrd.intros(12))
+oops
+
+lemma Roy_posix:
+  assumes "\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
+  shows "v \<succ>r v'"
+using assms
+apply(induct r arbitrary: v v' rule: rexp.induct)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Roy.cases)
+apply(simp_all)
+apply (metis ValOrd.intros(7))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Roy.cases)
+apply(simp_all)
+apply (metis ValOrd.intros(8))
+prefer 2
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Roy.cases)
+apply(simp_all)
+apply(clarify)
+apply (metis ValOrd.intros(6))
+apply(clarify)
+apply (metis Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
+apply(erule Roy.cases)
+apply(simp_all)
+apply (metis ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
+apply(clarify)
+apply (metis ValOrd.intros(5))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule Roy.cases)
+apply(simp_all)
+apply(clarify)
+apply(case_tac "v1a = v1")
+apply(simp)
+apply(rule ValOrd.intros)
+apply (metis prefix_append)
+apply(rule ValOrd.intros)
+prefer 2
+apply(simp)
+apply(simp add: prefix_def)
+apply(auto)[1]
+apply(simp add: append_eq_append_conv2)
+apply(auto)[1]
+apply(drule_tac x="v1a" in meta_spec)
+apply(rotate_tac 9)
+apply(drule_tac x="v1" in meta_spec)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(drule_tac x="us" in spec)
+apply(drule_tac mp)
+apply (metis Prf_flat_L)
+apply(auto)[1]
+oops
+
 
 lemma ValOrd_anti:
   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"
@@ -1577,57 +2054,6 @@
 apply(simp_all)
 apply(auto)[1]
 prefer 2
-apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
-prefer 2
-apply(auto)[1]
-apply(rotate_tac 5)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply (metis (no_types) Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
-apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
-apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
-apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
-apply (metis Prf.intros(7) ValOrd.intros(11) not_Cons_self2)
-apply (metis Prf.intros(7) ValOrd.intros(11) ValOrd_refl not_Cons_self2)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(rotate_tac 3)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(clarify)
-apply(rotate_tac 4)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(clarify)
-
-
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(auto)[1]
-prefer 2
-prefer 3
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(rotate_tac 3)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(auto)[1]
 oops