--- a/thys/Re1.thy~	Mon Oct 06 14:22:13 2014 +0100
+++ b/thys/Re1.thy~	Mon Oct 06 15:24:41 2014 +0100
@@ -135,6 +135,10 @@
 where
   "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
 
+definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
+where
+  "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v \<ge> flat v') \<longrightarrow> v \<succ>r v')"
+
 
 (*
 lemma POSIX_SEQ:
@@ -168,6 +172,33 @@
 done
 *)
 
+
+
+
+lemma POSIX_ALT2:
+  assumes "POSIX (Left v1) (ALT r1 r2)"
+  shows "POSIX v1 r1"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply(drule_tac x="Left v'" in spec)
+apply(simp)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+done
+
+lemma POSIX2_ALT:
+  assumes "POSIX2 (Left v1) (ALT r1 r2)"
+  shows "POSIX2 v1 r1"
+using assms
+unfolding POSIX2_def
+apply(auto)
+
+done
+
 lemma POSIX_ALT:
   assumes "POSIX (Left v1) (ALT r1 r2)"
   shows "POSIX v1 r1"
@@ -183,6 +214,23 @@
 apply(simp_all)
 done
 
+lemma POSIX2_ALT:
+  assumes "POSIX2 (Left v1) (ALT r1 r2)"
+  shows "POSIX2 v1 r1"
+using assms
+apply(simp add: POSIX2_def)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(drule_tac x="Left v'" in spec)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+done
+
+
 lemma POSIX_ALT1a:
   assumes "POSIX (Right v2) (ALT r1 r2)"
   shows "POSIX v2 r2"
@@ -198,6 +246,22 @@
 apply(simp_all)
 done
 
+lemma POSIX2_ALT1a:
+  assumes "POSIX2 (Right v2) (ALT r1 r2)"
+  shows "POSIX2 v2 r2"
+using assms
+unfolding POSIX2_def
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(drule_tac x="Right v'" in spec)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+done
+
 
 lemma POSIX_ALT1b:
   assumes "POSIX (Right v2) (ALT r1 r2)"
@@ -223,6 +287,25 @@
 apply(rule ValOrd.intros)
 by simp
 
+lemma POSIX2_ALT_I1:
+  assumes "POSIX2 v1 r1" 
+  shows "POSIX2 (Left v1) (ALT r1 r2)"
+using assms
+unfolding POSIX2_def
+apply(auto)
+apply(rule Prf.intros)
+apply(simp)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rule ValOrd.intros)
+apply(auto)
+apply(rule ValOrd.intros)
+
+
+by simp
+
 lemma POSIX_ALT_I2:
   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
   shows "POSIX (Right v2) (ALT r1 r2)"
@@ -291,6 +374,14 @@
   value.
 *}
 
+lemma mkeps_POSIX2:
+  assumes "nullable r"
+  shows "POSIX2 (mkeps r) r"
+using assms
+apply(induct r)
+apply(auto)[1]
+apply(simp add: POSIX2_def)
+
 lemma mkeps_POSIX:
   assumes "nullable r"
   shows "POSIX (mkeps r) r"
@@ -333,6 +424,51 @@
 by (simp add: ValOrd.intros(5))
 
 
+lemma mkeps_POSIX2:
+  assumes "nullable r"
+  shows "POSIX2 (mkeps r) r"
+using assms
+apply(induct r)
+apply(simp)
+apply(simp)
+apply(simp add: POSIX2_def)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(simp)
+apply(simp)
+apply(simp add: POSIX2_def)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(simp add: mkeps_nullable)
+apply(simp add: mkeps_nullable)
+apply(auto)[1]
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros(2))
+apply(simp)
+apply(simp only: nullable.simps)
+apply(erule disjE)
+apply(simp)
+thm POSIX2_ALT1a
+apply(rule POSIX2_ALT)
+apply(simp add: POSIX2_def)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(simp add: mkeps_nullable)
+apply(auto)[1]
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(simp)
+apply(rule ValOrd.intros)
+
+
 section {* Derivatives *}
 
 fun