--- a/thys/Re1.thy	Wed Mar 04 19:34:47 2015 +0000
+++ b/thys/Re1.thy	Mon Mar 09 10:49:17 2015 +0000
@@ -318,6 +318,23 @@
 apply metis
 done
 
+
+lemma 
+  "\<lbrakk>POSIX (mkeps r2) r2; nullable r2; \<not> nullable r1\<rbrakk>
+   \<Longrightarrow> POSIX (val.Right (mkeps r2)) (ALT r1 r2)" 
+apply(auto simp add: POSIX_def)
+apply(rule Prf.intros(3))
+apply(auto)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp add: mkeps_flat)
+apply(auto)[1]
+apply (metis Prf_flat_L nullable_correctness)
+apply(rule ValOrd.intros)
+apply(auto)
+done
+
 lemma mkeps_POSIX:
   assumes "nullable r"
   shows "POSIX (mkeps r) r"
@@ -719,6 +736,89 @@
 oops
 *)
 
+
+lemma LeftRight:
+  assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"
+  and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2" 
+  shows "(injval (ALT r1 r2) c (Left v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Right v2))"
+using assms
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(rule ValOrd.intros)
+apply(clarify)
+apply(subst v4)
+apply(simp)
+apply(subst v4)
+apply(simp)
+apply(simp)
+done
+
+lemma RightLeft:
+  assumes "(Right v1) \<succ>(der c (ALT r1 r2)) (Left v2)"
+  and "\<turnstile> v1 : der c r2" "\<turnstile> v2 : der c r1" 
+  shows "(injval (ALT r1 r2) c (Right v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Left v2))"
+using assms
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(rule ValOrd.intros)
+apply(clarify)
+apply(subst v4)
+apply(simp)
+apply(subst v4)
+apply(simp)
+apply(simp)
+done
+
+lemma h: 
+  assumes "nullable r1" "\<turnstile> v1 : der c r1"
+  shows "injval r1 c v1 \<succ>r1 mkeps r1"
+using assms
+apply(induct r1 arbitrary: v1 rule: der.induct)
+apply(simp)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(auto)[1]
+apply (metis ValOrd.intros(6))
+apply (metis ValOrd.intros(6))
+apply (metis ValOrd.intros(3) le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral)
+apply(auto)[1]
+apply (metis ValOrd.intros(4) length_greater_0_conv list.distinct(1) list.size(3) mkeps_flat v4)
+apply (metis ValOrd.intros(4) length_greater_0_conv list.distinct(1) list.size(3) mkeps_flat v4)
+apply (metis ValOrd.intros(5))
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply (metis ValOrd.intros(2) list.distinct(1) mkeps_flat v4)
+apply(clarify)
+by (metis ValOrd.intros(1))
+
+lemma LeftRightSeq:
+  assumes "(Left (Seq v1 v2)) \<succ>(der c (SEQ r1 r2)) (Right v3)"
+  and "nullable r1" "\<turnstile> v1 : der c r1"
+  shows "(injval (SEQ r1 r2) c (Seq v1 v2)) \<succ>(SEQ r1 r2) (injval (SEQ r1 r2) c (Right v2))"
+using assms
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(simp)
+apply(rule ValOrd.intros(2))
+prefer 2
+apply (metis list.distinct(1) mkeps_flat v4)
+by (metis h)
+
 lemma Prf_inj:
   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*)
   shows "(injval r c v1) \<succ>r (injval r c v2)"
@@ -832,6 +932,7 @@
 apply(simp add: inj_on_def)
 apply metis
 apply(clarify)
+apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(clarify)
@@ -840,9 +941,8 @@
 apply(clarify)
 apply(simp)
 apply(rule ValOrd.intros(2))
-prefer 2
+apply (metis h)
 apply (metis list.distinct(1) mkeps_flat v4)
-defer
 apply(clarify)
 apply(erule Prf.cases)
 apply(simp_all)[5]
@@ -855,8 +955,14 @@
 apply(simp_all)[8]
 apply(clarify)
 apply(simp)
-apply(rule ValOrd.intros(2))
 prefer 2
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd.intros(1))
+apply(metis)
+thm mkeps_flat v4
 apply (metis list.distinct(1) mkeps_flat v4)
 defer
 apply(clarify)