diff -r c6351a96bf80 -r a7e98deebb5c thys2/GeneralRegexBound.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/GeneralRegexBound.thy	Wed Mar 09 17:33:08 2022 +0000
@@ -0,0 +1,97 @@
+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
+