diff -r 38cde0214ad5 -r c33cfa1e813a thys/Re1.thy
--- a/thys/Re1.thy	Thu Jan 29 09:05:40 2015 +0000
+++ b/thys/Re1.thy	Thu Jan 29 23:39:08 2015 +0000
@@ -724,192 +724,19 @@
 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 by (metis list.sel(3))
 
-lemma Prf_proj:
-  assumes "v1 \<succ>r v2" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<exists>s. (flat v1) = c # s" "\<exists>s. (flat v2) = c # s"
-  shows "(projval r c v1) \<succ>(der c r) (projval r c v2)"
-using assms
-apply(induct arbitrary: v1 v2 rule: der.induct)
-apply(simp)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(case_tac "c = c'")
-apply(simp)
-apply (metis ValOrd.intros(7))
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(simp)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply metis
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply metis
-apply(clarify)
-apply(simp)
-apply(auto)
-defer
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(simp)
-apply (metis Prf_flat_L nullable_correctness)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply (metis Prf_flat_L nullable_correctness)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply (metis Prf_flat_L nullable_correctness)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply (metis Prf_flat_L nullable_correctness)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros(2))
-apply (metis append_Cons list.inject neq_Nil_conv)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(auto)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(auto)[1]
-apply(rule ValOrd.intros)
-apply metis
-apply(clarify)
-apply(rule ValOrd.intros)
-
-apply(rule ValOrd.intros)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-defer
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(simp add: append_eq_Cons_conv)
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(simp)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-
-apply(simp)
-
-apply (metis Prf_flat_L nullable_correctness)
-
-
-
-
-apply(rule ValOrd.intros(2))
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(simp)
-
 lemma Prf_inj:
   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"
   shows "(injval r c v1) \<succ>r (injval r c v2)"
 using assms
 apply(induct arbitrary: v1 v2 rule: der.induct)
+(* NULL case *)
 apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
+(* EMPTY case *)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
+(* CHAR case *)
 apply(case_tac "c = c'")
 apply(simp)
 apply(erule ValOrd.cases)
@@ -918,6 +745,7 @@
 apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
+(* ALT case *)
 apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
@@ -956,6 +784,7 @@
 apply(simp_all)[5]
 apply(erule Prf.cases)
 apply(simp_all)[5]
+(* SEQ case*)
 apply(simp)
 apply(case_tac "nullable r1")
 defer
@@ -976,10 +805,12 @@
 apply(simp_all)[5]
 apply(erule Prf.cases)
 apply(simp_all)[5]
+(* nullable case - unfinished *)
 apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
 apply(clarify)
+apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(erule Prf.cases)
@@ -994,10 +825,8 @@
 apply(simp)
 apply (metis impossible_Cons le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral v4)
 apply(rule ValOrd.intros(2))
-
-apply(rotate_tac 1)
-apply(drule meta_mp)
-apply(rule
+apply(drule_tac x="proj r1 c" in spec)
+oops
 
 lemma POSIX_der:
   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
@@ -1005,10 +834,10 @@
 using assms
 unfolding POSIX_def
 apply(auto)
+thm v4
 apply(subst (asm) v4)
 apply(assumption)
 apply(drule_tac x="projval r c v'" in spec)
-apply(drule mp)
 apply(auto)
 apply(rule v3_proj)
 apply(simp)