|
1 theory BasicIdentities |
|
2 imports "RfltsRdistinctProps" |
|
3 begin |
|
4 |
|
5 |
|
6 |
|
7 lemma rder_rsimp_ALTs_commute: |
|
8 shows " (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)" |
|
9 apply(induct rs) |
|
10 apply simp |
|
11 apply(case_tac rs) |
|
12 apply simp |
|
13 apply auto |
|
14 done |
|
15 |
|
16 |
|
17 |
|
18 lemma rsimp_aalts_smaller: |
|
19 shows "rsize (rsimp_ALTs rs) \<le> rsize (RALTS rs)" |
|
20 apply(induct rs) |
|
21 apply simp |
|
22 apply simp |
|
23 apply(case_tac "rs = []") |
|
24 apply simp |
|
25 apply(subgoal_tac "\<exists>rsp ap. rs = ap # rsp") |
|
26 apply(erule exE)+ |
|
27 apply simp |
|
28 apply simp |
|
29 by(meson neq_Nil_conv) |
|
30 |
|
31 |
|
32 |
|
33 |
|
34 |
|
35 lemma rSEQ_mono: |
|
36 shows "rsize (rsimp_SEQ r1 r2) \<le>rsize (RSEQ r1 r2)" |
|
37 apply auto |
|
38 apply(induct r1) |
|
39 apply auto |
|
40 apply(case_tac "r2") |
|
41 apply simp_all |
|
42 apply(case_tac r2) |
|
43 apply simp_all |
|
44 apply(case_tac r2) |
|
45 apply simp_all |
|
46 apply(case_tac r2) |
|
47 apply simp_all |
|
48 apply(case_tac r2) |
|
49 apply simp_all |
|
50 done |
|
51 |
|
52 lemma ralts_cap_mono: |
|
53 shows "rsize (RALTS rs) \<le> Suc (rsizes rs)" |
|
54 by simp |
|
55 |
|
56 |
|
57 |
|
58 |
|
59 lemma rflts_mono: |
|
60 shows "rsizes (rflts rs) \<le> rsizes rs" |
|
61 apply(induct rs) |
|
62 apply simp |
|
63 apply(case_tac "a = RZERO") |
|
64 apply simp |
|
65 apply(case_tac "\<exists>rs1. a = RALTS rs1") |
|
66 apply(erule exE) |
|
67 apply simp |
|
68 apply(subgoal_tac "rflts (a # rs) = a # (rflts rs)") |
|
69 prefer 2 |
|
70 |
|
71 using rflts_def_idiot apply blast |
|
72 apply simp |
|
73 done |
|
74 |
|
75 lemma rdistinct_smaller: |
|
76 shows "rsizes (rdistinct rs ss) \<le> rsizes rs" |
|
77 apply (induct rs arbitrary: ss) |
|
78 apply simp |
|
79 by (simp add: trans_le_add2) |
|
80 |
|
81 |
|
82 lemma rsimp_alts_mono : |
|
83 shows "\<And>x. (\<And>xa. xa \<in> set x \<Longrightarrow> rsize (rsimp xa) \<le> rsize xa) \<Longrightarrow> |
|
84 rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {})) \<le> Suc (rsizes x)" |
|
85 apply(subgoal_tac "rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {} )) |
|
86 \<le> rsize (RALTS (rdistinct (rflts (map rsimp x)) {} ))") |
|
87 prefer 2 |
|
88 using rsimp_aalts_smaller apply auto[1] |
|
89 apply(subgoal_tac "rsize (RALTS (rdistinct (rflts (map rsimp x)) {})) \<le>Suc (rsizes (rdistinct (rflts (map rsimp x)) {}))") |
|
90 prefer 2 |
|
91 using ralts_cap_mono apply blast |
|
92 apply(subgoal_tac "rsizes (rdistinct (rflts (map rsimp x)) {}) \<le> rsizes (rflts (map rsimp x))") |
|
93 prefer 2 |
|
94 using rdistinct_smaller apply presburger |
|
95 apply(subgoal_tac "rsizes (rflts (map rsimp x)) \<le> rsizes (map rsimp x)") |
|
96 prefer 2 |
|
97 using rflts_mono apply blast |
|
98 apply(subgoal_tac "rsizes (map rsimp x) \<le> rsizes x") |
|
99 prefer 2 |
|
100 |
|
101 apply (simp add: sum_list_mono) |
|
102 by linarith |
|
103 |
|
104 |
|
105 |
|
106 |
|
107 |
|
108 lemma rsimp_mono: |
|
109 shows "rsize (rsimp r) \<le> rsize r" |
|
110 apply(induct r) |
|
111 apply simp_all |
|
112 apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \<le> rsize (RSEQ (rsimp r1) (rsimp r2))") |
|
113 apply force |
|
114 using rSEQ_mono |
|
115 apply presburger |
|
116 using rsimp_alts_mono by auto |
|
117 |
|
118 lemma idiot: |
|
119 shows "rsimp_SEQ RONE r = r" |
|
120 apply(case_tac r) |
|
121 apply simp_all |
|
122 done |
|
123 |
|
124 |
|
125 |
|
126 |
|
127 |
|
128 lemma idiot2: |
|
129 shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk> |
|
130 \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2" |
|
131 apply(case_tac r1) |
|
132 apply(case_tac r2) |
|
133 apply simp_all |
|
134 apply(case_tac r2) |
|
135 apply simp_all |
|
136 apply(case_tac r2) |
|
137 apply simp_all |
|
138 apply(case_tac r2) |
|
139 apply simp_all |
|
140 apply(case_tac r2) |
|
141 apply simp_all |
|
142 done |
|
143 |
|
144 lemma rders__onechar: |
|
145 shows " (rders_simp r [c]) = (rsimp (rders r [c]))" |
|
146 by simp |
|
147 |
|
148 lemma rders_append: |
|
149 "rders c (s1 @ s2) = rders (rders c s1) s2" |
|
150 apply(induct s1 arbitrary: c s2) |
|
151 apply(simp_all) |
|
152 done |
|
153 |
|
154 lemma rders_simp_append: |
|
155 "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2" |
|
156 apply(induct s1 arbitrary: c s2) |
|
157 apply(simp_all) |
|
158 done |
|
159 |
|
160 |
|
161 lemma rders_simp_one_char: |
|
162 shows "rders_simp r [c] = rsimp (rder c r)" |
|
163 apply auto |
|
164 done |
|
165 |
|
166 |
|
167 |
|
168 |
|
169 |
|
170 lemma k0a: |
|
171 shows "rflts [RALTS rs] = rs" |
|
172 apply(simp) |
|
173 done |
|
174 |
|
175 lemma bbbbs: |
|
176 assumes "good r" "r = RALTS rs" |
|
177 shows "rsimp_ALTs (rflts [r]) = RALTS rs" |
|
178 using assms |
|
179 by (metis good.simps(4) good.simps(5) k0a rsimp_ALTs.elims) |
|
180 |
|
181 lemma bbbbs1: |
|
182 shows "nonalt r \<or> (\<exists> rs. r = RALTS rs)" |
|
183 by (meson nonalt.elims(3)) |
|
184 |
|
185 |
|
186 |
|
187 lemma good0: |
|
188 assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r" "distinct rs" |
|
189 shows "good (rsimp_ALTs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)" |
|
190 using assms |
|
191 apply(induct rs rule: rsimp_ALTs.induct) |
|
192 apply(auto) |
|
193 done |
|
194 |
|
195 lemma flts1: |
|
196 assumes "good r" |
|
197 shows "rflts [r] \<noteq> []" |
|
198 using assms |
|
199 apply(induct r) |
|
200 apply(simp_all) |
|
201 using good.simps(4) by blast |
|
202 |
|
203 lemma flts2: |
|
204 assumes "good r" |
|
205 shows "\<forall>r' \<in> set (rflts [r]). good r' \<and> nonalt r'" |
|
206 using assms |
|
207 apply(induct r) |
|
208 apply(simp) |
|
209 apply(simp) |
|
210 apply(simp) |
|
211 prefer 2 |
|
212 apply(simp) |
|
213 apply(auto)[1] |
|
214 |
|
215 apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv) |
|
216 apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv) |
|
217 apply fastforce |
|
218 apply(simp) |
|
219 done |
|
220 |
|
221 |
|
222 |
|
223 lemma flts3: |
|
224 assumes "\<forall>r \<in> set rs. good r \<or> r = RZERO" |
|
225 shows "\<forall>r \<in> set (rflts rs). good r" |
|
226 using assms |
|
227 apply(induct rs rule: rflts.induct) |
|
228 apply(simp_all) |
|
229 by (metis UnE flts2 k0a) |
|
230 |
|
231 |
|
232 lemma k0: |
|
233 shows "rflts (r # rs1) = rflts [r] @ rflts rs1" |
|
234 apply(induct r arbitrary: rs1) |
|
235 apply(auto) |
|
236 done |
|
237 |
|
238 |
|
239 lemma good_SEQ: |
|
240 assumes "r1 \<noteq> RZERO" "r2 \<noteq> RZERO" " r1 \<noteq> RONE" |
|
241 shows "good (RSEQ r1 r2) = (good r1 \<and> good r2)" |
|
242 using assms |
|
243 apply(case_tac r1) |
|
244 apply(simp_all) |
|
245 apply(case_tac r2) |
|
246 apply(simp_all) |
|
247 apply(case_tac r2) |
|
248 apply(simp_all) |
|
249 apply(case_tac r2) |
|
250 apply(simp_all) |
|
251 apply(case_tac r2) |
|
252 apply(simp_all) |
|
253 done |
|
254 |
|
255 lemma rsize0: |
|
256 shows "0 < rsize r" |
|
257 apply(induct r) |
|
258 apply(auto) |
|
259 done |
|
260 |
|
261 |
|
262 |
|
263 |
|
264 |
|
265 |
|
266 |
|
267 |
|
268 |
|
269 |
|
270 |
|
271 lemma nn1qq: |
|
272 assumes "nonnested (RALTS rs)" |
|
273 shows "\<nexists> rs1. RALTS rs1 \<in> set rs" |
|
274 using assms |
|
275 apply(induct rs rule: rflts.induct) |
|
276 apply(auto) |
|
277 done |
|
278 |
|
279 |
|
280 |
|
281 lemma n0: |
|
282 shows "nonnested (RALTS rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)" |
|
283 apply(induct rs ) |
|
284 apply(auto) |
|
285 apply (metis list.set_intros(1) nn1qq nonalt.elims(3)) |
|
286 apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7)) |
|
287 using bbbbs1 apply fastforce |
|
288 by (metis bbbbs1 list.set_intros(2) nn1qq) |
|
289 |
|
290 |
|
291 |
|
292 |
|
293 lemma nn1c: |
|
294 assumes "\<forall>r \<in> set rs. nonnested r" |
|
295 shows "\<forall>r \<in> set (rflts rs). nonalt r" |
|
296 using assms |
|
297 apply(induct rs rule: rflts.induct) |
|
298 apply(auto) |
|
299 using n0 by blast |
|
300 |
|
301 lemma nn1bb: |
|
302 assumes "\<forall>r \<in> set rs. nonalt r" |
|
303 shows "nonnested (rsimp_ALTs rs)" |
|
304 using assms |
|
305 apply(induct rs rule: rsimp_ALTs.induct) |
|
306 apply(auto) |
|
307 using nonalt.simps(1) nonnested.elims(3) apply blast |
|
308 using n0 by auto |
|
309 |
|
310 lemma bsimp_ASEQ0: |
|
311 shows "rsimp_SEQ r1 RZERO = RZERO" |
|
312 apply(induct r1) |
|
313 apply(auto) |
|
314 done |
|
315 |
|
316 lemma nn1b: |
|
317 shows "nonnested (rsimp r)" |
|
318 apply(induct r) |
|
319 apply(simp_all) |
|
320 apply(case_tac "rsimp r1 = RZERO") |
|
321 apply(simp) |
|
322 apply(case_tac "rsimp r2 = RZERO") |
|
323 apply(simp) |
|
324 apply(subst bsimp_ASEQ0) |
|
325 apply(simp) |
|
326 apply(case_tac "\<exists>bs. rsimp r1 = RONE") |
|
327 apply(auto)[1] |
|
328 using idiot apply fastforce |
|
329 using idiot2 nonnested.simps(11) apply presburger |
|
330 by (metis (mono_tags, lifting) Diff_empty image_iff list.set_map nn1bb nn1c rdistinct_set_equality1) |
|
331 |
|
332 lemma nonalt_flts_rd: |
|
333 shows "\<lbrakk>xa \<in> set (rdistinct (rflts (map rsimp rs)) {})\<rbrakk> |
|
334 \<Longrightarrow> nonalt xa" |
|
335 by (metis Diff_empty ex_map_conv nn1b nn1c rdistinct_set_equality1) |
|
336 |
|
337 |
|
338 |
|
339 |
|
340 lemma bsimp_ASEQ2: |
|
341 shows "rsimp_SEQ RONE r2 = r2" |
|
342 apply(induct r2) |
|
343 apply(auto) |
|
344 done |
|
345 |
|
346 lemma elem_smaller_than_set: |
|
347 shows "xa \<in> set list \<Longrightarrow> rsize xa < Suc (rsizes list)" |
|
348 apply(induct list) |
|
349 apply simp |
|
350 by (metis image_eqI le_imp_less_Suc list.set_map member_le_sum_list) |
|
351 |
|
352 lemma rsimp_list_mono: |
|
353 shows "rsizes (map rsimp rs) \<le> rsizes rs" |
|
354 apply(induct rs) |
|
355 apply simp+ |
|
356 by (simp add: add_mono_thms_linordered_semiring(1) rsimp_mono) |
|
357 |
|
358 |
|
359 (*says anything coming out of simp+flts+db will be good*) |
|
360 lemma good2_obv_simplified: |
|
361 shows " \<lbrakk>\<forall>y. rsize y < Suc (rsizes rs) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO; |
|
362 xa \<in> set (rdistinct (rflts (map rsimp rs)) {})\<rbrakk> \<Longrightarrow> good xa" |
|
363 apply(subgoal_tac " \<forall>xa' \<in> set (map rsimp rs). good xa' \<or> xa' = RZERO") |
|
364 prefer 2 |
|
365 apply (simp add: elem_smaller_than_set) |
|
366 by (metis Diff_empty flts3 rdistinct_set_equality1) |
|
367 |
|
368 |
|
369 |
|
370 |
|
371 lemma good1: |
|
372 shows "good (rsimp a) \<or> rsimp a = RZERO" |
|
373 apply(induct a taking: rsize rule: measure_induct) |
|
374 apply(case_tac x) |
|
375 apply(simp) |
|
376 apply(simp) |
|
377 apply(simp) |
|
378 prefer 3 |
|
379 apply(simp) |
|
380 prefer 2 |
|
381 apply(simp only:) |
|
382 apply simp |
|
383 apply (smt (verit, ccfv_threshold) add_mono_thms_linordered_semiring(1) elem_smaller_than_set good0 good2_obv_simplified le_eq_less_or_eq nonalt_flts_rd order_less_trans plus_1_eq_Suc rdistinct_does_the_job rdistinct_smaller rflts_mono rsimp_ALTs.simps(1) rsimp_list_mono) |
|
384 apply simp |
|
385 apply(subgoal_tac "good (rsimp x41) \<or> rsimp x41 = RZERO") |
|
386 apply(subgoal_tac "good (rsimp x42) \<or> rsimp x42 = RZERO") |
|
387 apply(case_tac "rsimp x41 = RZERO") |
|
388 apply simp |
|
389 apply(case_tac "rsimp x42 = RZERO") |
|
390 apply simp |
|
391 using bsimp_ASEQ0 apply blast |
|
392 apply(subgoal_tac "good (rsimp x41)") |
|
393 apply(subgoal_tac "good (rsimp x42)") |
|
394 apply simp |
|
395 apply (metis bsimp_ASEQ2 good_SEQ idiot2) |
|
396 apply blast |
|
397 apply fastforce |
|
398 using less_add_Suc2 apply blast |
|
399 using less_iff_Suc_add by blast |
|
400 |
|
401 lemma RL_rnullable: |
|
402 shows "rnullable r = ([] \<in> RL r)" |
|
403 apply(induct r) |
|
404 apply(auto simp add: Sequ_def) |
|
405 done |
|
406 |
|
407 lemma RL_rder: |
|
408 shows "RL (rder c r) = Der c (RL r)" |
|
409 apply(induct r) |
|
410 apply(auto simp add: Sequ_def Der_def) |
|
411 apply (metis append_Cons) |
|
412 using RL_rnullable apply blast |
|
413 apply (metis append_eq_Cons_conv) |
|
414 apply (metis append_Cons) |
|
415 apply (metis RL_rnullable append_eq_Cons_conv) |
|
416 apply (metis Star.step append_Cons) |
|
417 using Star_decomp by auto |
|
418 |
|
419 |
|
420 |
|
421 |
|
422 lemma RL_rsimp_RSEQ: |
|
423 shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)" |
|
424 apply(induct r1 r2 rule: rsimp_SEQ.induct) |
|
425 apply(simp_all) |
|
426 done |
|
427 |
|
428 |
|
429 |
|
430 lemma RL_rsimp_RALTS: |
|
431 shows "RL (rsimp_ALTs rs) = (\<Union> (set (map RL rs)))" |
|
432 apply(induct rs rule: rsimp_ALTs.induct) |
|
433 apply(simp_all) |
|
434 done |
|
435 |
|
436 lemma RL_rsimp_rdistinct: |
|
437 shows "(\<Union> (set (map RL (rdistinct rs {})))) = (\<Union> (set (map RL rs)))" |
|
438 apply(auto) |
|
439 apply (metis Diff_iff rdistinct_set_equality1) |
|
440 by (metis Diff_empty rdistinct_set_equality1) |
|
441 |
|
442 lemma RL_rsimp_rflts: |
|
443 shows "(\<Union> (set (map RL (rflts rs)))) = (\<Union> (set (map RL rs)))" |
|
444 apply(induct rs rule: rflts.induct) |
|
445 apply(simp_all) |
|
446 done |
|
447 |
|
448 lemma RL_rsimp: |
|
449 shows "RL r = RL (rsimp r)" |
|
450 apply(induct r rule: rsimp.induct) |
|
451 apply(auto simp add: Sequ_def RL_rsimp_RSEQ) |
|
452 using RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts apply auto[1] |
|
453 by (smt (verit, del_insts) RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts UN_E image_iff list.set_map) |
|
454 |
|
455 |
|
456 |
|
457 lemma der_simp_nullability: |
|
458 shows "rnullable r = rnullable (rsimp r)" |
|
459 using RL_rnullable RL_rsimp by auto |
|
460 |
|
461 |
|
462 lemma qqq1: |
|
463 shows "RZERO \<notin> set (rflts (map rsimp rs))" |
|
464 by (metis ex_map_conv flts3 good.simps(1) good1) |
|
465 |
|
466 |
|
467 |
|
468 |
|
469 |
|
470 lemma flts_single1: |
|
471 assumes "nonalt r" "nonazero r" |
|
472 shows "rflts [r] = [r]" |
|
473 using assms |
|
474 apply(induct r) |
|
475 apply(auto) |
|
476 done |
|
477 |
|
478 lemma nonalt0_flts_keeps: |
|
479 shows "(a \<noteq> RZERO) \<and> (\<forall>rs. a \<noteq> RALTS rs) \<Longrightarrow> rflts (a # xs) = a # rflts xs" |
|
480 apply(case_tac a) |
|
481 apply simp+ |
|
482 done |
|
483 |
|
484 |
|
485 lemma nonalt0_fltseq: |
|
486 shows "\<forall>r \<in> set rs. r \<noteq> RZERO \<and> nonalt r \<Longrightarrow> rflts rs = rs" |
|
487 apply(induct rs) |
|
488 apply simp |
|
489 apply(case_tac "a = RZERO") |
|
490 apply fastforce |
|
491 apply(case_tac "\<exists>rs1. a = RALTS rs1") |
|
492 apply(erule exE) |
|
493 apply simp+ |
|
494 using nonalt0_flts_keeps by presburger |
|
495 |
|
496 |
|
497 |
|
498 |
|
499 lemma goodalts_nonalt: |
|
500 shows "good (RALTS rs) \<Longrightarrow> rflts rs = rs" |
|
501 apply(induct x == "RALTS rs" arbitrary: rs rule: good.induct) |
|
502 apply simp |
|
503 |
|
504 using good.simps(5) apply blast |
|
505 apply simp |
|
506 apply(case_tac "r1 = RZERO") |
|
507 using good.simps(1) apply force |
|
508 apply(case_tac "r2 = RZERO") |
|
509 using good.simps(1) apply force |
|
510 apply(subgoal_tac "rflts (r1 # r2 # rs) = r1 # r2 # rflts rs") |
|
511 prefer 2 |
|
512 apply (metis nonalt.simps(1) rflts_def_idiot) |
|
513 apply(subgoal_tac "\<forall>r \<in> set rs. r \<noteq> RZERO \<and> nonalt r") |
|
514 apply(subgoal_tac "rflts rs = rs") |
|
515 apply presburger |
|
516 using nonalt0_fltseq apply presburger |
|
517 using good.simps(1) by blast |
|
518 |
|
519 |
|
520 |
|
521 |
|
522 |
|
523 lemma test: |
|
524 assumes "good r" |
|
525 shows "rsimp r = r" |
|
526 |
|
527 using assms |
|
528 apply(induct rule: good.induct) |
|
529 apply simp |
|
530 apply simp |
|
531 apply simp |
|
532 apply simp |
|
533 apply simp |
|
534 apply(subgoal_tac "distinct (r1 # r2 # rs)") |
|
535 prefer 2 |
|
536 using good.simps(6) apply blast |
|
537 apply(subgoal_tac "rflts (r1 # r2 # rs ) = r1 # r2 # rs") |
|
538 prefer 2 |
|
539 using goodalts_nonalt apply blast |
|
540 |
|
541 apply(subgoal_tac "r1 \<noteq> r2") |
|
542 prefer 2 |
|
543 apply (meson distinct_length_2_or_more) |
|
544 apply(subgoal_tac "r1 \<notin> set rs") |
|
545 apply(subgoal_tac "r2 \<notin> set rs") |
|
546 apply(subgoal_tac "\<forall>r \<in> set rs. rsimp r = r") |
|
547 apply(subgoal_tac "map rsimp rs = rs") |
|
548 apply simp |
|
549 apply(subgoal_tac "\<forall>r \<in> {r1, r2}. r \<notin> set rs") |
|
550 apply (metis distinct_not_exist rdistinct_on_distinct) |
|
551 |
|
552 apply blast |
|
553 apply (meson map_idI) |
|
554 apply (metis good.simps(6) insert_iff list.simps(15)) |
|
555 |
|
556 apply (meson distinct.simps(2)) |
|
557 apply (simp add: distinct_length_2_or_more) |
|
558 apply simp+ |
|
559 done |
|
560 |
|
561 |
|
562 |
|
563 lemma rsimp_idem: |
|
564 shows "rsimp (rsimp r) = rsimp r" |
|
565 using test good1 |
|
566 by force |
|
567 |
|
568 corollary rsimp_inner_idem4: |
|
569 shows "rsimp r = RALTS rs \<Longrightarrow> rflts rs = rs" |
|
570 by (metis good1 goodalts_nonalt rrexp.simps(12)) |
|
571 |
|
572 |
|
573 corollary head_one_more_simp: |
|
574 shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)" |
|
575 by (simp add: rsimp_idem) |
|
576 |
|
577 |
|
578 |
|
579 |
|
580 lemma basic_regex_property1: |
|
581 shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO" |
|
582 apply(induct r rule: rsimp.induct) |
|
583 apply(auto) |
|
584 apply (metis idiot idiot2 rrexp.distinct(5)) |
|
585 by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2)) |
|
586 |
|
587 |
|
588 |
|
589 lemma no_alt_short_list_after_simp: |
|
590 shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
591 by (metis bbbbs good1 k0a rrexp.simps(12)) |
|
592 |
|
593 |
|
594 lemma no_further_dB_after_simp: |
|
595 shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs" |
|
596 apply(subgoal_tac "good (RALTS rs)") |
|
597 apply(subgoal_tac "distinct rs") |
|
598 using rdistinct_on_distinct apply blast |
|
599 apply (metis distinct.simps(1) distinct.simps(2) empty_iff good.simps(6) list.exhaust set_empty2) |
|
600 using good1 by fastforce |
|
601 |
|
602 |
|
603 lemma idem_after_simp1: |
|
604 shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa" |
|
605 apply(case_tac "rsimp aa") |
|
606 apply simp+ |
|
607 apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) |
|
608 by simp |
|
609 |
|
610 |
|
611 |
|
612 |
|
613 |
|
614 (*equalities with rsimp *) |
|
615 lemma identity_wwo0: |
|
616 shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)" |
|
617 by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) |
|
618 |
|
619 |
|
620 |
|
621 |
|
622 |
|
623 |
|
624 |
|
625 (*some basic facts about rsimp*) |
|
626 |
|
627 unused_thms |
|
628 |
|
629 |
|
630 end |