diff -r b409ecf47f64 -r a605dda64267 thys/Re.thy
--- a/thys/Re.thy	Mon Sep 08 21:13:36 2014 +0100
+++ b/thys/Re.thy	Tue Sep 09 05:12:01 2014 +0100
@@ -147,13 +147,15 @@
 using assms
 unfolding POSIX_def
 apply(auto)
-apply(rotate_tac 4)
+apply(rotate_tac 2)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(auto)[1]
 apply(rule ValOrd.intros)
+
 apply(auto)
 done
+*)
 
 lemma POSIX_ALT:
   assumes "POSIX (Left v1) (ALT r1 r2)"
@@ -167,7 +169,7 @@
 apply(rule Prf.intros)
 apply(auto)
 apply(erule ValOrd.cases)
-apply(simp_all)[7]
+apply(simp_all)
 done
 
 lemma POSIX_ALT1a:
@@ -182,12 +184,13 @@
 apply(rule Prf.intros)
 apply(auto)
 apply(erule ValOrd.cases)
-apply(simp_all)[7]
+apply(simp_all)
 done
 
+
 lemma POSIX_ALT1b:
   assumes "POSIX (Right v2) (ALT r1 r2)"
-  shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flats v' = flats v2) \<longrightarrow> v2 \<succ>r2 v')"
+  shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"
 using assms
 apply(drule_tac POSIX_ALT1a)
 unfolding POSIX_def
@@ -207,7 +210,7 @@
 apply(rule ValOrd.intros)
 apply(auto)
 apply(rule ValOrd.intros)
-by (metis flats_flat order_refl)
+by simp
 
 lemma POSIX_ALT_I2:
   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
@@ -219,13 +222,12 @@
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(auto)
-prefer 2
 apply(rule ValOrd.intros)
 apply metis
-apply(rule ValOrd.intros)
-apply(auto)
 done
-*)
+
+
+section {* The ordering is reflexive *}
 
 lemma ValOrd_refl:
   assumes "\<turnstile> v : r"
@@ -521,12 +523,21 @@
 apply(auto)
 apply(erule Prf.cases)
 apply(simp_all)[5]
-prefer 2 
-apply(case_tac "nullable r1")
-apply(simp)
-defer
-apply(simp)
+(* base cases done *)
+(* ALT case *)
 apply(erule Prf.cases)
 apply(simp_all)[5]
-apply(auto)[1]
-oops
+using POSIX_ALT POSIX_ALT_I1 apply blast
+apply(frule POSIX_ALT1a)
+apply(drule POSIX_ALT1b)
+apply(rule POSIX_ALT_I2)
+apply auto[1]
+apply(subst v4)
+apply(auto)[2]
+apply(rotate_tac 1)
+apply(drule_tac x="v2" in meta_spec)
+apply(simp)
+apply(subst (asm) (4) POSIX_def)
+apply(subst (asm) v4)
+apply(auto)[2]
+(* stuck in the ALT case *)