theory GeneralRegexBound
imports "BasicIdentities"
begin
lemma size_geq1:
shows "rsize r \<ge> 1"
by (induct r) auto
definition RSEQ_set where
"RSEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}"
definition RSEQ_set_cartesian where
"RSEQ_set_cartesian A = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}"
definition RALT_set where
"RALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> rsizes rs \<le> n}"
definition RALTs_set where
"RALTs_set A n \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> rsizes rs \<le> n}"
definition RNTIMES_set where
"RNTIMES_set A n \<equiv> {RNTIMES r m | m r. r \<in> A \<and> rsize r + m \<le> n}"
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> (RSEQ_set (sizeNregex n) n)
\<union> (RALTs_set (sizeNregex n) n))
\<union> (RNTIMES_set (sizeNregex n) n)"
apply(auto)
apply(case_tac x)
apply(auto simp add: RSEQ_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: RALTs_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: RNTIMES_set_def)
apply (simp add: sizeNregex_def)
using sizeNregex_def apply force
apply (simp add: sizeNregex_def)
apply (simp add: sizeNregex_def)
apply (simp add: sizeNregex_def)
apply (simp add: RALTs_set_def)
apply(simp add: sizeNregex_def)
apply(auto)
using ex_in_conv apply fastforce
apply (simp add: RNTIMES_set_def)
apply(simp add: sizeNregex_def)
by force
lemma s4:
"RSEQ_set A n \<subseteq> RSEQ_set_cartesian A"
using RSEQ_set_cartesian_def RSEQ_set_def by fastforce
lemma s5:
assumes "finite A"
shows "finite (RSEQ_set_cartesian A)"
using assms
apply(subgoal_tac "RSEQ_set_cartesian A = (\<lambda>(x1, x2). RSEQ x1 x2) ` (A \<times> A)")
apply simp
unfolding RSEQ_set_cartesian_def
apply(auto)
done
definition RALTs_set_length
where
"RALTs_set_length A n l \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> rsizes rs \<le> n \<and> length rs \<le> l}"
definition RALTs_set_length2
where
"RALTs_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 "RALTs_set_length A n l \<subseteq> RALTs_set_length2 A l"
apply(auto simp add: RALTs_set_length2_def RALTs_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 "rsizes 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 "rsizes rs \<le> n \<Longrightarrow> length rs \<le> n"
by (meson order.trans size_sum_more_than_len)
lemma t2:
shows "RALTs_set A n \<subseteq> RALTs_set_length A n n"
unfolding RALTs_set_length_def RALTs_set_def
apply(auto)
using sum_list_len by blast
lemma s8_aux:
assumes "finite A"
shows "finite (RALTs_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)) = RALTs_set_length2 A n"
unfolding RALTs_set_length2_def set_length2_def
by (auto)
ultimately have "finite (RALTs_set_length2 A n)"
by (metis finite_imageI)
then show ?thesis
by (metis infinite_super r000)
qed
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)
thm RNTIMES_set_def
lemma s9_aux0:
shows "RNTIMES_set (insert r A) n \<subseteq> RNTIMES_set A n \<union> (\<Union> i \<in> {..n}. {RNTIMES r i})"
apply(auto simp add: RNTIMES_set_def)
done
lemma s9_aux:
assumes "finite A"
shows "finite (RNTIMES_set A n)"
using assms
apply(induct A arbitrary: n)
apply(auto simp add: RNTIMES_set_def)[1]
apply(subgoal_tac "finite (RNTIMES_set F n \<union> (\<Union> i \<in> {..n}. {RNTIMES x i}))")
apply (metis finite_subset s9_aux0)
by blast
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)
by (simp add: s9_aux)
lemma three_easy_cases0:
shows "rsize (rders_simp RZERO s) \<le> Suc 0"
apply(induct s)
apply simp
apply simp
done
lemma three_easy_cases1:
shows "rsize (rders_simp RONE s) \<le> Suc 0"
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"
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
unused_thms
end