--- 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*)
--- a/thys2/SizeBoundStrong.thy Sat Mar 05 11:31:59 2022 +0000
+++ b/thys2/SizeBoundStrong.thy Mon Mar 07 12:27:27 2022 +0000
@@ -621,12 +621,15 @@
where
"dBStrong [] acc = []"
| "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc
- else (case (pruneRexp r (addToAcc r acc)) of
- AZERO \<Rightarrow> dBStrong rs ((addToAcc r acc) @ acc) |
- r1 \<Rightarrow> r1 # (dBStrong rs ((addToAcc r acc) @ acc))
+ else let newSubRexps = (addToAcc r acc) in
+ (case (pruneRexp r newSubRexps) of
+ AZERO \<Rightarrow> dBStrong rs (newSubRexps @ acc) |
+ r1 \<Rightarrow> r1 # (dBStrong rs (newSubRexps @ acc))
)
)
"
+
+
fun bsimpStrong :: "arexp \<Rightarrow> arexp "
where
"bsimpStrong (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong r1) (bsimpStrong r2)"
@@ -937,6 +940,22 @@
apply(simp_all)
done
+fun pAKC_aux :: "arexp list \<Rightarrow> arexp \<Rightarrow> rexp \<Rightarrow> arexp"
+ where
+"pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ctx)) \<subseteq> (L (erase (AALTs [] rsa))) then AZERO else
+ case r of (ASEQ bs r1 r2) \<Rightarrow> pAKC_aux rsa r1 (SEQ (erase r1) ctx) |
+ (AALTs bs rs) \<Rightarrow> AALTs bs (map (\<lambda>r. pAKC_aux rsa r ctx) rs) |
+ r \<Rightarrow> r
+)"
+
+|"pAKC_aux rsa (ASEQ bs1 a1 a2) ctx = (if (L (SEQ (SEQ (erase a1) (erase a2)) ctx)) \<subseteq>
+ L (erase (AALTs [] rsa))
+ then AZERO
+ else (pAKC_aux rsa a1 (ASEQ bs1 a2 ctx)))"
+| "pAKC_aux rsa (AALTs bs1 rs1) ctx = ctx "
+
+fun pruneAwayKnownComponents :: "arexp list \<Rightarrow> arexp \<Rightarrow> arexp" where
+"pruneAwayKnownComponents rsa (ASEQ bs r1 r2) = (pAKC_aux rsa r1 r2)"
@@ -955,6 +974,7 @@
| "AALTs bs [] \<leadsto> AZERO"
| "AALTs bs [r] \<leadsto> fuse bs r"
| "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
+| "pruneAwayKnownComponents rsa a2 = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)"
inductive