# HG changeset patch
# User Chengsong
# Date 1647362261 0
# Node ID 7a016eeb118de829ee70212d5f196abe426cac99
# Parent  dabd25e8e4e9e79cb84b0b9e2aa7d1f1fd382107
finiteness

diff -r dabd25e8e4e9 -r 7a016eeb118d thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Sat Mar 12 14:33:54 2022 +0000
+++ b/thys2/ClosedForms.thy	Tue Mar 15 16:37:41 2022 +0000
@@ -2,6 +2,33 @@
 "BasicIdentities"
 begin
 
+
+
+lemma simp_rdistinct_f: shows 
+"f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = rsimp (rsimp_ALTs (rdistinct (map f rs) frset))  "
+  apply(induct rs arbitrary: rset)
+   apply simp
+   apply(case_tac "a \<in> rset")
+  apply(case_tac " f a \<in> frset")
+   apply simp
+   apply blast
+  apply(subgoal_tac "f a \<notin> frset")
+   apply(simp)
+   apply(subgoal_tac "f ` (insert a rset) = insert (f a) frset")
+  prefer 2
+  apply (meson image_insert)
+  
+
+  
+  sorry
+
+
+lemma distinct_der:
+  shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
+
+  sorry
+
+
 lemma alts_closed_form: shows 
 "rsimp (rders_simp (RALTS rs) s) = 
 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
@@ -14,6 +41,20 @@
    prefer 2
   apply (metis inside_simp_removal rders_simp_one_char)
   apply(simp only: )
+  apply(subst rders_simp_one_char)
+  apply(subst rsimp_idem)
+  apply(subgoal_tac "rsimp (rder x (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {}))) =
+                     rsimp ((rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))) ")
+  prefer 2
+  using rder_rsimp_ALTs_commute apply presburger
+  apply(simp only:)
+  apply(subgoal_tac "rsimp (rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))
+= rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
+   prefer 2
+  
+  using distinct_der apply presburger
+  apply(simp only:)
+
   sorry
 
 lemma alts_closed_form_variant: shows 
diff -r dabd25e8e4e9 -r 7a016eeb118d thys2/ClosedFormsBounds.thy
--- a/thys2/ClosedFormsBounds.thy	Sat Mar 12 14:33:54 2022 +0000
+++ b/thys2/ClosedFormsBounds.thy	Tue Mar 15 16:37:41 2022 +0000
@@ -1,14 +1,11 @@
-
+(**)
 theory ClosedFormsBounds
   imports "GeneralRegexBound" "ClosedForms"
 begin
-
 lemma alts_ders_lambda_shape_ders:
   shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s"
   by (simp add: image_iff)
 
-
-
 lemma rlist_bound:
   shows "\<forall>r \<in> set rs. rsize r \<le> N \<Longrightarrow> sum_list (map rsize rs) \<le> N * (length rs)"
   apply(induct rs)
@@ -46,20 +43,391 @@
   shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))"
   using rsimp_aalts_smaller by auto
 
+lemma no_elem_distinct :
+  shows "a \<notin> set rs \<Longrightarrow> rdistinct rs rset = rdistinct rs (insert a rset)"
+  apply(induct rs arbitrary: rset)
+   apply simp
+  by force
+  
+
+
+
+inductive good :: "rrexp \<Rightarrow> bool"
+  where
+"RZERO \<notin> set rs \<Longrightarrow> good (RALTS rs)"
+|"good RZERO"
+|"good RONE"
+|"good (RCHAR c)"
+|"good (RSEQ r1 r2)"
+|"good (RSTAR r0)"
+
+
+lemma after_flts_no0:
+  shows "\<forall>r \<in> set rs. good r \<Longrightarrow> RZERO \<notin> set (rflts rs)"
+  apply(induct rs)
+   apply simp
+  apply(case_tac a)
+       apply simp
+  apply simp
+  apply simp
+    apply simp
+  apply simp
+  using good.simps apply blast
+  apply simp
+  done
+
 lemma flts_has_no_zero:
-  shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)"
+  shows "\<forall>r \<in> set rs. good r \<Longrightarrow> rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)"
+  apply(subgoal_tac "RZERO \<notin> set (rflts rs)")  
+   apply (meson no_elem_distinct)
+  apply(insert after_flts_no0)
+  by blast
+
+lemma shape_of_alts:
+  shows "\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs) \<Longrightarrow> RZERO \<notin> alts_set \<and> RONE \<notin> alts_set"
+  by fastforce
+
+lemma quantified2_implies1:
+  shows "\<forall>r. P \<and> Q \<Longrightarrow> \<forall>r. P"
+  by auto
+
+lemma quantified_quantifiedAB_A:
+  shows " (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) \<Longrightarrow> \<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs"
+  by fastforce
+
+
+
+
+lemma list_distinct_removal:
+  shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rs1) rset = rdistinct rs1 rset"
+  apply(induct rs arbitrary: rset)
+   apply simp
+  by simp
+
+
+lemma rdistinct_mono_list:
+  shows " sum_list (map rsize (rdistinct (x5 @ rs) rset )) \<le>
+        ( sum_list (map rsize x5)) + (sum_list (map rsize (rdistinct  rs ((set x5 ) \<union> rset))))"
+  apply(induct x5 arbitrary: rs rset)
+   apply simp
+  apply(case_tac "a \<in> rset")
+   apply simp
+   apply (simp add: add.assoc insert_absorb trans_le_add2)
+  apply simp
+  by (metis Un_insert_right)
+
+
+lemma flts_size_reduction_alts:
+  shows " \<And>a rs noalts_set alts_set corr_set x5.
+       \<lbrakk>\<And>noalts_set alts_set corr_set.
+           (\<forall>r\<in>noalts_set. \<forall>xs. r \<noteq> RALTS xs) \<and>
+           (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) \<Longrightarrow>
+           Suc (sum_list (map rsize (rdistinct (rflts rs) (noalts_set \<union> corr_set))))
+           \<le> Suc (sum_list (map rsize (rdistinct rs (insert RZERO (noalts_set \<union> alts_set)))));
+        (\<forall>r\<in>noalts_set. \<forall>xs. r \<noteq> RALTS xs) \<and>
+        (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set);
+        a = RALTS x5\<rbrakk>
+       \<Longrightarrow> Suc (sum_list (map rsize (rdistinct (rflts (a # rs)) (noalts_set \<union> corr_set))))
+           \<le> Suc (sum_list
+                    (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))))"
+  apply(case_tac "a \<in> alts_set")
+   apply simp
+   apply(subgoal_tac "set x5 \<subseteq> corr_set")
+  apply(subst list_distinct_removal)
+  apply auto[1]
+    apply presburger
+   apply fastforce
+  apply (subgoal_tac "a \<notin> noalts_set")
+  prefer 2
+  apply blast
+  apply simp
+  apply(subgoal_tac "sum_list (map rsize (rdistinct (x5 @ rflts rs) (noalts_set \<union> corr_set))) 
+                   \<le> sum_list (map rsize x5 ) + sum_list (map rsize (rdistinct (rflts rs) ((set x5) \<union> (noalts_set \<union> corr_set))))")
+  prefer 2
+  using rdistinct_mono_list apply presburger
+  apply(subgoal_tac "insert (RALTS x5) (noalts_set \<union> alts_set) = noalts_set \<union> (insert (RALTS x5) alts_set)")
+   apply(simp only:)
+  apply(subgoal_tac "sum_list (map rsize x5) + 
+sum_list (map rsize (rdistinct (rflts rs) (noalts_set \<union> (corr_set \<union> (set x5))))) \<le>
+Suc (sum_list (map rsize x5) +
+                   sum_list
+                    (map rsize
+                      (rdistinct rs (insert RZERO (noalts_set \<union> insert (RALTS x5) alts_set)))))")
+  
+  apply (simp add: Un_left_commute inf_sup_aci(5))
+   apply(subgoal_tac "sum_list (map rsize (rdistinct (rflts rs) (noalts_set \<union> (corr_set \<union> set x5))))
+\<le> sum_list
+                    (map rsize
+                      (rdistinct rs (insert RZERO (noalts_set \<union> insert (RALTS x5) alts_set))))")
+    apply linarith
+   apply(subgoal_tac "\<forall>r \<in>  insert (RALTS x5) alts_set. \<exists>xs1.( r = RALTS xs1 \<and> set xs1 \<subseteq> corr_set \<union> set x5)")
+    apply presburger
+   apply (meson insert_iff sup.cobounded2 sup.coboundedI1)
+  by blast
+
+
+
 
-  sorry
+lemma flts_vs_nflts1:
+  shows "(\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs)
+ \<and> (\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set))  
+\<Longrightarrow>  (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set)  )))
+         \<le>  (sum_list (map rsize (rdistinct rs (insert RZERO (noalts_set \<union> alts_set) ))))"
+    apply(induct rs arbitrary: noalts_set alts_set corr_set)
+   apply simp
+  apply(case_tac a)
+       apply(case_tac "RZERO \<in> noalts_set")
+        apply simp
+       apply(subgoal_tac "RZERO \<notin> alts_set")
+        apply simp
+       apply fastforce
+      apply(case_tac "RONE \<in> noalts_set")
+       apply simp
+      apply(subgoal_tac "RONE \<notin> alts_set")
+  prefer 2
+  apply fastforce
+      apply(case_tac "RONE \<in> corr_set")
+       apply(subgoal_tac "rflts (a # rs) = RONE # rflts rs")
+        apply(simp only:)
+        apply(subgoal_tac "rdistinct (RONE # rflts rs) (noalts_set \<union> corr_set) = 
+                           rdistinct (rflts rs) (noalts_set \<union> corr_set)")
+         apply(simp only:)
+  apply(subgoal_tac "rdistinct (RONE # rs) (insert RZERO (noalts_set \<union> alts_set)) =
+                     RONE # (rdistinct rs (insert RONE (insert RZERO (noalts_set \<union> alts_set)))) ")
+          apply(simp only:)
+  apply(subgoal_tac "rdistinct (rflts rs) (noalts_set \<union> corr_set) = 
+                     rdistinct (rflts rs) (insert RONE (noalts_set \<union> corr_set))")
+  apply (simp only:)
+  apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
+            apply(simp only:)
+  apply(subgoal_tac "insert RONE (insert RZERO (noalts_set \<union> alts_set)) = 
+                     insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
+             apply(simp only:)
+  apply(subgoal_tac "  (sum_list
+                    (map rsize ( rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))
+                   \<le>  (sum_list
+                    (map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))")
+  apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
+  apply (metis (no_types, opaque_lifting) add_Suc_right le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
+            apply fastforce
+           apply fastforce
+  apply (metis Un_iff insert_absorb)
+         apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1))
+        apply (meson UnCI rdistinct.simps(2))
+  using rflts.simps(4) apply presburger
+      apply simp
+      apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
+  apply(simp only:)
+  apply (metis Un_insert_left insertE rrexp.distinct(15))
+      apply fastforce
+     apply(case_tac "a \<in> noalts_set")
+      apply simp
+  apply(subgoal_tac "a \<notin> alts_set")
+      prefer 2
+      apply blast
+  apply(case_tac "a \<in> corr_set")
+      apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
+  prefer 2
+  apply fastforce
+      apply(simp only:)
+      apply(subgoal_tac "  sum_list
+               (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))
+\<le>
+                sum_list
+               (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set))))")
+
+       apply(subgoal_tac 
+"sum_list (map rsize (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)))
+\<le>
+ sum_list (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))")
+  apply fastforce
+       apply simp
+  apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
+        apply(simp only:)
+        apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
+  apply(simp only:)
+  apply (metis insertE rrexp.distinct(21))
+        apply blast
+  
+  apply fastforce
+  apply force
+     apply simp
+     apply (metis Un_insert_left insert_iff rrexp.distinct(21))
+    apply(case_tac "a \<in> noalts_set")
+     apply simp
+  apply(subgoal_tac "a \<notin> alts_set")
+      prefer 2
+      apply blast
+  apply(case_tac "a \<in> corr_set")
+      apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
+  prefer 2
+  apply fastforce
+      apply(simp only:)
+      apply(subgoal_tac "  sum_list
+               (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))
+\<le>
+                sum_list
+               (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set))))")
+
+       apply(subgoal_tac 
+"sum_list (map rsize (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)))
+\<le>
+ sum_list (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))")
+  apply fastforce
+       apply simp
+  apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
+        apply(simp only:)
+        apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
+  apply(simp only:)
+
+
+  apply (metis insertE rrexp.distinct(25))
+  apply blast
+  apply fastforce
+  apply force
+     apply simp
+  
+    apply (metis Un_insert_left insertE rrexp.distinct(25))
+
+  using Suc_le_mono flts_size_reduction_alts apply presburger
+     apply(case_tac "a \<in> noalts_set")
+      apply simp
+  apply(subgoal_tac "a \<notin> alts_set")
+      prefer 2
+      apply blast
+  apply(case_tac "a \<in> corr_set")
+      apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
+  prefer 2
+  apply fastforce
+      apply(simp only:)
+      apply(subgoal_tac "  sum_list
+               (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))
+\<le>
+                sum_list
+               (map rsize (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set))))")
+
+       apply(subgoal_tac 
+"sum_list (map rsize (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)))
+\<le>
+ sum_list (map rsize (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))))")
+  apply fastforce
+       apply simp
+  apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
+        apply(simp only:)
+        apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
+  apply(simp only:)
+  apply (metis insertE rrexp.distinct(29))
+
+        apply blast
+  
+  apply fastforce
+  apply force
+     apply simp
+  apply (metis Un_insert_left insert_iff rrexp.distinct(29))
+  done
+
+
+
+
 
 lemma flts_vs_nflts:
-  shows "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs
- \<and> (\<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)  
+  shows "(\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs)
+ \<and> (\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set))  
 \<Longrightarrow> Suc (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set)  )))
-         \<le> Suc (sum_list (map rsize (rdistinct rs (noalts_set \<union> alts_set) )))"
-  apply(induct rs arbitrary: noalts_set)
+         \<le> Suc (sum_list (map rsize (rdistinct rs (insert RZERO (noalts_set \<union> alts_set) ))))"
+  apply(induct rs arbitrary: noalts_set alts_set corr_set)
    apply simp
+  apply(case_tac a)
+       apply(case_tac "RZERO \<in> noalts_set")
+        apply simp
+       apply(subgoal_tac "RZERO \<notin> alts_set")
+        apply simp
+       apply fastforce
+      apply(case_tac "RONE \<in> noalts_set")
+       apply simp
+      apply(subgoal_tac "RONE \<notin> alts_set")
+  prefer 2
+  apply fastforce
+      apply(case_tac "RONE \<in> corr_set")
+       apply(subgoal_tac "rflts (a # rs) = RONE # rflts rs")
+        apply(simp only:)
+        apply(subgoal_tac "rdistinct (RONE # rflts rs) (noalts_set \<union> corr_set) = 
+                           rdistinct (rflts rs) (noalts_set \<union> corr_set)")
+         apply(simp only:)
+  apply(subgoal_tac "rdistinct (RONE # rs) (insert RZERO (noalts_set \<union> alts_set)) =
+                     RONE # (rdistinct rs (insert RONE (insert RZERO (noalts_set \<union> alts_set)))) ")
+          apply(simp only:)
+  apply(subgoal_tac "rdistinct (rflts rs) (noalts_set \<union> corr_set) = 
+                     rdistinct (rflts rs) (insert RONE (noalts_set \<union> corr_set))")
+  apply (simp only:)
+  apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
+            apply(simp only:)
+  apply(subgoal_tac "insert RONE (insert RZERO (noalts_set \<union> alts_set)) = 
+                     insert RZERO ((insert RONE noalts_set) \<union> alts_set)")
+             apply(simp only:)
+  apply(subgoal_tac " Suc (sum_list
+                    (map rsize ( rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))
+                   \<le> Suc (sum_list
+                    (map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))")
+  apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
+  apply (metis (no_types, opaque_lifting) add_Suc_right le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
+            apply fastforce
+           apply fastforce
+  apply (metis Un_iff insert_absorb)
+         apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1))
+        apply (meson UnCI rdistinct.simps(2))
+  using rflts.simps(4) apply presburger
+      apply simp
+      apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
+  apply(simp only:)
+  apply (metis Un_insert_left insertE rrexp.distinct(15))
+      apply fastforce
+     apply(case_tac "a \<in> noalts_set")
+      apply simp
+  apply(subgoal_tac "a \<notin> alts_set")
+      prefer 2
+      apply blast
+  apply(case_tac "a \<in> corr_set")
+      apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
+  prefer 2
+  apply fastforce
+      apply(simp only:)
+  apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+  apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+     apply(case_tac "a \<in> noalts_set")
+      apply simp
+  apply(subgoal_tac "a \<notin> alts_set")
+      prefer 2
+      apply blast
+  apply(case_tac "a \<in> corr_set")
+      apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
+  prefer 2
+  apply fastforce
+      apply(simp only:)
+  apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+  apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+   prefer 2
+     apply(case_tac "a \<in> noalts_set")
+      apply simp
+  apply(subgoal_tac "a \<notin> alts_set")
+      prefer 2
+      apply blast
+  apply(case_tac "a \<in> corr_set")
+      apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
+  prefer 2
+  apply fastforce
+      apply(simp only:)
+  apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+  apply (metis add_mono_thms_linordered_semiring(1) flts_vs_nflts1 le_numeral_extra(4) plus_1_eq_Suc)
+  using flts_size_reduction_alts apply presburger
+  done
 
-  sorry
+
+
+
+
+(*  apply(rutac x = "\<lambda>a rs noalts_set alts_set corr_set. set xs ")*)
+  
 
 lemma distinct_simp_ineq_general:
   shows "rsimp ` no_simp = has_simp \<and> finite no_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
@@ -73,10 +441,14 @@
   apply(case_tac "rsimp a \<in> no_simp")
    apply(subgoal_tac "rsimp a \<in> has_simp")
   prefer 2
-  apply (simp add: rev_image_eqI rsimp_idem)
-  sledgehammer[timeout = 100]
-
-  sorry
+    apply (simp add: rev_image_eqI rsimp_idem)
+  apply simp
+   apply (metis finite_insert image_insert insert_absorb trans_le_add2)
+  apply(case_tac "rsimp a \<notin> has_simp")
+  apply simp
+   apply (metis add_mono_thms_linordered_semiring(1) finite.insertI image_insert rsimp_mono)
+  apply simp
+  by (metis finite.insertI image_insert insert_absorb trans_le_add2)
 
 
 lemma not_mentioned_elem_distinct_strong:
@@ -92,13 +464,40 @@
 
 
 
-
+lemma larger_acc_smaller_distinct_res0:
+  shows " ss \<subseteq> SS \<Longrightarrow> sum_list (map rsize (rdistinct rs SS)) \<le> sum_list (map rsize (rdistinct rs ss))"
+  apply(induct rs arbitrary: ss SS)
+  apply simp
+  apply(case_tac "a \<in> ss")
+   apply(subgoal_tac "a \<in> SS")
+    apply simp
+   apply blast
+  apply(case_tac "a \<in> SS")
+   apply simp
+   apply(subgoal_tac "insert a ss \<subseteq> SS")
+    apply simp
+  apply (simp add: trans_le_add2)
+  apply blast
+  apply(simp)
+  apply(subgoal_tac "insert a ss \<subseteq> insert a SS")
+   apply blast
+  by blast
 
 
 lemma without_flts_ineq:
   shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> 
          Suc (sum_list (map rsize (rdistinct (    rs  ) {}  )))"
-  by (metis empty_iff flts_vs_nflts sup_bot_left)
+proof -
+  have " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le>  
+         Suc (sum_list (map rsize (rdistinct rs (insert RZERO {}))))"
+    by (metis empty_iff flts_vs_nflts sup_bot_left)
+  also have "... \<le>  Suc (sum_list (map rsize (rdistinct rs {})))" 
+    by (simp add: larger_acc_smaller_distinct_res0)
+  finally show ?thesis sledgehammer
+    by blast
+qed
+
+
 
 
 
@@ -131,24 +530,7 @@
   shows "a \<notin> ss \<Longrightarrow> rdistinct (a  # rs) ss = a # rdistinct rs (insert a ss) "
   by auto
 
-lemma larger_acc_smaller_distinct_res0:
-  shows " ss \<subseteq> SS \<Longrightarrow> sum_list (map rsize (rdistinct rs SS)) \<le> sum_list (map rsize (rdistinct rs ss))"
-  apply(induct rs arbitrary: ss SS)
-  apply simp
-  apply(case_tac "a \<in> ss")
-   apply(subgoal_tac "a \<in> SS")
-    apply simp
-   apply blast
-  apply(case_tac "a \<in> SS")
-   apply simp
-   apply(subgoal_tac "insert a ss \<subseteq> SS")
-    apply simp
-  apply (simp add: trans_le_add2)
-  apply blast
-  apply(simp)
-  apply(subgoal_tac "insert a ss \<subseteq> insert a SS")
-   apply blast
-  by blast
+
 
 
 lemma larger_acc_smaller_distinct_res:
@@ -393,7 +775,7 @@
 
 
 
-
+unused_thms
 
 
 
diff -r dabd25e8e4e9 -r 7a016eeb118d thys2/GeneralRegexBound.thy
--- a/thys2/GeneralRegexBound.thy	Sat Mar 12 14:33:54 2022 +0000
+++ b/thys2/GeneralRegexBound.thy	Tue Mar 15 16:37:41 2022 +0000
@@ -1,5 +1,5 @@
 theory GeneralRegexBound imports 
-"BasicIdentities"
+"BasicIdentities" 
 begin
 
 
@@ -17,19 +17,257 @@
   "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 SEQ_set_cartesian where
-"SEQ_set_cartesian A n  = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}"
+"SEQ_set_cartesian A  = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}"
 
 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 ALTs_set
+  where
+  "ALTs_set A n \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> sum_list (map rsize rs) \<le> n}"
+
+
+
+lemma alts_set_2defs:
+  shows "ALT_set A n = ALTs_set A n"
+  apply(subgoal_tac "ALT_set A n \<subseteq> ALTs_set A n")
+   apply(subgoal_tac "ALTs_set A n \<subseteq> ALT_set A n")
+    apply auto[1]
+  prefer 2
+  using ALT_set_def ALTs_set_def apply fastforce
+  apply(subgoal_tac "\<forall>r \<in> ALTs_set A n. r \<in> ALT_set A n")
+   apply blast
+  apply(rule ballI)
+  apply(subgoal_tac "\<exists>rs. r = RALTS rs \<and> sum_list (map rsize rs) \<le> n")
+   prefer 2
+  using ALTs_set_def apply fastforce
+  apply(erule exE)
+  apply(subgoal_tac "set rs \<subseteq> A")
+  prefer 2
+  apply (simp add: ALTs_set_def subsetI)
+  using ALT_set_def by blast
+
+
 
 definition
   "sizeNregex N \<equiv> {r. rsize r \<le> N}"
 
+
+
+lemma sizenregex_induct1:
+  "sizeNregex (Suc n) = (({RZERO, RONE} \<union> {RCHAR c| c. True}) 
+                       \<union> (RSTAR ` sizeNregex n) \<union>
+                         (SEQ_set (sizeNregex n) n)
+                       \<union>  (ALTs_set (sizeNregex n) n))"
+  apply(auto)
+        apply(case_tac x)
+             apply(auto simp add: SEQ_set_def)
+  using sizeNregex_def apply force
+  using sizeNregex_def apply auto[1]
+  apply (simp add: sizeNregex_def)
+         apply (simp add: sizeNregex_def)
+         apply (simp add: ALTs_set_def)
+  apply (metis imageI list.set_map member_le_sum_list order_trans)
+  apply (simp add: sizeNregex_def)
+  apply (simp add: sizeNregex_def)
+  apply (simp add: sizeNregex_def)
+  using sizeNregex_def apply force
+  apply (simp add: sizeNregex_def)
+  apply (simp add: sizeNregex_def)
+  apply (simp add: ALTs_set_def)
+  apply(simp add: sizeNregex_def)
+  apply(auto)
+  using ex_in_conv by fastforce
+
+lemma sizeN_inclusion:
+  shows "sizeNregex n   \<subseteq> sizeNregex (Suc n)"
+  by (simp add: Collect_mono sizeNregex_def)
+
+lemma ralts_nil_in_altset:
+  shows " RALTS [] \<in> ALT_set (sizeNregex n) n "
+  using ALT_set_def by auto
+
+
 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
+  apply(subgoal_tac "sizeNregex (Suc n) =  {RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True} \<union>
+SEQ_set ( sizeNregex n) n \<union> ALT_set (sizeNregex n) n \<union> (RSTAR ` (sizeNregex n))")
+  using sizeN_inclusion apply blast
+  apply(subgoal_tac " {RZERO, RONE, RALTS []} \<union> {RCHAR c |c. True} \<union> SEQ_set (sizeNregex n) n \<union>
+    ALT_set (sizeNregex n) n \<union>
+    RSTAR ` sizeNregex n =  (({RZERO, RONE} \<union> {RCHAR c| c. True}) 
+                       \<union> (RSTAR ` sizeNregex n) \<union>
+                         (SEQ_set (sizeNregex n) n)
+                       \<union>  (ALTs_set (sizeNregex n) n))")
+  using sizenregex_induct1 apply presburger
+  apply(subgoal_tac "{RZERO, RONE} \<union> {RCHAR c |c. True} \<union> SEQ_set (sizeNregex n) n \<union>
+    ALT_set (sizeNregex n) n \<union>
+    RSTAR ` sizeNregex n =
+    {RZERO, RONE} \<union> {RCHAR c |c. True} \<union> RSTAR ` sizeNregex n \<union> SEQ_set (sizeNregex n) n \<union>
+    ALTs_set (sizeNregex n) n ")
+  prefer 2
+  using alts_set_2defs apply auto[1]
+  apply(subgoal_tac " {RZERO, RONE, RALTS []} \<union> {RCHAR c |c. True} \<union> SEQ_set (sizeNregex n) n \<union>
+    ALT_set (sizeNregex n) n \<union>
+    RSTAR ` sizeNregex n = 
+ {RZERO, RONE} \<union> {RCHAR c |c. True} \<union> SEQ_set (sizeNregex n) n \<union>
+    (insert (RALTS []) (ALT_set (sizeNregex n) n)) \<union>
+    RSTAR ` sizeNregex n")
+  prefer 2
+  apply fastforce
+  by (simp add: insert_absorb ralts_nil_in_altset)
+
+
+
+lemma s4:
+  "SEQ_set A n \<subseteq> SEQ_set_cartesian A"
+  using SEQ_set_cartesian_def SEQ_set_def by fastforce
+
+lemma s5:
+  "finite A \<Longrightarrow> finite (SEQ_set_cartesian A)"
+  apply(subgoal_tac "SEQ_set_cartesian A = (\<lambda>(x1, x2). RSEQ x1 x2) ` (A \<times> A)")
+  apply simp
+  unfolding SEQ_set_cartesian_def
+  apply(auto)
+  done
+
+thm size_list_def
+
+definition ALTs_set_length
+  where
+  "ALTs_set_length A n l \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A 
+                                      \<and> sum_list (map rsize rs) \<le> n 
+                                      \<and> length rs \<le> l}"
+
+
+definition ALTs_set_length2
+  where
+  "ALTs_set_length2 A l \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> length rs \<le> l}"
+
+definition set_length2
+  where
+  "set_length2 A l \<equiv> {rs. \<forall>r \<in> set rs. r \<in> A \<and> length rs \<le> l}"
+
+
+lemma r000: 
+  shows "ALTs_set_length A n l \<subseteq> ALTs_set_length2 A l"
+  apply(auto simp add: ALTs_set_length2_def ALTs_set_length_def)
+  done
+
+
+lemma r02: 
+  shows "set_length2 A 0 \<subseteq> {[]}"
+  apply(auto simp add: set_length2_def)
+  apply(case_tac x)
+  apply(auto)
+  done
+
+lemma r03:
+  shows "set_length2 A (Suc n) \<subseteq> 
+          {[]} \<union> (\<lambda>(h, t). h # t) ` (A \<times> (set_length2 A n))"
+  apply(auto simp add: set_length2_def)
+  apply(case_tac x)
+   apply(auto)
+  done
+
+lemma r1:
+  assumes "finite A" 
+  shows "finite (set_length2 A n)"
+  using assms
+  apply(induct n)
+  apply(rule finite_subset)
+    apply(rule r02)
+   apply(simp)    
+  apply(rule finite_subset)
+   apply(rule r03)
+  apply(simp)
+  done
+
+lemma size_sum_more_than_len:
+  shows "sum_list (map rsize rs) \<ge> length rs"
+  apply(induct rs)
+   apply simp
+  apply simp
+  apply(subgoal_tac "rsize a \<ge> 1")
+   apply linarith
+  using size_geq1 by auto
+
+
+lemma sum_list_len:
+  shows " sum_list (map rsize rs) \<le> n \<Longrightarrow> length rs \<le> n"
+  by (meson order.trans size_sum_more_than_len)
+
+  
+
+
+lemma t2:
+  shows "ALTs_set A n \<subseteq> ALTs_set_length A n n"
+  unfolding ALTs_set_length_def ALTs_set_def
+  apply(auto)
+  using sum_list_len by blast
+
+  
+thm ALTs_set_def
+
+lemma s8_aux:
+  assumes "finite A" 
+  shows "finite (ALTs_set_length A n n)"
+proof -
+  have "finite A" by fact
+  then have "finite (set_length2 A n)"
+    by (simp add: r1)
+  moreover have "(RALTS ` (set_length2 A n)) = ALTs_set_length2 A n"
+    unfolding ALTs_set_length2_def set_length2_def
+    by (auto)
+  ultimately have "finite (ALTs_set_length2 A n)"
+    by (metis finite_imageI)
+  then show ?thesis
+    by (metis infinite_super r000)
+qed
+
+lemma s1:
+  shows "{r::rrexp . rsize r = 1} = ({RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True})"
+  apply(auto)
+  apply(case_tac x)
+  apply(simp_all)
+    apply (metis One_nat_def Suc_n_not_le_n size_geq1)
+  apply (metis One_nat_def Suc_n_not_le_n ex_in_conv set_empty2 size_geq1)
+  by (metis not_one_le_zero size_geq1)
+
+
+
+lemma char_finite:
+  shows "finite  {RCHAR c |c. True}"
+  apply simp
+  apply(subgoal_tac "finite (RCHAR ` (UNIV::char set))")
+   prefer 2
+   apply simp
+  by (simp add: full_SetCompr_eq)
+
+
+lemma finite_size_n:
+  shows
+  "finite (sizeNregex n)"
+  apply(induct n)
+   apply(simp add: sizeNregex_def)
+  apply (metis (mono_tags, lifting) not_finite_existsD not_one_le_zero size_geq1)
+  apply(subst sizenregex_induct1)
+  apply(simp only: finite_Un)
+  apply(rule conjI)+
+      apply(simp)
+  using char_finite apply blast
+    apply(simp)
+   apply(rule finite_subset)
+    apply(rule s4)
+   apply(rule s5)
+   apply(simp)
+  apply(rule finite_subset)
+   apply(rule t2)
+  apply(rule s8_aux)
+  apply(simp)
+  done
+
 
 
 lemma chars_finite:
@@ -53,42 +291,33 @@
    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"
-  using SEQ_set_cartesian_def SEQ_set_def by fastforce
-
-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
 
 lemma three_easy_cases0: shows 
 "rsize (rders_simp RZERO s) \<le> Suc 0"
-  sorry
+  apply(induct s)
+   apply simp
+  apply simp
+  done
 
 
 lemma three_easy_cases1: shows 
 "rsize (rders_simp RONE s) \<le> Suc 0"
-  sorry
+    apply(induct s)
+   apply simp
+  apply simp
+  using three_easy_cases0 by auto
+
 
 lemma three_easy_casesC: shows
 "rsize (rders_simp (RCHAR c) s) \<le> Suc 0"
-
-  sorry
+  apply(induct s)
+   apply simp
+  apply simp
+  apply(case_tac " a = c")
+  using three_easy_cases1 apply blast
+  apply simp
+  using three_easy_cases0 by force
+