3008 apply(subst k0) |
3008 apply(subst k0) |
3009 apply(subst WWW3) |
3009 apply(subst WWW3) |
3010 apply(simp add: flts_append) |
3010 apply(simp add: flts_append) |
3011 done |
3011 done |
3012 |
3012 |
|
3013 lemma hardest: |
|
3014 shows "bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]))) = |
|
3015 bsimp (AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2)))" |
|
3016 apply(case_tac "bsimp a1") |
|
3017 apply(case_tac "bsimp a2") |
|
3018 apply simp |
|
3019 apply simp |
|
3020 apply(rule_tac t="bsimp a1" |
|
3021 and s="AZERO" in subst) |
|
3022 apply simp |
|
3023 apply(rule_tac t="bsimp a2" |
|
3024 and s="ACHAR x31 x32" in subst) |
|
3025 apply simp |
|
3026 apply simp |
|
3027 apply(rule_tac t="bsimp a1" |
|
3028 and s="AZERO" in subst) |
|
3029 apply simp |
|
3030 apply(rule_tac t="bsimp a2" |
|
3031 and s="ASEQ x41 x42 x43" in subst) |
|
3032 apply simp |
|
3033 apply(case_tac "bnullable x42") |
|
3034 apply(simp only: bder.simps) |
|
3035 apply(simp) |
|
3036 apply(case_tac "flts |
|
3037 [bsimp_ASEQ [] (bsimp (bder c x42)) (bsimp x43), |
|
3038 bsimp (fuse (bmkeps x42) (bder c x43))]") |
|
3039 apply(simp) |
|
3040 apply simp |
|
3041 (*counterexample finder*) |
|
3042 |
|
3043 |
3013 lemma XXX2a_long_without_good: |
3044 lemma XXX2a_long_without_good: |
3014 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
3045 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
3015 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
3046 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
3016 apply(case_tac x) |
3047 apply(case_tac x) |
3017 apply(simp) |
3048 apply(simp) |