# HG changeset patch
# User Chengsong
# Date 1639498665 0
# Node ID 28458dec90f8678d95247d53c357d884971a5f81
# Parent  ee53acaf24205f778949891875f0f59f2dfcf857# Parent  a8b4d8593bdb56e9e2537af7345cb5f15bacfc2b
merged

diff -r ee53acaf2420 -r 28458dec90f8 thys2/SizeBound.thy
--- 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>