2661 shows "map (bsimp \<circ> bder c) as1 = map bsimp (map (bder c) as1)" |
2661 shows "map (bsimp \<circ> bder c) as1 = map bsimp (map (bder c) as1)" |
2662 apply(induct as1) |
2662 apply(induct as1) |
2663 apply(auto) |
2663 apply(auto) |
2664 done |
2664 done |
2665 |
2665 |
|
2666 lemma WWW6: |
|
2667 shows "bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]) ) ) = |
|
2668 bsimp(bsimp_AALTs x51 (map (bder c) (flts [bsimp a1, bsimp a2]))) " |
|
2669 using bder_bsimp_AALTs by auto |
|
2670 |
|
2671 lemma WWW7: |
|
2672 shows "bsimp (bsimp_AALTs x51 (map (bder c) (flts [bsimp a1, bsimp a2]))) = |
|
2673 bsimp(bsimp_AALTs x51 (flts (map (bder c) [bsimp a1, bsimp a2])))" |
|
2674 sorry |
|
2675 |
|
2676 |
|
2677 lemma stupid: |
|
2678 assumes "a = b" |
|
2679 shows "bsimp(a) = bsimp(b)" |
|
2680 using assms |
|
2681 apply(auto) |
|
2682 done |
|
2683 (* |
|
2684 proving idea: |
|
2685 bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) = bsimp_AALTs x51 (map (bder c) (flts [a1]++[a2])) |
|
2686 = bsimp_AALTs x51 (map (bder c) ((flts [a1])++(flts [a2]))) = |
|
2687 bsimp_AALTs x51 (map (bder c) (flts [a1]))++(map (bder c) (flts [a2])) = A |
|
2688 and then want to prove that |
|
2689 map (bder c) (flts [a]) = flts [bder c a] under the condition |
|
2690 that a is either a seq with the first elem being not nullable, or a character equal to c, |
|
2691 or an AALTs, or a star |
|
2692 Then, A = bsimp_AALTs x51 (flts [bder c a]) ++ (map (bder c) (flts [a2])) = A1 |
|
2693 Using the same condition for a2, we get |
|
2694 A1 = bsimp_AALTs x51 (flts [bder c a1]) ++ (flts [bder c a2]) |
|
2695 =bsimp_AALTs x51 flts ([bder c a1] ++ [bder c a2]) |
|
2696 =bsimp_AALTs x51 flts ([bder c a1, bder c a2]) |
|
2697 *) |
|
2698 lemma manipulate_flts: |
|
2699 shows "bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) = |
|
2700 bsimp_AALTs x51 ((map (bder c) (flts [a1])) @ (map (bder c) (flts [a2])))" |
|
2701 by (metis k0 map_append) |
|
2702 |
|
2703 lemma go_inside_flts: |
|
2704 assumes " (bder c a1 \<noteq> AZERO) " |
|
2705 "\<not>(\<exists> a01 a02 x02. ( (a1 = ASEQ x02 a01 a02) \<and> bnullable(a01) ) )" |
|
2706 shows "map (bder c) (flts [a1]) = flts [bder c a1]" |
|
2707 using assms |
|
2708 apply - |
|
2709 apply(case_tac a1) |
|
2710 apply(simp) |
|
2711 apply(simp) |
|
2712 apply(case_tac "x32 = c") |
|
2713 prefer 2 |
|
2714 apply(simp) |
|
2715 apply(simp) |
|
2716 apply(simp) |
|
2717 apply (simp add: WWW4) |
|
2718 apply(simp add: bder_fuse) |
|
2719 done |
|
2720 |
|
2721 lemma medium010: |
|
2722 assumes " (bder c a1 = AZERO) " |
|
2723 shows "map (bder c) (flts [a1]) = [AZERO] \<or> map (bder c) (flts [a1]) = []" |
|
2724 using assms |
|
2725 apply - |
|
2726 apply(case_tac a1) |
|
2727 apply(simp) |
|
2728 apply(simp) |
|
2729 apply(simp) |
|
2730 apply(simp) |
|
2731 apply(simp) |
|
2732 apply(simp) |
|
2733 done |
|
2734 |
|
2735 lemma medium011: |
|
2736 assumes " (bder c a1 = AZERO) " |
|
2737 shows "flts (map (bder c) [a1, a2]) = flts [bder c a2]" |
|
2738 using assms |
|
2739 apply - |
|
2740 apply(simp) |
|
2741 done |
|
2742 |
|
2743 lemma medium01central: |
|
2744 shows "bsimp(bsimp_AALTs x51 (map (bder c) (flts [a2])) ) = bsimp(bsimp_AALTs x51 (flts [bder c a2]))" |
|
2745 sorry |
|
2746 |
|
2747 |
|
2748 lemma plus_bsimp: |
|
2749 assumes "bsimp( bsimp a) = bsimp (bsimp b)" |
|
2750 shows "bsimp a = bsimp b" |
|
2751 using assms |
|
2752 apply - |
|
2753 by (simp add: bsimp_idem) |
|
2754 lemma patience_good5: |
|
2755 assumes "bsimp r = AALTs x y" |
|
2756 shows " \<exists> a aa list. y = a#aa#list" |
|
2757 by (metis Nil_is_map_conv arexp.simps(13) assms bsimp_AALTs.elims flts1 good.simps(5) good1 k0a) |
|
2758 |
|
2759 |
|
2760 (*this does not hold actually |
|
2761 lemma bsimp_equiv0: |
|
2762 shows "bsimp(bsimp r) = bsimp(bsimp (AALTs [] [r]))" |
|
2763 apply(simp) |
|
2764 apply(case_tac "bsimp r") |
|
2765 apply(simp) |
|
2766 apply(simp) |
|
2767 apply(simp) |
|
2768 apply(simp) |
|
2769 thm good1 |
|
2770 using good1 |
|
2771 apply - |
|
2772 apply(drule_tac x="r" in meta_spec) |
|
2773 apply(erule disjE) |
|
2774 |
|
2775 apply(simp only: bsimp_AALTs.simps) |
|
2776 apply(simp only:flts.simps) |
|
2777 apply(drule patience_good5) |
|
2778 apply(clarify) |
|
2779 apply(subst bsimp_AALTs_qq) |
|
2780 apply simp |
|
2781 prefer 2 |
|
2782 sorry*) |
|
2783 |
|
2784 (*exercise: try multiple ways of proving this*) |
|
2785 (*this lemma does not hold......... |
|
2786 lemma bsimp_equiv1: |
|
2787 shows "bsimp r = bsimp (AALTs [] [r])" |
|
2788 using plus_bsimp |
|
2789 apply - |
|
2790 using bsimp_equiv0 by blast |
|
2791 (*apply(simp) |
|
2792 apply(case_tac "bsimp r") |
|
2793 apply(simp) |
|
2794 apply(simp) |
|
2795 apply(simp) |
|
2796 apply(simp) |
|
2797 (*use lemma good1*) |
|
2798 thm good1 |
|
2799 using good1 |
|
2800 apply - |
|
2801 apply(drule_tac x="r" in meta_spec) |
|
2802 apply(erule disjE) |
|
2803 |
|
2804 apply(subst flts_single1) |
|
2805 apply(simp only: bsimp_AALTs.simps) |
|
2806 prefer 2 |
|
2807 |
|
2808 thm flts_single1 |
|
2809 |
|
2810 find_theorems "flts _ = _"*) |
|
2811 *) |
|
2812 lemma bsimp_equiv2: |
|
2813 shows "bsimp (AALTs x51 [r]) = bsimp (AALT x51 AZERO r)" |
|
2814 sorry |
|
2815 |
|
2816 lemma medium_stupid_isabelle: |
|
2817 assumes "rs = a # list" |
|
2818 shows "bsimp_AALTs x51 (AZERO # rs) = AALTs x51 (AZERO#rs)" |
|
2819 using assms |
|
2820 apply - |
|
2821 apply(simp) |
|
2822 done |
|
2823 (* |
|
2824 lemma mediumlittle: |
|
2825 shows "bsimp(bsimp_AALTs x51 rs) = bsimp(bsimp_AALTs x51 (AZERO # rs))" |
|
2826 apply(case_tac rs) |
|
2827 apply(simp) |
|
2828 apply(case_tac list) |
|
2829 apply(subst medium_stupid_isabelle) |
|
2830 apply(simp) |
|
2831 prefer 2 |
|
2832 apply simp |
|
2833 apply(rule_tac s="a#list" and t="rs" in subst) |
|
2834 apply(simp) |
|
2835 apply(rule_tac t="list" and s= "[]" in subst) |
|
2836 apply(simp) |
|
2837 (*dunno what is the rule for x#nil = x*) |
|
2838 apply(case_tac a) |
|
2839 apply(simp) |
|
2840 apply(simp) |
|
2841 apply(simp) |
|
2842 prefer 3 |
|
2843 apply simp |
|
2844 apply(simp only:bsimp_AALTs.simps) |
|
2845 |
|
2846 apply simp |
|
2847 apply(case_tac "bsimp x42") |
|
2848 apply(simp) |
|
2849 apply simp |
|
2850 apply(case_tac "bsimp x43") |
|
2851 apply simp |
|
2852 apply simp |
|
2853 apply simp |
|
2854 apply simp |
|
2855 apply(simp only:bsimp_ASEQ.simps) |
|
2856 using good1 |
|
2857 apply - |
|
2858 apply(drule_tac x="x43" in meta_spec) |
|
2859 apply(erule disjE) |
|
2860 apply(subst bsimp_AALTs_qq) |
|
2861 using patience_good5 apply force |
|
2862 apply(simp only:bsimp_AALTs.simps) |
|
2863 apply(simp only:fuse.simps) |
|
2864 apply(simp only:flts.simps) |
|
2865 (*OK from here you actually realize this lemma doesnt hold*) |
|
2866 apply(simp) |
|
2867 apply(simp) |
|
2868 apply(rule_tac t="rs" and s="a#list" in subst) |
|
2869 apply(simp) |
|
2870 apply(rule_tac t="list" and s="[]" in subst) |
|
2871 apply(simp) |
|
2872 (*apply(simp only:bsimp_AALTs.simps)*) |
|
2873 (*apply(simp only:fuse.simps)*) |
|
2874 sorry |
|
2875 *) |
|
2876 lemma singleton_list_map: |
|
2877 shows"map f [a] = [f a]" |
|
2878 apply simp |
|
2879 done |
|
2880 lemma map_application2: |
|
2881 shows"map f [a,b] = [f a, f b]" |
|
2882 apply simp |
|
2883 done |
|
2884 |
|
2885 (* bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]))) = |
|
2886 bsimp (AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2)))*) |
|
2887 (*This equality does not hold*) |
|
2888 lemma medium01: |
|
2889 assumes " (bder c a1 = AZERO) " |
|
2890 shows "bsimp(bsimp_AALTs x51 (map (bder c) (flts [ a1, a2]))) = |
|
2891 bsimp(bsimp_AALTs x51 (flts (map (bder c) [ a1, a2])))" |
|
2892 apply(subst manipulate_flts) |
|
2893 using assms |
|
2894 apply - |
|
2895 apply(subst medium011) |
|
2896 apply(simp) |
|
2897 apply(case_tac "map (bder c) (flts [a1]) = []") |
|
2898 apply(simp) |
|
2899 using medium01central apply blast |
|
2900 apply(frule medium010) |
|
2901 apply(erule disjE) |
|
2902 prefer 2 |
|
2903 apply(simp) |
|
2904 apply(simp) |
|
2905 apply(case_tac a2) |
|
2906 apply simp |
|
2907 apply simp |
|
2908 apply simp |
|
2909 apply(simp only:flts.simps) |
|
2910 (*HOW do i say here to replace ASEQ ..... back into a2*) |
|
2911 (*how do i say here to use the definition of map function |
|
2912 without lemma, of course*) |
|
2913 (*how do i say here that AZERO#map (bder c) [ASEQ x41 x42 x43]'s list.len >1 |
|
2914 without a lemma, of course*) |
|
2915 apply(subst singleton_list_map) |
|
2916 apply(simp only: bsimp_AALTs.simps) |
|
2917 apply(case_tac "bder c (ASEQ x41 x42 x43)") |
|
2918 apply simp |
|
2919 apply simp |
|
2920 apply simp |
|
2921 prefer 3 |
|
2922 apply simp |
|
2923 apply(rule_tac t="bder c (ASEQ x41 x42 x43)" |
|
2924 and s="ASEQ x41a x42a x43a" in subst) |
|
2925 apply simp |
|
2926 apply(simp only: flts.simps) |
|
2927 apply(simp only: bsimp_AALTs.simps) |
|
2928 apply(simp only: fuse.simps) |
|
2929 apply(subst (2) bsimp_idem[symmetric]) |
|
2930 apply(subst (1) bsimp_idem[symmetric]) |
|
2931 apply(simp only:bsimp.simps) |
|
2932 apply(subst map_application2) |
|
2933 apply(simp only: bsimp.simps) |
|
2934 apply(simp only:flts.simps) |
|
2935 (*want to happily change between a2 and ASEQ x41 42 43, and eliminate now |
|
2936 redundant conditions such as map (bder c) (flts [a1]) = [AZERO] *) |
|
2937 apply(case_tac "bsimp x42a") |
|
2938 apply(simp) |
|
2939 apply(case_tac "bsimp x43a") |
|
2940 apply(simp) |
|
2941 apply(simp) |
|
2942 apply(simp) |
|
2943 apply(simp) |
|
2944 prefer 2 |
|
2945 apply(simp) |
|
2946 apply(rule_tac t="bsimp x43a" |
|
2947 and s="AALTs x51a x52" in subst) |
|
2948 apply simp |
|
2949 apply(simp only:bsimp_ASEQ.simps) |
|
2950 apply(simp only:fuse.simps) |
|
2951 apply(simp only:flts.simps) |
|
2952 |
|
2953 using medium01central mediumlittle by auto |
|
2954 |
|
2955 |
|
2956 |
|
2957 lemma medium1: |
|
2958 assumes " (bder c a1 \<noteq> AZERO) " |
|
2959 "\<not>(\<exists> a01 a02 x02. ( (a1 = ASEQ x02 a01 a02) \<and> bnullable(a01) ) )" |
|
2960 " (bder c a2 \<noteq> AZERO)" |
|
2961 "\<not>(\<exists> a11 a12 x12. ( (a2 = ASEQ x12 a11 a12) \<and> bnullable(a11) ) )" |
|
2962 shows "bsimp_AALTs x51 (map (bder c) (flts [ a1, a2])) = |
|
2963 bsimp_AALTs x51 (flts (map (bder c) [ a1, a2]))" |
|
2964 using assms |
|
2965 apply - |
|
2966 apply(subst manipulate_flts) |
|
2967 apply(case_tac "a1") |
|
2968 apply(simp) |
|
2969 apply(simp) |
|
2970 apply(case_tac "x32 = c") |
|
2971 prefer 2 |
|
2972 apply(simp) |
|
2973 prefer 2 |
|
2974 apply(case_tac "bnullable x42") |
|
2975 apply(simp) |
|
2976 apply(simp) |
|
2977 |
|
2978 apply(case_tac "a2") |
|
2979 apply(simp) |
|
2980 apply(simp) |
|
2981 apply(case_tac "x32 = c") |
|
2982 prefer 2 |
|
2983 apply(simp) |
|
2984 apply(simp) |
|
2985 apply(case_tac "bnullable x42a") |
|
2986 apply(simp) |
|
2987 apply(subst go_inside_flts) |
|
2988 apply(simp) |
|
2989 apply(simp) |
|
2990 apply(simp) |
|
2991 apply(simp) |
|
2992 apply (simp add: WWW4) |
|
2993 apply(simp) |
|
2994 apply (simp add: WWW4) |
|
2995 apply (simp add: go_inside_flts) |
|
2996 apply (metis (no_types, lifting) go_inside_flts k0 list.simps(8) list.simps(9)) |
|
2997 by (smt bder.simps(6) flts.simps(1) flts.simps(6) flts.simps(7) go_inside_flts k0 list.inject list.simps(9)) |
|
2998 |
2666 lemma big0: |
2999 lemma big0: |
2667 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
3000 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
2668 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
3001 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
2669 by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append) |
3002 by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append) |
2670 |
3003 |