|
1 theory GeneralRegexBound |
|
2 imports "BasicIdentities" |
|
3 begin |
|
4 |
|
5 lemma size_geq1: |
|
6 shows "rsize r \<ge> 1" |
|
7 by (induct r) auto |
|
8 |
|
9 definition RSEQ_set where |
|
10 "RSEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}" |
|
11 |
|
12 definition RSEQ_set_cartesian where |
|
13 "RSEQ_set_cartesian A = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}" |
|
14 |
|
15 definition RALT_set where |
|
16 "RALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> rsizes rs \<le> n}" |
|
17 |
|
18 definition RALTs_set where |
|
19 "RALTs_set A n \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> rsizes rs \<le> n}" |
|
20 |
|
21 definition |
|
22 "sizeNregex N \<equiv> {r. rsize r \<le> N}" |
|
23 |
|
24 |
|
25 lemma sizenregex_induct1: |
|
26 "sizeNregex (Suc n) = (({RZERO, RONE} \<union> {RCHAR c| c. True}) |
|
27 \<union> (RSTAR ` sizeNregex n) |
|
28 \<union> (RSEQ_set (sizeNregex n) n) |
|
29 \<union> (RALTs_set (sizeNregex n) n))" |
|
30 apply(auto) |
|
31 apply(case_tac x) |
|
32 apply(auto simp add: RSEQ_set_def) |
|
33 using sizeNregex_def apply force |
|
34 using sizeNregex_def apply auto[1] |
|
35 apply (simp add: sizeNregex_def) |
|
36 apply (simp add: sizeNregex_def) |
|
37 apply (simp add: RALTs_set_def) |
|
38 apply (metis imageI list.set_map member_le_sum_list order_trans) |
|
39 apply (simp add: sizeNregex_def) |
|
40 apply (simp add: sizeNregex_def) |
|
41 apply (simp add: sizeNregex_def) |
|
42 using sizeNregex_def apply force |
|
43 apply (simp add: sizeNregex_def) |
|
44 apply (simp add: sizeNregex_def) |
|
45 apply (simp add: RALTs_set_def) |
|
46 apply(simp add: sizeNregex_def) |
|
47 apply(auto) |
|
48 using ex_in_conv by fastforce |
|
49 |
|
50 lemma s4: |
|
51 "RSEQ_set A n \<subseteq> RSEQ_set_cartesian A" |
|
52 using RSEQ_set_cartesian_def RSEQ_set_def by fastforce |
|
53 |
|
54 lemma s5: |
|
55 assumes "finite A" |
|
56 shows "finite (RSEQ_set_cartesian A)" |
|
57 using assms |
|
58 apply(subgoal_tac "RSEQ_set_cartesian A = (\<lambda>(x1, x2). RSEQ x1 x2) ` (A \<times> A)") |
|
59 apply simp |
|
60 unfolding RSEQ_set_cartesian_def |
|
61 apply(auto) |
|
62 done |
|
63 |
|
64 |
|
65 definition RALTs_set_length |
|
66 where |
|
67 "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}" |
|
68 |
|
69 |
|
70 definition RALTs_set_length2 |
|
71 where |
|
72 "RALTs_set_length2 A l \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> length rs \<le> l}" |
|
73 |
|
74 definition set_length2 |
|
75 where |
|
76 "set_length2 A l \<equiv> {rs. \<forall>r \<in> set rs. r \<in> A \<and> length rs \<le> l}" |
|
77 |
|
78 |
|
79 lemma r000: |
|
80 shows "RALTs_set_length A n l \<subseteq> RALTs_set_length2 A l" |
|
81 apply(auto simp add: RALTs_set_length2_def RALTs_set_length_def) |
|
82 done |
|
83 |
|
84 |
|
85 lemma r02: |
|
86 shows "set_length2 A 0 \<subseteq> {[]}" |
|
87 apply(auto simp add: set_length2_def) |
|
88 apply(case_tac x) |
|
89 apply(auto) |
|
90 done |
|
91 |
|
92 lemma r03: |
|
93 shows "set_length2 A (Suc n) \<subseteq> |
|
94 {[]} \<union> (\<lambda>(h, t). h # t) ` (A \<times> (set_length2 A n))" |
|
95 apply(auto simp add: set_length2_def) |
|
96 apply(case_tac x) |
|
97 apply(auto) |
|
98 done |
|
99 |
|
100 lemma r1: |
|
101 assumes "finite A" |
|
102 shows "finite (set_length2 A n)" |
|
103 using assms |
|
104 apply(induct n) |
|
105 apply(rule finite_subset) |
|
106 apply(rule r02) |
|
107 apply(simp) |
|
108 apply(rule finite_subset) |
|
109 apply(rule r03) |
|
110 apply(simp) |
|
111 done |
|
112 |
|
113 lemma size_sum_more_than_len: |
|
114 shows "rsizes rs \<ge> length rs" |
|
115 apply(induct rs) |
|
116 apply simp |
|
117 apply simp |
|
118 apply(subgoal_tac "rsize a \<ge> 1") |
|
119 apply linarith |
|
120 using size_geq1 by auto |
|
121 |
|
122 |
|
123 lemma sum_list_len: |
|
124 shows "rsizes rs \<le> n \<Longrightarrow> length rs \<le> n" |
|
125 by (meson order.trans size_sum_more_than_len) |
|
126 |
|
127 |
|
128 lemma t2: |
|
129 shows "RALTs_set A n \<subseteq> RALTs_set_length A n n" |
|
130 unfolding RALTs_set_length_def RALTs_set_def |
|
131 apply(auto) |
|
132 using sum_list_len by blast |
|
133 |
|
134 lemma s8_aux: |
|
135 assumes "finite A" |
|
136 shows "finite (RALTs_set_length A n n)" |
|
137 proof - |
|
138 have "finite A" by fact |
|
139 then have "finite (set_length2 A n)" |
|
140 by (simp add: r1) |
|
141 moreover have "(RALTS ` (set_length2 A n)) = RALTs_set_length2 A n" |
|
142 unfolding RALTs_set_length2_def set_length2_def |
|
143 by (auto) |
|
144 ultimately have "finite (RALTs_set_length2 A n)" |
|
145 by (metis finite_imageI) |
|
146 then show ?thesis |
|
147 by (metis infinite_super r000) |
|
148 qed |
|
149 |
|
150 lemma char_finite: |
|
151 shows "finite {RCHAR c |c. True}" |
|
152 apply simp |
|
153 apply(subgoal_tac "finite (RCHAR ` (UNIV::char set))") |
|
154 prefer 2 |
|
155 apply simp |
|
156 by (simp add: full_SetCompr_eq) |
|
157 |
|
158 |
|
159 lemma finite_size_n: |
|
160 shows "finite (sizeNregex n)" |
|
161 apply(induct n) |
|
162 apply(simp add: sizeNregex_def) |
|
163 apply (metis (mono_tags, lifting) not_finite_existsD not_one_le_zero size_geq1) |
|
164 apply(subst sizenregex_induct1) |
|
165 apply(simp only: finite_Un) |
|
166 apply(rule conjI)+ |
|
167 apply(simp) |
|
168 |
|
169 using char_finite apply blast |
|
170 apply(simp) |
|
171 apply(rule finite_subset) |
|
172 apply(rule s4) |
|
173 apply(rule s5) |
|
174 apply(simp) |
|
175 apply(rule finite_subset) |
|
176 apply(rule t2) |
|
177 apply(rule s8_aux) |
|
178 apply(simp) |
|
179 done |
|
180 |
|
181 lemma three_easy_cases0: |
|
182 shows "rsize (rders_simp RZERO s) \<le> Suc 0" |
|
183 apply(induct s) |
|
184 apply simp |
|
185 apply simp |
|
186 done |
|
187 |
|
188 |
|
189 lemma three_easy_cases1: |
|
190 shows "rsize (rders_simp RONE s) \<le> Suc 0" |
|
191 apply(induct s) |
|
192 apply simp |
|
193 apply simp |
|
194 using three_easy_cases0 by auto |
|
195 |
|
196 |
|
197 lemma three_easy_casesC: |
|
198 shows "rsize (rders_simp (RCHAR c) s) \<le> Suc 0" |
|
199 apply(induct s) |
|
200 apply simp |
|
201 apply simp |
|
202 apply(case_tac " a = c") |
|
203 using three_easy_cases1 apply blast |
|
204 apply simp |
|
205 using three_easy_cases0 by force |
|
206 |
|
207 |
|
208 unused_thms |
|
209 |
|
210 |
|
211 end |
|
212 |