equal
deleted
inserted
replaced
2654 lemma WWW4: |
2654 lemma WWW4: |
2655 shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)" |
2655 shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)" |
2656 apply(induct as1) |
2656 apply(induct as1) |
2657 apply(auto) |
2657 apply(auto) |
2658 using bder_fuse by blast |
2658 using bder_fuse by blast |
2659 |
2659 |
|
2660 lemma WWW5: |
|
2661 shows "map (bsimp \<circ> bder c) as1 = map bsimp (map (bder c) as1)" |
|
2662 apply(induct as1) |
|
2663 apply(auto) |
|
2664 done |
2660 |
2665 |
2661 lemma big0: |
2666 lemma big0: |
2662 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
2667 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
2663 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
2668 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
2664 by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append) |
2669 by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append) |
2665 |
2670 |
2666 |
2671 lemma bignA: |
|
2672 shows "bsimp (AALTs x51 (AALTs bs1 as1 # as2)) = |
|
2673 bsimp (AALTs x51 ((map (fuse bs1) as1) @ as2))" |
|
2674 apply(simp) |
|
2675 apply(subst k0) |
|
2676 apply(subst WWW3) |
|
2677 apply(simp add: flts_append) |
|
2678 done |
2667 |
2679 |
2668 lemma XXX2a_long_without_good: |
2680 lemma XXX2a_long_without_good: |
2669 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2681 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2670 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
2682 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
2671 apply(case_tac x) |
2683 apply(case_tac x) |
2673 apply(simp) |
2685 apply(simp) |
2674 apply(simp) |
2686 apply(simp) |
2675 prefer 3 |
2687 prefer 3 |
2676 apply(simp) |
2688 apply(simp) |
2677 (* AALT case *) |
2689 (* AALT case *) |
2678 prefer 2 |
2690 prefer 2 |
|
2691 apply(simp only:) |
|
2692 (* *) |
|
2693 apply(simp) |
|
2694 apply(subst WWW5) |
|
2695 |
|
2696 |
|
2697 |
|
2698 |
2679 apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]") |
2699 apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]") |
2680 apply(clarify) |
2700 apply(clarify) |
2681 apply(simp del: bsimp.simps) |
2701 apply(simp del: bsimp.simps) |
2682 apply(subst (2) CT1) |
2702 apply(subst (2) CT1) |
2683 apply(simp del: bsimp.simps) |
2703 apply(simp del: bsimp.simps) |