# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1411131661 -3600
# Node ID 26b8a5213355eba22206e8d68fa28abffc8285e7
# Parent  14d41b5b57b31932c2ca2f18a3a542fdaa8747f4
changed theory name

diff -r 14d41b5b57b3 -r 26b8a5213355 thys/Re1.thy
--- a/thys/Re1.thy	Fri Sep 19 12:54:03 2014 +0100
+++ b/thys/Re1.thy	Fri Sep 19 14:01:01 2014 +0100
@@ -1,5 +1,5 @@
 
-theory Re
+theory Re1
   imports "Main" 
 begin
 
@@ -127,6 +127,16 @@
   "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')"
 
 (*
+an alternative definition: might cause problems
+with theorem mkeps_POSIX
+*)
+
+definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
+where
+  "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
+
+
+(*
 lemma POSIX_SEQ:
   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
   shows "POSIX v1 r1 \<and> POSIX v2 r2"
@@ -514,6 +524,8 @@
 defer
 apply(auto)
 apply (metis POSIX_ALT_I1)
+(* maybe it is too early to instantiate this existential quantifier *)
+(* potentially this is the wrong POSIX value *)
 apply(rule_tac x = "Seq v va" in exI )
 apply(simp (no_asm) add: POSIX_def)
 apply(auto)