--- a/progs/scala/re.scala	Mon Mar 09 10:49:17 2015 +0000
+++ b/progs/scala/re.scala	Fri Mar 13 21:27:03 2015 +0000
@@ -371,12 +371,13 @@
   time(lexing_simp(WHILE_REGS, prog2 * i))
 }
 
-val a0 = (EMPTY | "c") ~ ("b" | "cb")
-val a1 = der('c', a0)
+val a0 = (EMPTY | "a") ~ ("b" | "abc")
+val a1 = der('a', a0)
 pretty(a1)
-val List(b1,b2,b3) = values(a1).toList
-vpretty(b1)
-vpretty(b3)
-vpretty(inj(a0,'c',b1))
-vpretty(inj(a0,'c',b3))
+values(a1).toList
+val List(u2,_,u1) = values(a1).toList
+vpretty(u1)
+vpretty(u2)
+vpretty(inj(a0,'a',u1))
+vpretty(inj(a0,'a',u2))
 

--- a/thys/Re1.thy	Mon Mar 09 10:49:17 2015 +0000
+++ b/thys/Re1.thy	Fri Mar 13 21:27:03 2015 +0000
@@ -819,6 +819,11 @@
 apply (metis list.distinct(1) mkeps_flat v4)
 by (metis h)
 
+lemma Prf_inj_test:
+  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)"
+sorry
+
 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)"
@@ -943,6 +948,7 @@
 apply(rule ValOrd.intros(2))
 apply (metis h)
 apply (metis list.distinct(1) mkeps_flat v4)
+(* last case *)
 apply(clarify)
 apply(erule Prf.cases)
 apply(simp_all)[5]
@@ -951,10 +957,6 @@
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(clarify)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(clarify)
-apply(simp)
 prefer 2
 apply(clarify)
 apply(erule ValOrd.cases)
@@ -962,35 +964,56 @@
 apply(clarify)
 apply(rule ValOrd.intros(1))
 apply(metis)
+apply(rule ValOrd.intros(2))
+prefer 2
 thm mkeps_flat v4
 apply (metis list.distinct(1) mkeps_flat v4)
-defer
-apply(clarify)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(clarify)
-apply(rule ValOrd.intros(1))
-apply(metis)
-apply(drule_tac x="v1" in meta_spec)
-apply(rotate_tac 7)
-apply(drule_tac x="projval r1 c (mkeps r1)" in meta_spec)
-apply(drule meta_mp)
+oops
 
-defer
-apply(erule ValOrd.cases)
-apply(simp_all del: injval.simps)[8]
+lemma POSIX_der:
+  assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
+  shows "POSIX (injval r c v) r"
+using assms
+unfolding POSIX_def
+apply(auto)
+thm v3
+apply (metis v3)
+thm v4
+apply(subst (asm) v4)
+apply(assumption)
+apply(drule_tac x="projval r c v'" in spec)
+apply(drule mp)
+apply(rule conjI)
+thm v3_proj
+apply(rule v3_proj)
 apply(simp)
-apply(clarify)
+apply(rule_tac x="flat v" in exI)
+apply(simp)
+thm t
+apply(rule_tac c="c" in  t)
 apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros(2))
+thm v4_proj
+apply(subst v4_proj)
+apply(simp)
+apply(rule_tac x="flat v" in exI)
+apply(simp)
+apply(simp)
+thm Prf_inj_test
+apply(drule Prf_inj_test)
+apply(simp)
+apply (metis v3_proj)
+apply(rule_tac c="c" in  t)
+apply(simp)
+thm v4_proj
+apply(subst v4_proj)
+apply(simp)
+apply(rule_tac x="flat v" in exI)
+apply(simp)
+apply(simp)
+
+apply(simp add: Cons_eq_append_conv)
+apply(auto)[1]
+
 
 
 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
@@ -1607,30 +1630,7 @@
 *}
 oops
 
-lemma POSIX_der:
-  assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
-  shows "POSIX (injval r c v) r"
-using assms
-unfolding POSIX_def
-apply(auto)
-thm v4
-apply(subst (asm) v4)
-apply(assumption)
-apply(drule_tac x="projval r c v'" in spec)
-apply(auto)
-apply(rule v3_proj)
-apply(simp)
-apply(rule_tac x="flat v" in exI)
-apply(simp)
-apply(rule_tac c="c" in  t)
-apply(simp)
-apply(subst v4_proj)
-apply(simp)
-apply(rule_tac x="flat v" in exI)
-apply(simp)
-apply(simp)
-apply(simp add: Cons_eq_append_conv)
-apply(auto)[1]
+
 
 text {*
   Injection followed by projection is the identity.