--- a/thys2/SizeBound4.thy	Sat Jan 22 22:57:28 2022 +0000
+++ b/thys2/SizeBound4.thy	Tue Jan 25 13:12:50 2022 +0000
@@ -937,7 +937,7 @@
   by (metis bnullable_correctness)
 
 
-lemma rewritesnullable: 
+lemma rewrites_bnullable_eq: 
   assumes "r1 \<leadsto>* r2" 
   shows "bnullable r1 = bnullable r2"
 using assms 
@@ -946,25 +946,34 @@
   using bnullable0(1) by auto
 
 lemma rewrite_bmkeps_aux: 
-  shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)"
-  and   "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)" 
+  shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 \<Longrightarrow> bmkeps r1 = bmkeps r2"
+  and   "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 \<Longrightarrow> bmkepss rs1 = bmkepss rs2" 
 proof (induct rule: rrewrite_srewrite.inducts)
   case (bs3 bs1 bs2 r)
-  then show ?case by (simp add: bmkeps_fuse) 
+  have IH2: "bnullable (ASEQ bs1 (AONE bs2) r)" by fact
+  then show "bmkeps (ASEQ bs1 (AONE bs2) r) = bmkeps (fuse (bs1 @ bs2) r)"
+    by (simp add: bmkeps_fuse)
 next
   case (bs7 bs r)
-  then show ?case by (simp add: bmkeps_fuse) 
+  have IH2: "bnullable (AALTs bs [r])" by fact
+  then show "bmkeps (AALTs bs [r]) = bmkeps (fuse bs r)" 
+    by (simp add: bmkeps_fuse)
 next
   case (ss3 r1 r2 rs)
-  then show ?case
-    by (metis bmkepss.simps(2) bnullable0(1))
+  have IH1: "bnullable r1 \<Longrightarrow> bmkeps r1 = bmkeps r2" by fact
+  have as: "r1 \<leadsto> r2" by fact
+  from IH1 as show "bmkepss (r1 # rs) = bmkepss (r2 # rs)"
+    by (simp add: bnullable0)
 next
   case (ss5 bs1 rs1 rsb)
-  then show ?case
+  have "bnullables (AALTs bs1 rs1 # rsb)" by fact
+  then show "bmkepss (AALTs bs1 rs1 # rsb) = bmkepss (map (fuse bs1) rs1 @ rsb)"
     by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)
 next
   case (ss6 a1 a2 rsa rsb rsc)
-  then show ?case
+  have as1: "erase a1 = erase a2" by fact
+  have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact
+  show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3
     by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness)
 qed (auto)
 
@@ -981,7 +990,7 @@
   have a1: "bnullable r1" by fact
   have a2: "r1 \<leadsto>* r2" by fact
   have a3: "r2 \<leadsto> r3" by fact
-  have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable) 
+  have a4: "bnullable r2" using a1 a2 by (simp add: rewrites_bnullable_eq) 
   then have "bmkeps r2 = bmkeps r3"
     using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast 
   then show "bmkeps r1 = bmkeps r3" using IH by simp
@@ -1047,23 +1056,22 @@
 
 
 lemma rewrite_preserves_bder: 
-  shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
+  shows "r1 \<leadsto> r2 \<Longrightarrow> bder c r1 \<leadsto>* bder c r2"
   and   "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"
 proof(induction rule: rrewrite_srewrite.inducts)
   case (bs1 bs r2)
-  then show ?case
+  show "bder c (ASEQ bs AZERO r2) \<leadsto>* bder c AZERO"
     by (simp add: continuous_rewrite) 
 next
   case (bs2 bs r1)
-  then show ?case 
+  show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO"
     apply(auto)
     apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2)
     by (simp add: r_in_rstar rrewrite_srewrite.bs2)
 next
   case (bs3 bs1 bs2 r)
-  then show ?case 
+  show "bder c (ASEQ bs1 (AONE bs2) r) \<leadsto>* bder c (fuse (bs1 @ bs2) r)"
     apply(simp)
-    
     by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
 next
   case (bs4 r1 r2 bs r3)
@@ -1082,41 +1090,45 @@
     using star_seq2 by blast
 next
   case (bs6 bs)
-  then show ?case
+  show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"
     using rrewrite_srewrite.bs6 by force 
 next
   case (bs7 bs r)
-  then show ?case
+  show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
     by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) 
 next
   case (bs10 rs1 rs2 bs)
-  then show ?case
+  have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact
+  then show "bder c (AALTs bs rs1) \<leadsto>* bder c (AALTs bs rs2)" 
     using contextrewrites0 by force    
 next
   case ss1
-  then show ?case by simp
+  show "map (bder c) [] s\<leadsto>* map (bder c) []" by simp
 next
   case (ss2 rs1 rs2 r)
-  then show ?case
+  have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact
+  then show "map (bder c) (r # rs1) s\<leadsto>* map (bder c) (r # rs2)"
     by (simp add: srewrites7) 
 next
   case (ss3 r1 r2 rs)
-  then show ?case
+  have IH: "bder c r1 \<leadsto>* bder c r2" by fact
+  then show "map (bder c) (r1 # rs) s\<leadsto>* map (bder c) (r2 # rs)"
     by (simp add: srewrites7) 
 next
   case (ss4 rs)
-  then show ?case
+  show "map (bder c) (AZERO # rs) s\<leadsto>* map (bder c) rs"
     using rrewrite_srewrite.ss4 by fastforce 
 next
   case (ss5 bs1 rs1 rsb)
-  then show ?case 
+  show "map (bder c) (AALTs bs1 rs1 # rsb) s\<leadsto>* map (bder c) (map (fuse bs1) rs1 @ rsb)"
     apply(simp)
     using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast
 next
   case (ss6 a1 a2 bs rsa rsb)
-  then show ?case
+  have as: "erase a1 = erase a2" by fact
+  show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\<leadsto>* map (bder c) (bs @ [a1] @ rsa @ rsb)"
     apply(simp only: map_append)
-    by (smt (verit, best) erase_bder list.simps(8) list.simps(9) local.ss6 rrewrite_srewrite.ss6 srewrites.simps)
+    by (smt (verit, best) erase_bder list.simps(8) list.simps(9) as rrewrite_srewrite.ss6 srewrites.simps)
 qed
 
 lemma rewrites_preserves_bder: