diff -r 3c8cfdf95252 -r f067e59b58d9 thys/ReStar.thy
--- a/thys/ReStar.thy	Sat Jan 30 13:12:36 2016 +0000
+++ b/thys/ReStar.thy	Mon Feb 01 13:46:28 2016 +0000
@@ -201,6 +201,18 @@
 section {* Relation between values and regular expressions *}
 
 inductive 
+  NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
+where
+ "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
+| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
+| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
+| "\<Turnstile> Void : EMPTY"
+| "\<Turnstile> Char c : CHAR c"
+| "\<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
  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
@@ -209,7 +221,15 @@
 | "\<turnstile> Void : EMPTY"
 | "\<turnstile> Char c : CHAR c"
 | "\<turnstile> Star [] : STAR r"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Star vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Star (v#vs) : STAR r"
+| "\<lbrakk>\<turnstile> v : r; \<turnstile> Star vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Star (v # vs) : STAR r"
+
+lemma NPrf_imp_Prf:
+  assumes "\<Turnstile> v : r" 
+  shows "\<turnstile> v : r"
+using assms
+apply(induct)
+apply(auto intro: Prf.intros)
+done
 
 lemma not_nullable_flat:
   assumes "\<turnstile> v : r" "\<not>nullable r"
@@ -278,6 +298,48 @@
 apply(simp)
 done
 
+lemma Prf_Star_flat_L:
+  assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>"
+using assms
+apply(induct v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct)
+apply(auto)
+apply(simp add: star3)
+apply(auto)
+apply(rule_tac x="Suc x" in exI)
+apply(auto simp add: Sequ_def)
+apply(rule_tac x="flat v" in exI)
+apply(rule_tac x="flat (Star vs)" in exI)
+apply(auto)
+by (metis Prf_flat_L)
+
+lemma L_flat_Prf2:
+  "L(r) = {flat v | v. \<turnstile> v : r}"
+apply(induct r)
+apply(auto)
+using L.simps(1) Prf_flat_L 
+apply(blast)
+using Prf.intros(4) 
+apply(force)
+using L.simps(2) Prf_flat_L 
+apply(blast)
+using Prf.intros(5) apply force
+using L.simps(3) Prf_flat_L apply blast
+using L_flat_Prf apply auto[1]
+apply (smt L.simps(4) Sequ_def mem_Collect_eq)
+using Prf_flat_L 
+apply(fastforce)
+apply(metis Prf.intros(2) flat.simps(3))
+apply(metis Prf.intros(3) flat.simps(4))
+apply(erule Prf.cases)
+apply(simp)
+apply(simp)
+apply(auto)
+using L_flat_Prf apply auto[1]
+apply (smt Collect_cong L.simps(6) mem_Collect_eq)
+using Prf_Star_flat_L 
+apply(fastforce)
+done
+
 
 section {* Values Sets *}
 
@@ -450,6 +512,7 @@
 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 | "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)"
+| "injval (STAR r) c (Seq v (Star vs)) = Star ((injval r c v) # vs)" 
 
 fun 
   lex :: "rexp \<Rightarrow> string \<Rightarrow> val option"
@@ -477,6 +540,7 @@
      (if flat v1 = [] then Right(projval r2 c v2) 
       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
                           else Seq (projval r1 c v1) v2)"
+| "projval (STAR r) c (Star (v # vs)) = Seq (projval r c v) (Star vs)"
 
 
 
@@ -496,8 +560,6 @@
 apply(auto)
 done
 
-(* HERE *)
-
 lemma v3:
   assumes "\<turnstile> v : der c r" 
   shows "\<turnstile> (injval r c v) : r"
@@ -505,70 +567,83 @@
 apply(induct arbitrary: v rule: der.induct)
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(case_tac "c = c'")
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis Prf.intros(5))
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis Prf.intros(2))
 apply (metis Prf.intros(3))
 apply(simp)
 apply(case_tac "nullable r1")
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(auto)[1]
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(auto)[1]
 apply (metis Prf.intros(1))
 apply(auto)[1]
 apply (metis Prf.intros(1) mkeps_nullable)
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(auto)[1]
 apply(rule Prf.intros)
 apply(auto)[2]
-done
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)
+apply (metis Prf.intros(6) Prf.intros(7))
+by (metis Prf.intros(7))
 
 lemma v3_proj:
-  assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
-  shows "\<turnstile> (projval r c v) : der c r"
+  assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
+  shows "\<Turnstile> (projval r c v) : der c r"
 using assms
-apply(induct rule: Prf.induct)
+apply(induct rule: NPrf.induct)
 prefer 4
 apply(simp)
 prefer 4
 apply(simp)
-apply (metis Prf.intros(4))
+apply (metis NPrf.intros(4))
 prefer 2
 apply(simp)
-apply (metis Prf.intros(2))
+apply (metis NPrf.intros(2))
 prefer 2
 apply(simp)
-apply (metis Prf.intros(3))
+apply (metis NPrf.intros(3))
 apply(auto)
-apply(rule Prf.intros)
+apply(rule NPrf.intros)
 apply(simp)
-apply (metis Prf_flat_L nullable_correctness)
-apply(rule Prf.intros)
-apply(rule Prf.intros)
+apply (metis NPrf_imp_Prf not_nullable_flat)
+apply(rule NPrf.intros)
+apply(rule NPrf.intros)
 apply (metis Cons_eq_append_conv)
 apply(simp)
-apply(rule Prf.intros)
+apply(rule NPrf.intros)
 apply (metis Cons_eq_append_conv)
 apply(simp)
+(* Star case *)
+apply(rule NPrf.intros)
+apply (metis Cons_eq_append_conv)
+apply(auto)
 done
 
 lemma v4:
@@ -578,44 +653,51 @@
 apply(induct arbitrary: v rule: der.induct)
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(simp)
 apply(case_tac "c = c'")
 apply(simp)
 apply(auto)[1]
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(simp)
 apply(case_tac "nullable r1")
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
+apply(simp_all (no_asm_use))[7]
 apply(auto)[1]
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(clarify)
 apply(simp only: injval.simps flat.simps)
 apply(auto)[1]
 apply (metis mkeps_flat)
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[7]
 done
 
 lemma v4_proj:
-  assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
+  assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
   shows "c # flat (projval r c v) = flat v"
 using assms
-apply(induct rule: Prf.induct)
+apply(induct rule: NPrf.induct)
 prefer 4
 apply(simp)
 prefer 4
@@ -625,15 +707,19 @@
 prefer 2
 apply(simp)
 apply(auto)
-by (metis Cons_eq_append_conv)
+apply (metis Cons_eq_append_conv)
+apply(simp add: append_eq_Cons_conv)
+apply(auto)
+done
 
 lemma v4_proj2:
-  assumes "\<turnstile> v : r" and "(flat v) = c # s"
+  assumes "\<Turnstile> v : r" and "(flat v) = c # s"
   shows "flat (projval r c v) = s"
 using assms
 by (metis list.inject v4_proj)
 
 
+
 section {* Alternative Posix definition *}
 
 inductive 
@@ -646,7 +732,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)"
+| "[] \<in> STAR r \<rightarrow> Star []"
 
 lemma PMatch_mkeps:
   assumes "nullable r"
@@ -666,8 +753,9 @@
 apply(simp)
 apply (rule PMatch.intros)
 apply(simp)
-by (metis nullable_correctness)
-
+apply (metis nullable_correctness)
+apply(metis PMatch.intros(7))
+done
 
 lemma PMatch1:
   assumes "s \<in> r \<rightarrow> v"
@@ -680,6 +768,22 @@
 apply (metis Prf.intros(2))
 apply (metis Prf.intros(3))
 apply (metis Prf.intros(1))
+apply (metis Prf.intros(7))
+by (metis Prf.intros(6))
+
+lemma PMatch1N:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "\<Turnstile> v : r" 
+using assms
+apply(induct s r v rule: PMatch.induct)
+apply(auto)
+apply (metis NPrf.intros(4))
+apply (metis NPrf.intros(5))
+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)
 done
 
 lemma PMatch_Values:
@@ -696,38 +800,40 @@
 apply(induct c r arbitrary: s v rule: der.induct)
 apply(auto)
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(case_tac "c = c'")
 apply(simp)
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis PMatch.intros(2))
 apply(simp)
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis PMatch.intros(3))
 apply(clarify)
 apply(rule PMatch.intros)
 apply metis
 apply(simp add: L_flat_Prf)
 apply(auto)[1]
-thm v3_proj
+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(simp)
+apply (metis NPrf_imp_Prf)
+defer
+(* SEQ case *)
 apply(case_tac "nullable r1")
 apply(simp)
-defer
+prefer 2
 apply(simp)
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(clarify)
 apply(subst append.simps(2)[symmetric])
 apply(rule PMatch.intros)
@@ -736,6 +842,7 @@
 apply(auto)[1]
 apply(simp add: L_flat_Prf)
 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)
@@ -743,14 +850,15 @@
 apply(rule_tac x="projval r1 c v" in exI)
 apply(rule conjI)
 apply (metis v4_proj2)
-apply(simp)
+apply (metis NPrf_imp_Prf)
 apply metis
+defer
 (* nullable case *)
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(clarify)
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(clarify)
 apply(subst append.simps(2)[symmetric])
 apply(rule PMatch.intros)
@@ -759,16 +867,17 @@
 apply(auto)[1]
 apply(simp add: L_flat_Prf)
 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 v4_proj2)
+apply (metis NPrf_imp_Prf v4_proj2)
 apply(simp)
+defer
 (* interesting case *)
 apply(clarify)
 apply(simp)
-thm L.simps
 apply(subst (asm) L.simps(4)[symmetric])
 apply(simp only: L_flat_Prf)
 apply(simp)
@@ -783,12 +892,33 @@
 apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
 apply(drule mp)
 apply(simp)
-apply (metis append_Cons butlast_snoc last_snoc neq_Nil_conv rotate1.simps(2) v4_proj2)
+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(rule NPrf_imp_Prf)
 apply(rule v3_proj)
-apply(simp)
-by (metis Cons_eq_append_conv)
+defer
+apply (metis Cons_eq_append_conv)
+(* Star case *)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(rotate_tac 2)
+apply(frule_tac PMatch1)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+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 *)
+
+
 
 lemma lex_correct1:
   assumes "s \<notin> L r"