2478 assumes "s \<in> L (erase r)" |
2437 assumes "s \<in> L (erase r)" |
2479 shows "retrieve r (flex (erase r) id s (mkeps (ders s (erase r)))) |
2438 shows "retrieve r (flex (erase r) id s (mkeps (ders s (erase r)))) |
2480 = retrieve (bders r s) (mkeps (erase (bders r s)))" |
2439 = retrieve (bders r s) (mkeps (erase (bders r s)))" |
2481 using assms |
2440 using assms |
2482 using LB LC lexer_correct_Some by auto |
2441 using LB LC lexer_correct_Some by auto |
2483 |
|
2484 lemma LXXX: |
|
2485 assumes "s \<in> (erase r) \<rightarrow> v" "s \<in> (erase (bsimp r)) \<rightarrow> v'" |
|
2486 shows "retrieve r v = retrieve (bsimp r) v'" |
|
2487 using assms |
|
2488 apply - |
|
2489 thm LC |
|
2490 apply(subst LC) |
|
2491 apply(assumption) |
|
2492 apply(subst L0[symmetric]) |
|
2493 using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce |
|
2494 apply(subst (2) LC) |
|
2495 apply(assumption) |
|
2496 apply(subst (2) L0[symmetric]) |
|
2497 using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce |
|
2498 |
|
2499 oops |
|
2500 |
|
2501 |
|
2502 lemma L07a: |
|
2503 assumes "s \<in> L (erase r)" |
|
2504 shows "retrieve (bsimp r) (flex (erase (bsimp r)) id s (mkeps (ders s (erase (bsimp r))))) |
|
2505 = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))" |
|
2506 using assms |
|
2507 apply(induct s arbitrary: r) |
|
2508 apply(simp) |
|
2509 using L0a apply force |
|
2510 apply(drule_tac x="(bder a r)" in meta_spec) |
|
2511 apply(drule meta_mp) |
|
2512 apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) |
|
2513 apply(drule sym) |
|
2514 apply(simp) |
|
2515 apply(subst (asm) bder_retrieve) |
|
2516 apply (metis Posix_Prf Posix_flex Posix_mkeps ders.simps(2) lexer_correct_None lexer_flex) |
|
2517 apply(simp only: flex_fun_apply) |
|
2518 apply(simp) |
|
2519 using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars] |
|
2520 oops |
|
2521 |
|
2522 lemma L08: |
|
2523 assumes "s \<in> L (erase r)" |
|
2524 shows "retrieve (bders (bsimp r) s) (mkeps (erase (bders (bsimp r) s))) |
|
2525 = retrieve (bders r s) (mkeps (erase (bders r s)))" |
|
2526 using assms |
|
2527 apply(induct s arbitrary: r) |
|
2528 apply(simp) |
|
2529 using L0 bnullable_correctness nullable_correctness apply blast |
|
2530 apply(simp add: bders_append) |
|
2531 apply(drule_tac x="(bder a (bsimp r))" in meta_spec) |
|
2532 apply(drule meta_mp) |
|
2533 apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) |
|
2534 apply(drule sym) |
|
2535 apply(simp) |
|
2536 apply(subst LA) |
|
2537 apply (metis L0aa L_bsimp_erase Posix1(1) ders.simps(2) ders_correctness erase_bder erase_bders mkeps_nullable nullable_correctness) |
|
2538 apply(subst LA) |
|
2539 using lexer_correct_None lexer_flex mkeps_nullable apply force |
|
2540 |
|
2541 using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars] |
|
2542 |
|
2543 thm L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars] |
|
2544 oops |
|
2545 |
|
2546 lemma test: |
|
2547 assumes "s = [c]" |
|
2548 shows "retrieve (bders r s) v = XXX" and "YYY = retrieve r (flex (erase r) id s v)" |
|
2549 using assms |
|
2550 apply(simp only: bders.simps) |
|
2551 defer |
|
2552 using assms |
|
2553 apply(simp only: flex.simps id_simps) |
|
2554 using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] |
|
2555 find_theorems "retrieve (bders _ _) _" |
|
2556 find_theorems "retrieve _ (mkeps _)" |
|
2557 oops |
|
2558 |
|
2559 lemma L06X: |
|
2560 assumes "bnullable (bder c a)" |
|
2561 shows "bmkeps (bder c (bsimp a)) = bmkeps (bder c a)" |
|
2562 using assms |
|
2563 apply(induct a arbitrary: c) |
|
2564 apply(simp) |
|
2565 apply(simp) |
|
2566 apply(simp) |
|
2567 prefer 3 |
|
2568 apply(simp) |
|
2569 prefer 2 |
|
2570 apply(simp) |
|
2571 |
|
2572 defer |
|
2573 oops |
|
2574 |
2442 |
2575 lemma L06_2: |
2443 lemma L06_2: |
2576 assumes "bnullable (bders a [c,d])" |
2444 assumes "bnullable (bders a [c,d])" |
2577 shows "bmkeps (bders (bsimp a) [c,d]) = bmkeps (bsimp (bders (bsimp a) [c,d]))" |
2445 shows "bmkeps (bders (bsimp a) [c,d]) = bmkeps (bsimp (bders (bsimp a) [c,d]))" |
2578 using assms |
2446 using assms |
2945 shows "asize a < Suc (sum_list (map asize as))" |
2715 shows "asize a < Suc (sum_list (map asize as))" |
2946 using assms |
2716 using assms |
2947 apply(induct as arbitrary: a) |
2717 apply(induct as arbitrary: a) |
2948 apply(auto) |
2718 apply(auto) |
2949 using le_add2 le_less_trans not_less_eq by blast |
2719 using le_add2 le_less_trans not_less_eq by blast |
2950 |
2720 |
2951 |
2721 lemma PPP: |
2952 lemma XXX2a_long_without_good: |
2722 assumes "\<Turnstile> v : ders s r" |
2953 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2723 shows "bders (intern r) s >> code v" |
2954 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
2724 using assms |
2955 apply(case_tac x) |
2725 apply(induct s arbitrary: r v rule: rev_induct) |
2956 apply(simp) |
2726 apply(simp) |
2957 apply(simp) |
2727 apply (simp add: Posix_Prf contains2) |
2958 apply(simp) |
2728 apply(simp add: bders_append ders_append flex_append) |
2959 prefer 3 |
2729 apply(frule Prf_injval) |
2960 apply(simp) |
2730 apply(drule meta_spec) |
2961 (* AALT case *) |
2731 apply(drule meta_spec) |
2962 prefer 2 |
2732 apply(drule meta_mp) |
2963 apply(simp del: bsimp.simps) |
2733 apply(assumption) |
2964 apply(subst (2) CT1) |
2734 apply(subst retrieve_code) |
2965 apply(subst CT_exp) |
2735 apply(assumption) |
2966 apply(auto)[1] |
2736 apply(subst (asm) retrieve_code) |
2967 using asize_set apply blast |
2737 apply(assumption) |
2968 apply(subst CT1[symmetric]) |
2738 using contains7 contains7a contains6 retrieve_code |
2969 apply(simp) |
2739 apply(rule contains7) |
2970 oops |
2740 |
2971 |
2741 find_theorems "bder _ _ >> _" |
2972 lemma YY: |
2742 find_theorems "code _ = _" |
2973 assumes "flts (map bsimp as1) = xs" |
2743 find_theorems "\<Turnstile> _ : der _ _" |
2974 shows "flts (map bsimp (map (fuse bs1) as1)) = map (fuse bs1) xs" |
2744 |
2975 using assms |
2745 |
2976 apply(induct as1 arbitrary: bs1 xs) |
2746 |
2977 apply(simp) |
2747 find_theorems "_ >> (code _)" |
2978 apply(auto) |
2748 apply(induct s arbitrary: a bs rule: rev_induct) |
2979 by (metis bsimp_fuse flts_fuse k0 list.simps(9)) |
2749 apply(simp) |
2980 |
2750 apply(simp add: bders_simp_append bders_append) |
2981 |
2751 apply(rule contains55) |
2982 lemma flts_nonalt: |
2752 find_theorems "bder _ _ >> _" |
2983 assumes "flts (map bsimp xs) = ys" |
2753 apply(drule_tac x="bder a aa" in meta_spec) |
2984 shows "\<forall>y \<in> set ys. nonalt y" |
2754 apply(drule_tac x="bs" in meta_spec) |
2985 using assms |
2755 apply(simp) |
2986 apply(induct xs arbitrary: ys) |
2756 apply(rule contains55) |
2987 apply(auto) |
2757 find_theorems "bsimp _ >> _" |
2988 apply(case_tac xs) |
|
2989 apply(auto) |
|
2990 using flts2 good1 apply fastforce |
|
2991 by (smt ex_map_conv list.simps(9) nn1b nn1c) |
|
2992 |
|
2993 |
|
2994 lemma WWW3: |
|
2995 shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] = |
|
2996 flts (map bsimp (map (fuse bs1) as1))" |
|
2997 by (metis CT0 YY flts_nonalt flts_nothing qqq1) |
|
2998 |
|
2999 |
|
3000 |
|
3001 lemma WWW5: |
|
3002 shows "map (bsimp \<circ> bder c) as1 = map bsimp (map (bder c) as1)" |
|
3003 apply(induct as1) |
|
3004 apply(auto) |
|
3005 done |
|
3006 |
|
3007 lemma big0: |
|
3008 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
|
3009 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
|
3010 by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append) |
|
3011 |
|
3012 lemma bignA: |
|
3013 shows "bsimp (AALTs x51 (AALTs bs1 as1 # as2)) = |
|
3014 bsimp (AALTs x51 ((map (fuse bs1) as1) @ as2))" |
|
3015 apply(simp) |
|
3016 apply(subst k0) |
|
3017 apply(subst WWW3) |
|
3018 apply(simp add: flts_append) |
|
3019 done |
|
3020 |
|
3021 lemma XXX2a_long_without_good: |
|
3022 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
|
3023 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
|
3024 apply(case_tac x) |
|
3025 apply(simp) |
|
3026 apply(simp) |
|
3027 apply(simp) |
|
3028 prefer 3 |
|
3029 apply(simp) |
|
3030 (* SEQ case *) |
|
3031 apply(simp only:) |
|
3032 apply(subst CT1_SEQ) |
|
3033 apply(simp only: bsimp.simps) |
|
3034 |
|
3035 (* AALT case *) |
|
3036 prefer 2 |
|
3037 apply(simp only:) |
|
3038 apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]") |
|
3039 apply(clarify) |
|
3040 apply(simp del: bsimp.simps) |
|
3041 apply(subst (2) CT1) |
|
3042 apply(simp del: bsimp.simps) |
|
3043 apply(rule_tac t="bsimp (bder c a1)" and s="bsimp (bder c (bsimp a1))" in subst) |
|
3044 apply(simp del: bsimp.simps) |
|
3045 apply(rule_tac t="bsimp (bder c a2)" and s="bsimp (bder c (bsimp a2))" in subst) |
|
3046 apply(simp del: bsimp.simps) |
|
3047 apply(subst CT1a[symmetric]) |
|
3048 (* \<rightarrow> *) |
|
3049 apply(rule_tac t="AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2))" |
|
3050 and s="bder c (AALT x51 (bsimp a1) (bsimp a2))" in subst) |
|
3051 apply(simp) |
|
3052 apply(subst bsimp.simps) |
|
3053 apply(simp del: bsimp.simps bder.simps) |
|
3054 |
|
3055 apply(subst bder_bsimp_AALTs) |
|
3056 apply(subst bsimp.simps) |
|
3057 apply(subst WWW2[symmetric]) |
|
3058 apply(subst bsimp_AALTs_qq) |
|
3059 defer |
|
3060 apply(subst bsimp.simps) |
|
3061 |
|
3062 (* <- *) |
|
3063 apply(subst bsimp.simps) |
|
3064 apply(simp del: bsimp.simps) |
|
3065 apply(case_tac "\<exists>bs1 as1. bsimp a1 = AALTs bs1 as1") |
|
3066 apply(case_tac "\<exists>bs2 as2. bsimp a2 = AALTs bs2 as2") |
|
3067 apply(clarify) |
|
3068 apply(simp only:) |
|
3069 apply(simp del: bsimp.simps bder.simps) |
|
3070 apply(subst bsimp_AALTs_qq) |
|
3071 prefer 2 |
|
3072 apply(simp del: bsimp.simps) |
|
3073 apply(subst big0) |
|
3074 apply(simp add: WWW4) |
|
3075 apply (m etis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq) |
|
3076 oops |
|
3077 |
|
3078 lemma XXX2a_long_without_good: |
|
3079 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
|
3080 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
|
3081 apply(case_tac x) |
|
3082 apply(simp) |
|
3083 apply(simp) |
|
3084 apply(simp) |
|
3085 prefer 3 |
|
3086 apply(simp) |
|
3087 (* AALT case *) |
|
3088 prefer 2 |
|
3089 apply(subgoal_tac "nonnested (bsimp x)") |
|
3090 prefer 2 |
|
3091 using nn1b apply blast |
|
3092 apply(simp only:) |
|
3093 apply(drule_tac x="AALTs x51 (flts x52)" in spec) |
|
3094 apply(drule mp) |
|
3095 defer |
|
3096 apply(drule_tac x="c" in spec) |
|
3097 apply(simp) |
|
3098 apply(rotate_tac 2) |
|
3099 |
|
3100 apply(drule sym) |
|
3101 apply(simp) |
|
3102 |
|
3103 apply(simp only: bder.simps) |
|
3104 apply(simp only: bsimp.simps) |
|
3105 apply(subst bder_bsimp_AALTs) |
|
3106 apply(case_tac x52) |
|
3107 apply(simp) |
|
3108 apply(simp) |
|
3109 apply(case_tac list) |
|
3110 apply(simp) |
|
3111 apply(case_tac a) |
|
3112 apply(simp) |
|
3113 apply(simp) |
|
3114 apply(simp) |
|
3115 defer |
|
3116 apply(simp) |
|
3117 |
|
3118 |
|
3119 (* case AALTs list is not empty *) |
|
3120 apply(simp) |
|
3121 apply(subst k0) |
|
3122 apply(subst (2) k0) |
|
3123 apply(simp) |
|
3124 apply(case_tac "bsimp a = AZERO") |
|
3125 apply(subgoal_tac "bsimp (bder c a) = AZERO") |
|
3126 prefer 2 |
|
3127 using less_iff_Suc_add apply auto[1] |
|
3128 apply(simp) |
|
3129 apply(drule_tac x="AALTs x51 list" in spec) |
|
3130 apply(drule mp) |
|
3131 apply(simp add: asize0) |
|
3132 apply(drule_tac x="c" in spec) |
|
3133 apply(simp add: bder_bsimp_AALTs) |
|
3134 apply(case_tac "nonalt (bsimp a)") |
|
3135 prefer 2 |
|
3136 apply(drule_tac x="bsimp (AALTs x51 (a#list))" in spec) |
|
3137 apply(drule mp) |
|
3138 apply(rule order_class.order.strict_trans2) |
|
3139 apply(rule bsimp_AALTs_size3) |
|
3140 apply(auto)[1] |
|
3141 apply(simp) |
|
3142 apply(subst (asm) bsimp_idem) |
|
3143 apply(drule_tac x="c" in spec) |
|
3144 apply(simp) |
|
3145 find_theorems "_ < _ \<Longrightarrow> _ \<le> _ \<Longrightarrow>_ < _" |
|
3146 apply(rule le_trans) |
|
3147 apply(subgoal_tac "flts [bsimp a] = [bsimp a]") |
|
3148 prefer 2 |
|
3149 using k0b apply blast |
|
3150 apply(simp) |
|
3151 find_theorems "asize _ < asize _" |
|
3152 |
|
3153 using bder_bsimp_AALTs |
|
3154 apply(case_tac list) |
|
3155 apply(simp) |
|
3156 sledgeha mmer [timeout=6000] |
|
3157 |
|
3158 apply(case_tac "\<exists>r \<in> set (map bsimp x52). \<not>nonalt r") |
|
3159 apply(drule_tac x="bsimp (AALTs x51 x52)" in spec) |
|
3160 apply(drule mp) |
|
3161 using bsimp_AALTs_size3 apply blast |
|
3162 apply(drule_tac x="c" in spec) |
|
3163 apply(subst (asm) (2) test) |
|
3164 |
|
3165 apply(case_tac x52) |
|
3166 apply(simp) |
|
3167 apply(simp) |
|
3168 apply(case_tac "bsimp a = AZERO") |
|
3169 apply(simp) |
|
3170 apply(subgoal_tac "bsimp (bder c a) = AZERO") |
|
3171 prefer 2 |
|
3172 apply auto[1] |
|
3173 apply (metis L.simps(1) L_bsimp_erase der.simps(1) der_correctness erase.simps(1) erase_bder xxx_bder2) |
|
3174 apply(simp) |
|
3175 apply(drule_tac x="AALTs x51 list" in spec) |
|
3176 apply(drule mp) |
|
3177 apply(simp add: asize0) |
|
3178 apply(simp) |
|
3179 apply(case_tac list) |
|
3180 prefer 2 |
|
3181 apply(simp) |
|
3182 apply(case_tac "bsimp aa = AZERO") |
|
3183 apply(simp) |
|
3184 apply(subgoal_tac "bsimp (bder c aa) = AZERO") |
|
3185 prefer 2 |
|
3186 apply auto[1] |
|
3187 apply (metis add.left_commute bder.simps(1) bsimp.simps(3) less_add_Suc1) |
|
3188 apply(simp) |
|
3189 apply(drule_tac x="AALTs x51 (a#lista)" in spec) |
|
3190 apply(drule mp) |
|
3191 apply(simp add: asize0) |
|
3192 apply(simp) |
|
3193 apply (metis flts.simps(2) k0) |
|
3194 apply(subst k0) |
|
3195 apply(subst (2) k0) |
|
3196 |
|
3197 |
|
3198 using less_add_Suc1 apply fastforce |
|
3199 apply(subst k0) |
|
3200 |
|
3201 |
|
3202 apply(simp) |
|
3203 apply(case_tac "bsimp a = AZERO") |
|
3204 apply(simp) |
|
3205 apply(subgoal_tac "bsimp (bder c a) = AZERO") |
|
3206 prefer 2 |
|
3207 apply auto[1] |
|
3208 apply(simp) |
|
3209 apply(case_tac "nonalt (bsimp a)") |
|
3210 apply(subst bsimp_AALTs1) |
|
3211 apply(simp) |
|
3212 using less_add_Suc1 apply fastforce |
|
3213 |
|
3214 apply(subst bsimp_AALTs1) |
|
3215 |
|
3216 using nn11a apply b last |
|
3217 |
|
3218 (* SEQ case *) |
|
3219 apply(clarify) |
|
3220 apply(subst bsimp.simps) |
|
3221 apply(simp del: bsimp.simps) |
|
3222 apply(auto simp del: bsimp.simps)[1] |
|
3223 apply(subgoal_tac "bsimp x42 \<noteq> AZERO") |
|
3224 prefer 2 |
|
3225 using b3 apply force |
|
3226 apply(case_tac "bsimp x43 = AZERO") |
|
3227 apply(simp) |
|
3228 apply (simp add: bsimp_ASEQ0) |
|
3229 apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) less_add_Suc2) |
|
3230 apply(case_tac "\<exists>bs. bsimp x42 = AONE bs") |
|
3231 apply(clarify) |
|
3232 apply(simp) |
|
3233 apply(subst bsimp_ASEQ2) |
|
3234 apply(subgoal_tac "bsimp (bder c x42) = AZERO") |
|
3235 prefer 2 |
|
3236 using less_add_Suc1 apply fastforce |
|
3237 apply(simp) |
|
3238 apply(frule_tac x="x43" in spec) |
|
3239 apply(drule mp) |
|
3240 apply(simp) |
|
3241 apply(drule_tac x="c" in spec) |
|
3242 apply(subst bder_fuse) |
|
3243 apply(subst bsimp_fuse[symmetric]) |
|
3244 apply(simp) |
|
3245 apply(subgoal_tac "bmkeps x42 = bs") |
|
3246 prefer 2 |
|
3247 apply (simp add: bmkeps_simp) |
|
3248 apply(simp) |
|
3249 apply(subst bsimp_fuse[symmetric]) |
|
3250 apply(case_tac "nonalt (bsimp (bder c x43))") |
|
3251 apply(subst bsimp_AALTs1) |
|
3252 using nn11a apply blast |
|
3253 using fuse_append apply blast |
|
3254 apply(subgoal_tac "\<exists>bs rs. bsimp (bder c x43) = AALTs bs rs") |
|
3255 prefer 2 |
|
3256 using bbbbs1 apply blast |
|
3257 apply(clarify) |
|
3258 apply(simp) |
|
3259 apply(case_tac rs) |
|
3260 apply(simp) |
|
3261 apply (metis arexp.distinct(7) good.simps(4) good1) |
|
3262 apply(simp) |
|
3263 apply(case_tac list) |
|
3264 apply(simp) |
|
3265 apply (metis arexp.distinct(7) good.simps(5) good1) |
|
3266 apply(simp del: bsimp_AALTs.simps) |
|
3267 apply(simp only: bsimp_AALTs.simps) |
|
3268 apply(simp) |
|
3269 |
|
3270 |
|
3271 |
|
3272 |
|
3273 (* HERE *) |
|
3274 apply(case_tac "x42 = AZERO") |
|
3275 apply(simp) |
|
3276 apply(case_tac "bsimp x43 = AZERO") |
|
3277 apply(simp) |
|
3278 apply (simp add: bsimp_ASEQ0) |
|
3279 apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO") |
|
3280 apply(simp) |
|
3281 apply (met is bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2) |
|
3282 apply(case_tac "\<exists>bs. bsimp x42 = AONE bs") |
|
3283 apply(clarify) |
|
3284 apply(simp) |
|
3285 apply(subst bsimp_ASEQ2) |
|
3286 apply(subgoal_tac "bsimp (bder c x42) = AZERO") |
|
3287 apply(simp) |
|
3288 prefer 2 |
|
3289 using less_add_Suc1 apply fastforce |
|
3290 apply(subgoal_tac "bmkeps x42 = bs") |
|
3291 prefer 2 |
|
3292 apply (simp add: bmkeps_simp) |
|
3293 apply(simp) |
|
3294 apply(case_tac "nonalt (bsimp (bder c x43))") |
|
3295 apply (metis bder_fuse bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) fuse_append k0b less_add_Suc2 nn11a) |
|
3296 apply(subgoal_tac "nonnested (bsimp (bder c x43))") |
|
3297 prefer 2 |
|
3298 using nn1b apply blast |
|
3299 apply(case_tac x43) |
|
3300 apply(simp) |
|
3301 apply(simp) |
|
3302 apply(simp) |
|
3303 prefer 3 |
|
3304 apply(simp) |
|
3305 apply (metis arexp.distinct(25) arexp.distinct(7) arexp.distinct(9) bsimp_ASEQ.simps(1) bsimp_ASEQ.simps(11) bsimp_ASEQ1 nn11a nonalt.elims(3) nonalt.simps(6)) |
|
3306 apply(simp) |
|
3307 apply(auto)[1] |
|
3308 apply(case_tac "(bsimp (bder c x42a)) = AZERO") |
|
3309 apply(simp) |
|
3310 |
|
3311 apply(simp) |
|
3312 |
|
3313 |
|
3314 |
|
3315 apply(subgoal_tac "(\<exists>bs1 rs1. 1 < length rs1 \<and> bsimp (bder c x43) = AALTs bs1 rs1 ) \<or> |
|
3316 (\<exists>bs1 r. bsimp (bder c x43) = fuse bs1 r)") |
|
3317 prefer 2 |
|
3318 apply (metis fuse_empty) |
|
3319 apply(erule disjE) |
|
3320 prefer 2 |
|
3321 apply(clarify) |
|
3322 apply(simp only:) |
|
3323 apply(simp) |
|
3324 apply(simp add: fuse_append) |
|
3325 apply(subst bder_fuse) |
|
3326 apply(subst bsimp_fuse[symmetric]) |
|
3327 apply(subst bder_fuse) |
|
3328 apply(subst bsimp_fuse[symmetric]) |
|
3329 apply(subgoal_tac "bsimp (bder c (bsimp x43)) = bsimp (bder c x43)") |
|
3330 prefer 2 |
|
3331 using less_add_Suc2 apply bl ast |
|
3332 apply(simp only: ) |
|
3333 apply(subst bsimp_fuse[symmetric]) |
|
3334 apply(simp only: ) |
|
3335 |
|
3336 apply(simp only: fuse.simps) |
|
3337 apply(simp) |
|
3338 apply(case_tac rs1) |
|
3339 apply(simp) |
|
3340 apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(4) good1 good_fuse) |
|
3341 apply(simp) |
|
3342 apply(case_tac list) |
|
3343 apply(simp) |
|
3344 apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse) |
|
3345 apply(simp only: bsimp_AALTs.simps map_cons.simps) |
|
3346 apply(auto)[1] |
|
3347 |
|
3348 |
|
3349 |
|
3350 apply(subst bsimp_fuse[symmetric]) |
|
3351 apply(subgoal_tac "bmkeps x42 = bs") |
|
3352 prefer 2 |
|
3353 apply (simp add: bmkeps_simp) |
|
3354 |
|
3355 |
|
3356 apply(simp) |
|
3357 |
|
3358 using b3 apply force |
|
3359 using bsimp_ASEQ0 test2 apply fo rce |
|
3360 thm good_SEQ test2 |
|
3361 apply (simp add: good_SEQ test2) |
|
3362 apply (simp add: good_SEQ test2) |
|
3363 apply(case_tac "x42 = AZERO") |
|
3364 apply(simp) |
|
3365 apply(case_tac "x43 = AZERO") |
|
3366 apply(simp) |
|
3367 apply (simp add: bsimp_ASEQ0) |
|
3368 apply(case_tac "\<exists>bs. x42 = AONE bs") |
|
3369 apply(clarify) |
|
3370 apply(simp) |
|
3371 apply(subst bsimp_ASEQ1) |
|
3372 apply(simp) |
|
3373 using bsimp_ASEQ0 test2 apply fo rce |
|
3374 apply (simp add: good_SEQ test2) |
|
3375 apply (simp add: good_SEQ test2) |
|
3376 apply (simp add: good_SEQ test2) |
|
3377 (* AALTs case *) |
|
3378 apply(simp) |
|
3379 using test2 by fa st force |
|
3380 |
|
3381 |
|
3382 lemma XXX4ab: |
|
3383 shows "good (bders_simp (bsimp r) s) \<or> bders_simp (bsimp r) s = AZERO" |
|
3384 apply(induct s arbitrary: r rule: rev_induct) |
|
3385 apply(simp) |
|
3386 apply (simp add: good1) |
|
3387 apply(simp add: bders_simp_append) |
|
3388 apply (simp add: good1) |
|
3389 done |
|
3390 |
2758 |
3391 lemma XXX4: |
2759 lemma XXX4: |
3392 assumes "good a" |
2760 assumes "good a" |
3393 shows "bders_simp a s = bsimp (bders a s)" |
2761 shows "bders_simp a s = bsimp (bders a s)" |
3394 using assms |
2762 using assms |