276 using leq1.intros(1) leq1.intros(16) apply auto[1] |
311 using leq1.intros(1) leq1.intros(16) apply auto[1] |
277 using leq1.intros(1) leq1.intros(16) apply force |
312 using leq1.intros(1) leq1.intros(16) apply force |
278 apply (simp add: leq1.intros(1) leq1.intros(16)) |
313 apply (simp add: leq1.intros(1) leq1.intros(16)) |
279 using leq1.intros(1) leq1.intros(16) by force |
314 using leq1.intros(1) leq1.intros(16) by force |
280 |
315 |
281 lemma dB_leq12: |
316 |
282 shows "AALTs bs (rs1 @ (distinctWith rs1 eq1 (set rs2))) \<le>1 AALTs bs (rs1 @ rs2)" |
|
283 apply(induct rs1 arbitrary: rs2) |
|
284 apply simp |
|
285 sorry |
|
286 |
317 |
287 |
318 |
288 lemma dB_leq1: |
319 lemma dB_leq1: |
289 shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs" |
320 shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs" |
290 sorry |
321 by (metis append_Nil empty_set leq1.intros(18)) |
|
322 |
|
323 lemma leq1_list: |
|
324 shows " |
|
325 \<lbrakk>\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> bsimp x2aa \<le>1 x2aa; |
|
326 bsimp_AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1 AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}); |
|
327 AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1 AALTs x1 (flts (map bsimp x2a)); |
|
328 AALTs x1 (flts (map bsimp x2a)) \<le>1 AALTs x1 (map bsimp x2a)\<rbrakk> |
|
329 \<Longrightarrow> AALTs x1 (map bsimp x2a) \<le>1 AALTs x1 x2a" |
|
330 apply(induct x2a) |
|
331 apply simp |
|
332 by (simp add: dB_leq1 flts_leq1 leq1.intros(16) leq1.intros(19)) |
|
333 |
|
334 |
|
335 |
|
336 lemma bsimp_leq1: |
|
337 shows "bsimp r \<le>1 r" |
|
338 apply(induct r) |
|
339 apply simp |
|
340 |
|
341 apply (simp add: leq1.intros(1)) |
|
342 |
|
343 using leq1.intros(1) apply force |
|
344 |
|
345 apply (simp add: leq1.intros(1)) |
|
346 |
|
347 |
|
348 apply (simp add: leq1.intros(15)) |
|
349 prefer 2 |
|
350 |
|
351 apply (simp add: leq1.intros(1)) |
|
352 prefer 2 |
|
353 |
|
354 apply (simp add: leq1.intros(1)) |
|
355 apply simp |
|
356 apply(subgoal_tac " bsimp_AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1 AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {})") |
|
357 apply(subgoal_tac " AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1 AALTs x1 ( (flts (map bsimp x2a)) )") |
|
358 apply(subgoal_tac " AALTs x1 ( (flts (map bsimp x2a)) ) \<le>1 AALTs x1 ( ( (map bsimp x2a)) )") |
|
359 |
|
360 apply(subgoal_tac " AALTs x1 ( map bsimp x2a ) \<le>1 AALTs x1 x2a ") |
|
361 |
|
362 apply (meson leq1.intros(17)) |
|
363 |
|
364 using leq1_list apply blast |
|
365 |
|
366 using flts_leq1 apply presburger |
|
367 |
|
368 using dB_leq1 apply blast |
|
369 |
|
370 using leq1.intros(19) by blast |
291 |
371 |
292 |
372 |
293 |
373 |
294 |
374 |
295 lemma stupid_leq1_1: |
375 lemma stupid_leq1_1: |
296 shows " rerase r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))" |
376 shows " rerase r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))" |
297 apply(induct r2) |
377 apply(induct r2) |
298 apply simp+ |
378 apply simp+ |
299 done |
379 done |
|
380 |
|
381 |
|
382 lemma rerase_arexp_additional1: |
|
383 shows " asize (AALTs bs (rs1 @ rs2)) = rsize (RALTS (map rerase rs1 @ map rerase rs2))" |
|
384 apply simp |
|
385 by (metis (mono_tags, lifting) asize_rsize comp_apply map_eq_conv) |
|
386 |
|
387 |
|
388 |
|
389 |
|
390 lemma rerase2: |
|
391 shows "rsizes (map rerase (distinctWith rs2 eq1 (set rs1))) \<le> rsizes (map rerase rs2)" |
|
392 apply(induct rs2 arbitrary: rs1) |
|
393 apply simp+ |
|
394 by (metis List.set_insert trans_le_add2) |
|
395 |
|
396 lemma rerase3: |
|
397 shows "rsize (RALTS (map rerase rs1 @ map rerase (distinctWith rs2 eq1 (set rs1)))) \<le> rsize (RALTS (map rerase rs1 @ map rerase rs2))" |
|
398 using rerase2 by force |
|
399 |
|
400 |
|
401 lemma bsimpalts_size: |
|
402 shows "asize (bsimp_AALTs bs rs) \<le> asize (AALTs bs rs)" |
|
403 apply(case_tac rs) |
|
404 apply simp |
|
405 apply(case_tac list) |
|
406 apply auto |
|
407 by (metis asize_rsize dual_order.refl le_SucI rerase_fuse) |
|
408 |
|
409 |
300 |
410 |
301 lemma leq1_size: |
411 lemma leq1_size: |
302 shows "r1 \<le>1 r2 \<Longrightarrow> asize r1 \<le> asize r2" |
412 shows "r1 \<le>1 r2 \<Longrightarrow> asize r1 \<le> asize r2" |
303 apply (induct rule: leq1.induct) |
413 apply (induct rule: leq1.induct) |
304 apply simp+ |
414 apply simp+ |
355 |
471 |
356 apply force |
472 apply force |
357 apply simp |
473 apply simp |
358 apply(simp add: asize_rsize) |
474 apply(simp add: asize_rsize) |
359 apply (simp add: rerase_fuse size_deciding_equality4) |
475 apply (simp add: rerase_fuse size_deciding_equality4) |
360 apply (metis Suc_n_not_le_n asize_rsize leq1.intros(15) leq1_size rsize.simps(5) trans_le_add2) |
476 apply (metis Suc_n_not_le_n asize_rsize leq1.intros(15) leq1_size rsize.simps(5) trans_le_add2) |
|
477 apply simp |
|
478 |
|
479 apply (metis asize_rsize leq1_size lessI nle_le not_add_less2 plus_1_eq_Suc rsize.simps(5) trans_le_add2) |
|
480 apply simp |
|
481 by (metis Suc_n_not_le_n bsimpalts_size rsize.simps(5) size_deciding_equality5 trans_le_add2) |
|
482 |
|
483 lemma leq1_neq: |
|
484 shows "\<lbrakk>r1 \<le>1 r2 ; r1 \<noteq> r2\<rbrakk> \<Longrightarrow> asize r1 < asize r2" |
|
485 apply(induct rule : leq1.induct) |
|
486 apply simp+ |
|
487 apply (metis asize_rsize lessI less_SucI rerase_fuse) |
|
488 apply simp+ |
|
489 |
|
490 apply (metis (mono_tags, lifting) comp_apply less_SucI map_eq_conv not_less_less_Suc_eq rerase_fuse size_deciding_equality3) |
|
491 apply simp |
|
492 |
|
493 apply (simp add: asize0) |
|
494 |
|
495 using less_Suc_eq apply auto[1] |
|
496 apply simp |
|
497 apply simp |
|
498 apply simp |
|
499 apply simp |
|
500 |
|
501 oops |
|
502 |
|
503 lemma leq1_leq_case1: |
|
504 shows " \<lbrakk>r1 \<le>1 r2; r1 = r2 \<or> rerase r1 \<noteq> rerase r2; r2 \<le>1 r3; r2 = r3 \<or> rerase r2 \<noteq> rerase r3\<rbrakk> \<Longrightarrow> r1 = r3 \<or> rerase r1 \<noteq> rerase r3" |
|
505 apply(induct rule: leq1.induct) |
|
506 apply simp+ |
|
507 |
|
508 apply (metis rerase.elims rrexp.distinct(1) rrexp.distinct(11) rrexp.distinct(3) rrexp.distinct(5) rrexp.distinct(7) rrexp.distinct(9)) |
|
509 apply simp |
|
510 |
|
511 apply (metis leq1_trans1 rerase.simps(1) rerase.simps(5)) |
|
512 |
|
513 apply (metis leq1_trans1 rerase.simps(5) rerase_fuse) |
|
514 apply simp |
|
515 apply auto |
|
516 |
|
517 oops |
|
518 |
|
519 |
|
520 |
|
521 lemma scomp_rerase3: |
|
522 shows "r1 ~1 r2 \<Longrightarrow> s_complexity r1 = s_complexity r2" |
|
523 apply(induct rule: eq1.induct) |
|
524 apply simp+ |
|
525 done |
|
526 |
|
527 |
|
528 |
|
529 |
|
530 lemma scomp_rerase2: |
|
531 shows "rerase r1 = rerase r2 \<Longrightarrow> s_complexity r1 = s_complexity r2" |
|
532 using eq1rerase scomp_rerase3 by blast |
|
533 |
|
534 |
|
535 |
|
536 |
|
537 |
|
538 lemma scomp_rerase: |
|
539 shows "s_complexity r1 < s_complexity r2 \<Longrightarrow>rerase r1 \<noteq> rerase r2" |
|
540 by (metis nat_neq_iff scomp_rerase2) |
|
541 |
|
542 thm bsimp_ASEQ.simps |
|
543 |
|
544 lemma scomp_bsimpalts: |
|
545 shows "s_complexity (bsimp_ASEQ bs1 r1' r2') \<le> s_complexity (ASEQ bs1 r1' r2')" |
|
546 apply(case_tac "r1' = AZERO") |
|
547 apply simp |
|
548 apply(case_tac "r2' = AZERO") |
|
549 apply simp |
|
550 apply(case_tac "\<exists>bs2. r1' = AONE bs2") |
|
551 apply(erule exE) |
|
552 |
|
553 apply simp |
|
554 |
|
555 apply (metis le_SucI le_add2 plus_1_eq_Suc rerase_fuse scomp_rerase2) |
|
556 apply(subgoal_tac "bsimp_ASEQ bs1 r1' r2' = ASEQ bs1 r1' r2'") |
|
557 apply simp |
|
558 using bsimp_ASEQ1 by presburger |
|
559 |
|
560 |
|
561 lemma scompsize_aux: |
|
562 shows "s_complexity (AALTs bs (rs1 @ distinctWith rs2 eq1 (set rs1))) \<le> s_complexity (AALTs bs (rs1 @ rs2))" |
361 sorry |
563 sorry |
362 |
564 |
363 |
565 |
|
566 |
|
567 lemma scomp_size_reduction: |
|
568 shows "r1 \<le>1 r2 \<Longrightarrow> s_complexity r1 \<le> s_complexity r2" |
|
569 apply(induct rule: leq1.induct) |
|
570 apply simp+ |
|
571 apply (metis le_SucI le_add2 plus_1_eq_Suc rerase_fuse scomp_rerase2) |
|
572 apply simp+ |
|
573 |
|
574 apply (smt (verit) comp_apply dual_order.eq_iff map_eq_conv plus_1_eq_Suc rerase_fuse scomp_rerase2 trans_le_add2) |
|
575 apply simp+ |
|
576 |
|
577 apply (metis le_SucI le_add2 plus_1_eq_Suc rerase_fuse scomp_rerase2) |
|
578 |
|
579 |
|
580 |
|
581 apply (smt (verit, del_insts) add_mono_thms_linordered_semiring(1) dual_order.trans le_numeral_extra(4) plus_1_eq_Suc s_complexity.simps(5) scomp_bsimpalts) |
|
582 apply simp |
|
583 apply simp |
|
584 |
|
585 using scompsize_aux apply auto[1] |
|
586 apply(case_tac rs) |
|
587 apply simp |
|
588 apply(case_tac "list") |
|
589 apply auto |
|
590 by (metis eq_imp_le le_imp_less_Suc less_imp_le_nat rerase_fuse scomp_rerase2) |
|
591 |
|
592 |
|
593 |
|
594 |
|
595 |
|
596 |
|
597 |
|
598 |
|
599 lemma compl_rrewrite_down: |
|
600 shows "r1 \<le>1 r2 \<Longrightarrow>r1 = r2 \<or> s_complexity r1 < s_complexity r2" |
|
601 |
|
602 apply(induct rule: leq1.induct) |
|
603 apply simp |
|
604 apply simp |
|
605 apply simp |
|
606 apply (smt (verit) fuse.elims lessI less_Suc_eq plus_1_eq_Suc s_complexity.simps(2) s_complexity.simps(3) s_complexity.simps(4) s_complexity.simps(5) s_complexity.simps(6) s_complexity.simps(7)) |
|
607 apply simp |
|
608 sorry |
|
609 |
|
610 |
|
611 lemma compl_rrewrite_down1: |
|
612 shows "\<lbrakk>r1 \<le>1 r2; s_complexity r1 = s_complexity r2 \<rbrakk> \<Longrightarrow> r1 = r2" |
|
613 using compl_rrewrite_down nat_less_le by auto |
|
614 |
|
615 |
364 |
616 |
365 lemma leq1_less_or_equal: shows |
617 lemma leq1_less_or_equal: shows |
366 "r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2" |
618 "r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2" |
367 apply(induct rule: leq1.induct) |
619 using compl_rrewrite_down scomp_rerase by blast |
368 apply simp |
620 |
369 apply simp |
621 |
370 apply simp |
622 |
371 apply (simp add: rerase_fuse) |
623 |
372 apply simp |
624 |
373 apply simp |
625 |
374 using r_finite1 rerase_fuse apply force |
626 |
375 apply simp |
|
376 apply simp |
|
377 apply(case_tac "r1 = r2") |
|
378 apply simp |
|
379 apply simp |
|
380 |
|
381 using leq1_trans1 apply presburger |
|
382 apply simp |
|
383 apply simp |
|
384 apply simp |
|
385 apply simp |
|
386 apply simp |
|
387 apply simp |
|
388 |
|
389 using r_finite1 rerase_fuse apply auto[1] |
|
390 apply (smt (verit, best) BlexerSimp.bsimp_ASEQ0 BlexerSimp.bsimp_ASEQ2 bsimp_ASEQ.simps(1) bsimp_ASEQ1 leq1_trans1 rerase.simps(5) rerase_bsimp_ASEQ rerase_fuse rrexp.inject(2) rsimp_SEQ.simps(22)) |
|
391 sorry |
|
392 |
|
393 |
|
394 |
|
395 |
|
396 |
|
397 lemma arexpfiniteaux4: |
|
398 shows" |
|
399 \<lbrakk>\<And>x. \<lbrakk>x \<in> set rs; rerase (bsimp x) = rerase x\<rbrakk> \<Longrightarrow> bsimp x = x; |
|
400 rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs)\<rbrakk> |
|
401 \<Longrightarrow> bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) = AALTs bs1 rs" |
|
402 apply(induct rs) |
|
403 apply simp |
|
404 |
|
405 |
|
406 |
|
407 |
|
408 |
|
409 |
|
410 sorry |
|
411 |
627 |
412 |
628 |
413 |
629 |
414 |
630 |
415 lemma arexp_finite1: |
631 lemma arexp_finite1: |
416 shows "rerase (bsimp b) = rerase b \<Longrightarrow> bsimp b = b" |
632 shows "rerase (bsimp b) = rerase b \<Longrightarrow> bsimp b = b" |
417 apply(induct rule: bsimp.induct) |
633 using bsimp_leq1 leq1_less_or_equal by blast |
418 apply simp |
634 |
419 apply (smt (verit) arexpfiniteaux1 arexpfiniteaux2 arexpfiniteaux3 bsimp_ASEQ1 rerase.simps(5) rrexp.inject(2)) |
635 lemma bsimp_idem: |
420 apply simp |
636 shows "bsimp (bsimp r ) = bsimp r" |
421 |
637 using arexp_finite1 bsimp_rerase rsimp_idem by presburger |
422 using arexpfiniteaux4 apply blast |
638 |
423 apply simp+ |
639 |
424 done |
640 |
425 (* |
641 |
426 apply(induct b) |
|
427 apply simp+ |
|
428 apply(case_tac "bsimp b2 = AZERO") |
|
429 apply simp |
|
430 apply (case_tac "bsimp b1 = AZERO") |
|
431 apply simp |
|
432 apply(case_tac "\<exists>bs. bsimp b1 = AONE bs") |
|
433 using arexpfiniteaux1 apply blast |
|
434 apply simp |
|
435 apply(subgoal_tac "bsimp_ASEQ x1 (bsimp b1) (bsimp b2) = ASEQ x1 (bsimp b1) (bsimp b2)") |
|
436 apply simp |
|
437 using bsimp_ASEQ1 apply presburger |
|
438 apply simp |
|
439 |
|
440 sorry |
|
441 *) |
|
442 |
|
443 |
|
444 lemma bitcodes_unchanging2: |
|
445 assumes "bsimp a = b" |
|
446 and "a ~1 b" |
|
447 shows "a = b" |
|
448 using assms |
|
449 apply(induct rule: eq1.induct) |
|
450 apply simp |
|
451 apply simp |
|
452 apply simp |
|
453 |
|
454 apply auto |
|
455 |
|
456 sorry |
|
457 |
|
458 |
|
459 |
|
460 lemma bsimp_reduces: |
|
461 shows "bsimp r \<le>1 r" |
|
462 apply(induct rule: bsimp.induct) |
|
463 apply simp |
|
464 apply (simp add: leq1.intros(15)) |
|
465 apply simp |
|
466 apply(case_tac rs) |
|
467 apply simp |
|
468 |
|
469 apply (simp add: leq1.intros(13)) |
|
470 apply(case_tac list) |
|
471 apply simp |
|
472 |
|
473 |
|
474 sorry |
|
475 |
|
476 |
|
477 |
|
478 lemma bitcodes_unchanging: |
|
479 shows "\<lbrakk>bsimp a = b; rerase a = rerase b \<rbrakk> \<Longrightarrow> a = b" |
|
480 apply(induction a arbitrary: b) |
|
481 apply simp+ |
|
482 apply(case_tac "\<exists>bs. bsimp a1 = AONE bs") |
|
483 apply(erule exE) |
|
484 apply simp |
|
485 prefer 2 |
|
486 apply(case_tac "bsimp a1 = AZERO") |
|
487 apply simp |
|
488 apply simp |
|
489 apply (metis BlexerSimp.bsimp_ASEQ0 bsimp_ASEQ1 rerase.simps(1) rerase.simps(5) rrexp.distinct(5) rrexp.inject(2)) |
|
490 |
|
491 sorry |
|
492 |
|
493 |
|
494 lemma bagnostic_shows_bsimp_idem: |
|
495 assumes "bitcode_agnostic bsimp" |
|
496 and "rerase (bsimp a) = rsimp (rerase a)" |
|
497 and "rsimp r = rsimp (rsimp r)" |
|
498 shows "bsimp a = bsimp (bsimp a)" |
|
499 |
|
500 oops |
|
501 |
|
502 theorem bsimp_idem: |
|
503 shows "bsimp (bsimp a) = bsimp a" |
|
504 using bitcodes_unchanging bsimp_rerase rsimp_idem by auto |
|
505 |
|
506 |
|
507 unused_thms |
|
508 |
642 |
509 end |
643 end |