2618 using asize_set apply blast |
2618 using asize_set apply blast |
2619 apply(subst CT1[symmetric]) |
2619 apply(subst CT1[symmetric]) |
2620 apply(simp) |
2620 apply(simp) |
2621 oops |
2621 oops |
2622 |
2622 |
2623 lemma big: |
2623 lemma YY: |
|
2624 assumes "flts (map bsimp as1) = xs" |
|
2625 shows "flts (map bsimp (map (fuse bs1) as1)) = map (fuse bs1) xs" |
|
2626 using assms |
|
2627 apply(induct as1 arbitrary: bs1 xs) |
|
2628 apply(simp) |
|
2629 apply(auto) |
|
2630 by (metis bsimp_fuse flts_fuse k0 list.simps(9)) |
|
2631 |
|
2632 |
|
2633 |
|
2634 lemma big0: |
|
2635 assumes as1p: "\<exists>as1'. map (fuse bs1) as1 = as1'" |
|
2636 and as2p: "\<exists>as2'. map (fuse bs2) as2 = as2'" |
2624 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
2637 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
2625 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
2638 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
2626 apply(simp add: comp_def bder_fuse) |
2639 apply - |
2627 apply(simp add: flts_append) |
2640 apply(subst CT1a) |
2628 |
2641 apply(subst (2) bsimp.simps) |
2629 sorry |
2642 apply(subst (2) bsimp.simps) |
|
2643 apply(subst (2) bsimp_idem[symmetric]) |
|
2644 apply(subst (2) bsimp.simps) |
|
2645 using as1p as2p |
|
2646 apply - |
|
2647 apply(erule exE)+ |
|
2648 apply(simp del: bsimp.simps) |
|
2649 apply(simp only: flts_append) |
|
2650 apply(case_tac "flts (map bsimp as1)") |
|
2651 apply(subgoal_tac "flts (map bsimp as1') = []") |
|
2652 prefer 2 |
|
2653 using YY apply auto[1] |
|
2654 apply(simp only:) |
|
2655 apply(simp del: bsimp_AALTs.simps bsimp.simps) |
|
2656 apply(subst bsimp_AALTs.simps) |
|
2657 apply(case_tac "flts (map bsimp as2)") |
|
2658 apply(subgoal_tac "flts (map bsimp as2') = []") |
|
2659 prefer 2 |
|
2660 using YY apply auto[1] |
|
2661 apply(simp) |
|
2662 apply(case_tac list) |
|
2663 apply(simp) |
|
2664 apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) [a]") |
|
2665 prefer 2 |
|
2666 using YY apply blast |
|
2667 apply(simp) |
|
2668 (* HERE TODAY *) |
|
2669 |
|
2670 |
|
2671 sorry |
|
2672 (* |
|
2673 |
|
2674 |
|
2675 using as1 apply auto[1] |
|
2676 apply(case_tac list) |
|
2677 apply(simp) |
|
2678 apply (metis as1 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less) |
|
2679 apply(simp only:) |
|
2680 apply(subgoal_tac "flts (map bsimp as1') = map (fuse bs1) (a # aa # lista)") |
|
2681 prefer 2 |
|
2682 apply (metis CTa arexp.distinct(7) as1 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 good.simps(1) good1 k0a map_idI test2) |
|
2683 apply(simp only:) |
|
2684 apply(simp only: bsimp_AALTs.simps) |
|
2685 apply(simp del: bsimp_AALTs.simps bsimp.simps) |
|
2686 apply(subst bsimp_AALTs.simps) |
|
2687 apply(case_tac "flts (map bsimp as2)") |
|
2688 apply(simp) |
|
2689 using as2 apply auto[1] |
|
2690 apply(case_tac listb) |
|
2691 apply(simp) |
|
2692 apply (metis as2 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less) |
|
2693 apply(simp only:) |
|
2694 apply(simp only: bsimp_AALTs.simps) |
|
2695 apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) (ab # ac # listc)") |
|
2696 prefer 2 |
|
2697 apply (metis arexp.distinct(7) as2 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 flts_qq good1 k0a test2) |
|
2698 apply(simp only:) |
|
2699 apply(simp del: bsimp.simps) |
|
2700 by (smt append_Cons bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem k0 k0a list.simps(8) list.simps(9)) |
|
2701 *) |
|
2702 |
|
2703 (* |
|
2704 lemma big: |
|
2705 assumes as1: "(AALTs bs1 as1) = bsimp (AALTs bs1 as1)" |
|
2706 and as2: "(AALTs bs2 as2) = bsimp (AALTs bs2 as2)" |
|
2707 and as1p: "\<exists>as1'. map (fuse bs1) as1 = as1'" |
|
2708 and as2p: "\<exists>as2'. map (fuse bs2) as2 = as2'" |
|
2709 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
|
2710 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
|
2711 apply - |
|
2712 apply(subst as1) |
|
2713 apply(subst as2) |
|
2714 apply(subst (2) bsimp.simps) |
|
2715 apply(subst (2) bsimp.simps) |
|
2716 apply(subst (2) bsimp_idem[symmetric]) |
|
2717 apply(subst (2) bsimp.simps) |
|
2718 using as1p as2p |
|
2719 apply - |
|
2720 apply(erule exE)+ |
|
2721 apply(simp del: bsimp.simps) |
|
2722 apply(simp only: flts_append) |
|
2723 apply(case_tac "flts (map bsimp as1)") |
|
2724 apply(simp) |
|
2725 using as1 apply auto[1] |
|
2726 apply(case_tac list) |
|
2727 apply(simp) |
|
2728 apply (metis as1 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less) |
|
2729 apply(simp only:) |
|
2730 apply(subgoal_tac "flts (map bsimp as1') = map (fuse bs1) (a # aa # lista)") |
|
2731 prefer 2 |
|
2732 apply (metis CTa arexp.distinct(7) as1 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 good.simps(1) good1 k0a map_idI test2) |
|
2733 apply(simp only:) |
|
2734 apply(simp only: bsimp_AALTs.simps) |
|
2735 apply(simp del: bsimp_AALTs.simps bsimp.simps) |
|
2736 apply(subst bsimp_AALTs.simps) |
|
2737 apply(case_tac "flts (map bsimp as2)") |
|
2738 apply(simp) |
|
2739 using as2 apply auto[1] |
|
2740 apply(case_tac listb) |
|
2741 apply(simp) |
|
2742 apply (metis as2 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less) |
|
2743 apply(simp only:) |
|
2744 apply(simp only: bsimp_AALTs.simps) |
|
2745 apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) (ab # ac # listc)") |
|
2746 prefer 2 |
|
2747 apply (metis arexp.distinct(7) as2 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 flts_qq good1 k0a test2) |
|
2748 apply(simp only:) |
|
2749 apply(simp del: bsimp.simps) |
|
2750 by (smt append_Cons bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem k0 k0a list.simps(8) list.simps(9)) |
|
2751 *) |
2630 |
2752 |
2631 lemma XXX2a_long_without_good: |
2753 lemma XXX2a_long_without_good: |
2632 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2754 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2633 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
2755 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
2634 apply(case_tac x) |
2756 apply(case_tac x) |