--- a/thys/ReStar.thy	Mon Feb 01 13:59:55 2016 +0000
+++ b/thys/ReStar.thy	Mon Feb 01 22:30:27 2016 +0000
@@ -211,7 +211,6 @@
 | "\<Turnstile> Star [] : STAR r"
 | "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Star vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Star (v # vs) : STAR r"
 
-
 inductive 
   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 where
@@ -231,6 +230,84 @@
 apply(auto intro: Prf.intros)
 done
 
+lemma NPrf_Prf_val:
+  shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"
+  and   "\<turnstile> Star vs : r \<Longrightarrow> \<exists>vs'. flat (Star vs') = flat (Star vs) \<and> \<Turnstile> Star vs' : r"
+using assms
+apply(induct v and vs arbitrary: r and r rule: val.inducts)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule_tac x="Void" in exI)
+apply(simp)
+apply(rule NPrf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule_tac x="Char c" in exI)
+apply(simp)
+apply(rule NPrf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule_tac x="r1" in meta_spec)
+apply(drule_tac x="r2" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Seq v' v'a" in exI)
+apply(simp)
+apply (metis NPrf.intros(1))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(drule_tac x="r2" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Right v'" in exI)
+apply(simp)
+apply (metis NPrf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(drule_tac x="r1" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Left v'" in exI)
+apply(simp)
+apply (metis NPrf.intros)
+apply(drule_tac x="r" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Star vs'" in exI)
+apply(simp)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis NPrf.intros(6))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule_tac x="ra" in meta_spec)
+apply(simp)
+apply(drule_tac x="STAR ra" in meta_spec)
+apply(simp)
+apply(auto)
+apply(case_tac "flat v = []")
+apply(rule_tac x="vs'" in exI)
+apply(simp)
+apply(rule_tac x="v' # vs'" in exI)
+apply(simp)
+apply(rule NPrf.intros)
+apply(auto)
+done
+
+lemma NPrf_Prf:
+  shows "{flat v | v. \<turnstile> v : r} = {flat v | v. \<Turnstile> v : r}"
+apply(auto)
+apply (metis NPrf_Prf_val(1))
+by (metis NPrf_imp_Prf)
+
+
 lemma not_nullable_flat:
   assumes "\<turnstile> v : r" "\<not>nullable r"
   shows "flat v \<noteq> []"
@@ -246,6 +323,11 @@
 apply(auto simp add: Sequ_def)
 done
 
+lemma NPrf_flat_L:
+  assumes "\<Turnstile> v : r" shows "flat v \<in> L r"
+using assms
+by (metis NPrf_imp_Prf Prf_flat_L)
+
 lemma Prf_Star:
   assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
   shows "\<turnstile> Star vs : STAR r"
@@ -275,6 +357,15 @@
 apply (metis empty_iff list.set(1))
 by (metis concat.simps(2) list.simps(9) set_ConsD)
 
+lemma Star_valN:
+  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"
+  shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r)"
+using assms
+apply(induct ss)
+apply(auto)
+apply (metis empty_iff list.set(1))
+by (metis concat.simps(2) list.simps(9) set_ConsD)
+
 lemma L_flat_Prf:
   "L(r) = {flat v | v. \<turnstile> v : r}"
 apply(induct r)
@@ -298,6 +389,12 @@
 apply(simp)
 done
 
+lemma L_flat_NPrf:
+  "L(r) = {flat v | v. \<Turnstile> v : r}"
+by (metis L_flat_Prf NPrf_Prf)
+
+text {* nicer proofs by Fahad *}
+
 lemma Prf_Star_flat_L:
   assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>"
 using assms
@@ -613,43 +710,6 @@
 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"
@@ -756,7 +816,6 @@
 by (metis list.inject v4_proj)
 
 
-
 section {* Alternative Posix definition *}
 
 inductive 
@@ -769,7 +828,8 @@
 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
     \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
-| "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Star vs; flat v \<noteq> []\<rbrakk> \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Star (v # vs)"
+| "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Star vs; flat v \<noteq> []\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Star (v # vs)"
 | "[] \<in> STAR r \<rightarrow> Star []"
 
 lemma PMatch_mkeps:
@@ -819,7 +879,10 @@
 apply (metis NPrf.intros(2))
 apply (metis NPrf.intros(3))
 apply (metis NPrf.intros(1))
-apply (metis NPrf.intros(7) PMatch1(2))
+apply(rule NPrf.intros)
+apply(simp)
+apply(simp)
+apply(simp)
 apply(rule NPrf.intros)
 done
 
@@ -854,16 +917,14 @@
 apply(clarify)
 apply(rule PMatch.intros)
 apply metis
-apply(simp add: L_flat_Prf)
+apply(simp add: L_flat_NPrf)
 apply(auto)[1]
-apply(subgoal_tac "\<Turnstile> v : r1")
 apply(frule_tac c="c" in v3_proj)
 apply metis
 apply(drule_tac x="projval r1 c v" in spec)
 apply(drule mp)
 apply (metis v4_proj2)
 apply (metis NPrf_imp_Prf)
-defer
 (* SEQ case *)
 apply(case_tac "nullable r1")
 apply(simp)
@@ -877,9 +938,8 @@
 apply metis
 apply metis
 apply(auto)[1]
-apply(simp add: L_flat_Prf)
+apply(simp add: L_flat_NPrf)
 apply(auto)[1]
-apply(subgoal_tac "\<Turnstile> v : r1")
 apply(frule_tac c="c" in v3_proj)
 apply metis
 apply(drule_tac x="s3" in spec)
@@ -889,7 +949,6 @@
 apply (metis v4_proj2)
 apply (metis NPrf_imp_Prf)
 apply metis
-defer
 (* nullable case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
@@ -902,16 +961,14 @@
 apply metis
 apply metis
 apply(auto)[1]
-apply(simp add: L_flat_Prf)
+apply(simp add: L_flat_NPrf)
 apply(auto)[1]
-apply(subgoal_tac "\<Turnstile> v : r1")
 apply(frule_tac c="c" in v3_proj)
 apply metis
 apply(drule_tac x="s3" in spec)
 apply(drule mp)
 apply (metis NPrf_imp_Prf v4_proj2)
 apply(simp)
-defer
 (* interesting case *)
 apply(clarify)
 apply(simp)
@@ -923,20 +980,18 @@
 apply (metis PMatch_mkeps)
 apply metis
 apply(auto)
-apply(simp only: L_flat_Prf)
+apply(simp only: L_flat_NPrf)
 apply(simp)
 apply(auto)
 apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
 apply(drule mp)
 apply(simp)
-apply(subgoal_tac "\<Turnstile> v : r1")
 apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2)
-defer
 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
-apply (metis Prf.intros(1))
+apply (metis NPrf_imp_Prf Prf.intros(1))
 apply(rule NPrf_imp_Prf)
 apply(rule v3_proj)
-defer
+apply(simp)
 apply (metis Cons_eq_append_conv)
 (* Star case *)
 apply(erule PMatch.cases)
@@ -949,11 +1004,16 @@
 apply(subst append.simps(2)[symmetric])
 apply(rule PMatch.intros)
 apply metis
-apply (metis Nil_is_append_conv PMatch.intros(6))
-apply (metis PMatch1(2) list.distinct(1))
 apply(auto)[1]
-(* HERE *)
-(* oops *)
+apply(rule PMatch.intros)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(subst v4)
+apply (metis NPrf_imp_Prf PMatch1N)
+apply(simp)
+apply (metis PMatch.intros(6) PMatch.intros(7) PMatch1(2) append_Nil2 list.discI)
+done
 
 
 
@@ -981,7 +1041,7 @@
 apply (metis mkeps_flat mkeps_nullable nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(drule meta_mp)
-apply(simp add: L_flat_Prf)
+apply(simp add: L_flat_NPrf)
 apply(auto)
 apply (metis v3_proj v4_proj2)
 apply (metis v3)
@@ -997,7 +1057,7 @@
 apply (metis PMatch_mkeps nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(drule meta_mp)
-apply(simp add: L_flat_Prf)
+apply(simp add: L_flat_NPrf)
 apply(auto)
 apply (metis v3_proj v4_proj2)
 apply(rule PMatch2)
@@ -1015,7 +1075,7 @@
 apply(rule PMatch2)
 apply(drule_tac x="der a r" in meta_spec)
 apply(drule meta_mp)
-apply(simp add: L_flat_Prf)
+apply(simp add: L_flat_NPrf)
 apply(auto)
 apply (metis v3_proj v4_proj2)
 done
@@ -1026,6 +1086,8 @@
 done
 
 
+(* NOT DONE YET *)
+
 section {* Sulzmann's Ordering of values *}
 
 thm PMatch.intros