
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) \<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




