|
1 theory GeneralRegexBound imports |
|
2 "BasicIdentities" |
|
3 begin |
|
4 |
|
5 |
|
6 lemma non_zero_size: |
|
7 shows "rsize r \<ge> Suc 0" |
|
8 apply(induct r) |
|
9 apply auto done |
|
10 |
|
11 corollary size_geq1: |
|
12 shows "rsize r \<ge> 1" |
|
13 by (simp add: non_zero_size) |
|
14 |
|
15 |
|
16 definition SEQ_set where |
|
17 "SEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}" |
|
18 |
|
19 definition SEQ_set_cartesian where |
|
20 "SEQ_set_cartesian A n = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}" |
|
21 |
|
22 definition ALT_set where |
|
23 "ALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> sum_list (map rsize rs) \<le> n}" |
|
24 |
|
25 |
|
26 definition |
|
27 "sizeNregex N \<equiv> {r. rsize r \<le> N}" |
|
28 |
|
29 lemma sizenregex_induct: |
|
30 shows "sizeNregex (Suc n) = sizeNregex n \<union> {RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True} \<union> |
|
31 SEQ_set ( sizeNregex n) n \<union> ALT_set (sizeNregex n) n \<union> (RSTAR ` (sizeNregex n))" |
|
32 sorry |
|
33 |
|
34 |
|
35 lemma chars_finite: |
|
36 shows "finite (RCHAR ` (UNIV::(char set)))" |
|
37 apply(simp) |
|
38 done |
|
39 |
|
40 thm full_SetCompr_eq |
|
41 |
|
42 lemma size1finite: |
|
43 shows "finite (sizeNregex (Suc 0))" |
|
44 apply(subst sizenregex_induct) |
|
45 apply(subst finite_Un)+ |
|
46 apply(subgoal_tac "sizeNregex 0 = {}") |
|
47 apply(rule conjI)+ |
|
48 apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def) |
|
49 apply simp |
|
50 apply (simp add: full_SetCompr_eq) |
|
51 apply (simp add: SEQ_set_def) |
|
52 apply (simp add: ALT_set_def) |
|
53 apply(simp add: full_SetCompr_eq) |
|
54 using non_zero_size not_less_eq_eq sizeNregex_def by fastforce |
|
55 |
|
56 lemma seq_included_in_cart: |
|
57 shows "SEQ_set A n \<subseteq> SEQ_set_cartesian A n" |
|
58 using SEQ_set_cartesian_def SEQ_set_def by fastforce |
|
59 |
|
60 lemma finite_seq: |
|
61 shows " finite (sizeNregex n) \<Longrightarrow> finite (SEQ_set (sizeNregex n) n)" |
|
62 apply(rule finite_subset) |
|
63 sorry |
|
64 |
|
65 |
|
66 lemma finite_size_n: |
|
67 shows "finite (sizeNregex n)" |
|
68 apply(induct n) |
|
69 apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def) |
|
70 apply(subst sizenregex_induct) |
|
71 apply(subst finite_Un)+ |
|
72 apply(rule conjI)+ |
|
73 apply simp |
|
74 apply simp |
|
75 apply (simp add: full_SetCompr_eq) |
|
76 |
|
77 sorry |
|
78 |
|
79 lemma three_easy_cases0: shows |
|
80 "rsize (rders_simp RZERO s) \<le> Suc 0" |
|
81 sorry |
|
82 |
|
83 |
|
84 lemma three_easy_cases1: shows |
|
85 "rsize (rders_simp RONE s) \<le> Suc 0" |
|
86 sorry |
|
87 |
|
88 lemma three_easy_casesC: shows |
|
89 "rsize (rders_simp (RCHAR c) s) \<le> Suc 0" |
|
90 |
|
91 sorry |
|
92 |
|
93 |
|
94 |
|
95 |
|
96 end |
|
97 |