--- 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"