--- a/thys3/PosixSpec.thy Wed Feb 15 11:52:22 2023 +0000
+++ b/thys3/PosixSpec.thy Thu Feb 16 23:23:22 2023 +0000
@@ -46,6 +46,9 @@
| "\<Turnstile> Void : ONE"
| "\<Turnstile> Char c : CH c"
| "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
+| "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> [];
+ \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = [];
+ length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n"
inductive_cases Prf_elims:
"\<Turnstile> v : ZERO"
@@ -54,6 +57,7 @@
"\<Turnstile> v : ONE"
"\<Turnstile> v : CH c"
"\<Turnstile> vs : STAR r"
+ "\<Turnstile> vs : NTIMES r n"
lemma Prf_Stars_appendE:
assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
@@ -61,6 +65,28 @@
using assms
by (auto intro: Prf.intros elim!: Prf_elims)
+lemma Pow_cstring:
+ fixes A::"string set"
+ assumes "s \<in> A ^^ n"
+ shows "\<exists>ss1 ss2. concat (ss1 @ ss2) = s \<and> length (ss1 @ ss2) = n \<and>
+ (\<forall>s \<in> set ss1. s \<in> A \<and> s \<noteq> []) \<and> (\<forall>s \<in> set ss2. s \<in> A \<and> s = [])"
+using assms
+apply(induct n arbitrary: s)
+ apply(auto)[1]
+ apply(auto simp add: Sequ_def)
+ apply(drule_tac x="s2" in meta_spec)
+ apply(simp)
+apply(erule exE)+
+ apply(clarify)
+apply(case_tac "s1 = []")
+apply(simp)
+apply(rule_tac x="ss1" in exI)
+apply(rule_tac x="s1 # ss2" in exI)
+apply(simp)
+apply(rule_tac x="s1 # ss1" in exI)
+apply(rule_tac x="ss2" in exI)
+ apply(simp)
+ done
lemma flats_Prf_value:
assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"
@@ -75,15 +101,48 @@
apply(simp)
apply(rule_tac x="v#vs" in exI)
apply(simp)
-done
+ done
+
+lemma Aux:
+ assumes "\<forall>s\<in>set ss. s = []"
+ shows "concat ss = []"
+using assms
+by (induct ss) (auto)
+lemma flats_cval:
+ assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"
+ shows "\<exists>vs1 vs2. flats (vs1 @ vs2) = concat ss \<and> length (vs1 @ vs2) = length ss \<and>
+ (\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []) \<and>
+ (\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = [])"
+using assms
+apply(induct ss rule: rev_induct)
+apply(rule_tac x="[]" in exI)+
+apply(simp)
+apply(simp)
+apply(clarify)
+apply(case_tac "flat v = []")
+apply(rule_tac x="vs1" in exI)
+apply(rule_tac x="v#vs2" in exI)
+apply(simp)
+apply(rule_tac x="vs1 @ [v]" in exI)
+apply(rule_tac x="vs2" in exI)
+apply(simp)
+by (simp add: Aux)
+
+lemma pow_Prf:
+ assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<in> A"
+ shows "flats vs \<in> A ^^ (length vs)"
+ using assms
+ by (induct vs) (auto)
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)
-
+ using assms
+ apply (induct v r rule: Prf.induct)
+ apply(auto simp add: Sequ_def Star_concat lang_pow_add)
+ by (metis pow_Prf)
+
lemma L_flat_Prf2:
assumes "s \<in> L r"
shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s"
@@ -105,7 +164,30 @@
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)
+ unfolding L.simps by (fastforce intro: Prf.intros)
+next
+ case (NTIMES r n)
+ have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
+ have "s \<in> L (NTIMES r n)" by fact
+ then obtain ss1 ss2 where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = n"
+ "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []"
+ using Pow_cstring by force
+ then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = n"
+ "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []"
+ using IH flats_cval
+ apply -
+ apply(drule_tac x="ss1 @ ss2" in meta_spec)
+ apply(drule_tac x="r" in meta_spec)
+ apply(drule meta_mp)
+ apply(simp)
+ apply (metis Un_iff)
+ apply(clarify)
+ apply(drule_tac x="vs1" in meta_spec)
+ apply(drule_tac x="vs2" in meta_spec)
+ apply(simp)
+ done
+ then show "\<exists>v. \<Turnstile> v : NTIMES r n \<and> flat v = s"
+ using Prf.intros(7) flat_Stars by blast
qed (auto intro: Prf.intros)
@@ -130,9 +212,11 @@
and "LV ONE s = (if s = [] then {Void} else {})"
and "LV (CH c) s = (if s = [c] then {Char c} else {})"
and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
+ and "LV (NTIMES r 0) s = (if s = [] then {Stars []} else {})"
unfolding LV_def
-by (auto intro: Prf.intros elim: Prf.cases)
-
+ apply (auto intro: Prf.intros elim: Prf.cases)
+ by (metis Prf.intros(7) append.right_neutral empty_iff list.set(1) list.size(3))
+
abbreviation
"Prefixes s \<equiv> {s'. prefix s' s}"
@@ -174,6 +258,64 @@
ultimately show "finite (Prefixes s)" by simp
qed
+definition
+ "Stars_Append Vs1 Vs2 \<equiv> {Stars (vs1 @ vs2) | vs1 vs2. Stars vs1 \<in> Vs1 \<and> Stars vs2 \<in> Vs2}"
+
+lemma finite_Stars_Append:
+ assumes "finite Vs1" "finite Vs2"
+ shows "finite (Stars_Append Vs1 Vs2)"
+ using assms
+proof -
+ define UVs1 where "UVs1 \<equiv> Stars -` Vs1"
+ define UVs2 where "UVs2 \<equiv> Stars -` Vs2"
+ from assms have "finite UVs1" "finite UVs2"
+ unfolding UVs1_def UVs2_def
+ by(simp_all add: finite_vimageI inj_on_def)
+ then have "finite ((\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2))"
+ by simp
+ moreover
+ have "Stars_Append Vs1 Vs2 = (\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2)"
+ unfolding Stars_Append_def UVs1_def UVs2_def by auto
+ ultimately show "finite (Stars_Append Vs1 Vs2)"
+ by simp
+qed
+
+lemma LV_NTIMES_subset:
+ "LV (NTIMES r n) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (NTIMES r i) [])"
+apply(auto simp add: LV_def)
+apply(auto elim!: Prf_elims)
+ apply(auto simp add: Stars_Append_def)
+ apply(rule_tac x="vs1" in exI)
+ apply(rule_tac x="vs2" in exI)
+ apply(auto)
+ using Prf.intros(6) apply(auto)
+ apply(rule_tac x="length vs2" in bexI)
+ thm Prf.intros
+ apply(subst append.simps(1)[symmetric])
+ apply(rule Prf.intros)
+ apply(auto)[1]
+ apply(auto)[1]
+ apply(simp)
+ apply(simp)
+ done
+
+lemma LV_NTIMES_Suc_empty:
+ shows "LV (NTIMES r (Suc n)) [] =
+ (\<lambda>(v, vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTIMES r n) [])))"
+unfolding LV_def
+apply(auto elim!: Prf_elims simp add: image_def)
+apply(case_tac vs1)
+apply(auto)
+apply(case_tac vs2)
+apply(auto)
+apply(subst append.simps(1)[symmetric])
+apply(rule Prf.intros)
+apply(auto)
+apply(subst append.simps(1)[symmetric])
+apply(rule Prf.intros)
+apply(auto)
+ done
+
lemma LV_STAR_finite:
assumes "\<forall>s. finite (LV r s)"
shows "finite (LV (STAR r) s)"
@@ -215,7 +357,22 @@
ultimately
show "finite (LV (STAR r) s)" by (simp add: finite_subset)
qed
-
+
+lemma finite_NTimes_empty:
+ assumes "\<And>s. finite (LV r s)"
+ shows "finite (LV (NTIMES r n) [])"
+ using assms
+ apply(induct n)
+ apply(auto simp add: LV_simps)
+ apply(subst LV_NTIMES_Suc_empty)
+ apply(rule finite_imageI)
+ apply(rule finite_cartesian_product)
+ using assms apply simp
+ apply(rule finite_vimageI)
+ apply(simp)
+ apply(simp add: inj_on_def)
+ done
+
lemma LV_finite:
shows "finite (LV r s)"
@@ -251,6 +408,15 @@
next
case (STAR r s)
then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite)
+next
+ case (NTIMES r n s)
+ have "\<And>s. finite (LV r s)" by fact
+ then have "finite (Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (NTIMES r i) []))"
+ apply(rule_tac finite_Stars_Append)
+ apply (simp add: LV_STAR_finite)
+ using finite_NTimes_empty by blast
+ then show "finite (LV (NTIMES r n) s)"
+ by (metis LV_NTIMES_subset finite_subset)
qed
@@ -271,6 +437,11 @@
\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
\<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
| Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []"
+| Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n;
+ \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))\<rbrakk>
+ \<Longrightarrow> (s1 @ s2) \<in> NTIMES r n \<rightarrow> Stars (v # vs)"
+| Posix_NTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk>
+ \<Longrightarrow> [] \<in> NTIMES r n \<rightarrow> Stars vs"
inductive_cases Posix_elims:
"s \<in> ZERO \<rightarrow> v"
@@ -279,19 +450,47 @@
"s \<in> ALT r1 r2 \<rightarrow> v"
"s \<in> SEQ r1 r2 \<rightarrow> v"
"s \<in> STAR r \<rightarrow> v"
+ "s \<in> NTIMES r n \<rightarrow> v"
lemma Posix1:
assumes "s \<in> r \<rightarrow> v"
shows "s \<in> L r" "flat v = s"
using assms
- by(induct s r v rule: Posix.induct)
- (auto simp add: Sequ_def)
+ apply(induct s r v rule: Posix.induct)
+ apply(auto simp add: pow_empty_iff)
+ apply (metis Suc_pred concI lang_pow.simps(2))
+ by (meson ex_in_conv set_empty)
+
+lemma Posix1a:
+ 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)
+ apply (metis Prf.intros(6) Prf_elims(6) set_ConsD val.inject(5))
+ prefer 2
+ apply (metis Posix1(2) Prf.intros(7) append_Nil empty_iff list.set(1))
+ apply(erule Prf_elims)
+ apply(auto)
+ apply(subst append.simps(2)[symmetric])
+ apply(rule Prf.intros)
+ apply(auto)
+ done
text \<open>
For a give value and string, our Posix definition
determines a unique value.
\<close>
+lemma List_eq_zipI:
+ assumes "list_all2 (\<lambda>v1 v2. v1 = v2) vs1 vs2"
+ and "length vs1 = length vs2"
+ shows "vs1 = vs2"
+ using assms
+ apply(induct vs1 vs2 rule: list_all2_induct)
+ apply(auto)
+ done
+
lemma Posix_determ:
assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
shows "v1 = v2"
@@ -356,6 +555,29 @@
case (Posix_STAR2 r v2)
have "[] \<in> STAR r \<rightarrow> v2" by fact
then show "Stars [] = v2" by cases (auto simp add: Posix1)
+next
+ case (Posix_NTIMES2 vs r n v2)
+ then show "Stars vs = v2"
+ apply(erule_tac Posix_elims)
+ apply(auto)
+ apply (simp add: Posix1(2))
+ apply(rule List_eq_zipI)
+ apply(auto simp add: list_all2_iff)
+ by (meson in_set_zipE)
+next
+ case (Posix_NTIMES1 s1 r v s2 n vs)
+ have "(s1 @ s2) \<in> NTIMES r n \<rightarrow> v2"
+ "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []"
+ "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1 )))" by fact+
+ then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs')"
+ apply(cases) apply (auto simp add: append_eq_append_conv2)
+ using Posix1(1) apply fastforce
+ apply (metis One_nat_def Posix1(1) Posix_NTIMES1.hyps(7) append.right_neutral append_self_conv2)
+ using Posix1(2) by blast
+ moreover
+ have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+ "\<And>v2. s2 \<in> NTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+ ultimately show "Stars (v # vs) = v2" by auto
qed
@@ -368,13 +590,9 @@
shows "v \<in> LV r s"
using assms unfolding LV_def
apply(induct rule: Posix.induct)
- apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)
- done
+ apply(auto simp add: intro!: Prf.intros elim!: Prf_elims Posix1a)
+ apply (smt (verit, best) One_nat_def Posix1a Posix_NTIMES1 L.simps(7))
+ using Posix1a Posix_NTIMES2 by blast
-lemma Posix_Prf:
- assumes "s \<in> r \<rightarrow> v"
- shows "\<Turnstile> v : r"
- using assms Posix_LV LV_def
- by simp
end