--- a/thys/SpecExt.thy Fri Sep 22 12:25:25 2017 +0100
+++ b/thys/SpecExt.thy Thu Oct 05 12:45:13 2017 +0100
@@ -493,11 +493,15 @@
length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n"
| "\<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) \<ge> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : FROMNTIMES r n"
+ length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : FROMNTIMES r n"
+| "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; length vs > n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : FROMNTIMES r n"
| "\<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) \<ge> n; length (vs1 @ vs2) \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NMTIMES r n m"
+ length (vs1 @ vs2) = n; length (vs1 @ vs2) \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NMTIMES r n m"
+| "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [];
+ length vs > n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : NMTIMES r n m"
+
inductive_cases Prf_elims:
"\<Turnstile> v : ZERO"
"\<Turnstile> v : SEQ r1 r2"
@@ -602,8 +606,12 @@
apply(auto simp add: Sequ_def Star_concat Pow_flats)
apply(meson Pow_flats atMost_iff)
using Pow_flats_appends apply blast
-apply(meson Pow_flats_appends atLeast_iff)
+using Pow_flats_appends apply blast
+apply (meson Pow_flats atLeast_iff less_imp_le)
+apply(rule_tac x="length vs1 + length vs2" in bexI)
apply(meson Pow_flats_appends atLeastAtMost_iff)
+apply(simp)
+apply(meson Pow_flats atLeastAtMost_iff less_or_eq_imp_le)
done
lemma L_flat_Prf2:
@@ -655,9 +663,9 @@
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 m where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = m" "n \<le> m"
"\<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 auto blast
+ using Pow_cstring by force
then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = m" "n \<le> m"
"\<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
@@ -673,7 +681,26 @@
apply(simp)
done
then show "\<exists>v. \<Turnstile> v : FROMNTIMES r n \<and> flat v = s"
- using Prf.intros(9) flat_Stars by blast
+ apply(case_tac "length vs1 \<le> n")
+ apply(rule_tac x="Stars (vs1 @ take (n - length vs1) vs2)" in exI)
+ apply(simp)
+ 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(10))
+ apply(auto)
+ done
next
case (NMTIMES r n m)
have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
@@ -699,8 +726,8 @@
apply(rule_tac x="Stars (vs1 @ vs2)" in exI)
apply(simp)
apply(rule Prf.intros)
- apply(auto)
- done
+ apply(auto)
+ sorry
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
@@ -740,17 +767,17 @@
done
abbreviation
- "Prefixes s \<equiv> {s'. prefixeq s' s}"
+ "Prefixes s \<equiv> {s'. prefix s' s}"
abbreviation
- "Suffixes s \<equiv> {s'. suffixeq s' s}"
+ "Suffixes s \<equiv> {s'. suffix s' s}"
abbreviation
- "SSuffixes s \<equiv> {s'. suffix s' s}"
+ "SSuffixes s \<equiv> {s'. strict_suffix s' s}"
lemma Suffixes_cons [simp]:
shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"
-by (auto simp add: suffixeq_def Cons_eq_append_conv)
+by (auto simp add: suffix_def Cons_eq_append_conv)
lemma finite_Suffixes:
@@ -761,7 +788,7 @@
shows "finite (SSuffixes s)"
proof -
have "SSuffixes s \<subseteq> Suffixes s"
- unfolding suffix_def suffixeq_def by auto
+ unfolding suffix_def strict_suffix_def by auto
then show "finite (SSuffixes s)"
using finite_Suffixes finite_subset by blast
qed
@@ -774,7 +801,7 @@
then have "finite (rev ` Suffixes (rev s))" by simp
moreover
have "rev ` (Suffixes (rev s)) = Prefixes s"
- unfolding suffixeq_def prefixeq_def image_def
+ unfolding suffix_def prefix_def image_def
by (auto)(metis rev_append rev_rev_ident)+
ultimately show "finite (Prefixes s)" by simp
qed
@@ -786,10 +813,10 @@
fix s::"char list"
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. LV r s'"
- def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)"
+ 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)"
have "finite S1" using assms
unfolding S1_def by (simp_all add: finite_Prefixes)
moreover
@@ -800,13 +827,22 @@
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 prefixeq_def suffix_def
+ unfolding LV_def image_def prefix_def strict_suffix_def
+ apply(auto)
+ apply(case_tac x)
apply(auto elim: Prf_elims)
apply(erule Prf_elims)
apply(auto)
apply(case_tac vs)
- apply(auto intro: Prf.intros)
- done
+ apply(auto intro: Prf.intros)
+ apply(rule exI)
+ apply(rule conjI)
+ apply(rule_tac x="flat a" in exI)
+ apply(rule conjI)
+ apply(rule_tac x="flats list" in exI)
+ apply(simp)
+ apply(blast)
+ using Prf.intros(6) by blast
ultimately
show "finite (LV (STAR r) s)" by (simp add: finite_subset)
qed
@@ -815,40 +851,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_finite:
- assumes "\<forall>s. finite (LV r s)"
- shows "finite (LV (NTIMES r n) s)"
-proof(induct s rule: length_induct)
- fix s::"char list"
- assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (NTIMES r n) s')"
- then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (NTIMES r n) s')"
- by (auto simp add: suffix_def)
- def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)"
- def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r s'"
- def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (NTIMES r n) 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)
- ultimately
- have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
- moreover
- have "LV (NTIMES r n) 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 vs1)
- apply(auto intro: Prf.intros)
-
- done
- ultimately
- show "finite (LV (STAR r) s)" by (simp add: finite_subset)
-qed
-*)
lemma LV_NTIMES_0:
shows "LV (NTIMES r 0) s \<subseteq> {Stars []}"
@@ -898,20 +900,51 @@
thm card_cartesian_product
-lemma LV_empty_finite:
- shows "card (LV (NTIMES r n) []) \<le> ((card (LV r [])) ^ n)"
-apply(induct n arbitrary:)
-using LV_NTIMES_0
-apply (metis card_empty card_insert_disjoint card_mono empty_iff finite.emptyI finite.insertI nat_power_eq_Suc_0_iff)
-apply(simp add: LV_NTIMES_3)
-apply(subst card_image)
-apply(simp add: inj_on_def)
-apply(subst card_cartesian_product)
-apply(subst card_vimage_inj)
-apply(simp add: inj_on_def)
-apply(auto simp add: LV_def elim: Prf_elims)[1]
-using nat_mult_le_cancel_disj by blast
+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
+
+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)
+ apply(auto)
+ done
+
+
+lemma LV_NTIMES_empty_finite:
+ assumes "finite (LV r [])"
+ shows "finite (LV (NTIMES r n) [])"
+ using assms
+ apply -
+ apply(rule finite_subset)
+ apply(rule test)
+ apply(rule finite_imageI)
+ apply(rule finite_list)
+ apply(simp)
+ done
+
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)
@@ -939,17 +972,18 @@
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. LV r1 s'"
- def S2 \<equiv> "\<Union>s' \<in> Suffixes s. LV r2 s'"
+ define f where "f \<equiv> \<lambda>(v1, v2). Seq v1 v2"
+ define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r1 s'"
+ define S2 where "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 "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)
+ unfolding LV_def image_def prefix_def suffix_def
+ apply (auto elim!: Prf_elims)
+ by (metis (mono_tags, lifting) mem_Collect_eq)
ultimately
show "finite (LV (SEQ r1 r2) s)"
by (simp add: finite_subset)