equal
deleted
inserted
replaced
3619 apply simp |
3619 apply simp |
3620 apply(drule in1) |
3620 apply(drule in1) |
3621 apply(subgoal_tac "rsX \<noteq> []") |
3621 apply(subgoal_tac "rsX \<noteq> []") |
3622 prefer 2 |
3622 prefer 2 |
3623 apply (metis arexp.distinct(7) good.simps(4) good1) |
3623 apply (metis arexp.distinct(7) good.simps(4) good1) |
3624 apply(subgoal_tac "\<exists>XX. XX \<in> set rsX") |
3624 by (metis contains0 contains49 f_cont1 in2 list.exhaust list.set_intros(1)) |
3625 prefer 2 |
|
3626 using neq_Nil_conv apply fastforce |
|
3627 apply(erule exE) |
|
3628 apply(rule_tac x="fuse bsX XX" in bexI) |
|
3629 prefer 2 |
|
3630 apply blast |
|
3631 apply(frule f_cont1) |
|
3632 apply(auto) |
|
3633 apply(rule contains0) |
|
3634 apply(drule contains49) |
|
3635 by (simp add: in2) |
|
3636 |
3625 |
3637 lemma CONTAINS1: |
3626 lemma CONTAINS1: |
3638 assumes "a >> bs" |
3627 assumes "a >> bs" |
3639 shows "a >>2 bs" |
3628 shows "a >>2 bs" |
3640 using assms |
3629 using assms |
3798 |
3787 |
3799 lemma COUNTEREXAMPLE: |
3788 lemma COUNTEREXAMPLE: |
3800 assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]" |
3789 assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]" |
3801 shows "bsimp r = XXX" |
3790 shows "bsimp r = XXX" |
3802 and "bder c r = XXX" |
3791 and "bder c r = XXX" |
|
3792 and "bder c (bsimp r) = XXX" |
3803 and "bsimp (bder c (bsimp r)) = XXX" |
3793 and "bsimp (bder c (bsimp r)) = XXX" |
3804 and "bsimp (bder c r) = XXX" |
3794 and "bsimp (bder c r) = XXX" |
3805 apply(simp_all add: assms) |
3795 apply(simp_all add: assms) |
3806 oops |
3796 oops |
3807 |
3797 |