--- a/thys2/SizeBound.thy Tue Dec 14 16:06:42 2021 +0000
+++ b/thys2/SizeBound.thy Tue Dec 14 16:17:45 2021 +0000
@@ -859,18 +859,6 @@
apply(simp_all)
done
-
-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
-
-
-
inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
where
"ASEQ bs AZERO r2 \<leadsto> AZERO"
@@ -880,8 +868,8 @@
| "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
| "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))"
(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
-| "AALTs bs (rsa@AZERO # rsb) \<leadsto> AALTs bs (rsa@rsb)"
-| "AALTs bs (rsa@(AALTs bs1 rs1)# rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)"
+| "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)"
+| "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)"
(*the below rule for extracting common prefixes between a list of rexp's bitcodes*)
(***| "AALTs bs (map (fuse bs1) rs) \<leadsto> AALTs (bs@bs1) rs"******)
(*opposite direction also allowed, which means bits are free to be moved around
@@ -1053,7 +1041,7 @@
lemma rrewrite0away: "AALTs bs (AZERO # rsb) \<leadsto> AALTs bs rsb"
- by (metis append_Nil rrewrite.intros(7))
+ by (metis append_Cons append_Nil rrewrite.intros(7))
lemma frewritesaalts:"rs f\<leadsto>* rs' \<Longrightarrow> (AALTs bs (rs1@rs)) \<leadsto>* (AALTs bs (rs1@rs'))"
@@ -1063,12 +1051,12 @@
apply(drule_tac x = "rs1 @ [AZERO]" in meta_spec)
apply(rule real_trans)
apply simp
- using r_in_rstar rrewrite.intros(7) apply presburger
+ using rrewrite.intros(7) apply auto[1]
apply(drule_tac x = "bsa" in meta_spec)
apply(drule_tac x = "rs1a @ [AALTs bs rs1]" in meta_spec)
apply(rule real_trans)
apply simp
- using r_in_rstar rrewrite.intros(8) apply presburger
+ using r_in_rstar rrewrite.intros(8) apply auto[1]
apply(drule_tac x = "bs" in meta_spec)
apply(drule_tac x = "rs1@[r]" in meta_spec)
apply(rule real_trans)
@@ -1080,9 +1068,7 @@
apply(induction rs)
apply simp
apply(case_tac "a = AZERO")
- apply (metis append_Nil flts.simps(2) many_steps_later rrewrite.intros(7))
-
-
+ apply (metis flts.simps(2) many_steps_later rrewrite0away)
apply(case_tac "\<exists>bs2 rs2. a = AALTs bs2 rs2")
apply(erule exE)+
@@ -1317,10 +1303,7 @@
using r2 apply blast
apply (metis list.set_intros(1))
- apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 bnullable.simps(4) rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
-
-
- thm qq1
+ apply (metis append_Nil bnullable.simps(1) rewrite_non_nullable_strong rrewrite.intros(10) spillbmkepslistr third_segment_bmkeps)
apply(subgoal_tac "bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ")
prefer 2
@@ -1352,8 +1335,7 @@
apply blast
apply (simp add: flts_append qs3)
-
- apply (meson rewrite_bmkepsalt)
+ apply (simp add: rewrite_bmkepsalt)
using q3a apply force
apply (simp add: q3a)
@@ -1437,13 +1419,11 @@
using contextrewrites2 r_in_rstar apply auto[1]
- apply (simp add: r_in_rstar rrewrite.intros(7))
-
using rrewrite.intros(8) apply auto[1]
-
- apply (metis append_assoc r_in_rstar rrewrite.intros(9))
-
- apply (metis r_in_rstar rrewrite.intros(10))
+ using rrewrite.intros(7) apply auto[1]
+ using rrewrite.intros(8) apply force
+ apply (metis append_assoc r_in_rstar rrewrite.intros(9))
+ apply (simp add: r_in_rstar rrewrite.intros(10))
apply (metis fuse_append r_in_rstar rrewrite.intros(11))
using rrewrite.intros(12) by auto
@@ -1465,12 +1445,8 @@
lemma rewrite_der_altmiddle: "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
apply simp
- apply(simp add: bder_fuse_list)
- apply(rule many_steps_later)
- apply(subst rrewrite.intros(8))
- apply simp
-
- by fastforce
+ apply(simp add: bder_fuse_list del: append.simps)
+ by (metis append.assoc map_map r_in_rstar rrewrite.intros(8) threelistsappend)
lemma lock_step_der_removal:
shows " erase a1 = erase a2 \<Longrightarrow>