|
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, ccfv_threshold) dual_order.trans insertE rrexp.distinct(17)) |
|
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(17)) |
|
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 nonalt.simps(1) nonalt.simps(4)) |
|
179 apply blast |
|
180 |
|
181 apply fastforce |
|
182 apply force |
|
183 apply simp |
|
184 apply (metis Un_insert_left insertE nonalt.simps(1) nonalt.simps(4)) |
|
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 apply (metis insertE rrexp.distinct(31)) |
|
208 apply blast |
|
209 apply fastforce |
|
210 apply force |
|
211 apply simp |
|
212 |
|
213 apply (metis Un_insert_left insertE rrexp.distinct(31)) |
|
214 |
|
215 using Suc_le_mono flts_size_reduction_alts apply presburger |
|
216 apply(case_tac "a \<in> noalts_set") |
|
217 apply simp |
|
218 apply(subgoal_tac "a \<notin> alts_set") |
|
219 prefer 2 |
|
220 apply blast |
|
221 apply(case_tac "a \<in> corr_set") |
|
222 apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)") |
|
223 prefer 2 |
|
224 apply fastforce |
|
225 apply(simp only:) |
|
226 apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))) \<le> |
|
227 rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))") |
|
228 |
|
229 apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)) \<le> |
|
230 rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set)))") |
|
231 apply fastforce |
|
232 apply simp |
|
233 apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set") |
|
234 apply(simp only:) |
|
235 apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set") |
|
236 apply(simp only:) |
|
237 apply (metis insertE rrexp.distinct(37)) |
|
238 |
|
239 apply blast |
|
240 |
|
241 apply fastforce |
|
242 apply force |
|
243 apply simp |
|
244 apply (metis Un_insert_left insert_iff rrexp.distinct(37)) |
|
245 apply(case_tac "a \<in> noalts_set") |
|
246 apply simp |
|
247 apply(subgoal_tac "a \<notin> alts_set") |
|
248 prefer 2 |
|
249 apply blast |
|
250 apply(case_tac "a \<in> corr_set") |
|
251 apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set \<union> corr_set)") |
|
252 prefer 2 |
|
253 apply fastforce |
|
254 apply(simp only:) |
|
255 apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))) \<le> |
|
256 rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))") |
|
257 |
|
258 apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)) \<le> |
|
259 rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set)))") |
|
260 apply fastforce |
|
261 apply simp |
|
262 apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set") |
|
263 apply(simp only:) |
|
264 apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set") |
|
265 apply(simp only:) |
|
266 apply (metis insertE nonalt.simps(1) nonalt.simps(7)) |
|
267 apply blast |
|
268 apply blast |
|
269 apply force |
|
270 apply(auto) |
|
271 by (metis Un_insert_left insert_iff rrexp.distinct(39)) |
|
272 |
|
273 |
|
274 lemma flts_vs_nflts: |
|
275 assumes "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs" |
|
276 and "\<forall>a \<in> alts_set. (\<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)" |
|
277 shows "rsizes (rdistinct (rflts rs) (noalts_set \<union> corr_set)) |
|
278 \<le> rsizes (rdistinct rs (insert RZERO (noalts_set \<union> alts_set)))" |
|
279 by (simp add: assms flts_vs_nflts1) |
|
280 |
|
281 lemma distinct_simp_ineq_general: |
|
282 assumes "rsimp ` no_simp = has_simp" "finite no_simp" |
|
283 shows "rsizes (rdistinct (map rsimp rs) has_simp) \<le> rsizes (rdistinct rs no_simp)" |
|
284 using assms |
|
285 apply(induct rs no_simp arbitrary: has_simp rule: rdistinct.induct) |
|
286 apply simp |
|
287 apply(auto) |
|
288 using add_le_mono rsimp_mono by presburger |
|
289 |
|
290 lemma larger_acc_smaller_distinct_res0: |
|
291 assumes "ss \<subseteq> SS" |
|
292 shows "rsizes (rdistinct rs SS) \<le> rsizes (rdistinct rs ss)" |
|
293 using assms |
|
294 apply(induct rs arbitrary: ss SS) |
|
295 apply simp |
|
296 by (metis distinct_early_app1 rdistinct_smaller) |
|
297 |
|
298 lemma without_flts_ineq: |
|
299 shows "rsizes (rdistinct (rflts rs) {}) \<le> rsizes (rdistinct rs {})" |
|
300 proof - |
|
301 have "rsizes (rdistinct (rflts rs) {}) \<le> rsizes (rdistinct rs (insert RZERO {}))" |
|
302 by (metis empty_iff flts_vs_nflts sup_bot_left) |
|
303 also have "... \<le> rsizes (rdistinct rs {})" |
|
304 by (simp add: larger_acc_smaller_distinct_res0) |
|
305 finally show ?thesis |
|
306 by blast |
|
307 qed |
|
308 |
|
309 |
|
310 lemma distinct_simp_ineq: |
|
311 shows "rsizes (rdistinct (map rsimp rs) {}) \<le> rsizes (rdistinct rs {})" |
|
312 using distinct_simp_ineq_general by blast |
|
313 |
|
314 |
|
315 lemma alts_simp_control: |
|
316 shows "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct rs {}))" |
|
317 proof - |
|
318 have "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct (rflts (map rsimp rs)) {}))" |
|
319 using alts_simp_ineq_unfold by auto |
|
320 moreover have "\<dots> \<le> Suc (rsizes (rdistinct (map rsimp rs) {}))" |
|
321 using without_flts_ineq by blast |
|
322 ultimately show "rsize (rsimp (RALTS rs)) \<le> Suc (rsizes (rdistinct rs {}))" |
|
323 by (meson Suc_le_mono distinct_simp_ineq le_trans) |
|
324 qed |
|
325 |
|
326 |
|
327 lemma larger_acc_smaller_distinct_res: |
|
328 shows "rsizes (rdistinct rs (insert a ss)) \<le> rsizes (rdistinct rs ss)" |
|
329 by (simp add: larger_acc_smaller_distinct_res0 subset_insertI) |
|
330 |
|
331 lemma triangle_inequality_distinct: |
|
332 shows "rsizes (rdistinct (a # rs) ss) \<le> rsize a + rsizes (rdistinct rs ss)" |
|
333 apply(case_tac "a \<in> ss") |
|
334 apply simp |
|
335 by (simp add: larger_acc_smaller_distinct_res) |
|
336 |
|
337 |
|
338 lemma distinct_list_size_len_bounded: |
|
339 assumes "\<forall>r \<in> set rs. rsize r \<le> N" "length rs \<le> lrs" |
|
340 shows "rsizes rs \<le> lrs * N " |
|
341 using assms |
|
342 by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1) |
|
343 |
|
344 |
|
345 |
|
346 lemma rdistinct_same_set: |
|
347 shows "r \<in> set rs \<longleftrightarrow> r \<in> set (rdistinct rs {})" |
|
348 apply(induct rs) |
|
349 apply simp |
|
350 by (metis rdistinct_set_equality) |
|
351 |
|
352 (* distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size *) |
|
353 lemma distinct_list_rexp_upto: |
|
354 assumes "\<forall>r\<in> set rs. (rsize r) \<le> N" |
|
355 shows "rsizes (rdistinct rs {}) \<le> (card (sizeNregex N)) * N" |
|
356 |
|
357 apply(subgoal_tac "distinct (rdistinct rs {})") |
|
358 prefer 2 |
|
359 using rdistinct_does_the_job apply blast |
|
360 apply(subgoal_tac "length (rdistinct rs {}) \<le> card (sizeNregex N)") |
|
361 apply(rule distinct_list_size_len_bounded) |
|
362 using assms |
|
363 apply (meson rdistinct_same_set) |
|
364 apply blast |
|
365 apply(subgoal_tac "\<forall>r \<in> set (rdistinct rs {}). rsize r \<le> N") |
|
366 prefer 2 |
|
367 using assms |
|
368 apply (meson rdistinct_same_set) |
|
369 apply(subgoal_tac "length (rdistinct rs {}) = card (set (rdistinct rs {}))") |
|
370 prefer 2 |
|
371 apply (simp add: distinct_card) |
|
372 apply(simp) |
|
373 by (metis card_mono finite_size_n mem_Collect_eq sizeNregex_def subsetI) |
|
374 |
|
375 |
|
376 lemma star_control_bounded: |
|
377 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
378 shows "rsizes (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates s r [[c]])) {}) |
|
379 \<le> (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r)))" |
|
380 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)) |
|
381 |
|
382 |
|
383 lemma star_closed_form_bounded: |
|
384 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
385 shows "rsize (rders_simp (RSTAR r) s) \<le> |
|
386 max ((Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r))))) (rsize (RSTAR r))" |
|
387 proof(cases s) |
|
388 case Nil |
|
389 then show "rsize (rders_simp (RSTAR r) s) |
|
390 \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))" |
|
391 by simp |
|
392 next |
|
393 case (Cons a list) |
|
394 then have "rsize (rders_simp (RSTAR r) s) = |
|
395 rsize (rsimp (RALTS ((map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])))))" |
|
396 using star_closed_form by fastforce |
|
397 also have "... \<le> Suc (rsizes (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])) {}))" |
|
398 using alts_simp_control by blast |
|
399 also have "... \<le> Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r)))" |
|
400 using star_control_bounded[OF assms] by (metis add_mono le_add1 mult_Suc plus_1_eq_Suc) |
|
401 also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))" |
|
402 by simp |
|
403 finally show ?thesis by simp |
|
404 qed |
|
405 |
|
406 |
|
407 thm ntimes_closed_form |
|
408 |
|
409 thm rsize.simps |
|
410 |
|
411 lemma nupdates_snoc: |
|
412 shows " (nupdates (xs @ [x]) r optlist) = nupdate x r (nupdates xs r optlist)" |
|
413 by (simp add: nupdates_append) |
|
414 |
|
415 lemma nupdate_elems: |
|
416 shows "\<forall>opt \<in> set (nupdate c r optlist). opt = None \<or> (\<exists>s n. opt = Some (s, n))" |
|
417 using nonempty_string.cases by auto |
|
418 |
|
419 lemma nupdates_elems: |
|
420 shows "\<forall>opt \<in> set (nupdates s r optlist). opt = None \<or> (\<exists>s n. opt = Some (s, n))" |
|
421 by (meson nonempty_string.cases) |
|
422 |
|
423 |
|
424 lemma opterm_optlist_result_shape: |
|
425 shows "\<forall>r' \<in> set (map (optermsimp r) optlist). r' = RZERO \<or> (\<exists>s m. r' = RSEQ (rders_simp r s) (RNTIMES r m))" |
|
426 apply(induct optlist) |
|
427 apply simp |
|
428 apply(case_tac a) |
|
429 apply simp+ |
|
430 by fastforce |
|
431 |
|
432 |
|
433 lemma opterm_optlist_result_shape2: |
|
434 shows "\<And>optlist. \<forall>r' \<in> set (map (optermsimp r) optlist). r' = RZERO \<or> (\<exists>s m. r' = RSEQ (rders_simp r s) (RNTIMES r m))" |
|
435 using opterm_optlist_result_shape by presburger |
|
436 |
|
437 |
|
438 lemma nupdate_n_leq_n: |
|
439 shows "\<forall>r \<in> set (nupdate c' r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)" |
|
440 apply(case_tac n) |
|
441 apply simp |
|
442 apply simp |
|
443 done |
|
444 (* |
|
445 lemma nupdate_induct_leqn: |
|
446 shows "\<lbrakk>\<forall>opt \<in> set optlist. opt = None \<or> (\<exists>s' m. opt = Some(s', m) \<and> m \<le> n) \<rbrakk> \<Longrightarrow> |
|
447 \<forall>opt \<in> set (nupdate c' r optlist). opt = None \<or> (\<exists>s' m. opt = Some (s', m) \<and> m \<le> n)" |
|
448 apply (case_tac optlist) |
|
449 apply simp |
|
450 apply(case_tac a) |
|
451 apply simp |
|
452 sledgehammer |
|
453 *) |
|
454 |
|
455 |
|
456 lemma nupdates_n_leq_n: |
|
457 shows "\<forall>r \<in> set (nupdates s r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)" |
|
458 apply(induct s rule: rev_induct) |
|
459 apply simp |
|
460 apply(subst nupdates_append) |
|
461 by (metis nupdates_elems_leqn nupdates_snoc) |
|
462 |
|
463 |
|
464 |
|
465 lemma ntimes_closed_form_list_elem_shape: |
|
466 shows "\<forall>r' \<in> set (map (optermsimp r) (nupdates s r [Some ([c], n)])). |
|
467 r' = RZERO \<or> (\<exists>s' m. r' = RSEQ (rders_simp r s') (RNTIMES r m) \<and> m \<le> n)" |
|
468 apply(insert opterm_optlist_result_shape2) |
|
469 apply(case_tac s) |
|
470 apply(auto) |
|
471 apply (metis rders_simp_one_char) |
|
472 by (metis case_prod_conv nupdates.simps(2) nupdates_n_leq_n option.simps(4) option.simps(5)) |
|
473 |
|
474 |
|
475 lemma ntimes_trivial1: |
|
476 shows "rsize RZERO \<le> N + rsize (RNTIMES r n)" |
|
477 by simp |
|
478 |
|
479 |
|
480 lemma ntimes_trivial20: |
|
481 shows "m \<le> n \<Longrightarrow> rsize (RNTIMES r m) \<le> rsize (RNTIMES r n)" |
|
482 by simp |
|
483 |
|
484 |
|
485 lemma ntimes_trivial2: |
|
486 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
487 shows " r' = RSEQ (rders_simp r s1) (RNTIMES r m) \<and> m \<le> n |
|
488 \<Longrightarrow> rsize r' \<le> Suc (N + rsize (RNTIMES r n))" |
|
489 apply simp |
|
490 by (simp add: add_mono_thms_linordered_semiring(1) assms) |
|
491 |
|
492 lemma ntimes_closed_form_list_elem_bounded: |
|
493 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
494 shows "\<forall>r' \<in> set (map (optermsimp r) (nupdates s r [Some ([c], n)])). rsize r' \<le> Suc (N + rsize (RNTIMES r n))" |
|
495 apply(rule ballI) |
|
496 apply(subgoal_tac "r' = RZERO \<or> (\<exists>s' m. r' = RSEQ (rders_simp r s') (RNTIMES r m) \<and> m \<le> n)") |
|
497 prefer 2 |
|
498 using ntimes_closed_form_list_elem_shape apply blast |
|
499 apply(case_tac "r' = RZERO") |
|
500 using le_SucI ntimes_trivial1 apply presburger |
|
501 apply(subgoal_tac "\<exists>s1 m. r' = RSEQ (rders_simp r s1) (RNTIMES r m) \<and> m \<le> n") |
|
502 apply(erule exE)+ |
|
503 using assms ntimes_trivial2 apply presburger |
|
504 by blast |
|
505 |
|
506 |
|
507 lemma P_holds_after_distinct: |
|
508 assumes "\<forall>r \<in> set rs. P r" |
|
509 shows "\<forall>r \<in> set (rdistinct rs rset). P r" |
|
510 by (simp add: assms rdistinct_set_equality1) |
|
511 |
|
512 |
|
513 |
|
514 lemma ntimes_control_bounded: |
|
515 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
516 shows "rsizes (rdistinct (map (optermsimp r) (nupdates s r [Some ([c], n)])) {}) |
|
517 \<le> (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n)))" |
|
518 apply(subgoal_tac "\<forall>r' \<in> set (rdistinct (map (optermsimp r) (nupdates s r [Some ([c], n)])) {}). |
|
519 rsize r' \<le> Suc (N + rsize (RNTIMES r n))") |
|
520 apply (meson distinct_list_rexp_upto rdistinct_same_set) |
|
521 apply(subgoal_tac "\<forall>r' \<in> set (map (optermsimp r) (nupdates s r [Some ([c], n)])). rsize r' \<le> Suc (N + rsize (RNTIMES r n))") |
|
522 apply (simp add: rdistinct_set_equality) |
|
523 by (metis assms nat_le_linear not_less_eq_eq ntimes_closed_form_list_elem_bounded) |
|
524 |
|
525 |
|
526 |
|
527 lemma ntimes_closed_form_bounded0: |
|
528 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
529 shows " (rders_simp (RNTIMES r 0) s) = RZERO \<or> (rders_simp (RNTIMES r 0) s) = RNTIMES r 0 |
|
530 " |
|
531 apply(induct s) |
|
532 apply simp |
|
533 by (metis always0 list.simps(3) rder.simps(7) rders.simps(2) rders_simp_same_simpders rsimp.simps(3)) |
|
534 |
|
535 lemma ntimes_closed_form_bounded1: |
|
536 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
537 shows " rsize (rders_simp (RNTIMES r 0) s) \<le> max (rsize RZERO) (rsize (RNTIMES r 0))" |
|
538 |
|
539 by (metis assms max.cobounded1 max.cobounded2 ntimes_closed_form_bounded0) |
|
540 |
|
541 lemma self_smaller_than_bound: |
|
542 shows "\<forall>s. rsize (rders_simp r s) \<le> N \<Longrightarrow> rsize r \<le> N" |
|
543 apply(drule_tac x = "[]" in spec) |
|
544 apply simp |
|
545 done |
|
546 |
|
547 lemma ntimes_closed_form_bounded_nil_aux: |
|
548 shows "max (rsize RZERO) (rsize (RNTIMES r 0)) = 1 + rsize r" |
|
549 by auto |
|
550 |
|
551 lemma ntimes_closed_form_bounded_nil: |
|
552 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
553 shows " rsize (rders_simp (RNTIMES r 0) s) \<le> 1 + rsize r" |
|
554 using assms ntimes_closed_form_bounded1 by auto |
|
555 |
|
556 lemma ntimes_ineq1: |
|
557 shows "(rsize (RNTIMES r n)) \<ge> 1 + rsize r" |
|
558 by simp |
|
559 |
|
560 lemma ntimes_ineq2: |
|
561 shows "1 + rsize r \<le> |
|
562 max ((Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n))))) (rsize (RNTIMES r n))" |
|
563 by (meson le_max_iff_disj ntimes_ineq1) |
|
564 |
|
565 lemma ntimes_closed_form_bounded: |
|
566 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
567 shows "rsize (rders_simp (RNTIMES r (Suc n)) s) \<le> |
|
568 max ((Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n))))) (rsize (RNTIMES r n))" |
|
569 proof(cases s) |
|
570 case Nil |
|
571 then show "rsize (rders_simp (RNTIMES r (Suc n)) s) |
|
572 \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * Suc (N + rsize (RNTIMES r n))) (rsize (RNTIMES r n))" |
|
573 by simp |
|
574 next |
|
575 case (Cons a list) |
|
576 |
|
577 then have "rsize (rders_simp (RNTIMES r (Suc n)) s) = |
|
578 rsize (rsimp (RALTS ((map (optermsimp r) (nupdates list r [Some ([a], n)])))))" |
|
579 using ntimes_closed_form by fastforce |
|
580 also have "... \<le> Suc (rsizes (rdistinct ((map (optermsimp r) (nupdates list r [Some ([a], n)]))) {}))" |
|
581 using alts_simp_control by blast |
|
582 also have "... \<le> Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n)))" |
|
583 using ntimes_control_bounded[OF assms] |
|
584 by (metis add_mono le_add1 mult_Suc plus_1_eq_Suc) |
|
585 also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * Suc (N + rsize (RNTIMES r n))) (rsize (RNTIMES r n))" |
|
586 by simp |
|
587 finally show ?thesis by simp |
|
588 qed |
|
589 |
|
590 |
|
591 lemma ntimes_closed_form_boundedA: |
|
592 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" |
|
593 shows "\<exists>N'. \<forall>s. rsize (rders_simp (RNTIMES r n) s) \<le> N'" |
|
594 apply(case_tac n) |
|
595 using assms ntimes_closed_form_bounded_nil apply blast |
|
596 using assms ntimes_closed_form_bounded by blast |
|
597 |
|
598 |
|
599 lemma star_closed_form_nonempty_bounded: |
|
600 assumes "\<forall>s. rsize (rders_simp r s) \<le> N" and "s \<noteq> []" |
|
601 shows "rsize (rders_simp (RSTAR r) s) \<le> |
|
602 ((Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r))))) " |
|
603 proof(cases s) |
|
604 case Nil |
|
605 then show ?thesis |
|
606 using local.Nil by fastforce |
|
607 next |
|
608 case (Cons a list) |
|
609 then have "rsize (rders_simp (RSTAR r) s) = |
|
610 rsize (rsimp (RALTS ((map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])))))" |
|
611 using star_closed_form by fastforce |
|
612 also have "... \<le> Suc (rsizes (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])) {}))" |
|
613 using alts_simp_control by blast |
|
614 also have "... \<le> Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r)))" |
|
615 by (smt (z3) add_mono_thms_linordered_semiring(1) assms(1) le_add1 map_eq_conv mult_Suc plus_1_eq_Suc star_control_bounded) |
|
616 also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))" |
|
617 by simp |
|
618 finally show ?thesis by simp |
|
619 qed |
|
620 |
|
621 |
|
622 |
|
623 lemma seq_estimate_bounded: |
|
624 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" |
|
625 and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
|
626 shows |
|
627 "rsizes (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}) |
|
628 \<le> (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))" |
|
629 proof - |
|
630 have a: "rsizes (rdistinct (map (rders_simp r2) (vsuf s r1)) {}) \<le> N2 * card (sizeNregex N2)" |
|
631 by (metis assms(2) distinct_list_rexp_upto ex_map_conv mult.commute) |
|
632 |
|
633 have "rsizes (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}) \<le> |
|
634 rsize (RSEQ (rders_simp r1 s) r2) + rsizes (rdistinct (map (rders_simp r2) (vsuf s r1)) {})" |
|
635 using triangle_inequality_distinct by blast |
|
636 also have "... \<le> rsize (RSEQ (rders_simp r1 s) r2) + N2 * card (sizeNregex N2)" |
|
637 by (simp add: a) |
|
638 also have "... \<le> Suc (N1 + (rsize r2) + N2 * card (sizeNregex N2))" |
|
639 by (simp add: assms(1)) |
|
640 finally show ?thesis |
|
641 by force |
|
642 qed |
|
643 |
|
644 |
|
645 lemma seq_closed_form_bounded2: |
|
646 assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" |
|
647 and "\<forall>s. rsize (rders_simp r2 s) \<le> N2" |
|
648 shows "rsize (rders_simp (RSEQ r1 r2) s) |
|
649 \<le> max (2 + N1 + (rsize r2) + (N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" |
|
650 proof(cases s) |
|
651 case Nil |
|
652 then show "rsize (rders_simp (RSEQ r1 r2) s) |
|
653 \<le> max (2 + N1 + (rsize r2) + (N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" |
|
654 by simp |
|
655 next |
|
656 case (Cons a list) |
|
657 then have "rsize (rders_simp (RSEQ r1 r2) s) = |
|
658 rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1)))))" |
|
659 using seq_closed_form_variant by (metis list.distinct(1)) |
|
660 also have "... \<le> Suc (rsizes (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))" |
|
661 using alts_simp_control by blast |
|
662 also have "... \<le> 2 + N1 + (rsize r2) + (N2 * card (sizeNregex N2))" |
|
663 using seq_estimate_bounded[OF assms] by auto |
|
664 ultimately show "rsize (rders_simp (RSEQ r1 r2) s) |
|
665 \<le> max (2 + N1 + (rsize r2) + N2 * card (sizeNregex N2)) (rsize (RSEQ r1 r2))" |
|
666 by auto |
|
667 qed |
|
668 |
|
669 lemma rders_simp_bounded: |
|
670 shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N" |
|
671 apply(induct r) |
|
672 apply(rule_tac x = "Suc 0 " in exI) |
|
673 using three_easy_cases0 apply force |
|
674 using three_easy_cases1 apply blast |
|
675 using three_easy_casesC apply blast |
|
676 apply(erule exE)+ |
|
677 apply(rule exI) |
|
678 apply(rule allI) |
|
679 apply(rule seq_closed_form_bounded2) |
|
680 apply(assumption) |
|
681 apply(assumption) |
|
682 apply (metis alts_closed_form_bounded size_list_estimation') |
|
683 using star_closed_form_bounded apply blast |
|
684 using ntimes_closed_form_boundedA by blast |
|
685 |
|
686 |
|
687 unused_thms |
|
688 export_code rders_simp rsimp rder in Scala module_name Example |
|
689 |
|
690 |
|
691 end |