diff -r 98362002c818 -r f83271c585d2 thys2/SizeBound.thy --- 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) \ AALTs bs (rsa@rsb)" | "AALTs bs (rsa@(AALTs bs1 rs1)# rsb) \ 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) \ AALTs (bs@bs1) rs" +(***| "AALTs bs (map (fuse bs1) rs) \ 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 \ 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 \ 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))) \ 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: "\ r1 \ r2; (bnullable r1)\ \ bmkeps r1 = bmkeps r2" +lemma rewrite_bmkeps: "\ r1 \ r2; bnullable r1\ \ 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 "\r \ set rsa. bnullable r") + using qq1 apply presburger + apply(case_tac "\r \ 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 \* 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 \ r2 \ (bder c r1) \* (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