3399 assumes "nullable (erase a)" |
3384 assumes "nullable (erase a)" |
3400 shows "FC a [] (mkeps (erase a)) = FC (bsimp a) [] (mkeps (erase (bsimp a)))" |
3385 shows "FC a [] (mkeps (erase a)) = FC (bsimp a) [] (mkeps (erase (bsimp a)))" |
3401 unfolding FC_def |
3386 unfolding FC_def |
3402 using L0 assms bnullable_correctness by auto |
3387 using L0 assms bnullable_correctness by auto |
3403 |
3388 |
3404 |
|
3405 lemma FC6: |
|
3406 assumes "nullable (erase (bders a s))" |
|
3407 shows "FC (bsimp a) s (mkeps (erase (bders (bsimp a) s))) = FC a s (mkeps (erase (bders a s)))" |
|
3408 apply(subst (2) FC4) |
|
3409 using assms mkeps_nullable apply auto[1] |
|
3410 apply(subst FC_nullable2) |
|
3411 using assms bnullable_correctness apply blast |
|
3412 oops |
|
3413 (* |
|
3414 lemma FC_bnullable: |
|
3415 assumes "bnullable (bders r s)" |
|
3416 shows "FC r s (mkeps (erase r)) = FC (bsimp r) s (mkeps (erase (bsimp r)))" |
|
3417 using assms |
|
3418 unfolding FC_def |
|
3419 using L0 L0a bder_retrieve L02_bders L04 |
|
3420 |
|
3421 apply(induct s arbitrary: r) |
|
3422 apply(simp add: FC_id) |
|
3423 apply (simp add: L0 assms) |
|
3424 apply(simp add: bders_append) |
|
3425 apply(drule_tac x="bder a r" in meta_spec) |
|
3426 apply(drule meta_mp) |
|
3427 apply(simp) |
|
3428 |
|
3429 apply(subst bder_retrieve[symmetric]) |
|
3430 apply(simp) |
|
3431 *) |
|
3432 |
|
3433 |
|
3434 lemma FC_bnullable: |
|
3435 assumes "bnullable (bders r s)" |
|
3436 shows "FC r s (mkeps (ders s (erase r))) = FC (bsimp r) s (mkeps (ders s (erase (bsimp r))))" |
|
3437 unfolding FC_def |
|
3438 oops |
|
3439 |
|
3440 lemma AA0: |
|
3441 assumes "bnullable (bders r s)" |
|
3442 assumes "bders r s >> FC r s (mkeps (erase (bders r s)))" |
|
3443 shows "bders (bsimp r) s >> FC (bsimp r) s (mkeps (erase (bders (bsimp r) s)))" |
|
3444 using assms |
|
3445 apply(subst (asm) FC_bders_iff) |
|
3446 apply(simp) |
|
3447 using bnullable_correctness mkeps_nullable apply fastforce |
|
3448 apply(subst FC_bders_iff) |
|
3449 apply(simp) |
|
3450 apply (metis LLLL(1) bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness) |
|
3451 apply(simp add: PPP1_eq) |
|
3452 unfolding FC_def |
|
3453 find_theorems "retrieve (bsimp _) _" |
|
3454 using contains7b |
|
3455 oops |
|
3456 |
|
3457 |
|
3458 lemma AA1: |
|
3459 |
|
3460 assumes "\<Turnstile> v : der c (erase r)" "\<Turnstile> v : der c (erase (bsimp r))" |
|
3461 assumes "bder c r >> FC r [c] v" |
|
3462 shows "bder c (bsimp r) >> FC (bsimp r) [c] v" |
|
3463 using assms |
|
3464 apply(subst (asm) FC_bder_iff) |
|
3465 apply(rule assms) |
|
3466 apply(subst FC_bder_iff) |
|
3467 apply(rule assms) |
|
3468 apply(simp add: PPP1_eq) |
|
3469 unfolding FC_def |
|
3470 find_theorems "retrieve (bsimp _) _" |
|
3471 using contains7b |
|
3472 oops |
|
3473 |
|
3474 |
|
3475 lemma PX_bder_simp_iff: |
|
3476 assumes "\<Turnstile> v: ders (s1 @ s2) r" |
|
3477 shows "bders (bsimp (bders (intern r) s1)) s2 >> code (PV r (s1 @ s2) v) \<longleftrightarrow> |
|
3478 bders (intern r) s1 >> code (PV r (s1 @ s2) v)" |
|
3479 using assms |
|
3480 apply(induct s2 arbitrary: r s1 v) |
|
3481 apply(simp) |
|
3482 apply (simp add: PV3 contains55) |
|
3483 apply(drule_tac x="r" in meta_spec) |
|
3484 apply(drule_tac x="s1 @ [a]" in meta_spec) |
|
3485 apply(drule_tac x="v" in meta_spec) |
|
3486 apply(simp) |
|
3487 apply(simp add: bders_append) |
|
3488 apply(subst (asm) PV_bder_IFF) |
|
3489 oops |
|
3490 |
3389 |
3491 lemma in1: |
3390 lemma in1: |
3492 assumes "AALTs bsX rsX \<in> set rs" |
3391 assumes "AALTs bsX rsX \<in> set rs" |
3493 shows "\<forall>r \<in> set rsX. fuse bsX r \<in> set (flts rs)" |
3392 shows "\<forall>r \<in> set rsX. fuse bsX r \<in> set (flts rs)" |
3494 using assms |
3393 using assms |
3727 apply(induct rs arbitrary: bs2 bs) |
3617 apply(induct rs arbitrary: bs2 bs) |
3728 apply(auto) |
3618 apply(auto) |
3729 apply (simp add: H1 TEMPLATE_contains61a) |
3619 apply (simp add: H1 TEMPLATE_contains61a) |
3730 by (metis append_Cons append_Nil contains50 f_cont2) |
3620 by (metis append_Cons append_Nil contains50 f_cont2) |
3731 |
3621 |
3732 lemma HK1: |
|
3733 assumes "r \<in> AALTs_subs a" |
|
3734 shows "bsimp r \<in> AALTs_subs (bsimp a)" |
|
3735 using assms |
|
3736 apply(induct a arbitrary: r) |
|
3737 apply(auto) |
|
3738 apply(case_tac "a1 = AZERO") |
|
3739 apply(simp) |
|
3740 oops |
|
3741 |
|
3742 lemma contains_equiv_def2: |
3622 lemma contains_equiv_def2: |
3743 shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>(\<Union> (AALTs_subs ` set as)). a >> bs1)" |
3623 shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>(\<Union> (AALTs_subs ` set as)). a >> bs1)" |
3744 by (metis H1 H3 UN_E UN_I contains0 contains49 contains59 contains60) |
3624 by (metis H1 H3 UN_E UN_I contains0 contains49 contains59 contains60) |
3745 |
3625 |
3746 lemma contains_equiv_def: |
3626 lemma contains_equiv_def: |
3747 shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)" |
3627 shows "(AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)" |
3748 by (meson contains0 contains49 contains59 contains60) |
3628 by (meson contains0 contains49 contains59 contains60) |
3749 |
3629 |
3750 lemma derc_alt00: |
3630 lemma map_fuse2: |
3751 assumes " bder c a >> bs" and "bder c (bsimp a) >> bs" |
3631 shows "map (bder c) (map (fuse bs) as) = map (fuse bs) (map (bder c) as)" |
3752 shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs" |
3632 by (simp add: map_bder_fuse) |
3753 using assms |
3633 |
3754 apply - |
3634 lemma map_fuse3: |
|
3635 shows "map (\<lambda>a. bders a s) (map (fuse bs) as) = map (fuse bs) (map (\<lambda>a. bders a s) as)" |
|
3636 apply(induct s arbitrary: bs as rule: rev_induct) |
|
3637 apply(auto simp add: bders_append map_fuse2) |
|
3638 using bder_fuse by blast |
|
3639 |
|
3640 lemma bders_AALTs: |
|
3641 shows "bders (AALTs bs2 as) s = AALTs bs2 (map (\<lambda>a. bders a s) as)" |
|
3642 apply(induct s arbitrary: bs2 as rule: rev_induct) |
|
3643 apply(auto simp add: bders_append) |
|
3644 done |
|
3645 |
|
3646 lemma bders_AALTs_contains: |
|
3647 shows "bders (AALTs bs2 as) s >> bs2 @ bs \<longleftrightarrow> |
|
3648 AALTs bs2 (map (\<lambda>a. bders a s) as) >> bs2 @ bs" |
|
3649 apply(induct s arbitrary: bs bs2 as) |
|
3650 apply(auto)[1] |
|
3651 apply(simp) |
|
3652 by (smt comp_apply map_eq_conv) |
|
3653 |
|
3654 |
|
3655 lemma derc_alt00_Urb: |
|
3656 shows "bder c (bsimp_AALTs bs2 (flts [bsimp a])) >> bs2 @ bs \<longleftrightarrow> |
|
3657 fuse bs2 (bder c (bsimp a)) >> bs2 @ bs" |
3755 apply(case_tac "bsimp a") |
3658 apply(case_tac "bsimp a") |
3756 prefer 6 |
3659 apply(auto) |
3757 apply(simp)+ |
3660 apply(subst (asm) bder_bsimp_AALTs) |
3758 apply(subst bder_bsimp_AALTs) |
3661 apply(subst (asm) map_fuse2) |
3759 by (metis append_Nil contains51c map_bder_fuse map_map) |
3662 using contains60 contains61 contains63 apply blast |
3760 |
3663 by (metis bder_bsimp_AALTs contains51c map_bder_fuse map_map) |
3761 lemma derc_alt01: |
3664 |
3762 shows "\<And>a list1 list2. |
3665 lemma ders_alt00_Urb: |
3763 \<lbrakk> bder c (bsimp a) >> bs ; |
3666 shows "bders (bsimp_AALTs bs2 (flts [bsimp a])) s >> bs2 @ bs \<longleftrightarrow> |
3764 bder c a >> bs; as = [a] @ list2; flts (map bsimp list1) = []; |
3667 fuse bs2 (bders (bsimp a) s) >> bs2 @ bs" |
3765 flts (map bsimp list2) \<noteq> []\<rbrakk> |
3668 apply(case_tac "bsimp a") |
3766 \<Longrightarrow> bder c (bsimp_AALTs [] (flts [bsimp a] @ flts (map bsimp list2))) >> bs" |
3669 apply (simp add: bders_AZERO(1)) |
3767 using bder_bsimp_AALTs contains51b derc_alt00 f_cont2 by fastforce |
3670 using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(4) apply presburger |
3768 |
3671 using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(5) apply presburger |
3769 lemma derc_alt10: |
3672 using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(6) apply presburger |
3770 shows "\<And>a list1 list2. |
3673 prefer 2 |
3771 \<lbrakk> a \<in> set as; bder c (bsimp a) >> bs; |
3674 using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(7) apply presburger |
3772 bder c a >> bs; as = list1 @ [a] @ list2; flts (map bsimp list1) \<noteq> []; |
3675 apply(auto simp add: bders_bsimp_AALTs) |
3773 flts(map bsimp list2) = []\<rbrakk> |
3676 apply(drule contains61) |
3774 \<Longrightarrow> bder c (bsimp_AALTs [] |
3677 apply(auto simp add: bders_AALTs) |
3775 (flts (map bsimp list1) @ |
3678 apply(rule contains63) |
3776 flts (map bsimp [a]) @ flts (map bsimp list2))) >> bs" |
3679 apply(rule contains60) |
3777 apply(subst bder_bsimp_AALTs) |
3680 apply(auto) |
3778 apply simp |
3681 using bders_fuse apply auto[1] |
3779 using bder_bsimp_AALTs contains50 derc_alt00 f_cont2 by fastforce |
3682 by (metis contains51c map_fuse3 map_map) |
3780 |
3683 |
3781 |
3684 lemma derc_alt00_Urb2a: |
3782 lemma derc_alt: |
3685 shows "bder c (bsimp_AALTs bs2 (flts [bsimp a])) >> bs2 @ bs \<longleftrightarrow> |
3783 assumes "bder c (AALTs [] as) >> bs" |
3686 bder c (bsimp a) >> bs" |
3784 and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))" |
3687 using contains0 contains49 derc_alt00_Urb by blast |
3785 shows "bder c (bsimp (AALTs [] as)) >> bs" |
3688 |
3786 using assms |
3689 |
3787 apply - |
3690 lemma derc_alt00_Urb2: |
3788 using contains_equiv_def |
3691 assumes "fuse bs2 (bder c (bsimp a)) >> bs2 @ bs" "a \<in> set as" |
3789 apply - |
3692 shows "bder c (bsimp_AALTs bs2 (flts (map bsimp as))) >> bs2 @ bs" |
3790 apply(simp) |
3693 using assms |
3791 apply(drule_tac x="[]" in meta_spec) |
|
3792 apply(drule_tac x="map (bder c) as" in meta_spec) |
|
3793 apply(drule_tac x="bs" in meta_spec) |
|
3794 |
|
3795 apply(simp) |
|
3796 apply(erule bexE) |
|
3797 apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2") |
3694 apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2") |
3798 prefer 2 |
3695 prefer 2 |
3799 using split_list_last apply fastforce |
3696 using split_list_last apply fastforce |
3800 apply(erule exE)+ |
3697 apply(erule exE)+ |
3801 apply(rule_tac t="as" and s="list1@[a]@list2" in subst) |
3698 apply(simp add: flts_append del: append.simps) |
3802 apply simp |
3699 using bder_bsimp_AALTs contains50 contains51b derc_alt00_Urb by auto |
3803 (*find_theorems "map _ _ = _"*) |
3700 |
3804 apply(subst map_append)+ |
3701 lemma ders_alt00_Urb2: |
3805 apply(subst k00)+ |
3702 assumes "fuse bs2 (bders (bsimp a) s) >> bs2 @ bs" "a \<in> set as" |
3806 apply(case_tac "flts (map bsimp list1) = Nil") |
3703 shows "bders (bsimp_AALTs bs2 (flts (map bsimp as))) s >> bs2 @ bs" |
3807 apply(case_tac "flts (map bsimp list2) = Nil") |
3704 using assms |
3808 apply simp |
3705 apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2") |
3809 using derc_alt00 apply blast |
3706 prefer 2 |
3810 apply simp |
3707 using split_list_last apply fastforce |
3811 using derc_alt01 apply blast |
3708 apply(erule exE)+ |
3812 apply(case_tac "flts (map bsimp list2) = Nil") |
3709 apply(simp add: flts_append del: append.simps) |
3813 using derc_alt10 apply blast |
3710 apply(simp add: bders_bsimp_AALTs) |
3814 by (smt bder_bsimp_AALTs contains50 contains51b derc_alt00 f_cont2 list.simps(8) list.simps(9) map_append) |
3711 apply(rule contains50) |
3815 |
3712 apply(rule contains51b) |
3816 |
3713 using bders_bsimp_AALTs ders_alt00_Urb by auto |
|
3714 |
|
3715 |
3817 lemma derc_alt2: |
3716 lemma derc_alt2: |
3818 assumes "bder c (AALTs bs2 as) >> bs2 @ bs" |
3717 assumes "bder c (AALTs bs2 as) >> bs2 @ bs" |
3819 and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))" |
3718 and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))" |
3820 shows "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs" |
3719 shows "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs" |
3821 proof - |
3720 using assms |
3822 from assms |
3721 apply - |
3823 have "bder c (AALTs [] as) >> bs" |
3722 apply(simp) |
3824 by (metis bder.simps(4) contains_equiv_def self_append_conv2) |
3723 apply(subst (asm) contains_equiv_def) |
3825 then have "bder c (bsimp (AALTs [] as)) >> bs" |
3724 apply(simp) |
3826 using assms(2) derc_alt by blast |
3725 apply(erule bexE) |
3827 then show "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs" |
3726 using contains0 derc_alt00_Urb2 by blast |
3828 by (metis bder_fuse bsimp_fuse_AALTs contains0) |
3727 |
3829 qed |
3728 |
3830 |
3729 |
3831 lemma inA: |
3730 lemma ders_alt2: |
3832 assumes "x \<in> set rs" "bder c (bsimp x) >> bs" |
3731 assumes "bders (AALTs bs2 as) s >> bs2 @ bs" |
3833 shows "\<exists>y. y \<in> set (flts (map bsimp rs))" |
3732 and "\<forall>a \<in> set as. ((bders a s >> bs) \<longrightarrow> (bders (bsimp a) s >> bs))" |
3834 using assms |
3733 shows "bders (bsimp (AALTs bs2 as)) s >> bs2 @ bs" |
3835 apply(induct rs arbitrary: x c bs) |
3734 using assms |
3836 apply(auto) |
3735 apply - |
3837 apply(case_tac "bsimp a = AZERO") |
3736 apply(simp add: bders_AALTs) |
3838 apply (metis append.left_neutral bder.simps(1) bsimp_AALTs.simps(1) contains61 in_set_conv_decomp neq_Nil_conv) |
3737 thm contains_equiv_def |
3839 apply (metis bsimp_AALTs.simps(1) flts4 good1 list.set_intros(1) neq_Nil_conv) |
3738 apply(subst (asm) contains_equiv_def) |
3840 by (metis Nil_is_append_conv k0 list.set_intros(1) neq_Nil_conv) |
3739 apply(simp) |
3841 |
3740 apply(erule bexE) |
3842 |
3741 using contains0 ders_alt00_Urb2 by blast |
3843 lemma inB: |
3742 |
3844 assumes "a \<noteq> AZERO" "good a" |
3743 |
3845 shows "AALTs_subs a \<noteq> {}" |
3744 |
3846 using assms |
|
3847 apply(induct a) |
|
3848 apply(auto) |
|
3849 apply(erule good.elims) |
|
3850 apply(auto) |
|
3851 by (metis empty_iff good.simps(1) good_fuse nn11a nonalt_10) |
|
3852 |
3745 |
3853 lemma bder_simp_contains: |
3746 lemma bder_simp_contains: |
3854 assumes "bder c a >> bs" |
3747 assumes "bder c a >> bs" |
3855 shows "bder c (bsimp a) >> bs" |
3748 shows "bder c (bsimp a) >> bs" |
3856 using assms |
3749 using assms |
3928 using contains59 f_cont1 apply blast |
3821 using contains59 f_cont1 apply blast |
3929 apply(auto) |
3822 apply(auto) |
3930 apply(rule derc_alt2[simplified]) |
3823 apply(rule derc_alt2[simplified]) |
3931 apply(simp) |
3824 apply(simp) |
3932 by blast |
3825 by blast |
3933 |
3826 |
3934 lemma CONTAINS1: |
3827 |
3935 assumes "a >> bs" |
3828 |
3936 shows "a >>2 bs" |
3829 lemma bder_simp_containsA: |
3937 using assms |
3830 assumes "bder c a >> bs" |
3938 apply(induct a bs) |
3831 shows "bsimp (bder c (bsimp a)) >> bs" |
3939 apply(auto intro: contains2.intros) |
3832 using assms |
3940 done |
3833 by (simp add: bder_simp_contains contains55) |
3941 |
3834 |
3942 lemma CONTAINS2: |
3835 lemma bder_simp_containsB: |
3943 assumes "a >>2 bs" |
3836 assumes "bsimp (bder c a) >> bs" |
3944 shows "a >> bs" |
3837 shows "bder c (bsimp a) >> bs" |
3945 using assms |
3838 using assms |
3946 apply(induct a bs) |
3839 by (simp add: PPP1_eq bder_simp_contains) |
3947 apply(auto intro: contains.intros) |
3840 |
3948 using contains55 by auto |
3841 lemma bder_simp_contains_IFF: |
3949 |
3842 assumes "good a" |
3950 lemma CONTAINS2_IFF: |
3843 shows "bsimp (bder c a) >> bs \<longleftrightarrow> bder c (bsimp a) >> bs" |
3951 shows "a >> bs \<longleftrightarrow> a >>2 bs" |
3844 using assms |
3952 using CONTAINS1 CONTAINS2 by blast |
3845 by (simp add: PPP1_eq test2) |
|
3846 |
|
3847 |
|
3848 lemma ders_seq: |
|
3849 assumes "bders (ASEQ bs a1 a2) s >> bs @ bs2" |
|
3850 and "\<And>s bs. bders a1 s >> bs \<Longrightarrow> bders (bsimp a1) s >> bs" |
|
3851 "\<And>s bs. bders a2 s >> bs \<Longrightarrow> bders (bsimp a2) s >> bs" |
|
3852 shows "bders (ASEQ bs (bsimp a1) (bsimp a2)) s >> bs @ bs2" |
|
3853 using assms(1) |
|
3854 apply(induct s arbitrary: a1 a2 bs bs2 rule: rev_induct) |
|
3855 apply(auto)[1] |
|
3856 thm CT1_SEQ PPP1_eq |
|
3857 apply (metis CT1_SEQ PPP1_eq) |
|
3858 apply(auto simp add: bders_append) |
|
3859 apply(drule bder_simp_contains) |
|
3860 oops |
|
3861 |
|
3862 |
|
3863 lemma bders_simp_contains: |
|
3864 assumes "bders a s >> bs" |
|
3865 shows "bders (bsimp a) s >> bs" |
|
3866 using assms |
|
3867 apply(induct a arbitrary: s bs) |
|
3868 apply(auto elim: contains.cases)[4] |
|
3869 prefer 2 |
|
3870 apply(subgoal_tac "\<exists>bsX. bs = x1 @ bsX") |
|
3871 prefer 2 |
|
3872 apply (metis bders_AALTs contains59 f_cont1) |
|
3873 apply(clarify) |
|
3874 apply(rule ders_alt2) |
|
3875 apply(assumption) |
|
3876 apply(auto)[1] |
|
3877 prefer 2 |
|
3878 apply simp |
|
3879 (* SEQ case *) |
|
3880 apply(case_tac "bsimp a1 = AZERO") |
|
3881 apply(simp) |
|
3882 apply (metis LLLL(1) bders_AZERO(1) bsimp.simps(1) bsimp.simps(3) bsimp_ASEQ.simps(1) contains55 ders_correctness erase_bders good.simps(1) good1a xxx_bder2) |
|
3883 apply(case_tac "bsimp a2 = AZERO") |
|
3884 apply(simp) |
|
3885 apply (metis LLLL(1) bders_AZERO(1) bsimp.simps(1) bsimp.simps(3) bsimp_ASEQ0 contains55 ders_correctness erase_bders good.simps(1) good1a xxx_bder2) |
|
3886 apply(case_tac "\<exists>bsX. bsimp a1 = AONE bsX") |
|
3887 apply(auto) |
|
3888 apply(subst bsimp_ASEQ2) |
|
3889 apply(case_tac s) |
|
3890 apply(simp) |
|
3891 apply (metis b1 bsimp.simps(1) contains55) |
|
3892 apply(simp) |
|
3893 apply(subgoal_tac "bnullable a1") |
|
3894 prefer 2 |
|
3895 using b3 apply fastforce |
|
3896 apply(auto) |
|
3897 apply(subst (asm) bders_AALTs) |
|
3898 apply(erule contains.cases) |
|
3899 apply(auto) |
|
3900 prefer 2 |
|
3901 apply(erule contains.cases) |
|
3902 apply(auto) |
|
3903 apply(simp add: fuse_append) |
|
3904 apply(simp add: bder_fuse bders_fuse) |
|
3905 apply (metis bders.simps(2) bmkeps.simps(1) bmkeps_simp contains0 contains49 f_cont1) |
|
3906 using contains_equiv_def apply auto[1] |
|
3907 apply(simp add: bder_fuse bders_fuse fuse_append) |
|
3908 apply(rule contains0) |
|
3909 oops |
|
3910 |
|
3911 |
|
3912 lemma T0: |
|
3913 assumes "s = []" |
|
3914 shows "bders (bsimp r) s >> bs \<longleftrightarrow> bders r s >> bs" |
|
3915 using assms |
|
3916 by (simp add: PPP1_eq test2) |
|
3917 |
|
3918 lemma T1: |
|
3919 assumes "s = [a]" "bders r s >> bs" |
|
3920 shows "bders (bsimp r) s >> bs" |
|
3921 using assms |
|
3922 apply(simp) |
|
3923 by (simp add: bder_simp_contains) |
|
3924 |
|
3925 lemma TX: |
|
3926 assumes "\<Turnstile> v : ders s (erase r)" "\<Turnstile> v : ders s (erase (bsimp r))" |
|
3927 shows "bders r s >> FC r s v \<longleftrightarrow> bders (bsimp r) s >> FC (bsimp r) s v" |
|
3928 using FC_def contains7b |
|
3929 using assms by metis |
|
3930 |
|
3931 lemma mkeps1: |
|
3932 assumes "s \<in> L (erase r)" |
|
3933 shows "\<Turnstile> mkeps (ders s (erase r)) : ders s (erase r)" |
|
3934 using assms |
|
3935 by (meson lexer_correct_None lexer_flex mkeps_nullable) |
|
3936 |
|
3937 lemma mkeps2: |
|
3938 assumes "s \<in> L (erase r)" |
|
3939 shows "\<Turnstile> mkeps (ders s (erase (bsimp r))) : ders s (erase (bsimp r))" |
|
3940 using assms |
|
3941 by (metis LLLL(1) lexer_correct_None lexer_flex mkeps_nullable) |
|
3942 |
|
3943 thm FC_def FE_def PX_def PV_def |
|
3944 |
|
3945 |
|
3946 lemma TX2: |
|
3947 assumes "s \<in> L (erase r)" |
|
3948 shows "bders r s >> FE r s \<longleftrightarrow> bders (bsimp r) s >> FE (bsimp r) s" |
|
3949 using assms |
|
3950 by (simp add: FE_def contains7b mkeps1 mkeps2) |
|
3951 |
|
3952 lemma TX3: |
|
3953 assumes "s \<in> L (erase r)" |
|
3954 shows "bders r s >> FE r s \<longleftrightarrow> bders (bsimp r) s >> FE (bders (bsimp r) s) []" |
|
3955 using assms |
|
3956 by (metis FE_PX FE_def L07 LLLL(1) PX_id TX2) |
|
3957 |
|
3958 find_theorems "FE _ _ = _" |
|
3959 find_theorems "FC _ _ _ = _" |
|
3960 find_theorems "(bder _ _ >> _ _ _ _) = _" |
|
3961 |
|
3962 |
|
3963 (* HERE *) |
|
3964 |
|
3965 lemma PX: |
|
3966 assumes "s \<in> L r" |
|
3967 shows "bders (intern r) s >> code (PX r s) \<Longrightarrow> bders (bsimp (intern r)) s >> code (PX r s)" |
|
3968 |
|
3969 using FC_def contains7b |
|
3970 using assms by me tis |
|
3971 |
|
3972 |
|
3973 |
|
3974 |
|
3975 apply(simp) |
|
3976 (*using FC_bders_iff2[of _ _ "[b]", simplified]*) |
|
3977 apply(subst (asm) FC_bders_iff2[of _ _ "[b]", simplified]) |
|
3978 apply(simp) |
|
3979 apply(subst (asm) FC_bder_iff) |
|
3980 apply(simp) |
|
3981 apply(drule bder_simp_contains) |
|
3982 using FC_bder_iff FC_bders_iff2 FC_bders_iff |
|
3983 apply(subst (asm) FC_bder_iff[symmetric]) |
|
3984 apply(subst FC_bder_iff) |
|
3985 using FC_bder_iff |
|
3986 |
|
3987 |
|
3988 apply (simp add: bder_simp_contains) |
|
3989 |
|
3990 lemma bder_simp_contains_IFF2: |
|
3991 assumes "bders r s >> bs" |
|
3992 shows "" |
|
3993 using assms |
|
3994 apply(induct s arbitrary: r bs rule: rev_induct) |
|
3995 apply(simp) |
|
3996 apply (simp add: contains55) |
|
3997 apply (simp add: bders_append bders_simp_append) |
|
3998 apply (simp add: PPP1_eq) |
|
3999 find_theorems "(bder _ _ >> _) = _" |
|
4000 apply(rule contains50) |
|
4001 |
|
4002 apply(case_tac "bders a xs = AZERO") |
|
4003 apply(simp) |
|
4004 apply(subgoal_tac "bders_simp a xs = AZERO") |
|
4005 prefer 2 |
|
4006 apply (metis L_bders_simp XXX4a_good_cons bders.simps(1) bders_simp.simps(1) bsimp.simps(3) good.simps(1) good1a test2 xxx_bder2) |
|
4007 apply(simp) |
|
4008 apply(case_tac xs) |
|
4009 apply(simp) |
|
4010 apply (simp add: PPP1_eq) |
|
4011 apply(simp) |
|
4012 apply(subgoal_tac "good (bders_simp a (aa # list)) \<or> (bders_simp a (aa # list) = AZERO)") |
|
4013 apply(auto) |
|
4014 apply(subst (asm) bder_simp_contains_IFF) |
|
4015 apply(simp) |
|
4016 |
|
4017 |
3953 |
4018 |
3954 lemma |
4019 lemma |
3955 assumes "bders (intern r) s >>2 bs" |
4020 assumes "s \<in> L (erase r)" |
3956 shows "bders_simp (intern r) s >>2 bs" |
4021 shows "bders_simp r s >> bs \<longleftrightarrow> bders r s >> bs" |
3957 using assms |
4022 using assms |
3958 apply(induct s arbitrary: r bs) |
4023 apply(induct s arbitrary: r bs) |
3959 apply(simp) |
4024 apply(simp) |
3960 apply(simp) |
4025 apply(simp add: bders_append bders_simp_append) |
|
4026 apply(rule iffI) |
|
4027 apply(drule_tac x="bsimp (bder a r)" in meta_spec) |
|
4028 apply(drule_tac x="bs" in meta_spec) |
|
4029 apply(drule meta_mp) |
|
4030 using L_bsimp_erase lexer_correct_None apply fastforce |
|
4031 apply(simp) |
|
4032 |
|
4033 |
|
4034 prefer 2 |
|
4035 |
|
4036 |
3961 oops |
4037 oops |
3962 |
4038 |
3963 |
4039 |
3964 lemma |
4040 lemma |
3965 assumes "s \<in> L r" |
4041 assumes "s \<in> L r" |