--- a/thys2/SizeBound.thy Thu Nov 04 09:45:41 2021 +0000
+++ b/thys2/SizeBound.thy Thu Nov 04 13:31:17 2021 +0000
@@ -883,7 +883,7 @@
| "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"
+(***| "AALTs bs (map (fuse bs1) rs) \<leadsto> AALTs (bs@bs1) rs"******)
(*opposite direction also allowed, which means bits are free to be moved around
as long as they are on the right path*)
| "AALTs (bs@bs1) rs \<leadsto> AALTs bs (map (fuse bs1) rs)"
@@ -1002,10 +1002,11 @@
apply(induction rs)
apply simp
apply(rule r_in_rstar)
- apply(simp add: rrewrite.intros(11))
+ apply (simp add: rrewrite.intros(10))
apply(case_tac "rs = Nil")
apply(simp)
using rrewrite.intros(12) apply auto[1]
+ using r_in_rstar rrewrite.intros(11) apply presburger
apply(subgoal_tac "length (a#rs) > 1")
apply(simp add: bsimp_AALTs_qq)
apply(simp)
@@ -1143,7 +1144,7 @@
(erase `
(set rs1 \<union> set rs2)))) ")
prefer 2
- using rrewrite.intros(13) apply force
+ using rrewrite.intros(12) apply force
using r_in_rstar apply force
apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)")
prefer 2
@@ -1155,7 +1156,7 @@
apply(subgoal_tac "AALTs bs (rsa @ a # distinctBy rs erase (insert (erase a) (erase ` set rsa))) \<leadsto>
AALTs bs (rsa @ distinctBy rs erase (insert (erase a) (erase ` set rsa)))")
apply force
- apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(13) same_append_eq somewhereMapInside)
+ apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(12) same_append_eq somewhereMapInside)
by force
@@ -1323,13 +1324,12 @@
apply(subgoal_tac "bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ")
prefer 2
- apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(11) third_segment_bmkeps)
-
- by (metis bnullable.simps(4) rewrite_non_nullable rrewrite.intros(10) third_segment_bmkeps)
+ apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(10) third_segment_bmkeps)
+ by (metis bnullable.simps(4) rewrite_non_nullable_strong rrewrite.intros(9) third_segment_bmkeps)
-lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; (bnullable r1)\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2"
+lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; bnullable r1\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2"
apply(frule rewrite_nullable)
apply simp
@@ -1354,16 +1354,37 @@
apply (simp add: flts_append qs3)
apply (meson rewrite_bmkepsalt)
-
- using bnullable.simps(4) q3a apply blast
+ using q3a apply force
apply (simp add: q3a)
-
- using bnullable.simps(1) apply blast
-
apply (simp add: b2)
-
- by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 bnullable.simps(4) set_append)
+ apply(simp del: append.simps)
+ apply(case_tac "bnullable a1")
+ apply (metis append.assoc in_set_conv_decomp qq1)
+ apply(case_tac "\<exists>r \<in> set rsa. bnullable r")
+ using qq1 apply presburger
+ apply(case_tac "\<exists>r \<in> set rsb. bnullable r")
+ apply (metis UnCI append.assoc qq1 set_append)
+ apply(case_tac "bnullable a2")
+ apply (metis bnullable_correctness)
+ apply(subst qq2)
+ apply blast
+ apply(auto)[1]
+ apply(subst qq2)
+ apply (metis empty_iff list.set(1) set_ConsD)
+ apply(auto)[1]
+ apply(subst qq2)
+ apply(auto)[2]
+ apply(subst qq2)
+ apply(auto)[2]
+ apply(subst qq2)
+ apply(auto)[2]
+ apply(subst qq2)
+ apply(auto)[2]
+ apply(subst qq2)
+ apply(auto)[2]
+ apply(simp)
+ done
lemma rewrites_bmkeps:
assumes "r1 \<leadsto>* r2" "bnullable r1"
@@ -1422,14 +1443,9 @@
apply (metis append_assoc r_in_rstar rrewrite.intros(9))
- apply (metis append_assoc r_in_rstar rrewrite.intros(10))
-
- apply (simp add: r_in_rstar rrewrite.intros(11))
-
- apply (metis fuse_append r_in_rstar rrewrite.intros(12))
-
- using rrewrite.intros(13) by auto
-
+ apply (metis r_in_rstar rrewrite.intros(10))
+ apply (metis fuse_append r_in_rstar rrewrite.intros(11))
+ using rrewrite.intros(12) by auto
lemma rewrites_fuse:
@@ -1462,7 +1478,7 @@
bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
apply(simp)
- using rrewrite.intros(13) by auto
+ using rrewrite.intros(12) by auto
lemma rewrite_after_der: "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
apply(induction r1 r2 arbitrary: c rule: rrewrite.induct)
@@ -1470,14 +1486,14 @@
apply (simp add: r_in_rstar rrewrite.intros(1))
apply simp
- apply (meson contextrewrites1 r_in_rstar rrewrite.intros(11) rrewrite.intros(2) rrewrite0away rs2)
+ apply (meson contextrewrites1 r_in_rstar rrewrite.intros(10) rrewrite.intros(2) rrewrite0away rs2)
apply(simp)
apply(rule many_steps_later)
apply(rule to_zero_in_alt)
apply(rule many_steps_later)
apply(rule alt_remove0_front)
apply(rule many_steps_later)
- apply(rule rrewrite.intros(12))
+ apply(rule rrewrite.intros(11))
using bder_fuse fuse_append rs1 apply presburger
apply(case_tac "bnullable r1")
prefer 2
@@ -1513,12 +1529,10 @@
using rewrite_der_altmiddle apply auto[1]
apply (metis bder.simps(4) bder_fuse_list map_map r_in_rstar rrewrite.intros(9))
-
- apply (metis List.map.compositionality bder.simps(4) bder_fuse_list r_in_rstar rrewrite.intros(10))
+ apply (simp add: r_in_rstar rrewrite.intros(10))
- apply (simp add: r_in_rstar rrewrite.intros(11))
-
- apply (metis bder.simps(4) bder_bsimp_AALTs bsimp_AALTs.simps(2) bsimp_AALTsrewrites)
+ apply (simp add: r_in_rstar rrewrite.intros(10))
+ using bder_fuse r_in_rstar rrewrite.intros(11) apply presburger
using lock_step_der_removal by auto