--- a/thys2/SizeBound6CT.thy Sat Mar 05 11:31:59 2022 +0000
+++ b/thys2/SizeBound6CT.thy Mon Mar 07 12:27:27 2022 +0000
@@ -868,182 +868,6 @@
|"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]"
*)
-definition SEQ_set where
- "SEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}"
-
-definition ALT_set where
-"ALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> sum_list (map rsize rs) \<le> n}"
-
-context notes rev_conj_cong[fundef_cong] begin
-function (sequential) rexp_enum :: "nat \<Rightarrow> rrexp set"
- where
-"rexp_enum 0 = {}"
-|"rexp_enum (Suc 0) = {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c::char. True }"
-|"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = n} \<union>
-{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc n \<and> i \<le> n \<and> j \<le> n} \<union>
-{RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union>
-(rexp_enum n)"
- by pat_completeness auto
-termination
- by (relation "measure size") auto
-end
-
-lemma rexp_enum_inclusion:
- shows "(rexp_enum n) \<subseteq> (rexp_enum (Suc n))"
- apply(induct n)
- apply auto[1]
- apply(simp)
- done
-
-lemma rexp_enum_mono:
- shows "n \<le> m \<Longrightarrow> (rexp_enum n) \<subseteq> (rexp_enum m)"
- by (simp add: lift_Suc_mono_le rexp_enum_inclusion)
-
-lemma zero_in_Suc0:
- shows "RZERO \<in> rexp_enum (Suc 0)"
-and "RZERO \<in> rexp_enum 1"
- apply simp
- by simp
-
-lemma one_in_Suc0:
- shows "RONE \<in> rexp_enum (Suc 0)"
-and "RONE \<in> rexp_enum 1"
- apply simp
- by simp
-
-lemma char_in_Suc0:
- shows "RCHAR c \<in> rexp_enum (Suc 0)"
- apply simp
- done
-
-
-lemma char_in1:
- shows "RCHAR c \<in> rexp_enum 1"
- using One_nat_def char_in_Suc0 by presburger
-
-lemma alts_nil_in_Suc0:
- shows "RALTS [] \<in> rexp_enum (Suc 0)"
- and "RALTS [] \<in> rexp_enum 1"
- apply simp
- by simp
-
-
-lemma zero_in_positive:
- shows "RZERO \<in> rexp_enum (Suc N)"
- by (metis le_add1 plus_1_eq_Suc rexp_enum_mono subsetD zero_in_Suc0(2))
-
-lemma one_in_positive:
- shows "RONE \<in> rexp_enum (Suc N)"
- by (metis le_add1 plus_1_eq_Suc rexp_enum_mono subsetD one_in_Suc0(2))
-
-lemma alts_in_positive:
- shows "RALTS [] \<in> rexp_enum (Suc N)"
- by (metis One_nat_def alts_nil_in_Suc0(1) le_add_same_cancel1 less_Suc_eq_le plus_1_eq_Suc rexp_enum_mono subsetD zero_less_Suc)
-
-lemma char_in_positive:
- shows "RCHAR c \<in> rexp_enum (Suc N)"
- apply(cases c)
- apply (metis Suc_eq_plus1 char_in1 le_add2 rexp_enum_mono subsetD)+
- done
-
-lemma enum_inductive_cases:
- shows "rsize (RSEQ r1 r2) = Suc n \<Longrightarrow> \<exists>i j. rsize r1 = i \<and> rsize r2 = j\<and> i + j = n"
- by (metis Suc_inject rsize.simps(5))
-
-
-lemma enumeration_finite:
- shows "\<exists>Nn. card (rexp_enum n) < Nn"
- apply(simp add:no_top_class.gt_ex)
- done
-
-
-lemma s1:
-"{r::rexp . size r = 0} = ({ZERO, ONE} \<union> {CH c| c. True})"
-apply(auto)
-apply(case_tac x)
-apply(simp_all)
-done
-
-
-
-
-lemma enum_Suc0:
- shows " rexp_enum (Suc 0) = {RZERO} \<union> {RONE} \<union> {RCHAR c | c. True} \<union> {RALTS []}"
- by auto
-
-lemma enumeration_chars_finite:
- shows "finite {RCHAR c |c. True}"
- apply(subgoal_tac "finite (RCHAR ` (UNIV::char set))")
- prefer 2
- using finite_code apply blast
- by (simp add: full_SetCompr_eq)
-
-lemma enum_Suc0_finite:
- shows "finite (rexp_enum (Suc 0))"
- apply(subgoal_tac "finite ( {RZERO} \<union> {RONE} \<union> {RCHAR c | c. True} \<union> {RALTS []})")
- using enum_Suc0 apply presburger
- using enumeration_chars_finite by blast
-
-lemma enum_1_finite:
- shows "finite (rexp_enum 1)"
- using enum_Suc0_finite by force
-
-lemma enum_stars_finite:
- shows " finite (rexp_enum n) \<Longrightarrow> finite {RSTAR r0 | r0. r0 \<in> (rexp_enum n)}"
- apply(induct n)
- apply simp
- apply simp
- done
-
-definition RSEQ_set
- where
- "RSEQ_set A B \<equiv> (\<lambda>(r1, r2) . (RSEQ r1 r2 )) ` (A \<times> B)"
-
-
-lemma enum_seq_finite:
- shows "(\<forall>k. k < n \<longrightarrow> finite (rexp_enum k)) \<Longrightarrow> finite
-{(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = n}"
- apply(induct n)
- apply simp
- apply(subgoal_tac "{(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = Suc n}
-\<subseteq> RSEQ_set (rexp_enum n) (rexp_enum n)")
- apply(subgoal_tac "finite ( RSEQ_set (rexp_enum n) (rexp_enum n))")
- using rev_finite_subset
- apply fastforce
-
- sorry
-
-
-
-lemma enum_induct_finite:
- shows " finite ( {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = n} \<union>
-{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc n \<and> i \<le> n \<and> j \<le> n} \<union>
-{RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union>
-(rexp_enum n))"
- apply(induct n)
- apply simp
- sorry
-
-lemma enumeration_finite2:
- shows "finite (rexp_enum n)"
- apply(cases n)
- apply auto[1]
- apply(case_tac nat)
- using enum_Suc0_finite apply blast
- apply(subgoal_tac "rexp_enum ( Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = n} \<union>
-{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc n \<and> i \<le> n \<and> j \<le> n} \<union>
-{RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union>
-(rexp_enum n)")
- prefer 2
- using rexp_enum.simps(3) apply presburger
- using enum_induct_finite by auto
-
-
-lemma size1_rexps:
- shows "RCHAR x \<in> rexp_enum 1"
- apply(cases x)
- apply auto
- done
lemma non_zero_size:
shows "rsize r \<ge> Suc 0"
@@ -1070,147 +894,68 @@
apply simp
done
-lemma rexp_enum_case3:
- shows "N \<ge> Suc 0 \<Longrightarrow> rexp_enum (Suc N) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = N} \<union>
-{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N} \<union>
-{RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
-(rexp_enum N)"
- apply(case_tac N)
- apply simp
- apply auto
- done
-
-
-
-lemma def_enum_alts:
- shows "\<lbrakk> r = RALTS x5; x5 = a # list;
- rsize a = i \<and> rsize (RALTS list) = j \<and> i + j = Suc N \<and> a \<in> (rexp_enum i) \<and> (RALTS list) \<in> (rexp_enum j) \<rbrakk>
- \<Longrightarrow> r \<in> rexp_enum (Suc N)"
- apply(subgoal_tac "N \<ge> 1")
- prefer 2
- apply (metis One_nat_def add_is_1 less_Suc0 linorder_le_less_linear non_zero_size)
- apply(subgoal_tac " rexp_enum (Suc N) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = N} \<union>
-{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc N\<and> i \<le> N \<and> j \<le> N} \<union>
-{RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
-(rexp_enum N)")
- prefer 2
- using One_nat_def rexp_enum_case3 apply presburger
- apply(subgoal_tac "i \<le> N \<and> j \<le> N")
- prefer 2
- using non_zero_size apply auto[1]
- apply(subgoal_tac "r \<in> {uu.
- \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}")
- apply auto[1]
- apply(subgoal_tac "RALTS (a # list) \<in> {uu.
- \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}")
- apply fastforce
- apply(subgoal_tac "a \<in> rexp_enum i")
- prefer 2
- apply linarith
- by blast
-
-thm rsize.elims
-
-lemma rexp_enum_covers:
- shows " rsize r \<le> N \<Longrightarrow> r \<in> rexp_enum N \<and> r \<in> rexp_enum (rsize r)"
- apply(induct N arbitrary : r)
- apply simp
-
- using rsize.elims apply auto[1]
- apply(case_tac "rsize r \<le> N")
- using enumeration_finite
-
- apply (meson in_mono rexp_enum_inclusion)
- apply(subgoal_tac "rsize r = Suc N")
- prefer 2
- using le_Suc_eq apply blast
+definition SEQ_set where
+ "SEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}"
- apply(case_tac r)
- prefer 5
- apply(case_tac x5)
- apply(subgoal_tac "rsize r =1")
- prefer 2
- using hand_made_def_rlist_size rlist_size.simps(2) rsize.simps(4) apply presburger
- apply simp
- apply(subgoal_tac "a \<in> rexp_enum (rsize a)")
- apply(subgoal_tac "RALTS list \<in> rexp_enum (rsize (RALTS list))")
-
- apply (meson def_enum_alts rexp_size_induct)
- apply(subgoal_tac "rsize (RALTS list) \<le> N")
- apply(subgoal_tac "RALTS list \<in> rexp_enum N")
- prefer 2
- apply presburger
- using def_enum_alts rexp_size_induct apply presburger
- using rexp_size_induct apply presburger
- using rexp_size_induct apply presburger
- using rexp_size_induct apply presburger
- apply(subgoal_tac "r \<in> rexp_enum 1")
- apply (metis rsize.simps(1))
- apply(subgoal_tac "rsize r = Suc 0")
- prefer 2
- using rsize.simps(1) apply presburger
- apply(subgoal_tac "r \<in> rexp_enum (Suc 0)")
- apply force
- using zero_in_Suc0 apply blast
- apply simp
-
- using one_in_positive apply auto[1]
-
- apply (metis char_in_positive)
- apply(subgoal_tac "rsize x41 \<le> N")
- apply(subgoal_tac "rsize x42 \<le> N")
- prefer 2
- apply auto[1]
- prefer 2
- using enum_inductive_cases nat_le_iff_add apply blast
- apply(subgoal_tac "x41 \<in> rexp_enum (rsize x41)")
- prefer 2
- apply blast
- apply(subgoal_tac "x42 \<in> rexp_enum (rsize x42)")
- prefer 2
- apply blast
- apply(subgoal_tac "rsize x42 + rsize x41 = N")
- prefer 2
- using add.commute enum_inductive_cases apply blast
- apply(subgoal_tac "rexp_enum (Suc N) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = N} \<union>
-{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N} \<union>
-{RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
-(rexp_enum N)")
- apply (smt (verit, del_insts) UnCI mem_Collect_eq old.nat.inject rsize.simps(5))
- apply (smt (verit, ccfv_threshold) One_nat_def nle_le not_less_eq_eq rexp_enum_case3 size_geq1)
- apply(subgoal_tac "x6 \<in> rexp_enum N")
- prefer 2
+definition SEQ_set_cartesian where
+"SEQ_set_cartesian A n = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}"
- apply force
- apply(subgoal_tac "N \<ge> Suc 0")
- prefer 2
- apply (metis less_Suc_eq_le non_zero_size rsize.simps(6))
- apply(subgoal_tac "rexp_enum (Suc N) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = N} \<union>
-{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N} \<union>
-{RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
-(rexp_enum N)")
- prefer 2
- using rexp_enum_case3 apply presburger
- by (metis (mono_tags, lifting) Un_iff mem_Collect_eq)
-
-
-
+definition ALT_set where
+"ALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> sum_list (map rsize rs) \<le> n}"
definition
"sizeNregex N \<equiv> {r. rsize r \<le> N}"
+lemma sizenregex_induct:
+ shows "sizeNregex (Suc n) = sizeNregex n \<union> {RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True} \<union>
+SEQ_set ( sizeNregex n) n \<union> ALT_set (sizeNregex n) n \<union> (RSTAR ` (sizeNregex n))"
+ sorry
-lemma sizeNregex_covered:
- shows "sizeNregex N \<subseteq> rexp_enum N"
- using rexp_enum_covers sizeNregex_def by auto
+lemma chars_finite:
+ shows "finite (RCHAR ` (UNIV::(char set)))"
+ apply(simp)
+ done
+
+thm full_SetCompr_eq
-lemma finiteness_of_sizeN_regex:
- shows "finite (sizeNregex N)"
- by (meson enumeration_finite2 rev_finite_subset sizeNregex_covered)
+lemma size1finite:
+ shows "finite (sizeNregex (Suc 0))"
+ apply(subst sizenregex_induct)
+ apply(subst finite_Un)+
+ apply(subgoal_tac "sizeNregex 0 = {}")
+ apply(rule conjI)+
+ apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def)
+ apply simp
+ apply (simp add: full_SetCompr_eq)
+ apply (simp add: SEQ_set_def)
+ apply (simp add: ALT_set_def)
+ apply(simp add: full_SetCompr_eq)
+ using non_zero_size not_less_eq_eq sizeNregex_def by fastforce
+
+lemma seq_included_in_cart:
+ shows "SEQ_set A n \<subseteq> SEQ_set_cartesian A n"
+ sledgehammer
+
+lemma finite_seq:
+ shows " finite (sizeNregex n) \<Longrightarrow> finite (SEQ_set (sizeNregex n) n)"
+ apply(rule finite_subset)
+ sorry
+lemma finite_size_n:
+ shows "finite (sizeNregex n)"
+ apply(induct n)
+ apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def)
+ apply(subst sizenregex_induct)
+ apply(subst finite_Un)+
+ apply(rule conjI)+
+ apply simp
+ apply simp
+ apply (simp add: full_SetCompr_eq)
+
+ sorry
(*below probably needs proved concurrently*)