3501 shows "(\<exists>bsX rsX. r = AALTs bsX rsX) \<or> (\<exists>bsX rX1 rX2. r = ASEQ bsX rX1 rX2 \<and> bnullable rX1)" |
3501 shows "(\<exists>bsX rsX. r = AALTs bsX rsX) \<or> (\<exists>bsX rX1 rX2. r = ASEQ bsX rX1 rX2 \<and> bnullable rX1)" |
3502 using assms |
3502 using assms |
3503 apply(induct r) |
3503 apply(induct r) |
3504 apply(auto) |
3504 apply(auto) |
3505 by (metis arexp.distinct(25) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 nonalt.elims(3) nonalt.simps(2)) |
3505 by (metis arexp.distinct(25) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 nonalt.elims(3) nonalt.simps(2)) |
3506 |
|
3507 |
|
3508 lemma [simp]: |
|
3509 shows "size (fuse bs r) = size r" |
|
3510 by (induct r) (auto) |
|
3511 |
|
3512 fun AALTs_subs where |
|
3513 "AALTs_subs (AZERO) = {}" |
|
3514 | "AALTs_subs (AONE bs) = {AONE bs}" |
|
3515 | "AALTs_subs (ACHAR bs c) = {ACHAR bs c}" |
|
3516 | "AALTs_subs (ASEQ bs r1 r2) = {ASEQ bs r1 r2}" |
|
3517 | "AALTs_subs (ASTAR bs r) = {ASTAR bs r}" |
|
3518 | "AALTs_subs (AALTs bs []) = {}" |
|
3519 | "AALTs_subs (AALTs bs (r#rs)) = AALTs_subs (fuse bs r) \<union> AALTs_subs (AALTs bs rs)" |
|
3520 |
|
3521 lemma nonalt_10: |
|
3522 assumes "nonalt r" "r \<noteq> AZERO" |
|
3523 shows "r \<in> AALTs_subs r" |
|
3524 using assms |
|
3525 apply(induct r) |
|
3526 apply(auto) |
|
3527 done |
|
3528 |
|
3529 lemma flt_fuse: |
|
3530 shows "flts (map (fuse bs) rs) = map (fuse bs) (flts rs)" |
|
3531 apply(induct rs arbitrary: bs rule: flts.induct) |
|
3532 apply(auto) |
|
3533 by (simp add: fuse_append) |
|
3534 |
|
3535 lemma AALTs_subs_fuse: |
|
3536 shows "AALTs_subs (fuse bs r) = (fuse bs) ` (AALTs_subs r)" |
|
3537 apply(induct r arbitrary: bs rule: AALTs_subs.induct) |
|
3538 apply(auto) |
|
3539 apply (simp add: fuse_append) |
|
3540 apply blast |
|
3541 by (simp add: fuse_append) |
|
3542 |
|
3543 lemma AALTs_subs_fuse2: |
|
3544 shows "AALTs_subs (AALTs bs rs) = AALTs_subs (AALTs [] (map (fuse bs) rs))" |
|
3545 apply(induct rs arbitrary: bs) |
|
3546 apply(auto) |
|
3547 apply (auto simp add: fuse_empty) |
|
3548 done |
|
3549 |
|
3550 lemma fuse_map: |
|
3551 shows "map (fuse (bs1 @ bs2)) rs = map (fuse bs1) (map (fuse bs2) rs)" |
|
3552 apply(induct rs) |
|
3553 apply(auto) |
|
3554 using fuse_append by blast |
|
3555 |
|
3556 |
|
3557 |
|
3558 lemma contains59_2: |
|
3559 assumes "AALTs bs rs >> bs2" |
|
3560 shows "\<exists>r\<in>AALTs_subs (AALTs bs rs). r >> bs2" |
|
3561 using assms |
|
3562 apply(induct rs arbitrary: bs bs2 taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct) |
|
3563 apply(case_tac x) |
|
3564 apply(auto) |
|
3565 using contains59 apply force |
|
3566 apply(erule contains.cases) |
|
3567 apply(auto) |
|
3568 apply(case_tac "r = AZERO") |
|
3569 apply(simp) |
|
3570 apply (metis bsimp_AALTs.simps(1) contains61 empty_iff empty_set) |
|
3571 apply(case_tac "nonalt r") |
|
3572 apply (metis UnCI bsimp_AALTs.simps(1) contains0 contains61 empty_iff empty_set nn11a nonalt_10) |
|
3573 apply(subgoal_tac "\<exists>bsX rsX. r = AALTs bsX rsX") |
|
3574 prefer 2 |
|
3575 using bbbbs1 apply blast |
|
3576 apply(auto) |
|
3577 apply (metis UnCI contains0 fuse.simps(4) less_add_Suc1) |
|
3578 apply(drule_tac x="rs" in spec) |
|
3579 apply(drule mp) |
|
3580 apply(simp add: asize0) |
|
3581 apply(drule_tac x="bsa" in spec) |
|
3582 apply(drule_tac x="bsa @ bs1" in spec) |
|
3583 apply(auto) |
|
3584 done |
|
3585 |
|
3586 lemma TEMPLATE_contains61a: |
|
3587 assumes "\<exists>r \<in> set rs. (fuse bs r) >> bs2" |
|
3588 shows "bsimp_AALTs bs rs >> bs2" |
|
3589 using assms |
|
3590 apply(induct rs arbitrary: bs2 bs) |
|
3591 apply(auto) |
|
3592 apply (metis bsimp_AALTs.elims contains60 list.distinct(1) list.inject list.set_intros(1)) |
|
3593 by (metis append_Cons append_Nil contains50 f_cont2) |
|
3594 |
|
3595 |
|
3596 |
|
3597 |
|
3598 lemma H1: |
|
3599 assumes "r >> bs2" "r \<in> AALTs_subs a" |
|
3600 shows "a >> bs2" |
|
3601 using assms |
|
3602 apply(induct a arbitrary: r bs2 rule: AALTs_subs.induct) |
|
3603 apply(auto) |
|
3604 apply (simp add: contains60) |
|
3605 by (simp add: contains59 contains60) |
|
3606 |
|
3607 lemma H3: |
|
3608 assumes "a >> bs" |
|
3609 shows "\<exists>r \<in> AALTs_subs a. r >> bs" |
|
3610 using assms |
|
3611 apply(induct a bs) |
|
3612 apply(auto intro: contains.intros) |
|
3613 using contains.intros(4) contains59_2 by fastforce |
|
3614 |
|
3615 lemma H4: |
|
3616 shows "AALTs_subs (AALTs bs rs1) \<subseteq> AALTs_subs (AALTs bs (rs1 @ rs2))" |
|
3617 apply(induct rs1) |
|
3618 apply(auto) |
|
3619 done |
|
3620 |
|
3621 lemma H5: |
|
3622 shows "AALTs_subs (AALTs bs rs2) \<subseteq> AALTs_subs (AALTs bs (rs1 @ rs2))" |
|
3623 apply(induct rs1) |
|
3624 apply(auto) |
|
3625 done |
|
3626 |
|
3627 lemma H7: |
|
3628 shows "AALTs_subs (AALTs bs (rs1 @ rs2)) = AALTs_subs (AALTs bs rs1) \<union> AALTs_subs (AALTs bs rs2)" |
|
3629 apply(induct rs1) |
|
3630 apply(auto) |
|
3631 done |
|
3632 |
|
3633 lemma H6: |
|
3634 shows "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)" |
|
3635 apply(induct rs arbitrary: bs rule: flts.induct) |
|
3636 apply(auto) |
|
3637 apply (metis AALTs_subs_fuse2 H7 Un_iff fuse_map) |
|
3638 apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map) |
|
3639 by (simp add: H7) |
|
3640 |
|
3641 |
|
3642 lemma H2: |
|
3643 assumes "r >> bs2" "r \<in> AALTs_subs (AALTs bs rs)" |
|
3644 shows "r \<in> AALTs_subs (AALTs bs (flts rs))" |
|
3645 using assms |
|
3646 apply(induct rs arbitrary: r bs bs2 rule: flts.induct) |
|
3647 apply(auto) |
|
3648 apply (metis AALTs_subs_fuse2 H4 fuse_map in_mono) |
|
3649 using H7 by blast |
|
3650 |
|
3651 lemma H00: |
|
3652 shows " (\<Union> (AALTs_subs ` (set (map (bder c o fuse bs) rs)))) \<subseteq> ((bder c) ` (AALTs_subs (AALTs bs rs)))" |
|
3653 apply(induct rs arbitrary: bs c) |
|
3654 apply(auto simp add: image_def) |
|
3655 |
|
3656 |
|
3657 |
|
3658 lemma contains61a_2: |
|
3659 assumes "\<exists>r\<in>AALTs_subs (AALTs bs rs). r >> bs2" |
|
3660 shows "bsimp_AALTs bs rs >> bs2" |
|
3661 using assms |
|
3662 apply(induct rs arbitrary: bs2 bs) |
|
3663 apply(auto) |
|
3664 apply (simp add: H1 TEMPLATE_contains61a) |
|
3665 by (metis append_Cons append_Nil contains50 f_cont2) |
|
3666 |
3506 |
3667 |
3507 |
3668 lemma in2: |
3508 lemma in2: |
3669 assumes "bder c r >> bs2" and |
3509 assumes "bder c r >> bs2" and |
3670 "AALTs bsX rsX = bsimp r" and |
3510 "AALTs bsX rsX = bsimp r" and |
3671 "XX \<in> set rsX" "nonnested (bsimp r)" |
3511 "XX \<in> set rsX" "nonnested (bsimp r)" |
3672 shows "bder c (fuse bsX XX) >> bs2" |
3512 shows "bder c (fuse bsX XX) >> bs2" |
3673 using assms |
3513 |
3674 apply(induct r arbitrary: c bs2 bsX rsX XX) |
3514 sorry |
3675 apply(auto) |
|
3676 prefer 2 |
|
3677 oops |
|
3678 |
3515 |
3679 |
3516 |
3680 lemma |
3517 lemma |
3681 assumes "bder c a >> bs" |
3518 assumes "bder c a >> bs" |
3682 shows "bder c (bsimp a) >> bs" |
3519 shows "bder c (bsimp a) >> bs" |