--- a/thys/BitCoded.thy Thu May 23 13:30:09 2019 +0100
+++ b/thys/BitCoded.thy Tue Jun 11 00:26:42 2019 +0100
@@ -623,7 +623,7 @@
shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"
apply(induct rs rule: flts.induct)
apply(simp_all)
- by (metis (mono_tags, lifting) add_mono_thms_linordered_semiring(1) comp_apply fuse_size le_SucI order_refl sum_list_cong)
+ by (metis (mono_tags, lifting) add_mono comp_apply eq_imp_le fuse_size le_SucI map_eq_conv)
lemma bsimp_AALTs_size:
@@ -650,11 +650,6 @@
apply(induct rs)
apply(auto)
by (simp add: add_mono bsimp_size)
-
-
-
-
-
lemma bsimp_AALTs_size2:
assumes "\<forall>r \<in> set rs. nonalt r"
@@ -664,6 +659,7 @@
apply(simp_all add: fuse_size)
done
+
lemma qq:
shows "map (asize \<circ> fuse bs) rs = map asize rs"
apply(induct rs)
@@ -682,7 +678,26 @@
prefer 2
apply (simp add: flts_size le_imp_less_Suc)
using less_Suc_eq by auto
-
+
+lemma bsimp_AALTs_size3:
+ assumes "\<exists>r \<in> set (map bsimp rs). \<not>nonalt r"
+ shows "asize (bsimp (AALTs bs rs)) < asize (AALTs bs rs)"
+ using assms flts_size2
+ apply -
+ apply(clarify)
+ apply(simp)
+ apply(drule_tac x="map bsimp rs" in meta_spec)
+ apply(drule meta_mp)
+ apply (metis list.set_map nonalt.elims(3))
+ apply(simp)
+ apply(rule order_class.order.strict_trans1)
+ apply(rule bsimp_AALTs_size)
+ apply(simp)
+ by (smt Suc_leI bsimp_asize0 comp_def le_imp_less_Suc le_trans map_eq_conv not_less_eq)
+
+
+
+
lemma L_bsimp_ASEQ:
"L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
@@ -929,16 +944,6 @@
apply(simp)
done
-fun spill where
- "spill (AALTs bs rs) = map (fuse bs) rs"
-
-lemma k0a2:
- assumes "\<not> nonalt r"
- shows "flts [r] = spill r"
- using assms
- apply(case_tac r)
- apply(simp_all)
- done
lemma k0b:
assumes "nonalt r" "r \<noteq> AZERO"
@@ -1081,6 +1086,26 @@
apply(simp_all)
done
+
+lemma bsimp_AALTs1:
+ assumes "nonalt r"
+ shows "bsimp_AALTs bs (flts [r]) = fuse bs r"
+ using assms
+ apply(case_tac r)
+ apply(simp_all)
+ done
+
+lemma bbbbs:
+ assumes "good r" "r = AALTs bs1 rs"
+ shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"
+ using assms
+ by (metis (no_types, lifting) Nil_is_map_conv append.left_neutral append_butlast_last_id bsimp_AALTs.elims butlast.simps(2) good.simps(4) good.simps(5) k0a map_butlast)
+
+lemma bbbbs1:
+ shows "nonalt r \<or> (\<exists>bs rs. r = AALTs bs rs)"
+ using nonalt.elims(3) by auto
+
+
lemma good_fuse:
shows "good (fuse bs r) = good r"
apply(induct r arbitrary: bs)
@@ -1678,6 +1703,7 @@
apply (smt b3 bnullable.elims(2) bsimp_ASEQ.simps(17) bsimp_ASEQ.simps(19) bsimp_ASEQ.simps(20) bsimp_ASEQ.simps(21) bsimp_ASEQ.simps(22) bsimp_ASEQ.simps(24) bsimp_ASEQ.simps(25) bsimp_ASEQ.simps(26) bsimp_ASEQ.simps(27) bsimp_ASEQ.simps(29) bsimp_ASEQ.simps(30) bsimp_ASEQ.simps(31))
apply(simp)
apply(simp)
+ thm q3
apply(subst q3[symmetric])
apply simp
using b3 qq4 apply auto[1]
@@ -1840,18 +1866,6 @@
apply(auto)
done
-lemma ZZ0:
- assumes "bsimp a = AALTs bs rs"
- shows "bsimp (bder c a) = AALTs bs (map (bder c) rs)"
- using assms
- apply(induct a arbitrary: rs bs c)
- apply(simp_all)
- apply(auto)[1]
- prefer 2
- apply (metis arexp.distinct(25) arexp.distinct(7) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1)
- prefer 2
- oops
-
lemma ZZZ:
assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> bsimp (bder c (bsimp y)) = bsimp (bder c y)"
@@ -1908,8 +1922,6 @@
apply(subst (asm) (2) bmkeps_simp)
apply (metis b4 bders.simps(2) bders_simp.simps(2) bsimp_idem)
apply (subst (asm) (1) bsimp_idem)
- apply(simp)
- defer
oops
@@ -1932,27 +1944,6 @@
apply(simp)
done
-lemma QQ3:
- assumes "good a"
- shows "bmkeps (bsimp (bders (bsimp a) [c1, c2])) = bmkeps (bders_simp (bsimp a) [c1, c2])"
- using assms
- apply(simp)
-
- oops
-
-lemma QQ4:
- shows "bmkeps (bsimp (bders (bsimp a) [c1, c2, c3])) = bmkeps (bders_simp (bsimp a) [c1, c2, c3])"
- apply(simp)
- oops
-
-lemma QQ3:
- assumes "good a"
- shows "bsimp (bders (bders_simp a s2) s1)= bders_simp a (s1 @ s2)"
- using assms
- apply(induct s2 arbitrary: a s1)
- apply(simp)
- oops
-
lemma XXX2a_long:
assumes "good a"
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
@@ -2000,16 +1991,452 @@
using test2 by fastforce
lemma XXX2a_long_without_good:
+ assumes "a = AALTs bs0 [AALTs bs1 [AALTs bs2 [ASTAR [] (AONE bs7), AONE bs6, ASEQ bs3 (ACHAR bs4 d) (AONE bs5)]]]"
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
- apply(induct a arbitrary: c taking: asize rule: measure_induct)
+ "bsimp (bder c (bsimp a)) = XXX"
+ "bsimp (bder c a) = YYY"
+ using assms
+ apply(simp)
+ using assms
+ apply(simp)
+ prefer 2
+ using assms
+ apply(simp)
+ oops
+
+lemma bder_bsimp_AALTs:
+ shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"
+ apply(induct bs rs rule: bsimp_AALTs.induct)
+ apply(simp)
+ apply(simp)
+ apply (simp add: bder_fuse)
+ apply(simp)
+ done
+
+lemma flts_nothing:
+ assumes "\<forall>r \<in> set rs. r \<noteq> AZERO" "\<forall>r \<in> set rs. nonalt r"
+ shows "flts rs = rs"
+ using assms
+ apply(induct rs rule: flts.induct)
+ apply(auto)
+ done
+
+lemma flts_flts:
+ assumes "\<forall>r \<in> set rs. good r"
+ shows "flts (flts rs) = flts rs"
+ using assms
+ apply(induct rs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
+ apply(case_tac x)
+ apply(simp)
+ apply(simp)
+ apply(case_tac a)
+ apply(simp_all add: bder_fuse flts_append)
+ apply(subgoal_tac "\<forall>r \<in> set x52. r \<noteq> AZERO")
+ prefer 2
+ apply (metis Nil_is_append_conv bsimp_AALTs.elims good.simps(1) good.simps(5) good0 list.distinct(1) n0 nn1b split_list_last test2)
+ apply(subgoal_tac "\<forall>r \<in> set x52. nonalt r")
+ prefer 2
+ apply (metis n0 nn1b test2)
+ by (metis flts_fuse flts_nothing)
+
+lemma "good (bsimp a) \<or> bsimp a = AZERO"
+ by (simp add: good1)
+
+
+lemma
+ assumes "bnullable (bders r s)" "good r"
+ shows "bmkeps (bders (bsimp r) s) = bmkeps (bders r s)"
+ using assms
+ apply(induct s arbitrary: r)
+ apply(simp)
+ using bmkeps_simp apply auto[1]
+ apply(simp)
+ by (simp add: test2)
+
+lemma PP:
+ assumes "bnullable (bders r s)"
+ shows "bmkeps (bders (bsimp r) s) = bmkeps (bders r s)"
+ using assms
+ apply(induct s arbitrary: r)
+ apply(simp)
+ using bmkeps_simp apply auto[1]
+ apply(simp add: bders_append bders_simp_append)
+ oops
+
+lemma PP:
+ assumes "bnullable (bders r s)"
+ shows "bmkeps (bders_simp (bsimp r) s) = bmkeps (bders r s)"
+ using assms
+ apply(induct s arbitrary: r rule: rev_induct)
+ apply(simp)
+ using bmkeps_simp apply auto[1]
+ apply(simp add: bders_append bders_simp_append)
+ apply(drule_tac x="bder a (bsimp r)" in meta_spec)
+ apply(drule_tac meta_mp)
+ defer
+ oops
+
+
+lemma
+ assumes "asize (bsimp a) = asize a" "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]"
+ shows "bsimp a = a"
+ using assms
+ apply(simp)
+ oops
+
+
+lemma iii:
+ assumes "bsimp_AALTs bs rs \<noteq> AZERO"
+ shows "rs \<noteq> []"
+ using assms
+ apply(induct bs rs rule: bsimp_AALTs.induct)
+ apply(auto)
+ done
+
+lemma
+ assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> asize (bsimp y) = asize y \<longrightarrow> bsimp y \<noteq> AZERO \<longrightarrow> bsimp y = y"
+ "asize (bsimp_AALTs x51 (flts (map bsimp x52))) = Suc (sum_list (map asize x52))"
+ "bsimp_AALTs x51 (flts (map bsimp x52)) \<noteq> AZERO"
+ shows "bsimp_AALTs x51 (flts (map bsimp x52)) = AALTs x51 x52"
+ using assms
+ apply(induct x52 arbitrary: x51)
+ apply(simp)
+
+
+
+lemma
+ assumes "asize (bsimp a) = asize a" "bsimp a \<noteq> AZERO"
+ shows "bsimp a = a"
+ using assms
+ apply(induct a taking: asize rule: measure_induct)
+ apply(case_tac x)
+ apply(simp_all)
+ apply(case_tac "(bsimp x42) = AZERO")
+ apply(simp add: asize0)
+ apply(case_tac "(bsimp x43) = AZERO")
+ apply(simp add: asize0)
+ apply (metis bsimp_ASEQ0)
+ apply(case_tac "\<exists>bs. (bsimp x42) = AONE bs")
+ apply(auto)[1]
+ apply (metis b1 bsimp_size fuse_size less_add_Suc2 not_less)
+ apply (metis Suc_inject add.commute asize.simps(5) bsimp_ASEQ1 bsimp_size leD le_neq_implies_less less_add_Suc2 less_add_eq_less)
+ (* ALT case *)
+ apply(frule iii)
+ apply(case_tac x52)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(subst (asm) k0)
+ apply(subst (asm) (2) k0)
+ apply(subst (asm) (3) k0)
+ apply(case_tac "(bsimp a) = AZERO")
+ apply(simp)
+ apply (metis (no_types, lifting) Suc_le_lessD asize0 bsimp_AALTs_size le_less_trans less_add_same_cancel2 not_less_eq rt)
+ apply(simp)
+ apply(case_tac "nonalt (bsimp a)")
+ prefer 2
+ apply(drule_tac x="AALTs x51 (bsimp a # list)" in spec)
+ apply(drule mp)
+ apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
+ apply(drule mp)
+ apply(simp)
+ apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 lessI list.set_intros(1) list.simps(9) not_less_eq sum_list.Cons)
+ apply(drule mp)
+ apply(simp)
+ using bsimp_idem apply auto[1]
+ apply(simp add: bsimp_idem)
+ apply (metis append.left_neutral append_Cons asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k00 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
+ apply (metis bsimp.simps(2) bsimp_idem k0 list.simps(9) nn1b nonalt.elims(3) nonnested.simps(2))
+ apply(subgoal_tac "flts [bsimp a] = [bsimp a]")
+ prefer 2
+ using k0b apply blast
+ apply(clarify)
+ apply(simp only:)
+ apply(simp)
+ apply(case_tac "flts (map bsimp list) = Nil")
+ apply (metis bsimp_AALTs1 bsimp_size fuse_size less_add_Suc1 not_less)
+ apply (subgoal_tac "bsimp_AALTs x51 (bsimp a # flts (map bsimp list)) = AALTs x51 (bsimp a # flts (map bsimp list))")
+ prefer 2
+ apply (metis bsimp_AALTs.simps(3) neq_Nil_conv)
+ apply(auto)
+ apply (metis add.commute bsimp_size leD le_neq_implies_less less_add_Suc1 less_add_eq_less rt)
+
+ apply(drule_tac x="AALTs x51 list" in spec)
+ apply(drule mp)
+ apply(auto simp add: asize0)[1]
+
+
+
+(* HERE*)
+
+
+
+
+
+lemma OOO:
+ shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
+ apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
+ apply(case_tac x)
+ apply(simp)
+ apply(simp)
+ apply(case_tac "a = AZERO")
+ apply(simp)
+ apply(case_tac "list")
+ apply(simp)
+ apply(simp)
+ apply(case_tac "bsimp a = AZERO")
+ apply(simp)
+ apply(case_tac "list")
+ apply(simp)
+ apply(simp add: bsimp_fuse[symmetric])
+ apply(simp)
+ apply(case_tac "nonalt (bsimp a)")
+ apply(case_tac list)
+ apply(simp)
+ apply(subst k0b)
+ apply(simp)
+ apply(simp)
+ apply(simp add: bsimp_fuse)
+ apply(simp)
+ apply(subgoal_tac "asize (bsimp a) < asize a \<or> asize (bsimp a) = asize a")
+ prefer 2
+ using bsimp_size le_neq_implies_less apply blast
+ apply(erule disjE)
+ apply(drule_tac x="(bsimp a) # list" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply(simp)
+ apply (metis bsimp.simps(2) bsimp_AALTs.elims bsimp_AALTs.simps(2) bsimp_fuse bsimp_idem list.distinct(1) list.inject list.simps(9))
+ apply(subgoal_tac "\<exists>bs rs. bsimp a = AALTs bs rs \<and> rs \<noteq> Nil \<and> length rs > 1")
+ prefer 2
+ apply (metis bbbbs1 bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) good.simps(5) good1 length_0_conv length_Suc_conv less_one list.simps(8) nat_neq_iff not_less_eq)
+ apply(auto)
+ sledgehammer [timeout=6000]
+
+
+
+
+ defer
+ apply(case_tac list)
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply (simp add: bsimp_fuse bsimp_idem)
+ apply(case_tac a)
+ apply(simp_all)
+
+
+ apply(subst k0b)
+ apply(simp)
+ apply(subst (asm) k0)
+ apply(subst (asm) (2) k0)
+
+
+ find_theorems "asize _ < asize _"
+ using bsimp_AALTs_size3
+ apply -
+ apply(drule_tac x="a # list" in meta_spec)
+ apply(drule_tac x="bs" in meta_spec)
+ apply(drule meta_mp)
+ apply(simp)
+ apply(simp)
+ apply(drule_tac x="(bsimp a) # list" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply(subst (asm) k0)
+ apply(subst (asm) (2) k0)
+ thm k0
+ apply(subst (asm) k0b)
+ apply(simp)
+ apply(simp)
+
+ defer
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ defer
+ apply(simp)
+ find_theorems "asize _ < asize _"
+ find_theorems "asize _ < asize _"
+apply(subst k0b)
+ apply(simp)
+ apply(simp)
+
+
+ apply(rule nn11a)
+ apply(simp)
+ apply (metis good.simps(1) good1 good_fuse)
+ apply(simp)
+ using fuse_append apply blast
+ apply(subgoal_tac "\<exists>bs rs. bsimp x43 = AALTs bs rs")
+ prefer 2
+ using nonalt.elims(3) apply blast
+ apply(clarify)
+ apply(simp)
+ apply(case_tac rs)
+ apply(simp)
+ apply (metis arexp.distinct(7) good.simps(4) good1)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ apply (metis arexp.distinct(7) good.simps(5) good1)
+ apply(simp)
+
+
+
+
+
+
+ find_theorems "flts [_] = [_]"
+ apply(case_tac x52)
+ apply(simp)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ apply(case_tac a)
+ apply(simp_all)
+
+
+lemma XXX2a_long_without_good:
+ shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+ apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
apply(case_tac x)
apply(simp)
apply(simp)
apply(simp)
prefer 3
apply(simp)
+ (* AALT case *)
+ prefer 2
+ apply(simp only:)
apply(simp)
- apply(auto)[1]
+ apply(subst bder_bsimp_AALTs)
+ apply(case_tac x52)
+ apply(simp)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+
+ apply(case_tac "\<exists>r \<in> set (map bsimp x52). \<not>nonalt r")
+ apply(drule_tac x="bsimp (AALTs x51 x52)" in spec)
+ apply(drule mp)
+ using bsimp_AALTs_size3 apply blast
+ apply(drule_tac x="c" in spec)
+ apply(subst (asm) (2) test)
+
+ apply(case_tac x52)
+ apply(simp)
+ apply(simp)
+ apply(case_tac "bsimp a = AZERO")
+ apply(simp)
+ apply(subgoal_tac "bsimp (bder c a) = AZERO")
+ prefer 2
+ apply auto[1]
+ apply (metis L.simps(1) L_bsimp_erase der.simps(1) der_correctness erase.simps(1) erase_bder xxx_bder2)
+ apply(simp)
+ apply(drule_tac x="AALTs x51 list" in spec)
+ apply(drule mp)
+ apply(simp add: asize0)
+ apply(simp)
+ apply(case_tac list)
+ prefer 2
+ apply(simp)
+ apply(case_tac "bsimp aa = AZERO")
+ apply(simp)
+ apply(subgoal_tac "bsimp (bder c aa) = AZERO")
+ prefer 2
+ apply auto[1]
+ apply (metis add.left_commute bder.simps(1) bsimp.simps(3) less_add_Suc1)
+ apply(simp)
+ apply(drule_tac x="AALTs x51 (a#lista)" in spec)
+ apply(drule mp)
+ apply(simp add: asize0)
+ apply(simp)
+ apply (metis flts.simps(2) k0)
+ apply(subst k0)
+ apply(subst (2) k0)
+
+
+ using less_add_Suc1 apply fastforce
+ apply(subst k0)
+
+
+ apply(simp)
+ apply(case_tac "bsimp a = AZERO")
+ apply(simp)
+ apply(subgoal_tac "bsimp (bder c a) = AZERO")
+ prefer 2
+ apply auto[1]
+ apply(simp)
+ apply(case_tac "nonalt (bsimp a)")
+ apply(subst bsimp_AALTs1)
+ apply(simp)
+ using less_add_Suc1 apply fastforce
+
+ apply(subst bsimp_AALTs1)
+
+ using nn11a apply b last
+
+ (* SEQ case *)
+ apply(clarify)
+ apply(subst bsimp.simps)
+ apply(simp del: bsimp.simps)
+ apply(auto simp del: bsimp.simps)[1]
+ apply(subgoal_tac "bsimp x42 \<noteq> AZERO")
+ prefer 2
+ using b3 apply force
+ apply(case_tac "bsimp x43 = AZERO")
+ apply(simp)
+ apply (simp add: bsimp_ASEQ0)
+ apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) less_add_Suc2)
+ apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
+ apply(clarify)
+ apply(simp)
+ apply(subst bsimp_ASEQ2)
+ apply(subgoal_tac "bsimp (bder c x42) = AZERO")
+ prefer 2
+ using less_add_Suc1 apply fastforce
+ apply(simp)
+ apply(frule_tac x="x43" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply(drule_tac x="c" in spec)
+ apply(subst bder_fuse)
+ apply(subst bsimp_fuse[symmetric])
+ apply(simp)
+ apply(subgoal_tac "bmkeps x42 = bs")
+ prefer 2
+ apply (simp add: bmkeps_simp)
+ apply(simp)
+ apply(subst bsimp_fuse[symmetric])
+ apply(case_tac "nonalt (bsimp (bder c x43))")
+ apply(subst bsimp_AALTs1)
+ using nn11a apply blast
+ using fuse_append apply blast
+ apply(subgoal_tac "\<exists>bs rs. bsimp (bder c x43) = AALTs bs rs")
+ prefer 2
+ using bbbbs1 apply blast
+ apply(clarify)
+ apply(simp)
+ apply(case_tac rs)
+ apply(simp)
+ apply (metis arexp.distinct(7) good.simps(4) good1)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ apply (metis arexp.distinct(7) good.simps(5) good1)
+ apply(simp del: bsimp_AALTs.simps)
+ apply(simp only: bsimp_AALTs.simps)
+ apply(simp)
+
+
+
+
+(* HERE *)
apply(case_tac "x42 = AZERO")
apply(simp)
apply(case_tac "bsimp x43 = AZERO")
@@ -2017,7 +2444,7 @@
apply (simp add: bsimp_ASEQ0)
apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO")
apply(simp)
- apply (metis bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2)
+ apply (met is bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2)
apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
apply(clarify)
apply(simp)
@@ -2067,7 +2494,7 @@
apply(subst bsimp_fuse[symmetric])
apply(subgoal_tac "bsimp (bder c (bsimp x43)) = bsimp (bder c x43)")
prefer 2
- using less_add_Suc2 apply blast
+ using less_add_Suc2 apply bl ast
apply(simp only: )
apply(subst bsimp_fuse[symmetric])
apply(simp only: )
@@ -2080,7 +2507,7 @@
apply(simp)
apply(case_tac list)
apply(simp)
- apply (metis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse)
+ apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse)
apply(simp only: bsimp_AALTs.simps map_cons.simps)
apply(auto)[1]
@@ -2095,7 +2522,7 @@
apply(simp)
using b3 apply force
- using bsimp_ASEQ0 test2 apply force
+ using bsimp_ASEQ0 test2 apply fo rce
thm good_SEQ test2
apply (simp add: good_SEQ test2)
apply (simp add: good_SEQ test2)
@@ -2109,13 +2536,13 @@
apply(simp)
apply(subst bsimp_ASEQ1)
apply(simp)
- using bsimp_ASEQ0 test2 apply force
+ using bsimp_ASEQ0 test2 apply fo rce
apply (simp add: good_SEQ test2)
apply (simp add: good_SEQ test2)
apply (simp add: good_SEQ test2)
(* AALTs case *)
apply(simp)
- using test2 by fastforce
+ using test2 by fa st force
lemma XXX4ab: