|
1 |
|
2 theory SizeBound6CT |
|
3 imports "Lexer" "PDerivs" |
|
4 begin |
|
5 |
|
6 section \<open>Bit-Encodings\<close> |
|
7 |
|
8 fun orderedSufAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list" |
|
9 where |
|
10 "orderedSufAux (Suc i) ss = (drop i ss) # (orderedSufAux i ss)" |
|
11 |"orderedSufAux 0 ss = Nil" |
|
12 |
|
13 fun |
|
14 orderedSuf :: "char list \<Rightarrow> char list list" |
|
15 where |
|
16 "orderedSuf s = orderedSufAux (length s) s" |
|
17 |
|
18 fun orderedPrefAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list" |
|
19 where |
|
20 "orderedPrefAux (Suc i) ss = (take i ss) # (orderedPrefAux i ss)" |
|
21 |"orderedPrefAux 0 ss = Nil" |
|
22 |
|
23 |
|
24 fun orderedPref :: "char list \<Rightarrow> char list list" |
|
25 where |
|
26 "orderedPref s = orderedPrefAux (length s) s" |
|
27 |
|
28 lemma shape_of_pref_1list: |
|
29 shows "orderedPref [c] = [[]]" |
|
30 apply auto |
|
31 done |
|
32 |
|
33 lemma shape_of_suf_1list: |
|
34 shows "orderedSuf [c] = [[c]]" |
|
35 by auto |
|
36 |
|
37 lemma shape_of_suf_2list: |
|
38 shows "orderedSuf [c2, c3] = [[c3], [c2,c3]]" |
|
39 by auto |
|
40 |
|
41 lemma shape_of_prf_2list: |
|
42 shows "orderedPref [c1, c2] = [[c1], []]" |
|
43 by auto |
|
44 |
|
45 |
|
46 lemma shape_of_suf_3list: |
|
47 shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]" |
|
48 by auto |
|
49 |
|
50 lemma throwing_elem_around: |
|
51 shows "orderedSuf (s1 @ [a] @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf ( s1 @ [a]) ))" |
|
52 and "orderedSuf (s1 @ [a] @ s) = (orderedSuf ([a] @ s) @ (map (\<lambda>s11. s11 @ ([a] @ s))) (orderedSuf s1) )" |
|
53 sorry |
|
54 |
|
55 |
|
56 lemma suf_cons: |
|
57 shows "orderedSuf (s1 @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf s1))" |
|
58 apply(induct s arbitrary: s1) |
|
59 apply simp |
|
60 apply(subgoal_tac "s1 @ a # s = (s1 @ [a]) @ s") |
|
61 prefer 2 |
|
62 apply simp |
|
63 apply(subgoal_tac "orderedSuf (s1 @ a # s) = orderedSuf ((s1 @ [a]) @ s)") |
|
64 prefer 2 |
|
65 apply presburger |
|
66 apply(drule_tac x="s1 @ [a]" in meta_spec) |
|
67 sorry |
|
68 |
|
69 |
|
70 |
|
71 lemma shape_of_prf_3list: |
|
72 shows "orderedPref [c1, c2, c3] = [[c1, c2], [c1], []]" |
|
73 by auto |
|
74 |
|
75 fun zip_concat :: "char list list \<Rightarrow> char list list \<Rightarrow> char list list" |
|
76 where |
|
77 "zip_concat (s1#ss1) (s2#ss2) = (s1@s2) # (zip_concat ss1 ss2)" |
|
78 | "zip_concat [] [] = []" |
|
79 | "zip_concat [] (s2#ss2) = s2 # (zip_concat [] ss2)" |
|
80 | "zip_concat (s1#ss1) [] = s1 # (zip_concat ss1 [])" |
|
81 |
|
82 |
|
83 |
|
84 lemma compliment_pref_suf: |
|
85 shows "zip_concat (orderedPref s) (orderedSuf s) = replicate (length s) s " |
|
86 apply(induct s) |
|
87 apply auto[1] |
|
88 sorry |
|
89 |
|
90 |
|
91 |
|
92 |
|
93 datatype rrexp = |
|
94 RZERO |
|
95 | RONE |
|
96 | RCHAR char |
|
97 | RSEQ rrexp rrexp |
|
98 | RALTS "rrexp list" |
|
99 | RSTAR rrexp |
|
100 |
|
101 abbreviation |
|
102 "RALT r1 r2 \<equiv> RALTS [r1, r2]" |
|
103 |
|
104 |
|
105 |
|
106 fun |
|
107 rnullable :: "rrexp \<Rightarrow> bool" |
|
108 where |
|
109 "rnullable (RZERO) = False" |
|
110 | "rnullable (RONE ) = True" |
|
111 | "rnullable (RCHAR c) = False" |
|
112 | "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)" |
|
113 | "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)" |
|
114 | "rnullable (RSTAR r) = True" |
|
115 |
|
116 |
|
117 fun |
|
118 rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp" |
|
119 where |
|
120 "rder c (RZERO) = RZERO" |
|
121 | "rder c (RONE) = RZERO" |
|
122 | "rder c (RCHAR d) = (if c = d then RONE else RZERO)" |
|
123 | "rder c (RALTS rs) = RALTS (map (rder c) rs)" |
|
124 | "rder c (RSEQ r1 r2) = |
|
125 (if rnullable r1 |
|
126 then RALT (RSEQ (rder c r1) r2) (rder c r2) |
|
127 else RSEQ (rder c r1) r2)" |
|
128 | "rder c (RSTAR r) = RSEQ (rder c r) (RSTAR r)" |
|
129 |
|
130 |
|
131 fun |
|
132 rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp" |
|
133 where |
|
134 "rders r [] = r" |
|
135 | "rders r (c#s) = rders (rder c r) s" |
|
136 |
|
137 fun rdistinct :: "'a list \<Rightarrow>'a set \<Rightarrow> 'a list" |
|
138 where |
|
139 "rdistinct [] acc = []" |
|
140 | "rdistinct (x#xs) acc = |
|
141 (if x \<in> acc then rdistinct xs acc |
|
142 else x # (rdistinct xs ({x} \<union> acc)))" |
|
143 |
|
144 lemma rdistinct_idem: |
|
145 shows "rdistinct (x # (rdistinct rs {x})) {} = x # (rdistinct rs {x})" |
|
146 |
|
147 sorry |
|
148 |
|
149 |
|
150 |
|
151 |
|
152 |
|
153 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
|
154 where |
|
155 "rflts [] = []" |
|
156 | "rflts (RZERO # rs) = rflts rs" |
|
157 | "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs" |
|
158 | "rflts (r1 # rs) = r1 # rflts rs" |
|
159 |
|
160 |
|
161 fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp" |
|
162 where |
|
163 "rsimp_ALTs [] = RZERO" |
|
164 | "rsimp_ALTs [r] = r" |
|
165 | "rsimp_ALTs rs = RALTS rs" |
|
166 |
|
167 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp" |
|
168 where |
|
169 "rsimp_SEQ RZERO _ = RZERO" |
|
170 | "rsimp_SEQ _ RZERO = RZERO" |
|
171 | "rsimp_SEQ RONE r2 = r2" |
|
172 | "rsimp_SEQ r1 r2 = RSEQ r1 r2" |
|
173 |
|
174 |
|
175 fun rsimp :: "rrexp \<Rightarrow> rrexp" |
|
176 where |
|
177 "rsimp (RSEQ r1 r2) = rsimp_SEQ (rsimp r1) (rsimp r2)" |
|
178 | "rsimp (RALTS rs) = rsimp_ALTs (rdistinct (rflts (map rsimp rs)) {}) " |
|
179 | "rsimp r = r" |
|
180 |
|
181 |
|
182 fun |
|
183 rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp" |
|
184 where |
|
185 "rders_simp r [] = r" |
|
186 | "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s" |
|
187 |
|
188 fun rsize :: "rrexp \<Rightarrow> nat" where |
|
189 "rsize RZERO = 1" |
|
190 | "rsize (RONE) = 1" |
|
191 | "rsize (RCHAR c) = 1" |
|
192 | "rsize (RALTS rs) = Suc (sum_list (map rsize rs))" |
|
193 | "rsize (RSEQ r1 r2) = Suc (rsize r1 + rsize r2)" |
|
194 | "rsize (RSTAR r) = Suc (rsize r)" |
|
195 |
|
196 |
|
197 fun rlist_size :: "rrexp list \<Rightarrow> nat" where |
|
198 "rlist_size (r # rs) = rsize r + rlist_size rs" |
|
199 | "rlist_size [] = 0" |
|
200 |
|
201 thm neq_Nil_conv |
|
202 |
|
203 |
|
204 lemma rsimp_aalts_smaller: |
|
205 shows "rsize (rsimp_ALTs rs) \<le> rsize (RALTS rs)" |
|
206 apply(induct rs) |
|
207 apply simp |
|
208 apply simp |
|
209 apply(case_tac "rs = []") |
|
210 apply simp |
|
211 apply(subgoal_tac "\<exists>rsp ap. rs = ap # rsp") |
|
212 apply(erule exE)+ |
|
213 apply simp |
|
214 apply simp |
|
215 by(meson neq_Nil_conv) |
|
216 |
|
217 |
|
218 lemma finite_list_of_ders: |
|
219 shows"\<exists>dersset. ( (finite dersset) \<and> (\<forall>s. (rders_simp r s) \<in> dersset) )" |
|
220 sorry |
|
221 |
|
222 |
|
223 |
|
224 |
|
225 |
|
226 |
|
227 (* |
|
228 lemma rders_shape: |
|
229 shows "s \<noteq> [] \<Longrightarrow> rders_simp (RSEQ r1 r2) s = |
|
230 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
|
231 (map (rders r2) (orderedSuf s))) )" |
|
232 apply(induct s arbitrary: r1 r2 rule: rev_induct) |
|
233 apply simp |
|
234 apply simp |
|
235 |
|
236 sorry |
|
237 *) |
|
238 |
|
239 |
|
240 |
|
241 fun rders_cond_list :: "rrexp \<Rightarrow> bool list \<Rightarrow> char list list \<Rightarrow> rrexp list" |
|
242 where |
|
243 "rders_cond_list r2 (True # bs) (s # strs) = (rders_simp r2 s) # (rders_cond_list r2 bs strs)" |
|
244 | "rders_cond_list r2 (False # bs) (s # strs) = rders_cond_list r2 bs strs" |
|
245 | "rders_cond_list r2 [] s = []" |
|
246 | "rders_cond_list r2 bs [] = []" |
|
247 |
|
248 fun nullable_bools :: "rrexp \<Rightarrow> char list list \<Rightarrow> bool list" |
|
249 where |
|
250 "nullable_bools r (s#strs) = (rnullable (rders r s)) # (nullable_bools r strs) " |
|
251 |"nullable_bools r [] = []" |
|
252 |
|
253 fun cond_list :: "rrexp \<Rightarrow> rrexp \<Rightarrow> char list \<Rightarrow> rrexp list" |
|
254 where |
|
255 "cond_list r1 r2 s = rders_cond_list r2 (nullable_bools r1 (orderedPref s) ) (orderedSuf s)" |
|
256 |
|
257 thm rsimp_SEQ.simps |
|
258 lemma rSEQ_mono: |
|
259 shows "rsize (rsimp_SEQ r1 r2) \<le>rsize ( RSEQ r1 r2)" |
|
260 apply auto |
|
261 apply(induct r1) |
|
262 apply auto |
|
263 apply(case_tac "r2") |
|
264 apply simp_all |
|
265 apply(case_tac r2) |
|
266 apply simp_all |
|
267 apply(case_tac r2) |
|
268 apply simp_all |
|
269 apply(case_tac r2) |
|
270 apply simp_all |
|
271 apply(case_tac r2) |
|
272 apply simp_all |
|
273 done |
|
274 |
|
275 lemma rsimp_mono: |
|
276 shows "rsize (rsimp r) \<le> rsize r" |
|
277 apply(induct r) |
|
278 apply simp_all |
|
279 apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \<le> rsize (RSEQ (rsimp r1) (rsimp r2))") |
|
280 |
|
281 apply force |
|
282 using rSEQ_mono |
|
283 apply presburger |
|
284 sorry |
|
285 |
|
286 lemma idiot: |
|
287 shows "rsimp_SEQ RONE r = r" |
|
288 apply(case_tac r) |
|
289 apply simp_all |
|
290 done |
|
291 |
|
292 lemma no_dup_after_simp: |
|
293 shows "RALTS rs = rsimp r \<Longrightarrow> distinct rs" |
|
294 sorry |
|
295 |
|
296 lemma no_further_dB_after_simp: |
|
297 shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs" |
|
298 sorry |
|
299 |
|
300 lemma longlist_withstands_rsimp_alts: |
|
301 shows "length rs \<ge> 2 \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
302 sorry |
|
303 |
|
304 lemma no_alt_short_list_after_simp: |
|
305 shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
306 sorry |
|
307 |
|
308 lemma idiot2: |
|
309 shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk> |
|
310 \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2" |
|
311 apply(case_tac r1) |
|
312 apply(case_tac r2) |
|
313 apply simp_all |
|
314 apply(case_tac r2) |
|
315 apply simp_all |
|
316 apply(case_tac r2) |
|
317 apply simp_all |
|
318 apply(case_tac r2) |
|
319 apply simp_all |
|
320 apply(case_tac r2) |
|
321 apply simp_all |
|
322 done |
|
323 |
|
324 lemma rsimp_aalts_another: |
|
325 shows "\<forall>r \<in> (set (map rsimp ((RSEQ (rders r1 s) r2) # |
|
326 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) )) ). (rsize r) < N " |
|
327 sorry |
|
328 |
|
329 |
|
330 |
|
331 lemma shape_derssimpseq_onechar: |
|
332 shows " (rders_simp r [c]) = (rsimp (rders r [c]))" |
|
333 and "rders_simp (RSEQ r1 r2) [c] = |
|
334 rsimp (RALTS ((RSEQ (rders r1 [c]) r2) # |
|
335 (rders_cond_list r2 (nullable_bools r1 (orderedPref [c])) (orderedSuf [c]))) )" |
|
336 apply simp |
|
337 apply(simp add: rders.simps) |
|
338 apply(case_tac "rsimp (rder c r1) = RZERO") |
|
339 apply auto |
|
340 apply(case_tac "rsimp (rder c r1) = RONE") |
|
341 apply auto |
|
342 apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp r2") |
|
343 prefer 2 |
|
344 using idiot |
|
345 apply simp |
|
346 apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp r2]) {})") |
|
347 prefer 2 |
|
348 apply auto |
|
349 apply(case_tac "rsimp r2") |
|
350 apply auto |
|
351 apply(subgoal_tac "rdistinct x5 {} = x5") |
|
352 prefer 2 |
|
353 using no_further_dB_after_simp |
|
354 apply metis |
|
355 apply(subgoal_tac "rsimp_ALTs (rdistinct x5 {}) = rsimp_ALTs x5") |
|
356 prefer 2 |
|
357 apply fastforce |
|
358 apply auto |
|
359 apply (metis no_alt_short_list_after_simp) |
|
360 apply (case_tac "rsimp r2 = RZERO") |
|
361 apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RZERO") |
|
362 prefer 2 |
|
363 apply(case_tac "rsimp ( rder c r1)") |
|
364 apply auto |
|
365 apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RSEQ (rsimp (rder c r1)) (rsimp r2)") |
|
366 prefer 2 |
|
367 apply auto |
|
368 sorry |
|
369 |
|
370 |
|
371 |
|
372 lemma shape_derssimpseq_onechar2: |
|
373 shows "rders_simp (RSEQ r1 r2) [c] = |
|
374 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # |
|
375 (rders_cond_list r2 (nullable_bools r1 (orderedPref [c])) (orderedSuf [c]))) )" |
|
376 sorry |
|
377 |
|
378 |
|
379 lemma rders__onechar: |
|
380 shows " (rders_simp r [c]) = (rsimp (rders r [c]))" |
|
381 by simp |
|
382 |
|
383 lemma rders_append: |
|
384 "rders c (s1 @ s2) = rders (rders c s1) s2" |
|
385 apply(induct s1 arbitrary: c s2) |
|
386 apply(simp_all) |
|
387 done |
|
388 |
|
389 lemma rders_simp_append: |
|
390 "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2" |
|
391 apply(induct s1 arbitrary: c s2) |
|
392 apply(simp_all) |
|
393 done |
|
394 |
|
395 lemma inside_simp_removal: |
|
396 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
|
397 |
|
398 sorry |
|
399 |
|
400 lemma set_related_list: |
|
401 shows "distinct rs \<Longrightarrow> length rs = card (set rs)" |
|
402 by (simp add: distinct_card) |
|
403 (*this section deals with the property of distinctBy: creates a list without duplicates*) |
|
404 lemma rdistinct_never_added_twice: |
|
405 shows "rdistinct (a # rs) {a} = rdistinct rs {a}" |
|
406 by force |
|
407 |
|
408 |
|
409 lemma rdistinct_does_the_job: |
|
410 shows "distinct (rdistinct rs s)" |
|
411 apply(induct rs arbitrary: s) |
|
412 apply simp |
|
413 apply simp |
|
414 sorry |
|
415 |
|
416 |
|
417 lemma simp_helps_der_pierce: |
|
418 shows " rsimp |
|
419 (rder x |
|
420 (rsimp_ALTs rs)) = |
|
421 rsimp |
|
422 (rsimp_ALTs |
|
423 (map (rder x ) |
|
424 rs |
|
425 ) |
|
426 )" |
|
427 sorry |
|
428 |
|
429 lemma simp_helps_der_pierce_dB: |
|
430 shows " rsimp |
|
431 (rsimp_ALTs |
|
432 (map (rder x) |
|
433 (rdistinct rs {}))) = |
|
434 rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))" |
|
435 |
|
436 sorry |
|
437 |
|
438 lemma simp_helps_der_pierce_flts: |
|
439 shows " rsimp |
|
440 (rsimp_ALTs |
|
441 (rdistinct |
|
442 (map (rder x) |
|
443 (rflts rs ) |
|
444 ) {} |
|
445 ) |
|
446 ) = |
|
447 rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}) )" |
|
448 |
|
449 sorry |
|
450 |
|
451 |
|
452 lemma unfold_ders_simp_inside_only: |
|
453 shows " (rders_simp (RSEQ r1 r2) xs = |
|
454 rsimp (RALTS (RSEQ (rders_simp r1 xs) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs)))) |
|
455 \<Longrightarrow> rsimp (rder x (rders_simp (RSEQ r1 r2) xs)) = rsimp (rder x (rsimp (RALTS(RSEQ (rders_simp r1 xs) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs)))))" |
|
456 by presburger |
|
457 |
|
458 |
|
459 |
|
460 lemma unfold_ders_simp_inside_only_nosimp: |
|
461 shows " (rders_simp (RSEQ r1 r2) xs = |
|
462 rsimp (RALTS (RSEQ (rders_simp r1 xs) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs)))) |
|
463 \<Longrightarrow> rsimp (rder x (rders_simp (RSEQ r1 r2) xs)) = rsimp (rder x (RALTS(RSEQ (rders_simp r1 xs) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs))))" |
|
464 using inside_simp_removal by presburger |
|
465 |
|
466 |
|
467 |
|
468 |
|
469 lemma rders_simp_one_char: |
|
470 shows "rders_simp r [c] = rsimp (rder c r)" |
|
471 apply auto |
|
472 done |
|
473 |
|
474 lemma rsimp_idem: |
|
475 shows "rsimp (rsimp r) = rsimp r" |
|
476 sorry |
|
477 |
|
478 lemma head_one_more_simp: |
|
479 shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)" |
|
480 by (simp add: rsimp_idem) |
|
481 |
|
482 lemma head_one_more_dersimp: |
|
483 shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)" |
|
484 using head_one_more_simp rders_simp_append rders_simp_one_char by presburger |
|
485 |
|
486 thm cond_list.simps |
|
487 |
|
488 lemma suffix_plus1char: |
|
489 shows "\<not> (rnullable (rders r1 s)) \<Longrightarrow> cond_list r1 r2 (s@[c]) = map (rder c) (cond_list r1 r2 s)" |
|
490 apply simp |
|
491 sorry |
|
492 |
|
493 lemma suffix_plus1charn: |
|
494 shows "rnullable (rders r1 s) \<Longrightarrow> cond_list r1 r2 (s@[c]) = (rder c r2) # (map (rder c) (cond_list r1 r2 s))" |
|
495 sorry |
|
496 |
|
497 lemma ders_simp_nullability: |
|
498 shows "rnullable (rders r s) = rnullable (rders_simp r s)" |
|
499 sorry |
|
500 |
|
501 lemma first_elem_seqder: |
|
502 shows "\<not>rnullable r1p \<Longrightarrow> map rsimp (rder x (RSEQ r1p r2) |
|
503 # rs) = map rsimp ((RSEQ (rder x r1p) r2) # rs) " |
|
504 by auto |
|
505 |
|
506 lemma first_elem_seqder1: |
|
507 shows "\<not>rnullable (rders_simp r xs) \<Longrightarrow> map rsimp ( (rder x (RSEQ (rders_simp r xs) r2)) # rs) = |
|
508 map rsimp ( (RSEQ (rsimp (rder x (rders_simp r xs))) r2) # rs)" |
|
509 by (simp add: rsimp_idem) |
|
510 |
|
511 lemma first_elem_seqdersimps: |
|
512 shows "\<not>rnullable (rders_simp r xs) \<Longrightarrow> map rsimp ( (rder x (RSEQ (rders_simp r xs) r2)) # rs) = |
|
513 map rsimp ( (RSEQ (rders_simp r (xs @ [x])) r2) # rs)" |
|
514 using first_elem_seqder1 rders_simp_append by auto |
|
515 |
|
516 lemma first_elem_seqder_nullable: |
|
517 shows "rnullable (rders_simp r1 xs) \<Longrightarrow> cond_list r1 r2 (xs @ [x]) = rder x r2 # map (rder x) (cond_list r1 r2 xs)" |
|
518 sorry |
|
519 |
|
520 |
|
521 (*nullable_seq_with_list1 related *) |
|
522 lemma LHS0_def_der_alt: |
|
523 shows "rsimp (rder x (RALTS ( (RSEQ (rders_simp r1 xs) r2) # (cond_list r1 r2 xs)))) = |
|
524 rsimp (RALTS ((rder x (RSEQ (rders_simp r1 xs) r2)) # (map (rder x) (cond_list r1 r2 xs))))" |
|
525 by fastforce |
|
526 |
|
527 lemma LHS1_def_der_seq: |
|
528 shows "rnullable (rders_simp r1 xs) \<Longrightarrow> |
|
529 rsimp (rder x (RALTS ( (RSEQ (rders_simp r1 xs) r2) # (cond_list r1 r2 xs)))) = |
|
530 rsimp(RALTS ((RALTS ((RSEQ (rders_simp r1 (xs @ [x])) r2) # [rder x r2]) ) # (map (rder x ) (cond_list r1 r2 xs))))" |
|
531 by (simp add: rders_simp_append rsimp_idem) |
|
532 |
|
533 |
|
534 |
|
535 |
|
536 |
|
537 lemma cond_list_head_last: |
|
538 shows "rnullable (rders r1 s) \<Longrightarrow> |
|
539 RALTS (r # (cond_list r1 r2 (s @ [c]))) = RALTS (r # ((rder c r2) # (map (rder c) (cond_list r1 r2 s))))" |
|
540 using suffix_plus1charn by blast |
|
541 |
|
542 |
|
543 lemma simp_flatten: |
|
544 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
|
545 |
|
546 sorry |
|
547 |
|
548 lemma RHS1: |
|
549 shows "rnullable (rders_simp r1 xs) \<Longrightarrow> |
|
550 rsimp (RALTS ((RSEQ (rders_simp r1 (xs @ [x])) r2) # |
|
551 (cond_list r1 r2 (xs @[x])))) = |
|
552 rsimp (RALTS ((RSEQ (rders_simp r1 (xs @ [x])) r2) # |
|
553 ( ((rder x r2) # (map (rder x) (cond_list r1 r2 xs)))))) " |
|
554 using first_elem_seqder_nullable by presburger |
|
555 |
|
556 |
|
557 lemma nullable_seq_with_list1: |
|
558 shows " rnullable (rders_simp r1 s) \<Longrightarrow> |
|
559 rsimp (rder c (RALTS ( (RSEQ (rders_simp r1 s) r2) # (cond_list r1 r2 s)) )) = |
|
560 rsimp (RALTS ( (RSEQ (rders_simp r1 (s @ [c])) r2) # (cond_list r1 r2 (s @ [c])) ) )" |
|
561 by (metis LHS1_def_der_seq append.left_neutral append_Cons first_elem_seqder_nullable simp_flatten) |
|
562 |
|
563 |
|
564 |
|
565 |
|
566 lemma nullable_seq_with_list: |
|
567 shows "rnullable (rders_simp r1 xs) \<Longrightarrow> rsimp (rder x (RALTS ((RSEQ (rders_simp r1 xs) r2) # |
|
568 (rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs)) ))) = |
|
569 rsimp (RALTS ((RSEQ (rders_simp r1 (xs@[x])) r2) # |
|
570 (rders_cond_list r2 (nullable_bools r1 (orderedPref (xs@[x]))) (orderedSuf (xs@[x]))) ) ) |
|
571 " |
|
572 apply(subgoal_tac "rsimp (rder x (RALTS ((RSEQ (rders_simp r1 xs) r2) # (cond_list r1 r2 xs)))) = |
|
573 rsimp (RALTS ((RSEQ (rders_simp r1 (xs@[x])) r2) # (cond_list r1 r2 (xs@[x]))))") |
|
574 apply auto[1] |
|
575 using nullable_seq_with_list1 by auto |
|
576 |
|
577 |
|
578 |
|
579 |
|
580 lemma r1r2ders_whole: |
|
581 "rsimp |
|
582 (RALTS |
|
583 (rder x (RSEQ (rders_simp r1 xs) r2) # |
|
584 map (rder x) (rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs)))) = |
|
585 rsimp( RALTS( ( (RSEQ (rders_simp r1 (xs@[x])) r2) |
|
586 # (rders_cond_list r2 (nullable_bools r1 (orderedPref (xs @ [x]))) (orderedSuf (xs @ [x])))))) " |
|
587 using ders_simp_nullability first_elem_seqdersimps nullable_seq_with_list1 suffix_plus1char by auto |
|
588 |
|
589 lemma rders_simp_same_simpders: |
|
590 shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)" |
|
591 apply(induct s rule: rev_induct) |
|
592 apply simp |
|
593 apply(case_tac "xs = []") |
|
594 apply simp |
|
595 apply(simp add: rders_append rders_simp_append) |
|
596 using inside_simp_removal by blast |
|
597 |
|
598 lemma shape_derssimp_seq: |
|
599 shows "\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = |
|
600 rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
601 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )" |
|
602 |
|
603 apply(induct s arbitrary: r1 r2 rule: rev_induct) |
|
604 apply simp |
|
605 apply(case_tac "xs = []") |
|
606 using shape_derssimpseq_onechar2 apply force |
|
607 apply(simp only: rders_simp_append) |
|
608 apply(simp only: rders_simp_one_char) |
|
609 |
|
610 apply(subgoal_tac "rsimp (rder x (rders_simp (RSEQ r1 r2) xs)) |
|
611 = rsimp (rder x (RALTS(RSEQ (rders_simp r1 xs) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs))))") |
|
612 prefer 2 |
|
613 using unfold_ders_simp_inside_only_nosimp apply presburger |
|
614 apply(subgoal_tac "rsimp (rder x (RALTS (RSEQ (rders_simp r1 xs) r2 |
|
615 # rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs)))) = |
|
616 rsimp ( (RALTS (rder x (RSEQ (rders_simp r1 xs) r2) |
|
617 # (map (rder x) (rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs)))))) |
|
618 ") |
|
619 prefer 2 |
|
620 apply simp |
|
621 using r1r2ders_whole rders_simp_append rders_simp_one_char by presburger |
|
622 |
|
623 (* |
|
624 |
|
625 apply(subgoal_tac " rsimp |
|
626 (rder x |
|
627 (rsimp_ALTs |
|
628 (rdistinct |
|
629 (rflts |
|
630 (rsimp_SEQ (rsimp (rders_simp r1 xs)) (rsimp r2) # |
|
631 map rsimp |
|
632 (rders_cond_list r2 (nullable_bools r1 (orderedPrefAux (length xs) xs)) (orderedSufAux (length xs) xs)))) |
|
633 {}))) = |
|
634 rsimp |
|
635 ( |
|
636 (rsimp_ALTs |
|
637 (map (rder x) |
|
638 (rdistinct |
|
639 (rflts |
|
640 (rsimp_SEQ (rsimp (rders_simp r1 xs)) (rsimp r2) # |
|
641 map rsimp |
|
642 (rders_cond_list r2 (nullable_bools r1 (orderedPrefAux (length xs) xs)) (orderedSufAux (length xs) xs)))) |
|
643 {}) |
|
644 ) |
|
645 ) |
|
646 ) ") |
|
647 prefer 2 |
|
648 *) |
|
649 |
|
650 lemma shape_derssimp_alts: |
|
651 shows "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders r s) rs))" |
|
652 apply(case_tac "s") |
|
653 apply simp |
|
654 apply simp |
|
655 sorry |
|
656 (* |
|
657 fun rexp_encode :: "rrexp \<Rightarrow> nat" |
|
658 where |
|
659 "rexp_encode RZERO = 0" |
|
660 |"rexp_encode RONE = 1" |
|
661 |"rexp_encode (RCHAR c) = 2" |
|
662 |"rexp_encode (RSEQ r1 r2) = ( 2 ^ (rexp_encode r1)) " |
|
663 *) |
|
664 lemma finite_chars: |
|
665 shows " \<exists>N. ( (\<forall>r \<in> (set rs). \<exists>c. r = RCHAR c) \<and> (distinct rs) \<longrightarrow> length rs < N)" |
|
666 apply(rule_tac x = "Suc 256" in exI) |
|
667 sorry |
|
668 |
|
669 definition all_chars :: "int \<Rightarrow> char list" |
|
670 where "all_chars n = map char_of [0..n]" |
|
671 (* |
|
672 fun rexp_enum :: "nat \<Rightarrow> rrexp list" |
|
673 where |
|
674 "rexp_enum 0 = []" |
|
675 |"rexp_enum (Suc 0) = RALTS [] # RZERO # (RONE # (map RCHAR (all_chars 255)))" |
|
676 |"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]" |
|
677 |
|
678 *) |
|
679 |
|
680 fun rexp_enum :: "nat \<Rightarrow> rrexp set" |
|
681 where |
|
682 "rexp_enum 0 = {}" |
|
683 |"rexp_enum (Suc 0) = {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c. c \<in> set (all_chars 255)}" |
|
684 |"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = n}" |
|
685 |
|
686 |
|
687 lemma finite_sized_rexp_forms_finite_set: |
|
688 shows " \<exists>SN. ( \<forall>r.( rsize r < N \<longrightarrow> r \<in> SN)) \<and> (finite SN)" |
|
689 apply(induct N) |
|
690 apply simp |
|
691 apply auto |
|
692 (*\<lbrakk>\<forall>r. rsize r < N \<longrightarrow> r \<in> SN; finite SN\<rbrakk> \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*) |
|
693 (* \<And>N. \<exists>SN. (\<forall>r. rsize r < N \<longrightarrow> r \<in> SN) \<and> finite SN \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*) |
|
694 sorry |
|
695 |
|
696 |
|
697 lemma finite_size_finite_regx: |
|
698 shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) " |
|
699 sorry |
|
700 |
|
701 (*below probably needs proved concurrently*) |
|
702 |
|
703 lemma finite_r1r2_ders_list: |
|
704 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
|
705 \<Longrightarrow> \<exists>l. \<forall>s. |
|
706 (length (rdistinct (map rsimp (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) {}) ) < l " |
|
707 sorry |
|
708 |
|
709 (* |
|
710 \<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = |
|
711 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
|
712 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) ) |
|
713 *) |
|
714 |
|
715 |
|
716 lemma sum_list_size2: |
|
717 shows "\<forall>z \<in>set rs. (rsize z ) \<le> Nr \<Longrightarrow> rlist_size rs \<le> (length rs) * Nr" |
|
718 apply(induct rs) |
|
719 apply simp |
|
720 by simp |
|
721 |
|
722 lemma sum_list_size: |
|
723 fixes rs |
|
724 shows " \<forall>r \<in> (set rs). (rsize r) \<le> Nr \<and> (length rs) \<le> l \<Longrightarrow> rlist_size rs \<le> l * Nr" |
|
725 by (metis dual_order.trans mult.commute mult_le_mono2 mult_zero_right sum_list_size2 zero_le) |
|
726 |
|
727 lemma seq_second_term_chain1: |
|
728 shows " \<forall>s. rlist_size (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) \<le> |
|
729 rlist_size (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))" |
|
730 |
|
731 sorry |
|
732 |
|
733 |
|
734 lemma seq_second_term_chain2: |
|
735 shows "\<forall>s. rlist_size (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) = |
|
736 rlist_size (map rsimp (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)))" |
|
737 |
|
738 oops |
|
739 |
|
740 lemma seq_second_term_bounded: |
|
741 fixes r2 r1 |
|
742 assumes "\<forall>s. rsize (rders_simp r2 s) < N2" |
|
743 shows "\<exists>N3. \<forall>s. rlist_size (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) < N3" |
|
744 |
|
745 sorry |
|
746 |
|
747 |
|
748 lemma seq_first_term_bounded: |
|
749 fixes r1 r2 |
|
750 shows "\<exists>Nr. \<forall>s. rsize (rders_simp r1 s) \<le> Nr \<Longrightarrow> \<exists>Nr'. \<forall>s. rsize (RSEQ (rders_simp r1 s) r2) \<le> Nr'" |
|
751 apply(erule exE) |
|
752 apply(rule_tac x = "Nr + (rsize r2) + 1" in exI) |
|
753 by simp |
|
754 |
|
755 |
|
756 lemma alts_triangle_inequality: |
|
757 shows "rsize (RALTS (r # rs)) \<le> rsize r + rlist_size rs + 1 " |
|
758 apply(subgoal_tac "rsize (RALTS (r # rs) ) = rsize r + rlist_size rs + 1") |
|
759 apply auto[1] |
|
760 apply(induct rs) |
|
761 apply simp |
|
762 apply auto |
|
763 done |
|
764 |
|
765 lemma seq_equal_term_nosimp_entire_bounded: |
|
766 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
|
767 \<Longrightarrow> \<exists>N3. \<forall>s. rsize (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
768 (rdistinct ((rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) ) {}) ) ) \<le> N3" |
|
769 apply(subgoal_tac "\<exists>N3. \<forall>s. rsize (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
770 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) ) \<le> |
|
771 rsize (RSEQ (rders_simp r1 s) r2) + |
|
772 rlist_size (map rsimp (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) + 1") |
|
773 prefer 2 |
|
774 using alts_triangle_inequality apply presburger |
|
775 using seq_first_term_bounded |
|
776 using seq_second_term_bounded |
|
777 apply(subgoal_tac "\<exists>N3. \<forall>s. rlist_size (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) < N3") |
|
778 prefer 2 |
|
779 apply meson |
|
780 apply(subgoal_tac "\<exists>Nr'. \<forall>s. rsize (RSEQ (rders_simp r1 s) r2) \<le> Nr'") |
|
781 prefer 2 |
|
782 apply (meson order_le_less) |
|
783 apply(erule exE) |
|
784 apply(erule exE) |
|
785 apply(erule exE) |
|
786 apply(rule_tac x = "N3a + Nr'" in exI) |
|
787 sorry |
|
788 |
|
789 lemma alts_simp_bounded_by_sloppy1_version: |
|
790 shows "\<forall>s. rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
791 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )) \<le> |
|
792 rsize (RALTS (rdistinct ((RSEQ (rders_simp r1 s) r2) # |
|
793 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) |
|
794 ) |
|
795 {} |
|
796 ) |
|
797 ) " |
|
798 sorry |
|
799 |
|
800 lemma alts_simp_bounded_by_sloppy1: |
|
801 shows "rsize (rsimp (RALTS (rdistinct ((RSEQ (rders_simp r1 s) r2) # |
|
802 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) |
|
803 ) |
|
804 {} |
|
805 ) |
|
806 )) \<le> |
|
807 rsize (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
808 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) |
|
809 ) |
|
810 )" |
|
811 sorry |
|
812 |
|
813 lemma hand_made_def_rlist_size: |
|
814 shows "rlist_size rs = sum_list (map rsize rs)" |
|
815 proof (induct rs) |
|
816 case Nil show ?case by simp |
|
817 next |
|
818 case (Cons a rs) thus ?case |
|
819 by simp |
|
820 qed |
|
821 |
|
822 (*this section deals with the property of distinctBy: creates a list without duplicates*) |
|
823 lemma distinct_mono: |
|
824 shows "rlist_size (rdistinct (a # s) {}) \<le> rlist_size (a # (rdistinct s {}) )" |
|
825 sorry |
|
826 |
|
827 lemma distinct_acc_mono: |
|
828 shows "A \<subseteq> B \<Longrightarrow> rlist_size (rdistinct s A) \<ge> rlist_size (rdistinct s B)" |
|
829 apply(induct s arbitrary: A B) |
|
830 apply simp |
|
831 apply(case_tac "a \<in> A") |
|
832 apply(subgoal_tac "a \<in> B") |
|
833 |
|
834 apply simp |
|
835 |
|
836 apply blast |
|
837 apply(subgoal_tac "rlist_size (rdistinct (a # s) A) = rlist_size (a # (rdistinct s (A \<union> {a})))") |
|
838 apply(case_tac "a \<in> B") |
|
839 apply(subgoal_tac "rlist_size (rdistinct (a # s) B) = rlist_size ( (rdistinct s B))") |
|
840 apply (metis Un_insert_right dual_order.trans insert_subset le_add_same_cancel2 rlist_size.simps(1) sup_bot_right zero_order(1)) |
|
841 apply simp |
|
842 apply auto |
|
843 by (meson insert_mono) |
|
844 |
|
845 |
|
846 lemma distinct_mono2: |
|
847 shows " rlist_size (rdistinct s {a}) \<le> rlist_size (rdistinct s {})" |
|
848 apply(induct s) |
|
849 apply simp |
|
850 apply simp |
|
851 using distinct_acc_mono by auto |
|
852 |
|
853 |
|
854 |
|
855 lemma distinct_mono_spares_first_elem: |
|
856 shows "rsize (RALTS (rdistinct (a # s) {})) \<le> rsize (RALTS (a # (rdistinct s {})))" |
|
857 apply simp |
|
858 apply (subgoal_tac "rlist_size ( (rdistinct s {a})) \<le> rlist_size ( (rdistinct s {})) ") |
|
859 using hand_made_def_rlist_size apply auto[1] |
|
860 using distinct_mono2 by auto |
|
861 |
|
862 lemma sloppy1_bounded_by_sloppiest: |
|
863 shows "rsize (RALTS (rdistinct ((RSEQ (rders_simp r1 s) r2) # |
|
864 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) |
|
865 ) |
|
866 {} |
|
867 ) |
|
868 ) \<le> rsize (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
869 (rdistinct (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) {}) |
|
870 |
|
871 |
|
872 ) |
|
873 )" |
|
874 |
|
875 sorry |
|
876 |
|
877 |
|
878 lemma alts_simp_bounded_by_sloppiest_version: |
|
879 shows "\<forall>s. rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
880 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )) \<le> |
|
881 rsize (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
882 (rdistinct (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) {}) ) ) " |
|
883 by (meson alts_simp_bounded_by_sloppy1_version order_trans sloppy1_bounded_by_sloppiest) |
|
884 |
|
885 |
|
886 lemma seq_equal_term_entire_bounded: |
|
887 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
|
888 \<Longrightarrow> \<exists>N3. \<forall>s. rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
889 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )) \<le> N3" |
|
890 using seq_equal_term_nosimp_entire_bounded |
|
891 apply(subgoal_tac " \<exists>N3. \<forall>s. rsize (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
892 (rdistinct (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) {}) ) ) \<le> N3") |
|
893 apply(erule exE) |
|
894 prefer 2 |
|
895 apply blast |
|
896 apply(subgoal_tac "\<forall>s. rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
897 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )) \<le> |
|
898 rsize (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
899 (rdistinct (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) {}) ) ) ") |
|
900 prefer 2 |
|
901 using alts_simp_bounded_by_sloppiest_version apply blast |
|
902 apply(rule_tac x = "Suc N3 " in exI) |
|
903 apply(rule allI) |
|
904 |
|
905 apply(subgoal_tac " rsize |
|
906 (rsimp |
|
907 (RALTS |
|
908 (RSEQ (rders_simp r1 s) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)))) |
|
909 \<le> rsize |
|
910 (RALTS |
|
911 (RSEQ (rders_simp r1 s) r2 # |
|
912 rdistinct (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) {}))") |
|
913 prefer 2 |
|
914 apply presburger |
|
915 apply(subgoal_tac " rsize |
|
916 (RALTS |
|
917 (RSEQ (rders_simp r1 s) r2 # |
|
918 rdistinct (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) {})) \<le> N3") |
|
919 |
|
920 apply linarith |
|
921 apply simp |
|
922 done |
|
923 |
|
924 |
|
925 |
|
926 lemma M1seq: |
|
927 fixes r1 r2 |
|
928 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
|
929 \<Longrightarrow> \<exists>N3.\<forall>s.(rsize (rders_simp (RSEQ r1 r2) s)) < N3" |
|
930 apply(frule seq_equal_term_entire_bounded) |
|
931 apply(erule exE) |
|
932 apply(rule_tac x = "max (N3+2) (Suc (Suc (rsize r1) + (rsize r2)))" in exI) |
|
933 apply(rule allI) |
|
934 apply(case_tac "s = []") |
|
935 prefer 2 |
|
936 apply (metis add_2_eq_Suc' le_imp_less_Suc less_SucI max.strict_coboundedI1 shape_derssimp_seq(2)) |
|
937 by (metis add.assoc less_Suc_eq max.strict_coboundedI2 plus_1_eq_Suc rders_simp.simps(1) rsize.simps(5)) |
|
938 (* apply (simp add: less_SucI shape_derssimp_seq(2)) |
|
939 apply (meson less_SucI less_max_iff_disj) |
|
940 apply simp |
|
941 done*) |
|
942 |
|
943 (*lemma empty_diff: |
|
944 shows "s = [] \<Longrightarrow> |
|
945 (rsize (rders_simp (RSEQ r1 r2) s)) \<le> |
|
946 (max |
|
947 (rsize (rsimp (RALTS (RSEQ (rders r1 s) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))))) |
|
948 (Suc (rsize r1 + rsize r2)) ) " |
|
949 apply simp |
|
950 done*) |
|
951 (*For star related bound*) |
|
952 |
|
953 lemma star_is_a_singleton_list_derc: |
|
954 shows " \<exists>Ss. rders_simp (RSTAR r) [c] = rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)" |
|
955 apply simp |
|
956 apply(rule_tac x = "[[c]]" in exI) |
|
957 apply auto |
|
958 done |
|
959 |
|
960 lemma rder_rsimp_ALTs_commute: |
|
961 shows " (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)" |
|
962 apply(induct rs) |
|
963 apply simp |
|
964 apply(case_tac rs) |
|
965 apply simp |
|
966 apply auto |
|
967 done |
|
968 |
|
969 lemma double_nested_ALTs_under_rsimp: |
|
970 shows "rsimp (rsimp_ALTs ((RALTS rs1) # rs)) = rsimp (RALTS (rs1 @ rs))" |
|
971 apply(case_tac rs1) |
|
972 apply simp |
|
973 |
|
974 apply (metis list.simps(8) list.simps(9) neq_Nil_conv rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) |
|
975 apply(case_tac rs) |
|
976 apply simp |
|
977 apply auto |
|
978 sorry |
|
979 |
|
980 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list => char list list" where |
|
981 "star_update c r [] = []" |
|
982 |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) |
|
983 then (s@[c]) # [c] # (star_update c r Ss) |
|
984 else s # (star_update c r Ss) )" |
|
985 |
|
986 lemma starseq_list_evolution: |
|
987 fixes r :: rrexp and Ss :: "char list list" and x :: char |
|
988 shows "rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss) ) = |
|
989 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)) )" |
|
990 apply(induct Ss) |
|
991 apply simp |
|
992 sorry |
|
993 |
|
994 |
|
995 lemma star_seqs_produce_star_seqs: |
|
996 shows "rsimp (rsimp_ALTs (map (rder x \<circ> (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) |
|
997 = rsimp (rsimp_ALTs (map ( (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss))" |
|
998 by (meson comp_apply) |
|
999 |
|
1000 lemma der_seqstar_res: |
|
1001 shows "rder x (RSEQ r1 r2) = RSEQ r3 r4" |
|
1002 oops |
|
1003 |
|
1004 lemma linearity_of_list_of_star_or_starseqs: |
|
1005 fixes r::rrexp and Ss::"char list list" and x::char |
|
1006 shows "\<exists>Ssa. rsimp (rder x (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) = |
|
1007 rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)" |
|
1008 apply(simp add: rder_rsimp_ALTs_commute) |
|
1009 apply(induct Ss) |
|
1010 apply simp |
|
1011 apply (metis list.simps(8) rsimp_ALTs.simps(1)) |
|
1012 |
|
1013 |
|
1014 sorry |
|
1015 |
|
1016 lemma starder_is_a_list_of_stars_or_starseqs: |
|
1017 shows "s \<noteq> [] \<Longrightarrow> \<exists>Ss. rders_simp (RSTAR r) s = rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)" |
|
1018 apply(induct s rule: rev_induct) |
|
1019 apply simp |
|
1020 apply(case_tac "xs = []") |
|
1021 using star_is_a_singleton_list_derc |
|
1022 apply(simp) |
|
1023 apply auto |
|
1024 apply(simp add: rders_simp_append) |
|
1025 using linearity_of_list_of_star_or_starseqs by blast |
|
1026 |
|
1027 |
|
1028 lemma finite_star: |
|
1029 shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) |
|
1030 \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3" |
|
1031 |
|
1032 sorry |
|
1033 |
|
1034 |
|
1035 lemma rderssimp_zero: |
|
1036 shows"rders_simp RZERO s = RZERO" |
|
1037 apply(induction s) |
|
1038 apply simp |
|
1039 by simp |
|
1040 |
|
1041 lemma rderssimp_one: |
|
1042 shows"rders_simp RONE (a # s) = RZERO" |
|
1043 apply(induction s) |
|
1044 apply simp |
|
1045 by simp |
|
1046 |
|
1047 lemma rderssimp_char: |
|
1048 shows "rders_simp (RCHAR c) s = RONE \<or> rders_simp (RCHAR c) s = RZERO \<or> rders_simp (RCHAR c) s = (RCHAR c)" |
|
1049 apply auto |
|
1050 by (metis rder.simps(2) rder.simps(3) rders_simp.elims rders_simp.simps(2) rderssimp_one rsimp.simps(4)) |
|
1051 |
|
1052 lemma finite_size_ders: |
|
1053 fixes r |
|
1054 shows " \<exists>Nr. \<forall>s. rsize (rders_simp r s) < Nr" |
|
1055 apply(induct r rule: rrexp.induct) |
|
1056 apply auto |
|
1057 apply(rule_tac x = "2" in exI) |
|
1058 using rderssimp_zero rsize.simps(1) apply presburger |
|
1059 apply(rule_tac x = "2" in exI) |
|
1060 apply (metis Suc_1 lessI rders_simp.elims rderssimp_one rsize.simps(1) rsize.simps(2)) |
|
1061 apply(rule_tac x = "2" in meta_spec) |
|
1062 apply (metis lessI rderssimp_char rsize.simps(1) rsize.simps(2) rsize.simps(3)) |
|
1063 |
|
1064 using M1seq apply blast |
|
1065 prefer 2 |
|
1066 |
|
1067 apply (simp add: finite_star) |
|
1068 sorry |
|
1069 |
|
1070 |
|
1071 unused_thms |
|
1072 lemma seq_ders_shape: |
|
1073 shows "E" |
|
1074 |
|
1075 oops |
|
1076 |
|
1077 (*rsimp (rders (RSEQ r1 r2) s) = |
|
1078 rsimp RALT [RSEQ (rders r1 s) r2, rders r2 si, ...] |
|
1079 where si is the i-th shortest suffix of s such that si \<in> L r2" |
|
1080 *) |
|
1081 |
|
1082 |
|
1083 end |