--- a/thys/ReStar.thy	Mon Feb 01 13:46:28 2016 +0000
+++ b/thys/ReStar.thy	Mon Feb 01 13:59:55 2016 +0000
@@ -1,5 +1,5 @@
    
-theory Re
+theory ReStar
   imports "Main" 
 begin
 
@@ -58,7 +58,7 @@
 lemma star1: 
   shows "s \<in> A\<star> \<Longrightarrow> \<exists>n. s \<in> A \<up> n"
   apply(induct rule: Star.induct)
-  apply (metis Re.pow.simps(1) insertI1)
+  apply (metis pow.simps(1) insertI1)
   apply(auto)
   apply(rule_tac x="Suc n" in exI)
   apply(auto simp add: Sequ_def)
@@ -67,7 +67,7 @@
 lemma star2:
   shows "s \<in> A \<up> n \<Longrightarrow> s \<in> A\<star>"
   apply(induct n arbitrary: s)
-  apply (metis Re.pow.simps(1) Star.simps empty_iff insertE)
+  apply (metis pow.simps(1) Star.simps empty_iff insertE)
   apply(auto simp add: Sequ_def)
   done
 
@@ -613,6 +613,43 @@
 apply (metis Prf.intros(6) Prf.intros(7))
 by (metis Prf.intros(7))
 
+lemma v3_NP:
+  assumes "\<Turnstile> v : der c r" 
+  shows "\<Turnstile> (injval r c v) : r"
+using assms
+apply(induct arbitrary: v rule: der.induct)
+apply(simp)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply (metis NPrf.intros(5))
+apply(simp)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply(simp)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply (metis NPrf.intros(2))
+apply (metis NPrf.intros(3))
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply (metis NPrf.intros(1))
+apply(auto)[1]
+oops
+
 lemma v3_proj:
   assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
   shows "\<Turnstile> (projval r c v) : der c r"