equal
deleted
inserted
replaced
2628 apply(simp) |
2628 apply(simp) |
2629 apply(auto) |
2629 apply(auto) |
2630 by (metis bsimp_fuse flts_fuse k0 list.simps(9)) |
2630 by (metis bsimp_fuse flts_fuse k0 list.simps(9)) |
2631 |
2631 |
2632 |
2632 |
|
2633 lemma flts_nonalt: |
|
2634 assumes "flts (map bsimp xs) = ys" |
|
2635 shows "\<forall>y \<in> set ys. nonalt y" |
|
2636 using assms |
|
2637 apply(induct xs arbitrary: ys) |
|
2638 apply(auto) |
|
2639 apply(case_tac xs) |
|
2640 apply(auto) |
|
2641 using flts2 good1 apply fastforce |
|
2642 by (smt ex_map_conv list.simps(9) nn1b nn1c) |
2633 |
2643 |
2634 lemma big0: |
2644 lemma big0: |
2635 assumes as1p: "\<exists>as1'. map (fuse bs1) as1 = as1'" |
2645 assumes as1p: "\<exists>as1'. map (fuse bs1) as1 = as1'" |
2636 and as2p: "\<exists>as2'. map (fuse bs2) as2 = as2'" |
2646 and as2p: "\<exists>as2'. map (fuse bs2) as2 = as2'" |
2637 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
2647 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
2662 apply(case_tac list) |
2672 apply(case_tac list) |
2663 apply(simp) |
2673 apply(simp) |
2664 apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) [a]") |
2674 apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) [a]") |
2665 prefer 2 |
2675 prefer 2 |
2666 using YY apply blast |
2676 using YY apply blast |
2667 apply(simp) |
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) |
2668 (* HERE TODAY *) |
2697 (* HERE TODAY *) |
2669 |
2698 |
2670 |
2699 |
2671 sorry |
2700 sorry |
2672 (* |
2701 (* |