theory ClosedFormsBounds
  imports "GeneralRegexBound" "ClosedForms"
begin



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 * (card (sizeNregex N)))) (rsize (RALTS rs) )"
  apply(induct s)
  apply simp
  apply(insert alts_closed_form_variant)

  
  sorry



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]]) ) {})  ) )"

  sorry

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"

  sorry


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)))
"
  sorry

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)) {})))"
  
  sorry

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))))"
  sorry

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 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