1 |
|
2 theory ClosedFormsBounds |
|
3 imports "GeneralRegexBound" "ClosedForms" |
|
4 begin |
|
5 lemma alts_ders_lambda_shape_ders: |
|
6 shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s" |
|
7 by (simp add: image_iff) |
|
8 |
|
9 lemma rlist_bound: |
|
10 assumes "\<forall>r \<in> set rs. rsize r \<le> N" |
|
11 shows "rsizes rs \<le> N * (length rs)" |
|
12 using assms |
|
13 apply(induct rs) |
|
14 apply simp |
|
15 by simp |
|
16 |
|
17 lemma alts_closed_form_bounded: |
|
18 assumes "\<forall>r \<in> set rs. \<forall>s. rsize (rders_simp r s) \<le> N" |
|
19 shows "rsize (rders_simp (RALTS rs) s) \<le> max (Suc (N * (length rs))) (rsize (RALTS rs))" |
|
20 proof (cases s) |
|
21 case Nil |
|
22 then show "rsize (rders_simp (RALTS rs) s) \<le> max (Suc (N * length rs)) (rsize (RALTS rs))" |
|
23 by simp |
|
24 next |
|
25 case (Cons a s) |
|
26 |
|
27 from assms have "\<forall>r \<in> set (map (\<lambda>r. rders_simp r (a # s)) rs ). rsize r \<le> N" |
|
28 by (metis alts_ders_lambda_shape_ders) |
|
29 then have a: "rsizes (map (\<lambda>r. rders_simp r (a # s)) rs ) \<le> N * (length rs)" |
|
30 by (metis length_map rlist_bound) |
|
31 |
|
32 have "rsize (rders_simp (RALTS rs) (a # s)) |
|
33 = rsize (rsimp (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs)))" |
|
34 by (metis alts_closed_form_variant list.distinct(1)) |
|
35 also have "... \<le> rsize (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs))" |
|
36 using rsimp_mono by blast |
|
37 also have "... = Suc (rsizes (map (\<lambda>r. rders_simp r (a # s)) rs))" |
|
38 by simp |
|
39 also have "... \<le> Suc (N * (length rs))" |
|
40 using a by blast |
|
41 finally have "rsize (rders_simp (RALTS rs) (a # s)) \<le> max (Suc (N * length rs)) (rsize (RALTS rs))" |
|
42 by auto |
|
43 then show ?thesis using local.Cons by simp |
|
44 qed |
|
45 |
|
46 lemma alts_simp_ineq_unfold: |
|
47 shows "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct (rflts (map rsimp rs)) {}))" |
|
48 using rsimp_aalts_smaller by auto |
|
49 |
|
50 |
|
51 lemma rdistinct_mono_list: |
|
52 shows "rsizes (rdistinct (x5 @ rs) rset) \<le> rsizes x5 + rsizes (rdistinct rs ((set x5 ) \<union> rset))" |
|
53 apply(induct x5 arbitrary: rs rset) |
|
54 apply simp |
|
55 apply(case_tac "a \<in> rset") |
|
56 apply simp |
|
57 apply (simp add: add.assoc insert_absorb trans_le_add2) |
|
58 apply simp |
|
59 by (metis Un_insert_right) |
|
60 |
|
61 |
|
62 lemma flts_size_reduction_alts: |
|
63 assumes a: "\<And>noalts_set alts_set corr_set. |
|
64 (\<forall>r\<in>noalts_set. \<forall>xs. r \<noteq> RALTS xs) \<and> |
|
65 (\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) \<Longrightarrow> |
|
66 Suc (rsizes (rdistinct (rflts rs) (noalts_set \<union> corr_set))) |
|
67 \<le> Suc (rsizes (rdistinct rs (insert RZERO (noalts_set \<union> alts_set))))" |
|
68 and b: "\<forall>r\<in>noalts_set. \<forall>xs. r \<noteq> RALTS xs" |
|
69 and c: "\<forall>a\<in>alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set" |
|
70 and d: "a = RALTS x5" |
|
71 shows "rsizes (rdistinct (rflts (a # rs)) (noalts_set \<union> corr_set)) |
|
72 \<le> rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))" |
|
73 |
|
74 apply(case_tac "a \<in> alts_set") |
|
75 using a b c d |
|
76 apply simp |
|
77 apply(subgoal_tac "set x5 \<subseteq> corr_set") |
|
78 apply(subst rdistinct_concat) |
|
79 apply auto[1] |
|
80 apply presburger |
|
81 apply fastforce |
|
82 using a b c d |
|
83 apply (subgoal_tac "a \<notin> noalts_set") |
|
84 prefer 2 |
|
85 apply blast |
|
86 apply simp |
|
87 apply(subgoal_tac "rsizes (rdistinct (x5 @ rflts rs) (noalts_set \<union> corr_set)) |
|
88 \<le> rsizes x5 + rsizes (rdistinct (rflts rs) ((set x5) \<union> (noalts_set \<union> corr_set)))") |
|
89 prefer 2 |
|
90 using rdistinct_mono_list apply presburger |
|
91 apply(subgoal_tac "insert (RALTS x5) (noalts_set \<union> alts_set) = noalts_set \<union> (insert (RALTS x5) alts_set)") |
|
92 apply(simp only:) |
|
93 apply(subgoal_tac "rsizes x5 + rsizes (rdistinct (rflts rs) (noalts_set \<union> (corr_set \<union> (set x5)))) \<le> |
|
94 rsizes x5 + rsizes (rdistinct rs (insert RZERO (noalts_set \<union> insert (RALTS x5) alts_set)))") |
|
95 |
|
96 apply (simp add: Un_left_commute inf_sup_aci(5)) |
|
97 apply(subgoal_tac "rsizes (rdistinct (rflts rs) (noalts_set \<union> (corr_set \<union> set x5))) \<le> |
|
98 rsizes (rdistinct rs (insert RZERO (noalts_set \<union> insert (RALTS x5) alts_set)))") |
|
99 apply linarith |
|
100 apply(subgoal_tac "\<forall>r \<in> insert (RALTS x5) alts_set. \<exists>xs1.( r = RALTS xs1 \<and> set xs1 \<subseteq> corr_set \<union> set x5)") |
|
101 apply presburger |
|
102 apply (meson insert_iff sup.cobounded2 sup.coboundedI1) |
|
103 by blast |
|
104 |
|
105 |
|
106 lemma flts_vs_nflts1: |
|
107 assumes "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs" |
|
108 and "\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)" |
|
109 shows "rsizes (rdistinct (rflts rs) (noalts_set \<union> corr_set)) |
|
110 \<le> rsizes (rdistinct rs (insert RZERO (noalts_set \<union> alts_set)))" |
|
111 using assms |
|
112 apply(induct rs arbitrary: noalts_set alts_set corr_set) |
|
113 apply simp |
|
114 apply(case_tac a) |
|
115 apply(case_tac "RZERO \<in> noalts_set") |
|
116 apply simp |
|
117 apply(subgoal_tac "RZERO \<notin> alts_set") |
|
118 apply simp |
|
119 apply fastforce |
|
120 apply(case_tac "RONE \<in> noalts_set") |
|
121 apply simp |
|
122 apply(subgoal_tac "RONE \<notin> alts_set") |
|
123 prefer 2 |
|
124 apply fastforce |
|
125 apply(case_tac "RONE \<in> corr_set") |
|
126 apply(subgoal_tac "rflts (a # rs) = RONE # rflts rs") |
|
127 apply(simp only:) |
|
128 apply(subgoal_tac "rdistinct (RONE # rflts rs) (noalts_set \<union> corr_set) = |
|
129 rdistinct (rflts rs) (noalts_set \<union> corr_set)") |
|
130 apply(simp only:) |
|
131 apply(subgoal_tac "rdistinct (RONE # rs) (insert RZERO (noalts_set \<union> alts_set)) = |
|
132 RONE # (rdistinct rs (insert RONE (insert RZERO (noalts_set \<union> alts_set)))) ") |
|
133 apply(simp only:) |
|
134 apply(subgoal_tac "rdistinct (rflts rs) (noalts_set \<union> corr_set) = |
|
135 rdistinct (rflts rs) (insert RONE (noalts_set \<union> corr_set))") |
|
136 apply (simp only:) |
|
137 apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set") |
|
138 apply(simp only:) |
|
139 apply(subgoal_tac "insert RONE (insert RZERO (noalts_set \<union> alts_set)) = |
|
140 insert RZERO ((insert RONE noalts_set) \<union> alts_set)") |
|
141 apply(simp only:) |
|
142 apply(subgoal_tac "rsizes (rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set))) |
|
143 \<le> rsizes (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))") |
|
144 apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15)) |
|
145 apply (metis (no_types, opaque_lifting) le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le) |
|
146 apply fastforce |
|
147 apply fastforce |
|
148 apply (metis Un_iff insert_absorb) |
|
149 apply (metis UnE insertE insert_is_Un rdistinct.simps(2) rrexp.distinct(1)) |
|
150 apply (meson UnCI rdistinct.simps(2)) |
|
151 using rflts.simps(4) apply presburger |
|
152 apply simp |
|
153 apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set") |
|
154 apply(simp only:) |
|
155 apply (metis Un_insert_left insertE rrexp.distinct(15)) |
|
156 apply fastforce |
|
157 apply(case_tac "a \<in> noalts_set") |
|
158 apply simp |
|
159 apply(subgoal_tac "a \<notin> alts_set") |
|
160 prefer 2 |
|
161 apply blast |
|
162 apply(case_tac "a \<in> corr_set") |
|
163 apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)") |
|
164 prefer 2 |
|
165 apply fastforce |
|
166 apply(simp only:) |
|
167 apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))) \<le> |
|
168 rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))") |
|
169 |
|
170 apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)) \<le> |
|
171 rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set)))") |
|
172 apply fastforce |
|
173 apply simp |
|
174 apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set") |
|
175 apply(simp only:) |
|
176 apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set") |
|
177 apply(simp only:) |
|
178 apply (metis insertE rrexp.distinct(21)) |
|
179 apply blast |
|
180 |
|
181 apply fastforce |
|
182 apply force |
|
183 apply simp |
|
184 apply (metis Un_insert_left insert_iff rrexp.distinct(21)) |
|
185 apply(case_tac "a \<in> noalts_set") |
|
186 apply simp |
|
187 apply(subgoal_tac "a \<notin> alts_set") |
|
188 prefer 2 |
|
189 apply blast |
|
190 apply(case_tac "a \<in> corr_set") |
|
191 apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)") |
|
192 prefer 2 |
|
193 apply fastforce |
|
194 apply(simp only:) |
|
195 apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))) \<le> |
|
196 rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))") |
|
197 |
|
198 apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)) \<le> |
|
199 rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set)))") |
|
200 apply fastforce |
|
201 apply simp |
|
202 apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set") |
|
203 apply(simp only:) |
|
204 apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set") |
|
205 apply(simp only:) |
|
206 |
|
207 |
|
208 apply (metis insertE rrexp.distinct(25)) |
|
209 apply blast |
|
210 apply fastforce |
|
211 apply force |
|
212 apply simp |
|
213 |
|
214 apply (metis Un_insert_left insertE rrexp.distinct(25)) |
|
215 |
|
216 using Suc_le_mono flts_size_reduction_alts apply presburger |
|
217 apply(case_tac "a \<in> noalts_set") |
|
218 apply simp |
|
219 apply(subgoal_tac "a \<notin> alts_set") |
|
220 prefer 2 |
|
221 apply blast |
|
222 apply(case_tac "a \<in> corr_set") |
|
223 apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)") |
|
224 prefer 2 |
|
225 apply fastforce |
|
226 apply(simp only:) |
|
227 apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))) \<le> |
|
228 rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))") |
|
229 |
|
230 apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)) \<le> |
|
231 rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set)))") |
|
232 apply fastforce |
|
233 apply simp |
|
234 apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set") |
|
235 apply(simp only:) |
|
236 apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set") |
|
237 apply(simp only:) |
|
238 apply (metis insertE rrexp.distinct(29)) |
|
239 |
|
240 apply blast |
|
241 |
|
242 apply fastforce |
|
243 apply force |
|
244 apply simp |
|
245 apply (metis Un_insert_left insert_iff rrexp.distinct(29)) |
|
246 done |
|
247 |
|
248 |
|
249 lemma flts_vs_nflts: |
|
250 assumes "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs" |
|
251 and "\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)" |
|
252 shows "rsizes (rdistinct (rflts rs) (noalts_set \<union> corr_set)) |
|
253 \<le> rsizes (rdistinct rs (insert RZERO (noalts_set \<union> alts_set)))" |
|
254 by (simp add: assms flts_vs_nflts1) |
|
255 |
|
256 lemma distinct_simp_ineq_general: |
|
257 assumes "rsimp ` no_simp = has_simp" "finite no_simp" |
|
258 shows "rsizes (rdistinct (map rsimp rs) has_simp) \<le> rsizes (rdistinct rs no_simp)" |
|
259 using assms |
|
260 apply(induct rs no_simp arbitrary: has_simp rule: rdistinct.induct) |
|
261 apply simp |
|
262 apply(auto) |
|
263 using add_le_mono rsimp_mono by presburger |
|
264 |
|
265 lemma larger_acc_smaller_distinct_res0: |
|
266 assumes "ss \<subseteq> SS" |
|
267 shows "rsizes (rdistinct rs SS) \<le> rsizes (rdistinct rs ss)" |
|
268 using assms |
|
269 apply(induct rs arbitrary: ss SS) |
|
270 apply simp |
|
271 by (metis distinct_early_app1 rdistinct_smaller) |
|
272 |
|
273 lemma without_flts_ineq: |
|
274 shows "rsizes (rdistinct (rflts rs) {}) \<le> rsizes (rdistinct rs {})" |
|
275 proof - |
|
276 have "rsizes (rdistinct (rflts rs) {}) \<le> rsizes (rdistinct rs (insert RZERO {}))" |
|
277 by (metis empty_iff flts_vs_nflts sup_bot_left) |
|
278 also have "... \<le> rsizes (rdistinct rs {})" |
|
279 by (simp add: larger_acc_smaller_distinct_res0) |
|
280 finally show ?thesis |
|
281 by blast |
|
282 qed |
|
283 |
|
284 |
|
285 lemma distinct_simp_ineq: |
|
286 shows "rsizes (rdistinct (map rsimp rs) {}) \<le> rsizes (rdistinct rs {})" |
|
287 using distinct_simp_ineq_general by blast |
|
288 |
|
289 |
|
290 lemma alts_simp_control: |
|
291 shows "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct rs {}))" |
|
292 proof - |
|
293 have "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct (rflts (map rsimp rs)) {}))" |
|
294 using alts_simp_ineq_unfold by auto |
|
295 moreover have "\<dots> \<le> Suc (rsizes (rdistinct (map rsimp rs) {}))" |
|
296 using without_flts_ineq by blast |
|
297 ultimately show "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct rs {}))" |
|
298 by (meson Suc_le_mono distinct_simp_ineq le_trans) |
|
299 qed |
|
300 |
|
301 |
|
302 lemma larger_acc_smaller_distinct_res: |
|
303 shows "rsizes (rdistinct rs (insert a ss)) \<le> rsizes (rdistinct rs ss)" |
|
304 by (simp add: larger_acc_smaller_distinct_res0 subset_insertI) |
|
305 |
|
306 lemma triangle_inequality_distinct: |
|
307 shows "rsizes (rdistinct (a # rs) ss) \<le> rsize a + rsizes (rdistinct rs ss)" |
|
308 apply(case_tac "a \<in> ss") |
|
309 apply simp |
|
310 by (simp add: larger_acc_smaller_distinct_res) |
|
311 |
|
312 |
|
313 lemma distinct_list_size_len_bounded: |
|
314 assumes "\<forall>r \<in> set rs. rsize r \<le> N" "length rs \<le> lrs" |
|
315 shows "rsizes rs \<le> lrs * N " |
|
316 using assms |
|
317 by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1) |
|
318 |
|
319 |
|
320 |
|
321 lemma rdistinct_same_set: |
|
322 shows "r \<in> set rs \<longleftrightarrow> r \<in> set (rdistinct rs {})" |
|
323 apply(induct rs) |
|
324 apply simp |
|
325 by (metis rdistinct_set_equality) |
|
326 |
|
327 (* distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size *) |
|
328 lemma distinct_list_rexp_upto: |
|
329 assumes "\<forall>r\<in> set rs. (rsize r) \<le> N" |
|
330 shows "rsizes (rdistinct rs {}) \<le> (card (sizeNregex N)) * N" |
|
331 |
|
332 apply(subgoal_tac "distinct (rdistinct rs {})") |
|
333 prefer 2 |
|
334 using rdistinct_does_the_job apply blast |
|
335 apply(subgoal_tac "length (rdistinct rs {}) \<le> card (sizeNregex N)") |
|
336 apply(rule distinct_list_size_len_bounded) |
|
337 using assms |
|
338 apply (meson rdistinct_same_set) |
|
339 apply blast |
|
340 apply(subgoal_tac "\<forall>r \<in> set (rdistinct rs {}). rsize r \<le> N") |
|
341 prefer 2 |
|
342 using assms |
|
343 apply (meson rdistinct_same_set) |
|
344 apply(subgoal_tac "length (rdistinct rs {}) = card (set (rdistinct rs {}))") |
|
345 prefer 2 |
|
346 apply (simp add: distinct_card) |
|
347 apply(simp) |
|
348 by (metis card_mono finite_size_n mem_Collect_eq sizeNregex_def subsetI) |
|
349 |
|
350 |
|
351 lemma star_control_bounded: |
|
352 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
353 shows "rsizes (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates s r [[c]])) {}) |
|
354 \<le> (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r)))" |
|
355 by (smt (verit) add_Suc_shift add_mono_thms_linordered_semiring(3) assms distinct_list_rexp_upto image_iff list.set_map plus_nat.simps(2) rsize.simps(5)) |
|
356 |
|
357 |
|
358 lemma star_closed_form_bounded: |
|
359 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
360 shows "rsize (rders_simp (RSTAR r) s) \<le> |
|
361 max ((Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r))))) (rsize (RSTAR r))" |
|
362 proof(cases s) |
|
363 case Nil |
|
364 then show "rsize (rders_simp (RSTAR r) s) |
|
365 \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))" |
|
366 by simp |
|
367 next |
|
368 case (Cons a list) |
|
369 then have "rsize (rders_simp (RSTAR r) s) = |
|
370 rsize (rsimp (RALTS ((map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])))))" |
|
371 using star_closed_form by fastforce |
|
372 also have "... \<le> Suc (rsizes (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])) {}))" |
|
373 using alts_simp_control by blast |
|
374 also have "... \<le> Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r)))" |
|
375 using star_control_bounded[OF assms] by (metis add_mono le_add1 mult_Suc plus_1_eq_Suc) |
|
376 also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))" |
|
377 by simp |
|
378 finally show ?thesis by simp |
|
379 qed |
|
380 |
|
381 |
|
382 lemma seq_estimate_bounded: |
|
383 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" |
|
384 and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
|
385 shows |
|
386 "rsizes (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}) |
|
387 \<le> (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))" |
|
388 proof - |
|
389 have a: "rsizes (rdistinct (map (rders_simp r2) (vsuf s r1)) {}) \<le> N2 * card (sizeNregex N2)" |
|
390 by (metis assms(2) distinct_list_rexp_upto ex_map_conv mult.commute) |
|
391 |
|
392 have "rsizes (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}) \<le> |
|
393 rsize (RSEQ (rders_simp r1 s) r2) + rsizes (rdistinct (map (rders_simp r2) (vsuf s r1)) {})" |
|
394 using triangle_inequality_distinct by blast |
|
395 also have "... \<le> rsize (RSEQ (rders_simp r1 s) r2) + N2 * card (sizeNregex N2)" |
|
396 by (simp add: a) |
|
397 also have "... \<le> Suc (N1 + (rsize r2) + N2 * card (sizeNregex N2))" |
|
398 by (simp add: assms(1)) |
|
399 finally show ?thesis |
|
400 by force |
|
401 qed |
|
402 |
|
403 |
|
404 lemma seq_closed_form_bounded2: |
|
405 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" |
|
406 and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
|
407 shows "rsize (rders_simp (RSEQ r1 r2) s) |
|
408 \<le> max (2 + N1 + (rsize r2) + (N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" |
|
409 proof(cases s) |
|
410 case Nil |
|
411 then show "rsize (rders_simp (RSEQ r1 r2) s) |
|
412 \<le> max (2 + N1 + (rsize r2) + (N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" |
|
413 by simp |
|
414 next |
|
415 case (Cons a list) |
|
416 then have "rsize (rders_simp (RSEQ r1 r2) s) = |
|
417 rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1)))))" |
|
418 using seq_closed_form_variant by (metis list.distinct(1)) |
|
419 also have "... \<le> Suc (rsizes (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))" |
|
420 using alts_simp_control by blast |
|
421 also have "... \<le> 2 + N1 + (rsize r2) + (N2 * card (sizeNregex N2))" |
|
422 using seq_estimate_bounded[OF assms] by auto |
|
423 ultimately show "rsize (rders_simp (RSEQ r1 r2) s) |
|
424 \<le> max (2 + N1 + (rsize r2) + N2 * card (sizeNregex N2)) (rsize (RSEQ r1 r2))" |
|
425 by auto |
|
426 qed |
|
427 |
|
428 |
|
429 lemma rders_simp_bounded: |
|
430 shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N" |
|
431 apply(induct r) |
|
432 apply(rule_tac x = "Suc 0 " in exI) |
|
433 using three_easy_cases0 apply force |
|
434 using three_easy_cases1 apply blast |
|
435 using three_easy_casesC apply blast |
|
436 apply(erule exE)+ |
|
437 apply(rule exI) |
|
438 apply(rule allI) |
|
439 apply(rule seq_closed_form_bounded2) |
|
440 apply(assumption) |
|
441 apply(assumption) |
|
442 apply (metis alts_closed_form_bounded size_list_estimation') |
|
443 using star_closed_form_bounded by blast |
|
444 |
|
445 |
|
446 unused_thms |
|
447 |
|
448 end |
|