--- a/thys/Spec.thy Fri Aug 11 20:29:01 2017 +0100
+++ b/thys/Spec.thy Fri Aug 18 14:51:29 2017 +0100
@@ -176,35 +176,6 @@
-section {* Lemmas about ders *}
-
-(* not really needed *)
-
-lemma ders_ZERO:
- shows "ders s (ZERO) = ZERO"
-apply(induct s)
-apply(simp_all)
-done
-
-lemma ders_ONE:
- shows "ders s (ONE) = (if s = [] then ONE else ZERO)"
-apply(induct s)
-apply(simp_all add: ders_ZERO)
-done
-
-lemma ders_CHAR:
- shows "ders s (CHAR c) =
- (if s = [c] then ONE else
- (if s = [] then (CHAR c) else ZERO))"
-apply(induct s)
-apply(simp_all add: ders_ZERO ders_ONE)
-done
-
-lemma ders_ALT:
- shows "ders s (ALT r1 r2) = ALT (ders s r1) (ders s r2)"
-by (induct s arbitrary: r1 r2)(simp_all)
-
-
section {* Values *}
datatype val =
@@ -236,109 +207,33 @@
"flat (Stars vs) = flats vs"
by (induct vs) (auto)
-
-section {* Relation between values and regular expressions *}
-
-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"
-| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
-| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
-| "\<turnstile> Void : ONE"
-| "\<turnstile> Char c : CHAR c"
-| "\<forall>v \<in> set vs. \<turnstile> v : r \<Longrightarrow> \<turnstile> Stars vs : STAR r"
-
-inductive_cases Prf_elims:
- "\<turnstile> v : ZERO"
- "\<turnstile> v : SEQ r1 r2"
- "\<turnstile> v : ALT r1 r2"
- "\<turnstile> v : ONE"
- "\<turnstile> v : CHAR c"
- "\<turnstile> vs : STAR r"
-
lemma Star_concat:
assumes "\<forall>s \<in> set ss. s \<in> A"
shows "concat ss \<in> A\<star>"
using assms by (induct ss) (auto)
-lemma Star_string:
+lemma Star_cstring:
assumes "s \<in> A\<star>"
- shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
+ shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])"
using assms
apply(induct rule: Star.induct)
-apply(auto)
+apply(auto)[1]
apply(rule_tac x="[]" in exI)
apply(simp)
+apply(erule exE)
+apply(clarify)
+apply(case_tac "s1 = []")
+apply(rule_tac x="ss" in exI)
+apply(simp)
apply(rule_tac x="s1#ss" in exI)
apply(simp)
done
-lemma Star_val:
- assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
- shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
-using assms
-apply(induct ss)
-apply(auto)
-apply(rule_tac x="[]" in exI)
-apply(simp)
-apply(rule_tac x="v#vs" in exI)
-apply(simp)
-done
-lemma Prf_Stars_append:
- assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"
- shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"
-using assms
-by (auto intro!: Prf.intros elim!: Prf_elims)
-
-lemma Prf_flat_L:
- assumes "\<turnstile> v : r"
- shows "flat v \<in> L r"
-using assms
-by (induct v r rule: Prf.induct)
- (auto simp add: Sequ_def Star_concat)
-
-
-lemma L_flat_Prf1:
- assumes "\<turnstile> v : r"
- shows "flat v \<in> L r"
-using assms
-by (induct) (auto simp add: Sequ_def Star_concat)
-
-lemma L_flat_Prf2:
- assumes "s \<in> L r"
- shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
-using assms
-proof(induct r arbitrary: s)
- case (STAR r s)
- have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> flat v = s" by fact
- have "s \<in> L (STAR r)" by fact
- then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r"
- using Star_string by auto
- then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<turnstile> v : r"
- using IH Star_val by blast
- then show "\<exists>v. \<turnstile> v : STAR r \<and> flat v = s"
- using Prf.intros(6) flat_Stars by blast
-next
- case (SEQ r1 r2 s)
- then show "\<exists>v. \<turnstile> v : SEQ r1 r2 \<and> flat v = s"
- unfolding Sequ_def L.simps by (fastforce intro: Prf.intros)
-next
- case (ALT r1 r2 s)
- then show "\<exists>v. \<turnstile> v : ALT r1 r2 \<and> flat v = s"
- unfolding L.simps by (fastforce intro: Prf.intros)
-qed (auto intro: Prf.intros)
-
-lemma L_flat_Prf:
- shows "L(r) = {flat v | v. \<turnstile> v : r}"
-using L_flat_Prf1 L_flat_Prf2 by blast
-
-
-section {* Canonical Values *}
+section {* Lexical Values *}
inductive
- CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
+ 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"
| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
@@ -347,34 +242,92 @@
| "\<Turnstile> Char c : CHAR c"
| "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
-lemma Prf_CPrf:
- assumes "\<Turnstile> v : r"
- shows "\<turnstile> v : r"
-using assms
-by (induct)(auto intro: Prf.intros)
+inductive_cases Prf_elims:
+ "\<Turnstile> v : ZERO"
+ "\<Turnstile> v : SEQ r1 r2"
+ "\<Turnstile> v : ALT r1 r2"
+ "\<Turnstile> v : ONE"
+ "\<Turnstile> v : CHAR c"
+ "\<Turnstile> vs : STAR r"
-lemma CPrf_Stars_appendE:
+lemma Prf_Stars_appendE:
assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r"
using assms
-apply(erule_tac CPrf.cases)
-apply(auto intro: CPrf.intros)
+by (auto intro: Prf.intros elim!: Prf_elims)
+
+
+lemma Star_cval:
+ assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"
+ shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])"
+using assms
+apply(induct ss)
+apply(auto)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+apply(case_tac "flat v = []")
+apply(rule_tac x="vs" in exI)
+apply(simp)
+apply(rule_tac x="v#vs" in exI)
+apply(simp)
done
-section {* Sets of Lexical and Canonical Values *}
+lemma L_flat_Prf1:
+ assumes "\<Turnstile> v : r"
+ shows "flat v \<in> L r"
+using assms
+by (induct) (auto simp add: Sequ_def Star_concat)
-definition
- LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
-where "LV r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}"
+lemma L_flat_Prf2:
+ assumes "s \<in> L r"
+ shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s"
+using assms
+proof(induct r arbitrary: s)
+ case (STAR r s)
+ have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
+ have "s \<in> L (STAR r)" by fact
+ then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []"
+ using Star_cstring by auto
+ then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []"
+ using IH Star_cval by metis
+ then show "\<exists>v. \<Turnstile> v : STAR r \<and> flat v = s"
+ using Prf.intros(6) flat_Stars by blast
+next
+ case (SEQ r1 r2 s)
+ then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s"
+ unfolding Sequ_def L.simps by (fastforce intro: Prf.intros)
+next
+ case (ALT r1 r2 s)
+ then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s"
+ unfolding L.simps by (fastforce intro: Prf.intros)
+qed (auto intro: Prf.intros)
+
+
+lemma L_flat_Prf:
+ shows "L(r) = {flat v | v. \<Turnstile> v : r}"
+using L_flat_Prf1 L_flat_Prf2 by blast
+
+
+
+section {* Sets of Lexical Values *}
+
+text {*
+ Shows that lexical values are finite for a given regex and string.
+*}
definition
- CV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
-where "CV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"
+ LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
+where "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"
-lemma LV_CV_subset:
- shows "CV r s \<subseteq> LV r s"
-unfolding CV_def LV_def by(auto simp add: Prf_CPrf)
+lemma LV_simps:
+ shows "LV ZERO s = {}"
+ and "LV ONE s = (if s = [] then {Void} else {})"
+ and "LV (CHAR c) s = (if s = [c] then {Char c} else {})"
+ and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
+unfolding LV_def
+by (auto intro: Prf.intros elim: Prf.cases)
+
abbreviation
"Prefixes s \<equiv> {s'. prefixeq s' s}"
@@ -389,13 +342,6 @@
shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"
by (auto simp add: suffixeq_def Cons_eq_append_conv)
-lemma CV_simps:
- shows "CV ZERO s = {}"
- and "CV ONE s = (if s = [] then {Void} else {})"
- and "CV (CHAR c) s = (if s = [c] then {Char c} else {})"
- and "CV (ALT r1 r2) s = Left ` CV r1 s \<union> Right ` CV r2 s"
-unfolding CV_def
-by (auto intro: CPrf.intros elim: CPrf.cases)
lemma finite_Suffixes:
shows "finite (Suffixes s)"
@@ -423,34 +369,17 @@
ultimately show "finite (Prefixes s)" by simp
qed
-lemma CV_SEQ_subset:
- "CV (SEQ r1 r2) s \<subseteq> (\<lambda>(v1,v2). Seq v1 v2) ` ((\<Union>s' \<in> Prefixes s. CV r1 s') \<times> (\<Union>s' \<in> Suffixes s. CV r2 s'))"
-unfolding image_def CV_def prefixeq_def suffixeq_def
-by (auto elim: CPrf.cases)
-
-lemma CV_STAR_subset:
- "CV (STAR r) s \<subseteq> {Stars []} \<union>
- (\<lambda>(v,vs). Stars (v#vs)) ` ((\<Union>s' \<in> Prefixes s. CV r s') \<times> (\<Union>s2 \<in> SSuffixes s. Stars -` (CV (STAR r) s2)))"
-unfolding image_def CV_def prefixeq_def suffix_def
-apply(auto)
-apply(erule CPrf.cases)
-apply(auto)
-apply(case_tac vs)
-apply(auto intro: CPrf.intros)
-done
-
-
-lemma CV_STAR_finite:
- assumes "\<forall>s. finite (CV r s)"
- shows "finite (CV (STAR r) s)"
+lemma LV_STAR_finite:
+ assumes "\<forall>s. finite (LV r s)"
+ shows "finite (LV (STAR r) s)"
proof(induct s rule: length_induct)
fix s::"char list"
- assume "\<forall>s'. length s' < length s \<longrightarrow> finite (CV (STAR r) s')"
- then have IH: "\<forall>s' \<in> SSuffixes s. finite (CV (STAR r) s')"
+ assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')"
+ then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')"
by (auto simp add: suffix_def)
def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)"
- def S1 \<equiv> "\<Union>s' \<in> Prefixes s. CV r s'"
- def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (CV (STAR r) s2)"
+ def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r s'"
+ def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)"
have "finite S1" using assms
unfolding S1_def by (simp_all add: finite_Prefixes)
moreover
@@ -459,44 +388,53 @@
ultimately
have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
moreover
- have "CV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" unfolding S1_def S2_def f_def
- by (rule CV_STAR_subset)
+ have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)"
+ unfolding S1_def S2_def f_def
+ unfolding LV_def image_def prefixeq_def suffix_def
+ apply(auto elim: Prf_elims)
+ apply(erule Prf_elims)
+ apply(auto)
+ apply(case_tac vs)
+ apply(auto intro: Prf.intros)
+ done
ultimately
- show "finite (CV (STAR r) s)" by (simp add: finite_subset)
+ show "finite (LV (STAR r) s)" by (simp add: finite_subset)
qed
-lemma CV_finite:
- shows "finite (CV r s)"
+lemma LV_finite:
+ shows "finite (LV r s)"
proof(induct r arbitrary: s)
case (ZERO s)
- show "finite (CV ZERO s)" by (simp add: CV_simps)
+ show "finite (LV ZERO s)" by (simp add: LV_simps)
next
case (ONE s)
- show "finite (CV ONE s)" by (simp add: CV_simps)
+ show "finite (LV ONE s)" by (simp add: LV_simps)
next
case (CHAR c s)
- show "finite (CV (CHAR c) s)" by (simp add: CV_simps)
+ show "finite (LV (CHAR c) s)" by (simp add: LV_simps)
next
case (ALT r1 r2 s)
- then show "finite (CV (ALT r1 r2) s)" by (simp add: CV_simps)
+ then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
next
case (SEQ r1 r2 s)
def f \<equiv> "\<lambda>(v1, v2). Seq v1 v2"
- def S1 \<equiv> "\<Union>s' \<in> Prefixes s. CV r1 s'"
- def S2 \<equiv> "\<Union>s' \<in> Suffixes s. CV r2 s'"
- have IHs: "\<And>s. finite (CV r1 s)" "\<And>s. finite (CV r2 s)" by fact+
+ def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r1 s'"
+ def S2 \<equiv> "\<Union>s' \<in> Suffixes s. LV r2 s'"
+ have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+
then have "finite S1" "finite S2" unfolding S1_def S2_def
by (simp_all add: finite_Prefixes finite_Suffixes)
moreover
- have "CV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)"
- unfolding f_def S1_def S2_def by (auto simp add: CV_SEQ_subset)
+ have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)"
+ unfolding f_def S1_def S2_def
+ unfolding LV_def image_def prefixeq_def suffixeq_def
+ by (auto elim: Prf.cases)
ultimately
- show "finite (CV (SEQ r1 r2) s)"
+ show "finite (LV (SEQ r1 r2) s)"
by (simp add: finite_subset)
next
case (STAR r s)
- then show "finite (CV (STAR r) s)" by (simp add: CV_STAR_finite)
+ then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite)
qed
@@ -533,14 +471,6 @@
by (induct s r v rule: Posix.induct)
(auto simp add: Sequ_def)
-lemma Posix_Prf:
- assumes "s \<in> r \<rightarrow> v"
- shows "\<turnstile> v : r"
-using assms
-apply(induct s r v rule: Posix.induct)
-apply(auto intro!: Prf.intros elim!: Prf_elims)
-done
-
text {*
Our Posix definition determines a unique value.
*}
@@ -616,30 +546,31 @@
Our POSIX value is a canonical value.
*}
-lemma Posix_CV:
+lemma Posix_LV:
assumes "s \<in> r \<rightarrow> v"
- shows "v \<in> CV r s"
+ shows "v \<in> LV r s"
using assms
apply(induct rule: Posix.induct)
-apply(auto simp add: CV_def intro: CPrf.intros elim: CPrf.cases)
+apply(auto simp add: LV_def intro: Prf.intros elim: Prf.cases)
apply(rotate_tac 5)
-apply(erule CPrf.cases)
+apply(erule Prf.cases)
apply(simp_all)
-apply(rule CPrf.intros)
+apply(rule Prf.intros)
apply(simp_all)
done
+(*
lemma test2:
assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
- shows "(Stars vs) \<in> CV (STAR r) (flat (Stars vs))"
+ shows "(Stars vs) \<in> LV (STAR r) (flat (Stars vs))"
using assms
apply(induct vs)
-apply(auto simp add: CV_def)
-apply(rule CPrf.intros)
+apply(auto simp add: LV_def)
+apply(rule Prf.intros)
apply(simp)
-apply(rule CPrf.intros)
+apply(rule Prf.intros)
apply(simp_all)
-by (metis (no_types, lifting) CV_def Posix_CV mem_Collect_eq)
-
+by (metis (no_types, lifting) LV_def Posix_LV mem_Collect_eq)
+*)
end
\ No newline at end of file