theory GeneralRegexBound imports 
"BasicIdentities"
begin


lemma non_zero_size:
  shows "rsize r \<ge> Suc 0"
  apply(induct r)
  apply auto done

corollary size_geq1:
  shows "rsize r \<ge> 1"
  by (simp add: non_zero_size)


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 SEQ_set_cartesian where
"SEQ_set_cartesian A n  = {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
  "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 chars_finite:
  shows "finite (RCHAR ` (UNIV::(char set)))"
  apply(simp)
  done

thm full_SetCompr_eq 

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


lemma three_easy_cases1: shows 
"rsize (rders_simp RONE s) \<le> Suc 0"
  sorry

lemma three_easy_casesC: shows
"rsize (rders_simp (RCHAR c) s) \<le> Suc 0"

  sorry




end