--- a/thys/Re1.thy	Mon Feb 09 12:13:10 2015 +0000
+++ b/thys/Re1.thy	Wed Feb 11 11:22:53 2015 +0000
@@ -76,6 +76,14 @@
 | "flat(Right v) = flat(v)"
 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
+fun head :: "val \<Rightarrow> string"
+where
+  "head(Void) = []"
+| "head(Char c) = [c]"
+| "head(Left v) = head(v)"
+| "head(Right v) = head(v)"
+| "head(Seq v1 v2) = head v1"
+
 fun flats :: "val \<Rightarrow> string list"
 where
   "flats(Void) = [[]]"
@@ -378,6 +386,7 @@
 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
+
 section {* Projection function *}
 
 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
@@ -529,6 +538,57 @@
 using assms
 by (metis list.inject v4_proj)
 
+lemma injval_inj: "inj_on (injval r c) {v. \<turnstile> v : der c r}"
+apply(induct c r rule: der.induct)
+unfolding inj_on_def
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+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(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply (metis list.distinct(1) mkeps_flat v4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis list.distinct(1) mkeps_flat v4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+done
+
 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 by (metis list.sel(3))
 
@@ -545,6 +605,101 @@
 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 by (metis Prf_flat_L nullable_correctness)
 
+lemma proj_inj_id:
+  assumes "\<turnstile> v : der c r" 
+  shows "projval r c (injval r c v) = v"
+using assms
+apply(induct c r arbitrary: v rule: der.induct)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply (metis list.distinct(1) v4)
+apply(auto)[1]
+apply (metis mkeps_flat)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(simp add: v4)
+done
+
+(*
+lemma 
+ assumes "\<turnstile> v : der c r" "flat v \<noteq> []"
+ shows "injval r c v \<succ>r mkeps r"
+using assms
+apply(induct c r arbitrary: v rule: der.induct)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply (metis ValOrd.intros(6))
+apply(clarify)
+apply (metis ValOrd.intros(4) drop_0 drop_all le_add2 list.distinct(1) list.size(3) mkeps_flat monoid_add_class.add.right_neutral nat_less_le v4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(simp)
+defer
+apply(rule ValOrd.intros)
+apply metis
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+defer
+apply(clarify)
+apply(rule ValOrd.intros)
+apply metis
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+defer
+apply(subst mkeps_flat)
+oops
+*)
+
 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)"
@@ -627,12 +782,74 @@
 apply(clarify)
 apply(rule ValOrd.intros(2))
 apply metis
-
+using injval_inj
+apply(simp add: inj_on_def)
+apply metis
+(* SEQ nullable case *)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd.intros(1))
+apply(simp)
+apply(rule ValOrd.intros(2))
+apply metis
+using injval_inj
+apply(simp add: inj_on_def)
+apply metis
+apply(clarify)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(simp)
+apply(rule ValOrd.intros(2))
+prefer 2
+apply (metis list.distinct(1) mkeps_flat v4)
+defer
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(simp)
+apply(rule ValOrd.intros(2))
+prefer 2
+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)
+
 defer
 apply(erule ValOrd.cases)
 apply(simp_all del: injval.simps)[8]