2639 apply(case_tac xs) |
2639 apply(case_tac xs) |
2640 apply(auto) |
2640 apply(auto) |
2641 using flts2 good1 apply fastforce |
2641 using flts2 good1 apply fastforce |
2642 by (smt ex_map_conv list.simps(9) nn1b nn1c) |
2642 by (smt ex_map_conv list.simps(9) nn1b nn1c) |
2643 |
2643 |
|
2644 lemma WWW2: |
|
2645 shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) = |
|
2646 bsimp_AALTs bs1 (flts (map bsimp as1))" |
|
2647 by (metis bsimp.simps(2) bsimp_idem) |
|
2648 |
|
2649 lemma WWW3: |
|
2650 shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] = |
|
2651 flts (map bsimp (map (fuse bs1) as1))" |
|
2652 by (metis CT0 YY flts_nonalt flts_nothing qqq1) |
|
2653 |
|
2654 lemma WWW4: |
|
2655 shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)" |
|
2656 apply(induct as1) |
|
2657 apply(auto) |
|
2658 using bder_fuse by blast |
|
2659 |
|
2660 |
2644 lemma big0: |
2661 lemma big0: |
2645 assumes as1p: "\<exists>as1'. map (fuse bs1) as1 = as1'" |
|
2646 and as2p: "\<exists>as2'. map (fuse bs2) as2 = as2'" |
|
2647 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
2662 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
2648 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
2663 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
2649 apply - |
2664 by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append) |
2650 apply(subst CT1a) |
2665 |
2651 apply(subst (2) bsimp.simps) |
2666 |
2652 apply(subst (2) bsimp.simps) |
|
2653 apply(subst (2) bsimp_idem[symmetric]) |
|
2654 apply(subst (2) bsimp.simps) |
|
2655 using as1p as2p |
|
2656 apply - |
|
2657 apply(erule exE)+ |
|
2658 apply(simp del: bsimp.simps) |
|
2659 apply(simp only: flts_append) |
|
2660 apply(case_tac "flts (map bsimp as1)") |
|
2661 apply(subgoal_tac "flts (map bsimp as1') = []") |
|
2662 prefer 2 |
|
2663 using YY apply auto[1] |
|
2664 apply(simp only:) |
|
2665 apply(simp del: bsimp_AALTs.simps bsimp.simps) |
|
2666 apply(subst bsimp_AALTs.simps) |
|
2667 apply(case_tac "flts (map bsimp as2)") |
|
2668 apply(subgoal_tac "flts (map bsimp as2') = []") |
|
2669 prefer 2 |
|
2670 using YY apply auto[1] |
|
2671 apply(simp) |
|
2672 apply(case_tac list) |
|
2673 apply(simp) |
|
2674 apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) [a]") |
|
2675 prefer 2 |
|
2676 using YY apply blast |
|
2677 apply(simp) |
|
2678 apply(subgoal_tac "nonalt a") |
|
2679 prefer 2 |
|
2680 apply (simp add: flts_nonalt) |
|
2681 apply(subgoal_tac "nonalt (fuse bs2 a)") |
|
2682 prefer 2 |
|
2683 using nn11a apply blast |
|
2684 apply (metis bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs1 bsimp_idem) |
|
2685 apply(simp only:) |
|
2686 apply(subgoal_tac "bsimp_AALTs bs2 (a # aa # lista) = AALTs bs2 (a # aa # lista)") |
|
2687 prefer 2 |
|
2688 using bsimp_AALTs.simps(3) apply blast |
|
2689 apply(simp only:) |
|
2690 apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2)(a # aa # lista) ") |
|
2691 prefer 2 |
|
2692 using YY apply blast |
|
2693 apply(simp only:) |
|
2694 apply(subst (1) bsimp_idem[symmetric]) |
|
2695 apply(simp) |
|
2696 apply (metis arexp.distinct(7) bbbbs bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem good1 list.simps(9) map_map) |
|
2697 (* HERE TODAY *) |
|
2698 |
|
2699 |
|
2700 sorry |
|
2701 (* |
|
2702 |
|
2703 |
|
2704 using as1 apply auto[1] |
|
2705 apply(case_tac list) |
|
2706 apply(simp) |
|
2707 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) |
|
2708 apply(simp only:) |
|
2709 apply(subgoal_tac "flts (map bsimp as1') = map (fuse bs1) (a # aa # lista)") |
|
2710 prefer 2 |
|
2711 apply (metis CTa arexp.distinct(7) as1 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 good.simps(1) good1 k0a map_idI test2) |
|
2712 apply(simp only:) |
|
2713 apply(simp only: bsimp_AALTs.simps) |
|
2714 apply(simp del: bsimp_AALTs.simps bsimp.simps) |
|
2715 apply(subst bsimp_AALTs.simps) |
|
2716 apply(case_tac "flts (map bsimp as2)") |
|
2717 apply(simp) |
|
2718 using as2 apply auto[1] |
|
2719 apply(case_tac listb) |
|
2720 apply(simp) |
|
2721 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) |
|
2722 apply(simp only:) |
|
2723 apply(simp only: bsimp_AALTs.simps) |
|
2724 apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) (ab # ac # listc)") |
|
2725 prefer 2 |
|
2726 apply (metis arexp.distinct(7) as2 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 flts_qq good1 k0a test2) |
|
2727 apply(simp only:) |
|
2728 apply(simp del: bsimp.simps) |
|
2729 by (smt append_Cons bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem k0 k0a list.simps(8) list.simps(9)) |
|
2730 *) |
|
2731 |
|
2732 (* |
|
2733 lemma big: |
|
2734 assumes as1: "(AALTs bs1 as1) = bsimp (AALTs bs1 as1)" |
|
2735 and as2: "(AALTs bs2 as2) = bsimp (AALTs bs2 as2)" |
|
2736 and as1p: "\<exists>as1'. map (fuse bs1) as1 = as1'" |
|
2737 and as2p: "\<exists>as2'. map (fuse bs2) as2 = as2'" |
|
2738 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
|
2739 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
|
2740 apply - |
|
2741 apply(subst as1) |
|
2742 apply(subst as2) |
|
2743 apply(subst (2) bsimp.simps) |
|
2744 apply(subst (2) bsimp.simps) |
|
2745 apply(subst (2) bsimp_idem[symmetric]) |
|
2746 apply(subst (2) bsimp.simps) |
|
2747 using as1p as2p |
|
2748 apply - |
|
2749 apply(erule exE)+ |
|
2750 apply(simp del: bsimp.simps) |
|
2751 apply(simp only: flts_append) |
|
2752 apply(case_tac "flts (map bsimp as1)") |
|
2753 apply(simp) |
|
2754 using as1 apply auto[1] |
|
2755 apply(case_tac list) |
|
2756 apply(simp) |
|
2757 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) |
|
2758 apply(simp only:) |
|
2759 apply(subgoal_tac "flts (map bsimp as1') = map (fuse bs1) (a # aa # lista)") |
|
2760 prefer 2 |
|
2761 apply (metis CTa arexp.distinct(7) as1 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 good.simps(1) good1 k0a map_idI test2) |
|
2762 apply(simp only:) |
|
2763 apply(simp only: bsimp_AALTs.simps) |
|
2764 apply(simp del: bsimp_AALTs.simps bsimp.simps) |
|
2765 apply(subst bsimp_AALTs.simps) |
|
2766 apply(case_tac "flts (map bsimp as2)") |
|
2767 apply(simp) |
|
2768 using as2 apply auto[1] |
|
2769 apply(case_tac listb) |
|
2770 apply(simp) |
|
2771 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) |
|
2772 apply(simp only:) |
|
2773 apply(simp only: bsimp_AALTs.simps) |
|
2774 apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) (ab # ac # listc)") |
|
2775 prefer 2 |
|
2776 apply (metis arexp.distinct(7) as2 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 flts_qq good1 k0a test2) |
|
2777 apply(simp only:) |
|
2778 apply(simp del: bsimp.simps) |
|
2779 by (smt append_Cons bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem k0 k0a list.simps(8) list.simps(9)) |
|
2780 *) |
|
2781 |
2667 |
2782 lemma XXX2a_long_without_good: |
2668 lemma XXX2a_long_without_good: |
2783 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2669 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2784 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
2670 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
2785 apply(case_tac x) |
2671 apply(case_tac x) |