# HG changeset patch
# User Chengsong
# Date 1646656047 0
# Node ID 09a57446696a8a1451c78cc8fb68bcd5a19e5994
# Parent  426a93160f4a39d72d39e78091308a38083c8571
some changes

diff -r 426a93160f4a -r 09a57446696a thys2/SizeBound6CT.thy
--- 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*)
 
diff -r 426a93160f4a -r 09a57446696a thys2/SizeBoundStrong.thy
--- 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