diff -r aa0a2a3f90a0 -r c80720289645 thys2/SizeBound.thy
--- a/thys2/SizeBound.thy	Fri Jan 07 22:29:14 2022 +0000
+++ b/thys2/SizeBound.thy	Tue Jan 11 23:55:13 2022 +0000
@@ -138,6 +138,14 @@
   apply(auto)
   done
 
+lemma fuse_Nil:
+  shows "fuse [] r = r"
+  by (induct r)(simp_all)
+
+lemma map_fuse_Nil:
+  shows "map (fuse []) rs = rs"
+  by (induct rs)(simp_all add: fuse_Nil)
+
 
 fun intern :: "rexp \<Rightarrow> arexp" where
   "intern ZERO = AZERO"
@@ -737,18 +745,6 @@
   done
 
 
-lemma bsimp_AALTs_qq:
-  assumes "1 < length rs"
-  shows "bsimp_AALTs bs rs = AALTs bs  rs"
-  using  assms
-  apply(case_tac rs)
-   apply(simp)
-  apply(case_tac list)
-   apply(simp_all)
-  done
-
-
-
 lemma bbbbs1:
   shows "nonalt r \<or> (\<exists>bs rs. r  = AALTs bs rs)"
   using nonalt.elims(3) by auto
@@ -868,23 +864,21 @@
        apply(simp_all)
   done
 
+
+
+
 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"
+| "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
 | "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
 | "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)"
-(*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
-as long as they are on the right path*)
-| "AALTs (bs@bs1) rs \<leadsto> AALTs bs (map (fuse bs1) rs)"
 | "AALTs bs [] \<leadsto> AZERO"
 | "AALTs bs [r] \<leadsto> fuse bs r"
 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
@@ -896,17 +890,22 @@
   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']
-*)
 
+(* 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')"
 
 
 lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
@@ -952,7 +951,6 @@
   apply auto
   done
 
-
 corollary srewrites_alt1: 
   assumes "rs1 s\<leadsto>* rs2"
   shows "AALTs bs rs1 \<leadsto>* AALTs bs rs2"
@@ -992,7 +990,8 @@
   and   "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
   by (simp_all)
 
-lemma trivialbsimpsrewrites: 
+
+lemma trivialbsimp_srewrites: 
   "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
 
   apply(induction rs)
@@ -1001,29 +1000,13 @@
   by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps)
 
 
-lemma bsimp_AALTsrewrites: 
+lemma bsimp_AALTs_rewrites: 
   "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
   apply(induction rs)
   apply simp
    apply(rule r_in_rstar)
-  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)
-  done 
-
-(* 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')"
+  using rrewrite.intros(9) apply blast
+  by (metis bsimp_AALTs.elims list.discI rrewrite.intros(10) rrewrites.simps)
 
 
 
@@ -1082,7 +1065,7 @@
   apply auto
   done
 
-lemma fltsrewrites: "  AALTs bs1 rs \<leadsto>* AALTs bs1 (flts rs)"
+lemma flts_rewrites: "  AALTs bs1 rs \<leadsto>* AALTs bs1 (flts rs)"
   apply(induction rs)
    apply simp
   apply(case_tac "a = AZERO")
@@ -1103,13 +1086,40 @@
   apply (meson fltsfrewrites fs4 nonalt.elims(3) nonazero.elims(3))
   by (metis append_Cons append_Nil fltsfrewrites frewritesaalts flts_append k0a)
 
-lemma alts_simpalts: "\<And>bs1 rs. (\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow> 
-AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)"
-  apply(subgoal_tac " rs s\<leadsto>*  (map bsimp rs)")
-   prefer 2
-  using trivialbsimpsrewrites apply auto[1]
-  using srewrites_alt1 by auto
+(* TEST *)
+lemma r: 
+  assumes "AALTs bs rs1 \<leadsto> AALTs bs rs2"
+  shows "AALTs bs (x # rs1) \<leadsto>* AALTs bs (x # rs2)"
+  using assms
+  apply(erule_tac rrewrite.cases)
+            apply(auto)
+  apply (metis append_Cons append_Nil rrewrite.intros(6) r_in_rstar)
+  apply (metis append_Cons append_self_conv2 rrewrite.intros(7) r_in_rstar)
+  apply (metis Cons_eq_appendI append_eq_append_conv2 rrewrite.intros(8) self_append_conv r_in_rstar)
+   apply(case_tac rs2)
+    apply(auto)
+  apply(case_tac r)
+         apply(auto)
+  apply (metis append_Nil2 append_butlast_last_id butlast.simps(2) last.simps list.distinct(1) list.map_disc_iff r_in_rstar rrewrite.intros(8))
+     apply(case_tac r)
+        apply(auto)
+   defer
+   apply(rule r_in_rstar)
+  apply (metis append_Cons append_Nil rrewrite.intros(11))
+  apply(rule real_trans)
+   apply(rule r_in_rstar)
+  using rrewrite.intros(8)[where ?rsb = "[]", of "bs" "[x]" "[]" , simplified]
+   apply(rule_tac rrewrite.intros(8)[where ?rsb = "[]", of "bs" "[x]" "[]" , simplified])
+  apply(simp add: map_fuse_Nil fuse_Nil)
+  done 
 
+lemma alts_simpalts: 
+  "(\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow> 
+  AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)"
+  apply(induct rs)
+   apply(auto)[1]
+  using trivialbsimp_srewrites apply auto[1]
+  by (simp add: srewrites_alt1 ss2)
 
 lemma threelistsappend: "rsa@a#rsb = (rsa@[a])@rsb"
   apply auto
@@ -1149,7 +1159,7 @@
                 (erase `
                  (set rs1 \<union> set rs2)))) ")
   prefer 2
-  using rrewrite.intros(12) apply force
+  using rrewrite.intros(11) apply force
   using r_in_rstar apply force
   apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)")
   prefer 2
@@ -1161,7 +1171,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(12) same_append_eq somewhereMapInside)
+  apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(11) same_append_eq somewhereMapInside)
   by force
 
  
@@ -1192,7 +1202,7 @@
 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)  
+    by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTs_rewrites flts_rewrites real_trans)  
 next
   case "3_1"
   then show "AZERO \<leadsto>* bsimp AZERO"
@@ -1262,7 +1272,7 @@
 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)
+  by (metis bnullable.simps(1) bnullable.simps(4) bsimp_AALTs.simps(1) bsimp_AALTs_rewrites qq2 rewritesnullable self_append_conv third_segment_bnullable)
 
 lemma rewrite_bmkepsalt: 
   "\<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
@@ -1302,25 +1312,21 @@
 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) 
+    by (metis bnullable.simps(1) bnullable.simps(4) bnullable_segment qq1 qq2 rewrite_nullable rrewrite.intros(9) 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)
+  case (9 bs)
   then show ?case
     by fastforce 
 next
-  case (11 bs r)
+  case (10 bs r)
   then show ?case
     by (simp add: b2) 
 next
-  case (12 a1 a2 bs rsa rsb rsc)
+  case (11 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
@@ -1393,21 +1399,17 @@
   then show ?case
     using rrewrite.intros(8) by force 
 next
-  case (9 bs bs1 rs)
+  case (9 bs)
   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)) 
+    by (simp add: r_in_rstar rrewrite.intros(9))
 next
-  case (11 bs r)
+  case (10 bs r)
   then show ?case
-    by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(11)) 
+    by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(10)) 
 next
-  case (12 a1 a2 bs rsa rsb rsc)
+  case (11 a1 a2 bs rsa rsb rsc)
   then show ?case
-    using fuse.simps(4) r_in_rstar rrewrite.intros(12) by auto 
+    using fuse.simps(4) r_in_rstar rrewrite.intros(11) by auto 
 qed
 
 lemma rewrites_fuse:  
@@ -1437,7 +1439,7 @@
                                   bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
   apply(simp)
   
-  using rrewrite.intros(12) by auto
+  using rrewrite.intros(11) by auto
 
 lemma rewrite_after_der: 
   assumes "r1 \<leadsto> r2"
@@ -1451,12 +1453,12 @@
   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)
+    by (meson contextrewrites1 r_in_rstar real_trans rrewrite.intros(9) 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)
+    by (metis bder_fuse fuse_append rrewrite.intros(10) rrewrite0away rrewrites.simps to_zero_in_alt)
 next
   case (4 r1 r2 bs r3)
   have as: "r1 \<leadsto> r2" by fact
@@ -1467,9 +1469,8 @@
   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
+  from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
+    using bder.simps(5) 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
@@ -1488,19 +1489,15 @@
     "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)
+  case (9 bs)
   then show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"
-    by (simp add: r_in_rstar rrewrite.intros(10))
+    by (simp add: r_in_rstar rrewrite.intros(9))
 next
-  case (11 bs r)
+  case (10 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)) 
+    by (simp add: bder_fuse r_in_rstar rrewrite.intros(10)) 
 next
-  case (12 a1 a2 bs rsa rsb rsc)
+  case (11 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 
@@ -1533,10 +1530,13 @@
     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 
 proof -
   have "bders r s \<leadsto>* bders_simp r s" by (rule central)
   then 
@@ -1545,6 +1545,8 @@
 qed  
 
 
+
+
 theorem main_main: 
   shows "blexer r s = blexer_simp r s"
   unfolding blexer_def blexer_simp_def