
diff -r c892847df987 -r 0c666a0c57d7 thys2/SizeBound.thy
--- a/thys2/SizeBound.thy	Tue Dec 14 16:32:33 2021 +0000
+++ b/thys2/SizeBound.thy	Fri Jan 07 22:25:26 2022 +0000
@@ -238,6 +238,12 @@
   apply(simp_all)
   done
 
+lemma bnullable_fuse:
+  shows "bnullable (fuse bs r) = bnullable r"
+  apply(induct r arbitrary: bs)
+  apply(auto)
+  done
+
 lemma retrieve_encode_STARS:
   assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"
   shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
@@ -691,7 +697,6 @@
   shows "bnullable (bders_simp r s) = bnullable (bders r s)"
   by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
 
-
 lemma qq1:
   assumes "\<exists>r \<in> set rs. bnullable r"
   shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)"
@@ -710,6 +715,17 @@
   apply(simp)
   by (metis append_assoc in_set_conv_decomp r1 r2)
   
+lemma qq3:
+  assumes "bnullable (AALTs bs (rs @ rs1))"
+          "bnullable (AALTs bs (rs @ rs2))"
+          "\<lbrakk>bnullable (AALTs bs rs1); bnullable (AALTs bs rs2); \<forall>r\<in>set rs. \<not>bnullable r\<rbrakk> \<Longrightarrow> 
+               bmkeps (AALTs bs rs1) = bmkeps (AALTs bs rs2)"
+  shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs (rs @ rs2))"
+  using assms
+  apply(case_tac "\<exists>r \<in> set rs. bnullable r")
+  using qq1 apply auto[1]
+  by (metis UnE bnullable.simps(4) qq2 set_append)
+  
 
 lemma flts_append:
   shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
@@ -739,10 +755,6 @@
   
 
 
-
-
-
-
 fun nonazero :: "arexp \<Rightarrow> bool"
   where
   "nonazero AZERO = False"
@@ -850,17 +862,15 @@
   apply(simp)
   using qq4 r1 r2 by auto
 
-
-
-  
 lemma bder_fuse:
   shows "bder c (fuse bs a) = fuse bs  (bder c a)"
   apply(induct a arbitrary: bs c)
        apply(simp_all)
   done
 
-inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
-  where
+inductive 
+  rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
+where
   "ASEQ bs AZERO r2 \<leadsto> AZERO"
 | "ASEQ bs r1 AZERO \<leadsto> AZERO"
 | "ASEQ bs (AONE bs1) r \<leadsto> fuse (bs@bs1) r"
@@ -880,17 +890,21 @@
 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
 
 
-inductive rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
-  where 
-rs1[intro, simp]:"r \<leadsto>* r"
+inductive 
+  rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
+where 
+  rs1[intro, simp]:"r \<leadsto>* r"
 | rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
-inductive srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto>* _" [100, 100] 100)
-  where
-ss1: "[] s\<leadsto>* []"
-|ss2: "\<lbrakk>r \<leadsto>* r'; rs s\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) s\<leadsto>* (r'#rs')"
-(*rs1 = [r1, r2, ..., rn] rs2 = [r1', r2', ..., rn']
-[r1, r2, ..., rn] \<leadsto>* [r1', r2, ..., rn] \<leadsto>* [...r2',...] \<leadsto>* [r1', r2',... rn']
+inductive 
+  srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto>* _" [100, 100] 100)
+where
+  ss1: "[] s\<leadsto>* []"
+| ss2: "\<lbrakk>r \<leadsto>* r'; rs s\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) s\<leadsto>* (r'#rs')"
+
+(*
+rs1 = [r1, r2, ..., rn] rs2 = [r1', r2', ..., rn']
+    [r1, r2, ..., rn] \<leadsto>* [r1', r2, ..., rn] \<leadsto>* [...r2',...] \<leadsto>* [r1', r2',... rn']
 *)
 
 
@@ -898,12 +912,12 @@
 lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
   using rrewrites.intros(1) rrewrites.intros(2) by blast
  
-lemma real_trans [trans]: 
+lemma real_trans[trans]: 
   assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
   shows "r1 \<leadsto>* r3"
   using a2 a1
   apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct) 
-   apply(auto)
+  apply(auto)
   done
 
 
@@ -978,7 +992,8 @@
   and   "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
   by (simp_all)
 
-lemma trivialbsimpsrewrites: "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
+lemma trivialbsimpsrewrites: 
+  "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
 
   apply(induction rs)
    apply simp
@@ -986,7 +1001,8 @@
   by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps)
 
 
-lemma bsimp_AALTsrewrites: "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
+lemma bsimp_AALTsrewrites: 
+  "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
   apply(induction rs)
   apply simp
    apply(rule r_in_rstar)
@@ -1000,12 +1016,14 @@
   apply(simp)
   done 
 
-inductive frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)
-  where
-fs1: "[] f\<leadsto>* []"
-|fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
-|fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
-|fs4: "\<lbrakk>rs f\<leadsto>* rs';nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"
+(* rewrites for lists *)
+inductive 
+  frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)
+where
+  fs1: "[] f\<leadsto>* []"
+| fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
+| fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
+| fs4: "\<lbrakk>rs f\<leadsto>* rs'; nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"
 
 
 
@@ -1105,7 +1123,8 @@
   apply auto
   by (metis split_list)
 
-lemma alts_dBrewrites_withFront: " AALTs bs (rsa @ rs) \<leadsto>* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))"
+lemma alts_dBrewrites_withFront: 
+  "AALTs bs (rsa @ rs) \<leadsto>* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))"
   apply(induction rs arbitrary: rsa)
    apply simp
   apply(drule_tac x = "rsa@[a]" in meta_spec)
@@ -1154,16 +1173,13 @@
   using alts_dBrewrites_withFront
   by (metis append_Nil dB_single_step empty_set image_empty)
 
-
-
-  
-
-
 lemma bsimp_rewrite: 
   shows "r \<leadsto>* bsimp r"
-  apply(induction r rule: bsimp.induct)
-       apply simp
-       apply(case_tac "bsimp r1 = AZERO")
+proof (induction r rule: bsimp.induct)
+  case (1 bs1 r1 r2)
+  then show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)"
+    apply(simp)
+    apply(case_tac "bsimp r1 = AZERO")
         apply simp
   using continuous_rewrite apply blast
        apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
@@ -1172,37 +1188,28 @@
         apply(subst bsimp_ASEQ2)
         apply (meson real_trans rrewrite.intros(3) rrewrites.intros(2) star_seq star_seq2)
        apply (smt (verit, best) bsimp_ASEQ0 bsimp_ASEQ1 real_trans rrewrite.intros(2) rs2 star_seq star_seq2)
-      defer
-  using bsimp_aalts_simpcases(2) apply blast
-  apply simp
-  apply simp
-  apply simp
-
-  apply auto
-
-
-  apply(subgoal_tac "AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)")
-   apply(subgoal_tac "AALTs bs1 (map bsimp rs) \<leadsto>* AALTs bs1 (flts (map bsimp rs))")
-  apply(subgoal_tac "AALTs bs1 (flts (map bsimp rs)) \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})")
-    apply(subgoal_tac "AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) \<leadsto>* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {} )")
-
-  
-      apply (meson real_trans)
-
-   apply (meson bsimp_AALTsrewrites)
-
-  apply (meson alts_dBrewrites)
-
-  using fltsrewrites apply auto[1]
-
-  using alts_simpalts by force
-
-
-lemma rewrite_non_nullable: "\<lbrakk>r1 \<leadsto> r2; \<not>bnullable r1 \<rbrakk> \<Longrightarrow> \<not>bnullable r2"
-  apply(induction r1 r2 rule: rrewrite.induct)
-             apply auto 
-      apply (metis bnullable_correctness erase_fuse)+
   done
+next
+  case (2 bs1 rs)
+  then show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)"
+    by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTsrewrites fltsrewrites real_trans)  
+next
+  case "3_1"
+  then show "AZERO \<leadsto>* bsimp AZERO"
+    by simp
+next
+  case ("3_2" v)
+  then show "AONE v \<leadsto>* bsimp (AONE v)" 
+    by simp
+next
+  case ("3_3" v va)
+  then show "ACHAR v va \<leadsto>* bsimp (ACHAR v va)" 
+    by simp
+next
+  case ("3_4" v va)
+  then show "ASTAR v va \<leadsto>* bsimp (ASTAR v va)" 
+    by simp
+qed
 
 lemma rewrite_non_nullable_strong: 
   assumes "r1 \<leadsto> r2"
@@ -1229,41 +1236,16 @@
   apply simp
   using rewrite_non_nullable_strong by blast
 
-lemma nonbnullable_lists_concat: " \<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk> \<Longrightarrow> 
-\<not>(\<exists>r0 \<in> (set (rs1@[r]@rs2)). bnullable r0 ) "
-  apply simp
-  apply blast
-  done
 
-
-
-lemma nomember_bnullable: "\<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk>
- \<Longrightarrow> \<not>bnullable (AALTs bs (rs1 @ [r] @ rs2))"
-  using bnullable.simps(4) nonbnullable_lists_concat by presburger
-
-lemma bnullable_segment: " bnullable (AALTs bs (rs1@[r]@rs2)) \<Longrightarrow> bnullable (AALTs bs rs1) \<or> bnullable (AALTs bs rs2) \<or> bnullable r"
-  apply(case_tac "\<exists>r0\<in>set rs1.  bnullable r0")
-  using r2 apply blast
-  apply(case_tac "bnullable r")
-
-  apply blast
-  apply(case_tac "\<exists>r0\<in>set rs2.  bnullable r0")
-
-  using bnullable.simps(4) apply presburger
-  apply(subgoal_tac "False")
-
-  apply blast
-
-  using nomember_bnullable by blast
-
-  
+lemma bnullable_segment: 
+  "bnullable (AALTs bs (rs1@[r]@rs2)) \<Longrightarrow> bnullable (AALTs bs rs1) \<or> bnullable (AALTs bs rs2) \<or> bnullable r"
+  by auto
 
 lemma bnullablewhichbmkeps: "\<lbrakk>bnullable  (AALTs bs (rs1@[r]@rs2)); \<not> bnullable (AALTs bs rs1); bnullable r \<rbrakk>
  \<Longrightarrow> bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)"
+  
   using qq2 bnullable_Hdbmkeps_Hd by force
 
-
-
 lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1)
     \<Longrightarrow> bmkeps (AALTs bs (AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs ( map (fuse bs1) rs1 @ rsb))"
   apply(subst bnullable_Hdbmkeps_Hd)
@@ -1271,102 +1253,84 @@
    apply simp
   by (metis bmkeps.simps(3) k0a list.set_intros(1) qq1 qq4 qs3)
 
-lemma third_segment_bnullable: "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
-bnullable (AALTs bs rs3)"
-  
-  by (metis append.left_neutral append_Cons bnullable.simps(1) bnullable_segment rrewrite.intros(7) rewrite_non_nullable)
+lemma third_segment_bnullable: 
+  "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
+   bnullable (AALTs bs rs3)"
+  apply(auto)
+  done
 
+lemma third_segment_bmkeps:  
+  "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
+   bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)"
+  by (metis bnullable.simps(1) bnullable.simps(4) bsimp_AALTs.simps(1) bsimp_AALTsrewrites qq2 rewritesnullable self_append_conv third_segment_bnullable)
 
-lemma third_segment_bmkeps:  "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
-bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)"
-  apply(subgoal_tac "bnullable (AALTs bs rs3)")
-   apply(subgoal_tac "\<forall>r \<in> set (rs1@rs2). \<not>bnullable r")
-  apply(subgoal_tac "bmkeps (AALTs bs (rs1@rs2@rs3)) = bmkeps (AALTs bs ((rs1@rs2)@rs3) )")
-  apply (metis bnullable.simps(4) qq2)
-
-  apply (metis append.assoc)
-
-  apply (metis append.assoc in_set_conv_decomp r2 third_segment_bnullable)
-
-  using third_segment_bnullable by blast
-
+lemma rewrite_bmkepsalt: 
+  "\<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
+       \<Longrightarrow> bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
+  apply(rule qq3)
+  apply(simp)
+  apply(simp)
+  apply(case_tac "bnullable (AALTs bs1 rs1)")
+  using spillbmkepslistr apply blast
+  apply(subst qq2)
+    apply(auto simp add: bnullable_fuse r1)
+  done
 
-lemma rewrite_bmkepsalt: " \<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
-       \<Longrightarrow> bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
-  apply(case_tac "bnullable (AALTs bs rsa)")
-  
-  using qq1 apply force
-  apply(case_tac "bnullable (AALTs bs1 rs1)")
-  apply(subst qq2)
-
-  
-  using r2 apply blast
-  
-    apply (metis list.set_intros(1))
-  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
-  
-  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_aux: 
+  assumes "r1 \<leadsto> r2" "bnullable r1" "bnullable r2"
+  shows "bmkeps r1 = bmkeps r2"
+  using assms 
+proof (induction r1 r2 rule: rrewrite.induct)
+  case (1 bs r2)
+  then show ?case by simp 
+next
+  case (2 bs r1)
+  then show ?case by simp
+next
+  case (3 bs bs1 r)
+  then show ?case by (simp add: b2) 
+next
+  case (4 r1 r2 bs r3)
+  then show ?case by simp
+next
+  case (5 r3 r4 bs r1)
+  then show ?case by simp
+next
+  case (6 r r' bs rs1 rs2)
+  then show ?case
+    by (metis append_Cons append_Nil bnullable.simps(4) bnullable_segment bnullablewhichbmkeps qq3 r1 rewrite_non_nullable_strong)
+next
+  case (7 bs rsa rsb)
+  then show ?case
+    by (metis bnullable.simps(1) bnullable.simps(4) bnullable_segment qq1 qq2 rewrite_nullable rrewrite.intros(10) rrewrite0away third_segment_bmkeps) 
+next
+  case (8 bs rsa bs1 rs1 rsb)
+  then show ?case
+    by (simp add: rewrite_bmkepsalt) 
+next
+  case (9 bs bs1 rs)
+  then show ?case
+    by (simp add: q3a) 
+next
+  case (10 bs)
+  then show ?case
+    by fastforce 
+next
+  case (11 bs r)
+  then show ?case
+    by (simp add: b2) 
+next
+  case (12 a1 a2 bs rsa rsb rsc)
+  then show ?case
+    by (smt (verit, ccfv_threshold) append_Cons append_eq_appendI append_self_conv2 bnullable_correctness list.set_intros(1) qq3 r1)
+qed
 
 
-lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; bnullable r1\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2"
-
-  apply(frule rewrite_nullable)
-  apply simp
-  apply(induction r1 r2 rule: rrewrite.induct)
-             apply simp
-  using bnullable.simps(1) bnullable.simps(5) apply blast
-         apply (simp add: b2)
-        apply simp
-         apply simp
-  apply(frule bnullable_segment)
-        apply(case_tac "bnullable (AALTs bs rs1)")
-  using qq1 apply force
-        apply(case_tac "bnullable r")
-  using bnullablewhichbmkeps rewrite_nullable apply presburger
-        apply(subgoal_tac "bnullable (AALTs bs rs2)")
-  apply(subgoal_tac "\<not> bnullable r'")
-  apply (simp add: qq2 r1)
+lemma rewrite_bmkeps: 
+  assumes "r1 \<leadsto> r2" "bnullable r1"
+  shows "bmkeps r1 = bmkeps r2"
+  using assms(1) assms(2) rewrite_bmkeps_aux rewrite_nullable by blast
   
-  using rewrite_non_nullable apply blast
-
-        apply blast
-       apply (simp add: flts_append qs3)
-  apply (simp add: rewrite_bmkepsalt)
-  using q3a apply force
-
-  apply (simp add: q3a)
-  apply (simp add: b2)
-  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" 
@@ -1389,50 +1353,68 @@
 lemma alts_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto> AALTs bs (r' # rs)"
   by (metis append_Cons append_Nil rrewrite.intros(6))
 
-lemma alt_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALT bs r r2 \<leadsto> AALT bs r' r2"
-  using alts_rewrite_front by blast
-
 lemma to_zero_in_alt: " AALT bs (ASEQ [] AZERO r) r2 \<leadsto>  AALT bs AZERO r2"
   by (simp add: alts_rewrite_front rrewrite.intros(1))
 
-lemma alt_remove0_front: " AALT bs AZERO r \<leadsto> AALTs bs [r]"
-  by (simp add: rrewrite0away)
-
-lemma alt_rewrites_back: "r2 \<leadsto>* r2' \<Longrightarrow>AALT bs r1 r2 \<leadsto>* AALT bs r1 r2'"
-  apply(induction r2 r2' arbitrary: bs rule: rrewrites.induct)
-   apply simp
-  by (meson rs1 rs2 srewrites_alt1 ss1 ss2)
-
-lemma rewrite_fuse: " r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto>* fuse bs r3"
-  apply(induction r2 r3 arbitrary: bs rule: rrewrite.induct)
-             apply auto
-
-           apply (simp add: continuous_rewrite)
-
-          apply (simp add: r_in_rstar rrewrite.intros(2))
-
-         apply (metis fuse_append r_in_rstar rrewrite.intros(3))
-
-  using r_in_rstar star_seq apply blast
-
-  using r_in_rstar star_seq2 apply blast
-
-  using contextrewrites2 r_in_rstar apply auto[1]
-  
-  using rrewrite.intros(8) apply auto[1]
-  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
-  
+lemma rewrite_fuse: 
+  assumes "r2 \<leadsto> r3"
+  shows "fuse bs r2 \<leadsto>* fuse bs r3"
+  using assms
+proof(induction r2 r3 arbitrary: bs rule: rrewrite.induct)
+  case (1 bs r2)
+  then show ?case
+    by (simp add: continuous_rewrite) 
+next
+  case (2 bs r1)
+  then show ?case
+    using rrewrite.intros(2) by force 
+next
+  case (3 bs bs1 r)
+  then show ?case
+    by (metis fuse.simps(5) fuse_append r_in_rstar rrewrite.intros(3)) 
+next
+  case (4 r1 r2 bs r3)
+  then show ?case
+    by (simp add: r_in_rstar star_seq) 
+next
+  case (5 r3 r4 bs r1)
+  then show ?case
+    using fuse.simps(5) r_in_rstar star_seq2 by auto  
+next
+  case (6 r r' bs rs1 rs2)
+  then show ?case
+    using contextrewrites2 r_in_rstar by force 
+next
+  case (7 bs rsa rsb)
+  then show ?case
+    using rrewrite.intros(7) by force  
+next
+  case (8 bs rsa bs1 rs1 rsb)
+  then show ?case
+    using rrewrite.intros(8) by force 
+next
+  case (9 bs bs1 rs)
+  then show ?case
+    by (metis append.assoc fuse.simps(4) r_in_rstar rrewrite.intros(9)) 
+next
+  case (10 bs)
+  then show ?case
+    by (simp add: r_in_rstar rrewrite.intros(10)) 
+next
+  case (11 bs r)
+  then show ?case
+    by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(11)) 
+next
+  case (12 a1 a2 bs rsa rsb rsc)
+  then show ?case
+    using fuse.simps(4) r_in_rstar rrewrite.intros(12) by auto 
+qed
 
 lemma rewrites_fuse:  
-  assumes "r2 \<leadsto>* r2'"
-  shows "fuse bs1 r2 \<leadsto>* fuse bs1 r2'"
+  assumes "r1 \<leadsto>* r2"
+  shows "fuse bs r1 \<leadsto>* fuse bs r2"
 using assms
-apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct)
+apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
 apply(auto intro: rewrite_fuse real_trans)
 done
 
@@ -1443,7 +1425,8 @@
 done
 
 
-lemma rewrite_der_altmiddle: "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
+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 del: append.simps)
   by (metis append.assoc map_map r_in_rstar rrewrite.intros(8) threelistsappend)
@@ -1456,63 +1439,72 @@
   
   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)
-  
-              apply (simp add: r_in_rstar rrewrite.intros(1))
-  apply simp
-  
-  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(11))
-  using bder_fuse fuse_append rs1 apply presburger
-          apply(case_tac "bnullable r1")
-  prefer 2
-           apply(subgoal_tac "\<not>bnullable r2")
-            prefer 2
-  using rewrite_non_nullable apply presburger
-           apply simp+
-  
-  using star_seq apply auto[1]
-          apply(subgoal_tac "bnullable r2")
-           apply simp+
-  apply(subgoal_tac "bmkeps r1 = bmkeps r2")
-  prefer 2
-  using rewrite_bmkeps apply auto[1]
-  using contextrewrites1 star_seq apply auto[1]
-  using rewrite_nullable apply auto[1]
-         apply(case_tac "bnullable r1")
-          apply simp
-          apply(subgoal_tac "ASEQ [] (bder c r1) r3 \<leadsto> ASEQ [] (bder c r1) r4") 
-           prefer 2
-  using rrewrite.intros(5) apply blast
-          apply(rule many_steps_later)
-           apply(rule alt_rewrite_front)
-           apply assumption
-  apply (meson alt_rewrites_back rewrites_fuse) 
-
-       apply (simp add: r_in_rstar rrewrite.intros(5))
-
-  using contextrewrites2 apply force
-
-  using rrewrite.intros(7) apply force
-  
-  using rewrite_der_altmiddle apply auto[1]
-  
-  apply (metis bder.simps(4) bder_fuse_list map_map r_in_rstar rrewrite.intros(9))
-  apply (simp add: r_in_rstar rrewrite.intros(10))
-
-  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
-
+lemma rewrite_after_der: 
+  assumes "r1 \<leadsto> r2"
+  shows "(bder c r1) \<leadsto>* (bder c r2)"
+  using assms
+proof(induction r1 r2 rule: rrewrite.induct)
+  case (1 bs r2)
+  then show "bder c (ASEQ bs AZERO r2) \<leadsto>* bder c AZERO"
+    by (simp add: continuous_rewrite) 
+next
+  case (2 bs r1)
+  then show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO"
+    apply(simp)
+    by (meson contextrewrites1 r_in_rstar real_trans rrewrite.intros(10) rrewrite.intros(2) rrewrite0away)
+next
+  case (3 bs bs1 r)
+  then show "bder c (ASEQ bs (AONE bs1) r) \<leadsto>* bder c (fuse (bs @ bs1) r)" 
+    apply(simp)
+    by (metis bder_fuse fuse_append rrewrite.intros(11) rrewrite0away rrewrites.simps to_zero_in_alt)
+next
+  case (4 r1 r2 bs r3)
+  have as: "r1 \<leadsto> r2" by fact
+  have IH: "bder c r1 \<leadsto>* bder c r2" by fact
+  from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"
+    by (simp add: contextrewrites1 rewrite_bmkeps rewrite_non_nullable_strong star_seq) 
+next
+  case (5 r3 r4 bs r1)
+  have as: "r3 \<leadsto> r4" by fact 
+  have IH: "bder c r3 \<leadsto>* bder c r4" by fact 
+  from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)" 
+    apply(simp)
+    using r_in_rstar rewrites_fuse srewrites_alt1 ss1 ss2 star_seq2 by presburger
+next
+  case (6 r r' bs rs1 rs2)
+  have as: "r \<leadsto> r'" by fact
+  have IH: "bder c r \<leadsto>* bder c r'" by fact
+  from as IH show "bder c (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto>* bder c (AALTs bs (rs1 @ [r'] @ rs2))" 
+    apply(simp)
+    using contextrewrites2 by force
+next
+  case (7 bs rsa rsb)
+  then show "bder c (AALTs bs (rsa @ [AZERO] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ rsb))" 
+    apply(simp)
+    using rrewrite.intros(7) by auto
+next
+  case (8 bs rsa bs1 rs1 rsb)
+  then show 
+    "bder c (AALTs bs (rsa @ [AALTs bs1 rs1] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
+    using rewrite_der_altmiddle by auto 
+next
+  case (9 bs bs1 rs)
+  then show "bder c (AALTs (bs @ bs1) rs) \<leadsto>* bder c (AALTs bs (map (fuse bs1) rs))"
+    by (metis bder.simps(4) bder_fuse_list list.map_comp r_in_rstar rrewrite.intros(9)) 
+next
+  case (10 bs)
+  then show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"
+    by (simp add: r_in_rstar rrewrite.intros(10))
+next
+  case (11 bs r)
+  then show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
+    by (simp add: bder_fuse r_in_rstar rrewrite.intros(11)) 
+next
+  case (12 a1 a2 bs rsa rsb rsc)
+  have as: "erase a1 = erase a2" by fact
+  then show "bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
+    using lock_step_der_removal by force 
+qed
 
 
 lemma rewrites_after_der: 
@@ -1523,6 +1515,7 @@
 apply(simp_all add: rewrite_after_der real_trans)
 done
 
+
 lemma central:  
   shows "bders r s \<leadsto>* bders_simp r s"
 proof(induct s arbitrary: r rule: rev_induct)
@@ -1540,20 +1533,27 @@
     by (simp add: bders_simp_append)
 qed
 
-
 lemma quasi_main: 
   assumes "bnullable (bders r s)"
   shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
-  using assms central rewrites_bmkeps by blast
+  using assms central rewrites_bmkeps 
+proof -
+  have "bders r s \<leadsto>* bders_simp r s" by (rule central)
+  then 
+  show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms
+    by (rule rewrites_bmkeps)
+qed  
+
 
 theorem main_main: 
   shows "blexer r s = blexer_simp r s"
-  by (simp add: b4 blexer_def blexer_simp_def quasi_main)
+  unfolding blexer_def blexer_simp_def
+  using b4 quasi_main by simp
 
 
 theorem blexersimp_correctness: 
   shows "lexer r s = blexer_simp r s"
-  using blexer_correctness main_main by auto
+  using blexer_correctness main_main by simp
 
 
 




