--- a/thys/SpecExt.thy Thu Oct 05 12:45:13 2017 +0100
+++ b/thys/SpecExt.thy Sat Oct 07 22:16:16 2017 +0100
@@ -311,8 +311,9 @@
apply(subst Pow_Sequ_Un)
apply(simp)
apply(simp only: Der_union Der_empty)
-apply(simp)
-apply(simp add: nullable_correctness del: Der_UNION)
+ apply(simp)
+(* FROMNTIMES *)
+ apply(simp add: nullable_correctness del: Der_UNION)
apply(subst Sequ_Union_in)
apply(subst Der_Pow_Sequ[symmetric])
apply(subst Pow.simps[symmetric])
@@ -326,7 +327,8 @@
apply(auto simp add: Sequ_def)[1]
apply(drule Pow_decomp)
apply(auto)[1]
-apply (metis append_Cons)
+ apply (metis append_Cons)
+(* NMTIMES *)
apply(simp add: nullable_correctness del: Der_UNION)
apply(rule impI)
apply(rule conjI)
@@ -663,10 +665,10 @@
case (FROMNTIMES 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 (FROMNTIMES r n)" by fact
- then obtain ss1 ss2 m where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = m" "n \<le> m"
+ then obtain ss1 ss2 k where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = k" "n \<le> k"
"\<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) = m" "n \<le> m"
+ then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = k" "n \<le> k"
"\<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 -
@@ -723,11 +725,26 @@
apply(simp)
done
then show "\<exists>v. \<Turnstile> v : NMTIMES r n m \<and> flat v = s"
- apply(rule_tac x="Stars (vs1 @ vs2)" in exI)
+ apply(case_tac "length vs1 \<le> n")
+ apply(rule_tac x="Stars (vs1 @ take (n - length vs1) vs2)" in exI)
apply(simp)
- apply(rule Prf.intros)
- apply(auto)
- sorry
+ apply(subgoal_tac "flats (take (n - length vs1) vs2) = []")
+ prefer 2
+ apply (meson flats_empty in_set_takeD)
+ apply(clarify)
+ apply(rule conjI)
+ apply(rule Prf.intros)
+ apply(simp)
+ apply (meson in_set_takeD)
+ apply(simp)
+ apply(simp)
+ apply (simp add: flats_empty)
+ apply(rule_tac x="Stars vs1" in exI)
+ apply(simp)
+ apply(rule conjI)
+ apply(rule Prf.intros)
+ apply(auto)
+ done
next
case (UPNTIMES r n s)
have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
@@ -806,6 +823,58 @@
ultimately show "finite (Prefixes s)" by simp
qed
+definition
+ "Stars_Cons V Vs \<equiv> {Stars (v # vs) | v vs. v \<in> V \<and> Stars vs \<in> Vs}"
+
+definition
+ "Stars_Append Vs1 Vs2 \<equiv> {Stars (vs1 @ vs2) | vs1 vs2. Stars vs1 \<in> Vs1 \<and> Stars vs2 \<in> Vs2}"
+
+fun Stars_Pow :: "val set \<Rightarrow> nat \<Rightarrow> val set"
+where
+ "Stars_Pow Vs 0 = {Stars []}"
+| "Stars_Pow Vs (Suc n) = Stars_Cons Vs (Stars_Pow Vs n)"
+
+lemma finite_Stars_Cons:
+ assumes "finite V" "finite Vs"
+ shows "finite (Stars_Cons V Vs)"
+ using assms
+proof -
+ from assms(2) have "finite (Stars -` Vs)"
+ by(simp add: finite_vimageI inj_on_def)
+ with assms(1) have "finite (V \<times> (Stars -` Vs))"
+ by(simp)
+ then have "finite ((\<lambda>(v, vs). Stars (v # vs)) ` (V \<times> (Stars -` Vs)))"
+ by simp
+ moreover have "Stars_Cons V Vs = (\<lambda>(v, vs). Stars (v # vs)) ` (V \<times> (Stars -` Vs))"
+ unfolding Stars_Cons_def by auto
+ ultimately show "finite (Stars_Cons V Vs)"
+ by simp
+qed
+
+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 finite_Stars_Pow:
+ assumes "finite Vs"
+ shows "finite (Stars_Pow Vs n)"
+by (induct n) (simp_all add: finite_Stars_Cons assms)
+
lemma LV_STAR_finite:
assumes "\<forall>s. finite (LV r s)"
shows "finite (LV (STAR r) s)"
@@ -816,18 +885,20 @@
by (auto simp add: strict_suffix_def)
define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)"
define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'"
- define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)"
+ define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. LV (STAR r) s2"
have "finite S1" using assms
unfolding S1_def by (simp_all add: finite_Prefixes)
moreover
with IH have "finite S2" unfolding S2_def
- by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI)
+ by (auto simp add: finite_SSuffixes)
ultimately
- have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
+ have "finite ({Stars []} \<union> Stars_Cons S1 S2)"
+ by (simp add: finite_Stars_Cons)
moreover
- have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)"
- unfolding S1_def S2_def f_def
- unfolding LV_def image_def prefix_def strict_suffix_def
+ have "LV (STAR r) s \<subseteq> {Stars []} \<union> (Stars_Cons S1 S2)"
+ unfolding S1_def S2_def f_def LV_def Stars_Cons_def
+ unfolding prefix_def strict_suffix_def
+ unfolding image_def
apply(auto)
apply(case_tac x)
apply(auto elim: Prf_elims)
@@ -837,12 +908,12 @@
apply(auto intro: Prf.intros)
apply(rule exI)
apply(rule conjI)
- apply(rule_tac x="flat a" in exI)
+ apply(rule_tac x="flats list" in exI)
apply(rule conjI)
- apply(rule_tac x="flats list" in exI)
+ apply(rule_tac x="flat a" in exI)
apply(simp)
apply(blast)
- using Prf.intros(6) by blast
+ using Prf.intros(6) flat_Stars by blast
ultimately
show "finite (LV (STAR r) s)" by (simp add: finite_subset)
qed
@@ -851,37 +922,6 @@
"LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s"
by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims)
-
-lemma LV_NTIMES_0:
- shows "LV (NTIMES r 0) s \<subseteq> {Stars []}"
-unfolding LV_def
-apply(auto elim: Prf_elims)
-done
-
-lemma LV_NTIMES_1:
- shows "LV (NTIMES r 1) s \<subseteq> (\<lambda>v. Stars [v]) ` (LV r s)"
-unfolding LV_def
-apply(auto elim!: Prf_elims)
-apply(case_tac vs1)
-apply(simp)
-apply(case_tac vs2)
-apply(simp)
-apply(simp)
-apply(simp)
-done
-
-lemma LV_NTIMES_2:
- shows "LV (NTIMES r 2) [] \<subseteq> (\<lambda>(v1,v2). Stars [v1,v2]) ` (LV r [] \<times> LV r [])"
-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(case_tac list)
-apply(auto)
-done
-
lemma LV_NTIMES_3:
shows "LV (NTIMES r (Suc n)) [] = (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTIMES r n) [])))"
unfolding LV_def
@@ -896,66 +936,147 @@
apply(subst append.simps(1)[symmetric])
apply(rule Prf.intros)
apply(auto)
-done
-
-thm card_cartesian_product
-
-lemma finite_list:
- assumes "finite A"
- shows "finite {vs. \<forall>v\<in>set vs. v \<in> A \<and> length vs = n}"
- apply(induct n)
- apply(simp)
- apply (smt Collect_cong empty_iff finite.emptyI finite.insertI
- in_listsI list.set(1) lists_empty mem_Collect_eq singleton_conv2)
- apply(rule_tac B="{[]} \<union> (\<lambda>(v,vs). v # vs) `(A \<times> {vs. \<forall>v\<in>set vs. v \<in> A \<and> length vs = n})" in finite_subset)
- apply(auto simp add: image_def)[1]
- apply(case_tac x)
- apply(simp)
- apply(simp)
- apply(simp)
- apply(rule finite_imageI)
- using assms
- apply(simp)
- done
-
-lemma test:
- "LV (NTIMES r n) [] \<subseteq> Stars ` {vs. \<forall>v \<in> set vs. v \<in> LV r [] \<and> length vs = n}"
-apply(auto simp add: LV_def elim: Prf_elims)
-done
+ done
-lemma test3:
- "LV (FROMNTIMES r n) [] \<subseteq> Stars ` {vs. \<forall>v \<in> set vs. v \<in> LV r [] \<and> length vs = n}"
- apply(auto simp add: image_def LV_def elim!: Prf_elims)
- apply blast
- apply(case_tac vs)
+lemma LV_FROMNTIMES_3:
+ shows "LV (FROMNTIMES r (Suc n)) [] =
+ (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (FROMNTIMES 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 (metis le_imp_less_Suc length_greater_0_conv less_antisym list.exhaust list.set_intros(1) not_less_eq zero_le)
+ prefer 2
+ using nth_mem apply blast
+ apply(case_tac vs1)
+ apply (smt Groups.add_ac(2) Prf.intros(9) add.right_neutral add_Suc_right append.simps(1) insert_iff length_append list.set(2) list.size(3) list.size(4))
apply(auto)
- done
-
-
+done
+
+lemma LV_NTIMES_4:
+ "LV (NTIMES r n) [] = Stars_Pow (LV r []) n"
+ apply(induct n)
+ apply(simp add: LV_def)
+ apply(auto elim!: Prf_elims simp add: image_def)[1]
+ apply(subst append.simps[symmetric])
+ apply(rule Prf.intros)
+ apply(simp_all)
+ apply(simp add: LV_NTIMES_3 image_def Stars_Cons_def)
+ apply blast
+ done
-lemma LV_NTIMES_empty_finite:
- assumes "finite (LV r [])"
- shows "finite (LV (NTIMES r n) [])"
- using assms
- apply -
+lemma LV_NTIMES_5:
+ "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 ttty:
+ "LV (FROMNTIMES r n) [] = Stars_Pow (LV r []) n"
+ apply(induct n)
+ apply(simp add: LV_def)
+ apply(auto elim: Prf_elims simp add: image_def)[1]
+ prefer 2
+ apply(subst append.simps[symmetric])
+ apply(rule Prf.intros)
+ apply(simp_all)
+ apply(erule Prf_elims)
+ apply(case_tac vs1)
+ apply(simp)
+ apply(simp)
+ apply(case_tac x)
+ apply(simp_all)
+ apply(simp add: LV_FROMNTIMES_3 image_def Stars_Cons_def)
+ apply blast
+ done
+
+lemma LV_FROMNTIMES_5:
+ "LV (FROMNTIMES r n) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (FROMNTIMES 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)
+ apply(rule_tac x="vs" in exI)
+ apply(rule_tac x="[]" in exI)
+ apply(auto)
+ by (metis Prf.intros(9) append_Nil atMost_iff empty_iff le_imp_less_Suc less_antisym list.set(1) nth_mem zero_le)
+
+lemma LV_FROMNTIMES_6:
+ assumes "\<forall>s. finite (LV r s)"
+ shows "finite (LV (FROMNTIMES r n) s)"
apply(rule finite_subset)
- apply(rule test)
- apply(rule finite_imageI)
- apply(rule finite_list)
- apply(simp)
- done
+ apply(rule LV_FROMNTIMES_5)
+ apply(rule finite_Stars_Append)
+ apply(rule LV_STAR_finite)
+ apply(rule assms)
+ apply(rule finite_UN_I)
+ apply(auto)
+ by (simp add: assms finite_Stars_Pow ttty)
-lemma LV_NTIMES_STAR:
- "LV (NTIMES r n) s \<subseteq> LV (STAR r) s"
-apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims)
-apply(rule Prf.intros)
-oops
+lemma LV_NMTIMES_5:
+ "LV (NMTIMES r n m) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (FROMNTIMES 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)
+ apply(rule_tac x="vs" in exI)
+ apply(rule_tac x="[]" in exI)
+ apply(auto)
+ by (metis Prf.intros(9) append_Nil atMost_iff empty_iff le_imp_less_Suc less_antisym list.set(1) nth_mem zero_le)
-lemma LV_FROMNTIMES_STAR:
- "LV (FROMNTIMES r n) s \<subseteq> LV (STAR r) s"
-apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims)
-oops
-
+lemma LV_NMTIMES_6:
+ assumes "\<forall>s. finite (LV r s)"
+ shows "finite (LV (NMTIMES r n m) s)"
+ apply(rule finite_subset)
+ apply(rule LV_NMTIMES_5)
+ apply(rule finite_Stars_Append)
+ apply(rule LV_STAR_finite)
+ apply(rule assms)
+ apply(rule finite_UN_I)
+ apply(auto)
+ by (simp add: assms finite_Stars_Pow ttty)
+
+
lemma LV_finite:
shows "finite (LV r s)"
proof(induct r arbitrary: s)
@@ -999,7 +1120,17 @@
case (FROMNTIMES r n s)
have "\<And>s. finite (LV r s)" by fact
then show "finite (LV (FROMNTIMES r n) s)"
-
+ by (simp add: LV_FROMNTIMES_6)
+next
+ case (NTIMES r n s)
+ have "\<And>s. finite (LV r s)" by fact
+ then show "finite (LV (NTIMES r n) s)"
+ by (metis (no_types, lifting) LV_NTIMES_4 LV_NTIMES_5 LV_STAR_finite finite_Stars_Append finite_Stars_Pow finite_UN_I finite_atMost finite_subset)
+next
+ case (NMTIMES r n m s)
+ have "\<And>s. finite (LV r s)" by fact
+ then show "finite (LV (NMTIMES r n m) s)"
+ by (simp add: LV_NMTIMES_6)
qed
@@ -1020,7 +1151,26 @@
\<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"
+| Posix_UPNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES 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 (UPNTIMES r (n - 1)))\<rbrakk>
+ \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r n \<rightarrow> Stars (v # vs)"
+| Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []"
+| Posix_FROMNTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk>
+ \<Longrightarrow> [] \<in> FROMNTIMES r n \<rightarrow> Stars vs"
+| Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES 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 (FROMNTIMES r (n - 1)))\<rbrakk>
+ \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> Stars (v # vs)"
+| Posix_NMTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n; n \<le> m\<rbrakk>
+ \<Longrightarrow> [] \<in> NMTIMES r n m \<rightarrow> Stars vs"
+| Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v \<noteq> []; n \<le> m;
+ \<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 (NMTIMES r n m))\<rbrakk>
+ \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)"
+
inductive_cases Posix_elims:
"s \<in> ZERO \<rightarrow> v"
"s \<in> ONE \<rightarrow> v"
@@ -1028,17 +1178,60 @@
"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"
+ "s \<in> UPNTIMES r n \<rightarrow> v"
+ "s \<in> FROMNTIMES r n \<rightarrow> v"
+ "s \<in> NMTIMES r n m \<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: Sequ_def)[18]
+ apply(case_tac n)
+ apply(simp)
+ apply(simp add: Sequ_def)
+ apply(auto)[1]
+ apply(simp)
+ apply(clarify)
+ apply(rule_tac x="Suc x" in bexI)
+ apply(simp add: Sequ_def)
+ apply(auto)[5]
+ using nth_mem nullable.simps(9) nullable_correctness apply auto[1]
+ apply simp
+ apply(simp)
+ apply(clarify)
+ apply(rule_tac x="Suc x" in bexI)
+ apply(simp add: Sequ_def)
+ apply(auto)[3]
+ apply(simp)
+ apply fastforce
+ apply(simp)
+ apply(simp)
+ apply(clarify)
+ apply(rule_tac x="Suc x" in bexI)
+ apply(auto simp add: Sequ_def)[2]
+ apply(simp)
+done
+
text {*
Our Posix definition determines a unique value.
*}
+
+lemma List_eq_zipI:
+ assumes "\<forall>(v1, v2) \<in> set (zip vs1 vs2). v1 = v2"
+ and "length vs1 = length vs2"
+ shows "vs1 = vs2"
+ using assms
+ apply(induct vs1 arbitrary: vs2)
+ apply(case_tac vs2)
+ apply(simp)
+ apply(simp)
+ apply(case_tac vs2)
+ apply(simp)
+ apply(simp)
+done
lemma Posix_determ:
assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
@@ -1104,6 +1297,89 @@
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)
+ by (meson in_set_zipE)
+next
+ case (Posix_NTIMES1 s1 r v s2 n vs v2)
+ 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
+next
+ case (Posix_UPNTIMES1 s1 r v s2 n vs v2)
+ have "(s1 @ s2) \<in> UPNTIMES r n \<rightarrow> v2"
+ "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES 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 (UPNTIMES r (n - 1 )))" by fact+
+ then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (UPNTIMES 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_UPNTIMES1.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> UPNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+ ultimately show "Stars (v # vs) = v2" by auto
+next
+ case (Posix_UPNTIMES2 r n v2)
+ then show "Stars [] = v2"
+ apply(erule_tac Posix_elims)
+ apply(auto)
+ by (simp add: Posix1(2))
+next
+ case (Posix_FROMNTIMES1 s1 r v s2 n vs v2)
+ have "(s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> v2"
+ "s1 \<in> r \<rightarrow> v" "s2 \<in> FROMNTIMES 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 (FROMNTIMES r (n - 1 )))" by fact+
+ then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs')"
+ apply(cases) apply (auto simp add: append_eq_append_conv2)
+ using Posix1(1) Posix1(2) apply blast
+ apply(drule_tac x="v" in meta_spec)
+ apply(drule_tac x="vs" in meta_spec)
+ apply(simp)
+ apply(drule meta_mp)
+ apply(case_tac n)
+ apply(simp)
+ apply(rule conjI)
+ apply (smt L.simps(9) One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps Suc_mono Suc_pred UN_E append.right_neutral append_Nil lessI less_antisym list.size(3) nat.simps(3) neq0_conv not_less_eq val.inject(5))
+ apply(rule List_eq_zipI)
+ apply(auto)[1]
+ sorry
+ moreover
+ have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+ "\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+ ultimately show "Stars (v # vs) = v2" by auto
+next
+ case (Posix_FROMNTIMES2 vs r n v2)
+ then show "Stars vs = v2"
+ apply(erule_tac Posix_elims)
+ apply(auto)
+ apply(rule List_eq_zipI)
+ apply(auto)
+ apply(meson in_set_zipE)
+ by (simp add: Posix1(2))
+next
+ case (Posix_NMTIMES1 s1 r v s2 n m vs v2)
+ then show "Stars (v # vs) = v2"
+ sorry
+next
+ case (Posix_NMTIMES2 vs r n m v2)
+ then show "Stars vs = v2"
+ sorry
qed
@@ -1116,7 +1392,60 @@
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)[7]
+ defer
+ defer
+ apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2]
+ apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq)
+ prefer 4
+ apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[1]
+ apply(subst append.simps(2)[symmetric])
+ apply(rule Prf.intros)
+ apply(auto)
+ prefer 4
+ apply (metis Prf.intros(8) append_Nil empty_iff list.set(1))
+ apply(erule Posix_elims)
+ apply(auto)
+ apply(rule_tac t="v # vsa" and s = "[v] @ vsa" in subst)
+ apply(simp)
+ apply(rule Prf.intros)
+ apply(simp)
+ apply(auto)[1]
+ apply(auto simp add: Sequ_def intro: Prf.intros elim: Prf_elims)[1]
+ apply(simp)
+ apply(rotate_tac 4)
+ apply(erule Prf_elims)
+ apply(auto)
+ apply(case_tac n)
+ apply(simp)
+
+ apply(subst append.simps(2)[symmetric])
+ apply(rule Prf.intros)
+ apply(auto)
+ apply(rule Prf.intros(10))
+ apply(auto)
+ apply (metis Prf.intros(11) append_Nil empty_iff list.set(1))
+ apply(rotate_tac 6)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(subst append.simps(2)[symmetric])
+ apply(rule Prf.intros)
+ apply(auto)
+ apply(rule_tac t="v # vsa" and s = "(v # vsa) @ []" in subst)
+ apply(simp)
+ apply(simp add: Prf.intros(12))
+ done
+
+lemma FROMNTIMES_0:
+ assumes "s \<in> FROMNTIMES r 0 \<rightarrow> v"
+ shows "s = [] \<and> v = Stars []"
+ using assms
+ apply(erule_tac Posix_elims)
+ apply(auto)
+ done
+
+lemma FROMNTIMES_der_0:
+ shows "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)"
+by(simp)
+
end
\ No newline at end of file