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)
  apply simp
  by simp


lemma alts_closed_form_bounded: shows
"\<forall>r \<in> set rs. \<forall>s. rsize(rders_simp r s ) \<le> N \<Longrightarrow> 
rsize (rders_simp (RALTS rs ) s) \<le> max (Suc ( N * (length rs))) (rsize (RALTS rs) )"
  apply(induct s)
  apply simp
  apply(subst alts_closed_form_variant)
   apply force
  apply(subgoal_tac "rsize (rsimp (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs))) \<le> rsize ( (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs)))")
   prefer 2
  using rsimp_mono apply presburger
  apply(subgoal_tac "rsize (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs)) =
                     Suc (sum_list  (map rsize (map (\<lambda>r. rders_simp r (a # s)) rs)))")
  prefer 2
  using rsize.simps(4) apply blast
  apply(subgoal_tac "sum_list (map rsize (map (\<lambda>r. rders_simp r (a # s)) rs )) \<le> N *  (length rs) ")
   apply linarith
  apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>r. rders_simp r (a # s)) rs ). rsize r \<le> N")
  prefer 2
  apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>r. rders_simp r (a # s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 (a # s)")
  prefer 2
  using alts_ders_lambda_shape_ders apply presburger
   apply metis
  apply(frule rlist_bound)
  by fastforce


lemma alts_simp_ineq_unfold:
  shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))"
  using rsimp_aalts_smaller by auto

lemma flts_has_no_zero:
  shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)"

  sorry

lemma not_mentioned_elem_distinct:
  shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs {})) = (r \<in> set (rdistinct rs {a}))"
  sorry



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)  
\<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)
   apply simp

  sorry

lemma distinct_simp_ineq_general:
  shows "rsimp ` no_simp = has_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
    \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))"

  sorry


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)




lemma distinct_simp_ineq:
  shows "Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))
    \<le> Suc (sum_list (map rsize (rdistinct rs {})))"
  
  using distinct_simp_ineq_general by blast
  



lemma alts_simp_control:
  shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))"
proof -
  have "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))"
    
    using alts_simp_ineq_unfold by auto
  then have "\<dots> \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))"
    using without_flts_ineq by blast

  show "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))"
    by (meson \<open>Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {}))) \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))\<close> \<open>rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))\<close> distinct_simp_ineq order_trans)
qed



lemma rdistinct_equality1:
  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:
  shows " (sum_list (map rsize (rdistinct rs ss))) \<ge> (sum_list (map rsize (rdistinct rs (insert a ss))))"
  apply(subgoal_tac "ss \<subseteq> (insert a ss)")
   apply(rule larger_acc_smaller_distinct_res0)
   apply simp
  by (simp add: subset_insertI)

lemma size_list_triangle1:
  shows  "sum_list (map rsize (a # (rdistinct as ss))) \<ge> rsize a + sum_list (map rsize (rdistinct as (insert a ss)))"
  by (simp add: larger_acc_smaller_distinct_res)


lemma triangle_inequality_distinct:
  shows "sum_list (map rsize (rdistinct (a # rs) ss)) \<le> rsize a + (sum_list (map rsize (rdistinct rs ss)))"
  apply(case_tac "a \<in> ss")
   apply simp
  apply(subst rdistinct_equality1)
   apply simp
  using size_list_triangle1 by auto

lemma same_regex_property_after_map:
  shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set  (map (f r2) Ss). P r"
  by auto

lemma same_property_after_distinct:
  shows " \<forall>r \<in> set  (map (f r2) Ss). P r \<Longrightarrow> \<forall>r \<in> set (rdistinct (map (f r2) Ss) xset). P r"
  apply(induct Ss arbitrary: xset)
   apply simp
  by auto

lemma same_regex_property_after_distinct:
  shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set (rdistinct (map (f r2) Ss) xset). P r"
  apply(rule same_property_after_distinct)
  apply(rule same_regex_property_after_map)
  by simp



lemma Sum_cons:
  shows "distinct (a # as) \<Longrightarrow> \<Sum> (set ((a::nat) # as)) =  a + \<Sum> (set  as)"
  by simp


lemma distinct_list_sizeNregex_bounded:
  shows "distinct rs \<and> (\<forall> r \<in> (set rs). rsize r \<le> N) \<Longrightarrow> sum_list (map rsize rs) \<le> N * length rs"
  apply(induct rs)
   apply simp
  by simp


lemma distinct_list_size_len_bounded:
  shows "distinct rs \<and> (\<forall>r \<in> set rs. rsize r \<le> N) \<and> length rs \<le> lrs \<Longrightarrow> sum_list (map rsize rs) \<le> lrs * N "
  by (metis distinct_list_sizeNregex_bounded dual_order.trans mult.commute mult_le_mono1)



lemma rdistinct_same_set:
  shows "(r \<in> set rs) =  (r \<in> set (rdistinct rs {}))"
  apply(induct rs)
   apply simp
  apply(case_tac "a \<in> set rs")
  apply(case_tac "r = a")
    apply (simp)
  apply (simp add: not_mentioned_elem_distinct)
  using not_mentioned_elem_distinct by fastforce



lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size:
  shows "\<forall>r\<in> set rs. (rsize r ) \<le> N \<Longrightarrow> sum_list (map rsize (rdistinct rs {})) \<le>
         (card (sizeNregex N))* N"
  apply(subgoal_tac "distinct (rdistinct rs {})")
  prefer 2
  using rdistinct_does_the_job apply blast
  apply(subgoal_tac "length (rdistinct rs {}) \<le> card (sizeNregex N)")
  apply(rule distinct_list_size_len_bounded)
   apply(rule conjI)+
    apply simp
   apply(rule conjI)
  apply (meson rdistinct_same_set)
   apply blast
  apply(subgoal_tac "\<forall>r \<in> set (rdistinct rs {}). rsize r \<le> N")
  prefer 2
   apply (meson rdistinct_same_set)
  apply(subgoal_tac "length (rdistinct rs {}) = card (set (rdistinct rs {}))")
  prefer 2
  using set_related_list apply blast
  apply(simp only:)
  by (metis card_mono finite_size_n mem_Collect_eq sizeNregex_def subset_code(1))






lemma star_closed_form_bounded_by_rdistinct_list_estimate:
  shows "rsize (rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
         (star_updates s r0 [[c]]) ) ))) \<le>
        Suc (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
         (star_updates s r0 [[c]]) ) {})  ) )"
  by (metis alts_simp_control )




lemma star_lambda_form:
  shows "\<forall> r \<in> set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) ls). 
        \<exists>s2. r = RSEQ (rders_simp r0 s2) (RSTAR r0) "
  by (meson ex_map_conv)


lemma star_lambda_ders:
  shows " \<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow>
    \<forall>r\<in>set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])).
       rsize r \<le> Suc (N + rsize (RSTAR r0))"
  apply(insert star_lambda_form)
  apply(simp)
  done




lemma star_control_bounded:
  shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow>        
      (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0))
         (star_updates s r0 [[c]]) ) {})  ) ) \<le> 
(card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0)))
"
  apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0))
         (star_updates s r0 [[c]]) ). (rsize r ) \<le> Suc (N + rsize (RSTAR r0))")
   prefer 2
  using star_lambda_ders apply blast
  using distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size by blast


lemma star_control_variant:
  assumes "\<forall>s. rsize (rders_simp r0 s) \<le> N"
  shows"Suc 
      (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) 
          (star_updates list r0 [[a]])) {}))) 
\<le>  (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) "
  apply(subgoal_tac    "(sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) 
          (star_updates list r0 [[a]])) {}))) 
\<le>  ( (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ")
  prefer 2
  using assms star_control_bounded apply presburger
  by simp



lemma star_closed_form_bounded:
  shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow>
              rsize (rders_simp (RSTAR r0) s) \<le> 
max (   (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0)))))   (rsize (RSTAR r0))"
  apply(case_tac s)
  apply simp
  apply(subgoal_tac " rsize (rders_simp (RSTAR r0) (a # list)) = 
rsize (rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates list r0 [[a]]) ) )))") 
   prefer 2
  using star_closed_form apply presburger
  apply(subgoal_tac "rsize (rsimp (
 RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates list    r0 [[a]]) ) ))) 
\<le>         Suc (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
         (star_updates list r0 [[a]]) ) {})  ) )")
  prefer 2
  using star_closed_form_bounded_by_rdistinct_list_estimate apply presburger
  apply(subgoal_tac "Suc (sum_list 
                 (map rsize
                   (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {}))) 
\<le>  (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0)))  ")
  apply auto[1]
  using star_control_variant by blast


lemma seq_list_estimate_control: shows 
" rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1))))
           \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))"
  by(metis alts_simp_control)

lemma map_ders_is_list_of_ders:
  shows  "\<forall>s. rsize (rders_simp r2 s) \<le> N2 \<Longrightarrow>
\<forall>r \<in> set (rdistinct (map (rders_simp r2) Ss) {}). rsize r \<le> N2"
  apply(rule same_regex_property_after_distinct)
  by simp

lemma seq_estimate_bounded: 
  assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" and "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
  shows
"Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le>
 Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))"
  apply(subgoal_tac " (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le>
  (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))")
   apply force
  apply(subgoal_tac " (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le>
                      (rsize (RSEQ (rders_simp r1 s) r2)) + (sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {})) )")
  prefer 2
  using triangle_inequality_distinct apply blast
  apply(subgoal_tac " sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {})) \<le> N2 * card (sizeNregex N2) ")
   apply(subgoal_tac "rsize (RSEQ (rders_simp r1 s) r2) \<le> Suc (N1 + rsize r2)")
    apply linarith
   apply (simp add: assms(1))
  apply(subgoal_tac "\<forall>r \<in> set (rdistinct (map (rders_simp r2) (vsuf s r1)) {}). rsize r \<le> N2")
  apply (metis (no_types, opaque_lifting) assms(2) distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size ex_map_conv mult.commute)
  using assms(2) map_ders_is_list_of_ders by blast


lemma seq_closed_form_bounded: shows
"\<lbrakk>\<forall>s. rsize (rders_simp r1 s) \<le> N1 ; \<forall>s. rsize (rders_simp r2 s) \<le> N2\<rbrakk> \<Longrightarrow>
rsize (rders_simp (RSEQ r1 r2) s) \<le> 
max (Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))) (rsize (RSEQ r1 r2)) "
  apply(case_tac s)
  apply simp
  apply(subgoal_tac " (rders_simp (RSEQ r1 r2) s) = 
rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))")
  prefer 2
  using seq_closed_form_variant apply blast
  apply(subgoal_tac "rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1))))
                    \<le>
Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))")
  apply(subgoal_tac "Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))
\<le> Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))")
  prefer 2
  using seq_estimate_bounded apply blast
   apply(subgoal_tac "rsize (rders_simp (RSEQ r1 r2) s) \<le> Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))")
  using le_max_iff_disj apply blast
   apply auto[1]
  using seq_list_estimate_control by presburger


lemma rders_simp_bounded: shows
"\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
  apply(induct r)
       apply(rule_tac x = "Suc 0 " in exI)
  using three_easy_cases0 apply force
  using three_easy_cases1 apply blast
  using three_easy_casesC apply blast
  using seq_closed_form_bounded apply blast
  apply (metis alts_closed_form_bounded size_list_estimation')
  using star_closed_form_bounded by blast
















(*Obsolete materials*)



end