--- a/thys/Re1.thy	Fri Sep 19 14:01:01 2014 +0100
+++ b/thys/Re1.thy	Mon Sep 22 14:57:02 2014 +0100
@@ -168,6 +168,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"
@@ -291,6 +318,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"