diff -r 48ce16d61e03 -r 61eff2abb0b6 thys2/SizeBound3.thy
--- a/thys2/SizeBound3.thy	Sat Apr 16 09:52:57 2022 +0100
+++ b/thys2/SizeBound3.thy	Tue Apr 19 09:08:01 2022 +0100
@@ -1,6 +1,6 @@
 
 theory SizeBound3
-  imports "Lexer" 
+  imports "ClosedFormsBounds"
 begin
 
 section \<open>Bit-Encodings\<close>
@@ -1160,17 +1160,1025 @@
   using blexer_correctness main_blexer_simp by simp
 
 
+fun 
+  rerase :: "arexp \<Rightarrow> rrexp"
+where
+  "rerase AZERO = RZERO"
+| "rerase (AONE _) = RONE"
+| "rerase (ACHAR _ c) = RCHAR c"
+| "rerase (AALTs bs rs) = RALTS (map rerase rs)"
+| "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)"
+| "rerase (ASTAR _ r) = RSTAR (rerase r)"
 
-export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
+
+
+lemma asize_rsize:
+  shows "rsize (rerase r) = asize r"
+  apply(induct r)
+       apply simp+
+  
+  apply (metis (mono_tags, lifting) comp_apply map_eq_conv)
+  by simp
+
+lemma rb_nullability:
+  shows " rnullable (rerase a) = bnullable a"
+  apply(induct a)
+       apply simp+
+  done
+
+lemma fuse_anything_doesnt_matter:
+  shows "rerase a = rerase (fuse bs a)"
+  by (smt (verit) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6))
+
+
+lemma rerase_preimage:
+  shows "rerase r = RZERO \<Longrightarrow> r = AZERO"
+  apply(case_tac r)
+       apply simp+
+  done
+
+lemma rerase_preimage2:
+  shows "rerase r = RONE \<Longrightarrow> \<exists>bs. r = AONE bs"
+  apply(case_tac r)
+       apply simp+
+  done
+
+lemma rerase_preimage3:
+  shows "rerase r= RCHAR c \<Longrightarrow> \<exists>bs. r = ACHAR bs c"
+  apply(case_tac r)
+       apply simp+
+  done
+
+lemma rerase_preimage4:
+  shows "rerase r = RSEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2"
+  apply(case_tac r)
+       apply(simp)+
+  done
+
+lemma rerase_preimage5:
+  shows "rerase r = RALTS rs \<Longrightarrow> \<exists>bs as. r = AALTs bs as \<and> map rerase as = rs"
+  apply(case_tac r)
+       apply(simp)+
+  done
+
+lemma rerase_preimage6:
+  shows "rerase r = RSTAR r0 \<Longrightarrow> \<exists>bs a0. r = ASTAR bs a0 \<and> rerase a0 = r0 "
+  apply(case_tac r)
+       apply(simp)+
+  done
+
+lemma map_rder_bder:
+  shows "\<lbrakk> \<And>xa a. \<lbrakk>xa \<in> set x; rerase a = xa\<rbrakk> \<Longrightarrow> rerase (bder c a) = rder c xa;
+         map rerase as = x\<rbrakk> \<Longrightarrow>
+        map rerase (map (bder c) as) = map (rder c) x"
+  apply(induct x arbitrary: as)
+   apply simp+
+  by force
 
 
-unused_thms
+lemma der_rerase:
+  shows "rerase a = r \<Longrightarrow> rerase (bder c a) = rder c r"
+  apply(induct r arbitrary: a)
+       apply simp
+  using rerase_preimage apply fastforce
+  using rerase_preimage2 apply force
+     apply (metis bder.simps(3) rder.simps(3) rerase.simps(1) rerase.simps(2) rerase_preimage3)
+    apply(insert rerase_preimage4)[1]
+    apply(subgoal_tac " \<exists>bs a1 a2. a = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2")
+  prefer 2
+     apply presburger
+    apply(erule exE)+
+    apply(erule conjE)+
+    apply(subgoal_tac " rerase (bder c a1) = rder c r1")
+  prefer 2
+     apply blast
+    apply(subgoal_tac " rerase (bder c a2) = rder c r2")
+  prefer 2
+     apply blast
+    apply(case_tac "rnullable r1")
+     apply(subgoal_tac "bnullable a1")
+  apply simp
+  using fuse_anything_doesnt_matter apply presburger
+  using rb_nullability apply blast
+    apply (metis bder.simps(5) rb_nullability rder.simps(5) rerase.simps(5))
+  apply simp
+   apply(insert rerase_preimage5)[1]
+   apply(subgoal_tac "\<exists>bs as. a = AALTs bs as \<and> map rerase as = x")
+  prefer 2
+  
+    apply blast
+   apply(erule exE)+
+   apply(erule conjE)+
+  apply(subgoal_tac "map rerase (map (bder c) as) = map (rder c) x")
+  using bder.simps(4) rerase.simps(4) apply presburger
+  using map_rder_bder apply blast
+  using fuse_anything_doesnt_matter rerase_preimage6 by force
+
+lemma der_rerase2:
+  shows "rerase (bder c a) = rder c (rerase a)"
+  using der_rerase by force
+
+lemma ders_rerase:
+  shows "rerase (bders a s) = rders (rerase a) s"
+  apply(induct s rule: rev_induct)
+   apply simp
+  by (simp add: bders_append der_rerase rders_append)
+
+lemma rerase_bsimp_ASEQ:
+  shows "rerase (bsimp_ASEQ x1 a1 a2) = rsimp_SEQ (rerase a1) (rerase a2)"
+  by (smt (verit, ccfv_SIG) SizeBound3.bsimp_ASEQ0 SizeBound3.bsimp_ASEQ2 basic_rsimp_SEQ_property1 basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 bsimp_ASEQ.simps(1) bsimp_ASEQ1 fuse_anything_doesnt_matter rerase.simps(1) rerase.simps(2) rerase.simps(5) rerase_preimage rerase_preimage2 rsimp_SEQ.simps(1))
+
+lemma rerase_bsimp_AALTs:
+  shows "rerase (bsimp_AALTs bs rs) = rsimp_ALTs (map rerase rs)"
+  apply(induct rs arbitrary: bs)
+   apply simp+
+  by (smt (verit, ccfv_threshold) Cons_eq_map_conv bsimp_AALTs.elims fuse_anything_doesnt_matter list.discI list.inject list.simps(9) rerase.simps(4) rsimp_ALTs.elims)
+
+
+fun anonalt :: "arexp \<Rightarrow> bool"
+  where
+  "anonalt (AALTs bs2 rs) = False"
+| "anonalt r = True"
+
+
+fun agood :: "arexp \<Rightarrow> bool" where
+  "agood AZERO = False"
+| "agood (AONE cs) = True" 
+| "agood (ACHAR cs c) = True"
+| "agood (AALTs cs []) = False"
+| "agood (AALTs cs [r]) = False"
+| "agood (AALTs cs (r1#r2#rs)) = (distinct (map erase (r1 # r2 # rs)) \<and>(\<forall>r' \<in> set (r1#r2#rs). agood r' \<and> anonalt r'))"
+| "agood (ASEQ _ AZERO _) = False"
+| "agood (ASEQ _ (AONE _) _) = False"
+| "agood (ASEQ _ _ AZERO) = False"
+| "agood (ASEQ cs r1 r2) = (agood r1 \<and> agood r2)"
+| "agood (ASTAR cs r) = True"
+
+
+fun anonnested :: "arexp \<Rightarrow> bool"
+  where
+  "anonnested (AALTs bs2 []) = True"
+| "anonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
+| "anonnested (AALTs bs2 (r # rs2)) = anonnested (AALTs bs2 rs2)"
+| "anonnested r = True"
 
 
-inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99)
-  where
- "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) "
+lemma  k0:
+  shows "flts (r # rs1) = flts [r] @ flts rs1"
+  apply(induct r arbitrary: rs1)
+   apply(auto)
+  done
+
+lemma  k00:
+  shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"
+  apply(induct rs1 arbitrary: rs2)
+   apply(auto)
+  by (metis append.assoc k0)
+
+
+lemma bbbbs:
+  assumes "agood r" "r = AALTs bs1 rs"
+  shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"
+  using  assms
+  by (smt (verit, ccfv_SIG) Cons_eq_map_conv agood.simps(4) agood.simps(5) append.right_neutral bsimp_AALTs.elims flts.simps(1) flts.simps(3) list.map_disc_iff)
+
+lemma bbbbs1:
+  shows "anonalt r \<or> (\<exists>bs rs. r  = AALTs bs rs)"
+  by (meson anonalt.elims(3))
+
+
+
+lemma good_fuse:
+  shows "agood (fuse bs r) = agood r"
+  apply(induct r arbitrary: bs)
+       apply(auto)
+     apply(case_tac r1)
+          apply(simp_all)
+  apply(case_tac r2)
+          apply(simp_all)
+  apply(case_tac r2)
+            apply(simp_all)
+  apply(case_tac r2)
+           apply(simp_all)
+  apply(case_tac r2)
+          apply(simp_all)
+  apply(case_tac r1)
+          apply(simp_all)
+  apply(case_tac r2)
+           apply(simp_all)
+  apply(case_tac r2)
+           apply(simp_all)
+  apply(case_tac r2)
+           apply(simp_all)
+  apply(case_tac r2)
+         apply(simp_all)
+  apply(case_tac x2a)
+    apply(simp_all)
+  apply(case_tac list)
+    apply(simp_all)
+  apply(case_tac x2a)
+    apply(simp_all)
+  apply(case_tac list)
+    apply(simp_all)
+  done
+
+lemma good0:
+  assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. anonalt r" "distinct (map erase rs)"
+  shows "agood (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. agood r)"
+  using  assms
+  apply(induct bs rs rule: bsimp_AALTs.induct)
+    apply simp+
+   apply (simp add: good_fuse)
+  apply(subgoal_tac "bsimp_AALTs bs1 (v # vb # vc) = AALTs bs1 (v # vb # vc)")
+   prefer 2
+
+  
+  using bsimp_AALTs.simps(3) apply presburger
+  apply(simp only:)
+  apply(subgoal_tac "agood (AALTs bs1 (v # vb # vc)) = ((\<forall>r \<in> (set (v # vb # vc)). agood r \<and> anonalt r) \<and> distinct (map erase (v # vb # vc)))")
+  prefer 2
+  using agood.simps(6) apply blast
+  apply(simp only:)
+  apply(subgoal_tac "((\<forall>r\<in>set (v # vb # vc). agood r \<and> anonalt r) \<and> distinct (map erase (v # vb # vc))) = ((\<forall>r\<in>set (v # vb # vc). agood r) \<and> distinct (map erase (v # vb # vc)))")
+  prefer 2
+  apply blast
+  apply(simp only:)
+  apply(subgoal_tac "((\<forall>r \<in> set (v # vb # vc). agood r) \<and> distinct (map erase (v # vb # vc))) = (\<forall> r \<in> set (v # vb # vc). agood r) ")
+  prefer 2
+   apply(subgoal_tac "distinct (map erase (v # vb # vc)) = True")
+  prefer 2
+    apply blast
+  prefer 2
+   apply force
+  apply simp
+  done
+
+
+lemma nn11a:
+  assumes "anonalt r"
+  shows "anonalt (fuse bs r)"
+  using assms
+  apply(induct r)
+       apply(auto)
+  done
+
 
 
 
+lemma flts0:
+  assumes "r \<noteq> AZERO" "anonalt r"
+  shows "flts [r] \<noteq> []"
+  using  assms
+  apply(induct r)
+       apply(simp_all)
+  done
+
+lemma flts1:
+  assumes "agood r" 
+  shows "flts [r] \<noteq> []"
+  using  assms
+  apply(induct r)
+       apply(simp_all)
+  apply(case_tac x2a)
+   apply(simp)
+  apply(simp)
+  done
+
+lemma flts2:
+  assumes "agood r" 
+  shows "\<forall>r' \<in> set (flts [r]). agood r' \<and> anonalt r'"
+  using  assms
+  apply(induct r)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 2
+    apply(simp)
+    apply(auto)[1]
+     apply (metis bsimp_AALTs.elims agood.simps(4) agood.simps(5) agood.simps(6) good_fuse)
+  apply (metis bsimp_AALTs.elims agood.simps(4) agood.simps(5) agood.simps(6) nn11a)
+   apply fastforce
+  apply(simp)
+  done  
+
+
+lemma flts3:
+  assumes "\<forall>r \<in> set rs. agood r \<or> r = AZERO" 
+  shows "\<forall>r \<in> set (flts rs). agood r"
+  using  assms
+  apply(induct rs arbitrary: rule: flts.induct)
+        apply(simp_all)
+  by (metis SizeBound3.flts2 UnE append.right_neutral flts.simps(1) flts.simps(3) list.set_map)
+
+
+lemma flts3b:
+  assumes "\<exists>r\<in>set rs. agood r"
+  shows "flts rs \<noteq> []"
+  using  assms
+  apply(induct rs arbitrary: rule: flts.induct)
+        apply(simp)
+       apply(simp)
+      apply(simp)
+      apply(auto)
+  done
+
+lemma k0a:
+  shows "flts [AALTs bs rs] = map (fuse bs)  rs"
+  apply(simp)
+  done
+
+
+lemma k0b:
+  assumes "anonalt r" "r \<noteq> AZERO"
+  shows "flts [r] = [r]"
+  using assms
+  apply(case_tac  r)
+  apply(simp_all)
+  done
+
+lemma flts4_nogood:
+  shows "bsimp_AALTs bs0 rs = AZERO \<Longrightarrow> \<forall>r \<in> set rs. \<not> agood r"
+  by (metis SizeBound3.flts3b arexp.distinct(7) bsimp_AALTs.elims flts.simps(1) flts.simps(2) fuse_anything_doesnt_matter rerase.simps(1) rerase_preimage)
+
+lemma flts4_append:
+  shows "bsimp_AALTs bs0 (rs @ flts rsa) = AZERO \<Longrightarrow> bsimp_AALTs bs0 rs = AZERO"
+  by (metis append_is_Nil_conv arexp.simps(13) bsimp_AALTs.elims bsimp_AALTs.simps(1) butlast_append butlast_snoc)
+
+lemma flts4:
+  assumes "bsimp_AALTs bs (flts rs) = AZERO"
+  shows "\<forall>r \<in> set rs. \<not> agood r"
+  using assms
+  apply(induct rs arbitrary: bs rule: flts.induct)
+        apply(auto)
+        defer
+        apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b anonalt.simps(1) anonalt.simps(2))
+       apply (metis agood.simps(1) agood.simps(2) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.distinct(1) list.inject)
+      apply (metis agood.simps(1) agood.simps(3) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.distinct(1) list.inject)
+     apply (metis agood.simps(1) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.discI list.inject)
+    apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
+  apply (metis agood.simps(1) agood.simps(33) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.discI list.inject)
+  by (metis SizeBound3.bbbbs SizeBound3.k0a arexp.simps(13) flts4_append)
+
+  
+lemma flts_nil:
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+            agood (bsimp y) \<or> bsimp y = AZERO"
+  and "\<forall>r\<in>set rs. \<not> agood (bsimp r)"
+  shows "flts (map bsimp rs) = []"
+  using assms
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(simp)
+  by force
+
+lemma flts_nil2:
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+            agood (bsimp y) \<or> bsimp y = AZERO"
+  and "bsimp_AALTs bs (flts (map bsimp rs)) = AZERO"
+  shows "flts (map bsimp rs) = []"
+  using assms
+  apply(induct rs arbitrary: bs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(simp)
+  apply(subst (asm) k0)
+  apply(auto)
+  apply (metis flts.simps(1) flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+  by (metis flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+  
+  
+
+lemma good_SEQ:
+  assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
+  shows "agood (ASEQ bs r1 r2) = (agood r1 \<and> agood r2)"
+  using assms
+  apply(case_tac r1)
+       apply(simp_all)
+  apply(case_tac r2)
+          apply(simp_all)
+  apply(case_tac r2)
+         apply(simp_all)
+  apply(case_tac r2)
+        apply(simp_all)
+  apply(case_tac r2)
+       apply(simp_all)
+  done
+
+lemma asize0:
+  shows "0 < asize r"
+  apply(induct  r)
+       apply(auto)
+  done
+
+lemma nn1qq:
+  assumes "anonnested (AALTs bs rs)"
+  shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs"
+  using assms
+  apply(induct rs rule: flts.induct)
+  apply(auto)
+  done
+
+lemma nn1c:
+  assumes "\<forall>r \<in> set rs. anonnested r"
+  shows "\<forall>r \<in> set (flts rs). anonalt r"
+  using assms
+  apply(induct rs rule: flts.induct)
+        apply(auto)
+  apply(rule nn11a)
+  by (metis nn1qq anonalt.elims(3))
+
+lemma n0:
+  shows "anonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. anonalt r)"
+  apply(induct rs  arbitrary: bs)
+   apply(auto)
+  apply (metis SizeBound3.nn1qq anonalt.elims(3) list.set_intros(1))
+  apply (metis SizeBound3.bbbbs1 SizeBound3.nn1qq list.set_intros(2))
+  by (metis anonalt.elims(2) anonnested.simps(3) anonnested.simps(4) anonnested.simps(5) anonnested.simps(6) anonnested.simps(7))
+
+  
+
+lemma nn1bb:
+  assumes "\<forall>r \<in> set rs. anonalt r"
+  shows "anonnested (bsimp_AALTs bs rs)"
+  using assms
+  apply(induct bs rs rule: bsimp_AALTs.induct)
+    apply(auto)
+   apply (metis nn11a anonalt.simps(1) anonnested.elims(3))
+  using n0 by auto
+
+lemma nn10:
+  assumes "anonnested (AALTs cs rs)" 
+  shows "anonnested (AALTs (bs @ cs) rs)"
+  using assms
+  apply(induct rs arbitrary: cs bs)
+   apply(simp_all)
+  apply(case_tac a)
+       apply(simp_all)
+  done
+
+lemma nn1a:
+  assumes "anonnested r"
+  shows "anonnested (fuse bs r)"
+  using assms
+  apply(induct bs r arbitrary: rule: fuse.induct)
+       apply(simp_all add: nn10)
+  done  
+
+lemma dB_keeps_property:
+  shows "(\<forall>r \<in> set rs. P r) \<longrightarrow> (\<forall>r \<in> set (distinctBy rs erase rset). P r)"
+  apply(induct rs arbitrary: rset)
+   apply simp+
+  done
+
+lemma dB_filters_out:
+  shows "erase a \<in> rset \<Longrightarrow> a \<notin> set (distinctBy rs erase (rset))"
+  apply(induct rs arbitrary: rset)
+   apply simp
+  apply(case_tac "a = aa")
+   apply simp+
+  done
+
+lemma dB_will_be_distinct:
+  shows "distinct (distinctBy rs erase (insert (erase a) rset)) \<Longrightarrow> distinct (a #  (distinctBy rs erase (insert (erase a) rset)))"
+  using dB_filters_out by force
+  
+
+
+lemma dB_does_the_job2:
+  shows "distinct (distinctBy rs erase rset)"
+  apply(induct rs arbitrary: rset)
+   apply simp
+  apply(case_tac "erase a \<in> rset")
+   apply simp
+  apply(drule_tac x = "insert (erase a) rset" in meta_spec)
+  apply(subgoal_tac "distinctBy (a # rs) erase rset = a # distinctBy rs erase (insert (erase a ) rset)")
+   apply(simp only:)
+  using dB_will_be_distinct apply presburger
+  by auto
+
+lemma dB_does_more_job:
+  shows "distinct (map erase (distinctBy rs erase rset))"
+  apply(induct rs arbitrary:rset)
+   apply simp
+  apply(case_tac "erase a \<in> rset")
+   apply simp+
+  using dB_filters_out by force
+
+lemma dB_mono2:
+  shows "rset \<subseteq> rset' \<Longrightarrow> distinctBy rs erase rset = [] \<Longrightarrow> distinctBy rs erase rset' = []"
+  apply(induct rs arbitrary: rset rset')
+   apply simp+
+  by (meson in_mono list.discI)
+
+
+lemma nn1b:
+  shows "anonnested (bsimp r)"
+  apply(induct r)
+       apply(simp_all)
+  apply(case_tac "bsimp r1 = AZERO")
+    apply(simp)
+ apply(case_tac "bsimp r2 = AZERO")
+   apply(simp)
+  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+    apply(auto)[1]
+  apply (simp add: nn1a)    
+   apply(subst bsimp_ASEQ1)
+      apply(auto)
+  apply(rule nn1bb)
+  apply(auto)
+  apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp x2a)). anonalt r")
+  prefer 2
+  apply (metis (mono_tags, lifting) SizeBound3.nn1c image_iff list.set_map)
+  apply(subgoal_tac "\<forall>r \<in> set (distinctBy (flts (map bsimp x2a)) erase {}). anonalt r")
+  prefer 2
+  using dB_keeps_property apply presburger
+  by blast
+
+
+lemma induct_smaller_elem_list:
+  shows  "\<forall>r \<in> set list. asize r < Suc (sum_list (map asize list))"
+  apply(induct list)
+   apply simp+
+  by fastforce
+
+lemma no0s_fltsbsimp:
+  shows "\<forall>r \<in> set (flts (map bsimp rs)).  r \<noteq> AZERO"
+  oops
+
+lemma flts_all0s:
+  shows "\<forall>r \<in> set rs. r = AZERO \<Longrightarrow> flts rs = []"
+  apply(induct rs)
+   apply simp+
+  done
+
+
+
+
+
+lemma good1:
+  shows "agood (bsimp a) \<or> bsimp a = AZERO" 
+  apply(induct a  taking: asize rule: measure_induct)
+  apply(case_tac x)
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  prefer 3
+    apply(simp)
+   prefer 2
+  (*  AALTs case  *)
+  apply(simp only:)
+   apply(case_tac "x52")
+    apply(simp)
+   (*  AALTs list at least one - case *)
+   apply(simp only: )
+  apply(frule_tac x="a" in spec)
+   apply(drule mp)
+    apply(simp)
+   (* either first element is agood, or AZERO *)
+    apply(erule disjE)
+     prefer 2
+    apply(simp)
+   (* in  the AZERO case, the size  is smaller *)
+   apply(drule_tac x="AALTs x51 list" in spec)
+   apply(drule mp)
+     apply(simp add: asize0)
+    apply(subst (asm) bsimp.simps)
+  apply(subst (asm) bsimp.simps)
+    apply(assumption)
+   (* in the agood case *)
+  apply(frule_tac x="AALTs x51 list" in spec)
+   apply(drule mp)
+    apply(simp add: asize0)
+   apply(erule disjE)
+    apply(rule disjI1)
+  apply(simp add: good0)
+    apply(subst good0)  
+  using SizeBound3.flts3b distinctBy.elims apply force
+  apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)))) anonalt")
+       prefer 2
+  apply (metis Cons_eq_map_conv SizeBound3.nn1b SizeBound3.nn1c ex_map_conv)
+  using dB_keeps_property apply presburger
+  using dB_does_more_job apply presburger
+  apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)) )) agood")
+  using dB_keeps_property apply presburger
+    apply(subgoal_tac "\<forall>r \<in> (set (bsimp a # map bsimp list)). (agood r) \<or> (r = AZERO)")
+  using SizeBound3.flts3 apply blast
+
+    apply(subgoal_tac "\<forall>r \<in> set list. asize r < Suc (asize a + sum_list (map asize list))")
+  
+  apply simp
+
+    apply(subgoal_tac "\<forall>r \<in> set list. asize r < Suc (sum_list (map asize list))")
+  
+     apply fastforce
+  using induct_smaller_elem_list apply blast
+
+
+  
+
+   apply simp
+   apply(subgoal_tac "agood (bsimp a)")
+  prefer 2
+    apply blast
+   apply(subgoal_tac "\<forall>r \<in> (set (map bsimp list)). r = AZERO \<or> agood r")
+    prefer 2
+  apply (metis add_Suc_right image_iff induct_smaller_elem_list list.set_map trans_less_add2)
+   apply(subgoal_tac "\<not>(\<exists> r\<in>set (map bsimp list). agood r)")
+  prefer 2
+    apply (metis SizeBound3.flts3 SizeBound3.flts3b distinctBy.elims empty_iff flts4_nogood list.set_intros(1))
+   apply(subgoal_tac "\<forall>r \<in> set (map bsimp list). r = AZERO")
+  prefer 2
+    apply blast
+  apply(subgoal_tac "flts (map bsimp list) = []")
+  prefer 2
+  using flts_all0s apply presburger
+  apply (smt (verit, del_insts) SizeBound3.flts2 SizeBound3.good0 SizeBound3.k0 dB_does_more_job dB_keeps_property distinctBy.simps(1) flts.simps(1))
+  apply(subgoal_tac "agood (bsimp x42) \<or> bsimp x42 = AZERO")
+   apply(subgoal_tac "agood (bsimp x43) \<or> bsimp x43 = AZERO")
+    apply(case_tac "bsimp x42 = AZERO")
+     apply simp
+    apply(case_tac "bsimp x43 = AZERO")
+     apply simp
+    apply(case_tac "\<exists>bs'. bsimp x42 = AONE bs'")
+  apply(erule exE)
+  apply simp
+  using good_fuse apply presburger
+  apply simp
+    apply(subgoal_tac "bsimp_ASEQ x41 (bsimp x42) (bsimp x43) = ASEQ x41 (bsimp x42) (bsimp x43)")
+  prefer 2
+  using bsimp_ASEQ1 apply presburger
+  using SizeBound3.good_SEQ apply presburger
+  using asize.simps(5) less_add_Suc2 apply presburger
+  by simp
+
+  
+
+
+
+
+lemma good1a:
+  assumes "L (erase a) \<noteq> {}"
+  shows "agood (bsimp a)"
+  using good1 assms
+  using L_bsimp_erase by force
+  
+
+
+lemma flts_append:
+  "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
+  apply(induct xs1  arbitrary: xs2  rule: rev_induct)
+   apply(auto)
+  apply(case_tac xs)
+   apply(auto)
+   apply(case_tac x)
+        apply(auto)
+  apply(case_tac x)
+        apply(auto)
+  done
+
+lemma g1:
+  assumes "agood (bsimp_AALTs bs rs)"
+  shows "bsimp_AALTs bs rs = AALTs bs rs \<or> (\<exists>r. rs = [r] \<and> bsimp_AALTs bs [r] = fuse bs r)"
+using assms
+    apply(induct rs arbitrary: bs)
+  apply(simp)
+  apply(case_tac rs)
+  apply(simp only:)
+  apply(simp)
+  apply(case_tac  list)
+  apply(simp)
+  by simp
+
+lemma flts_0:
+  assumes "anonnested (AALTs bs  rs)"
+  shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
+  using assms
+  apply(induct rs arbitrary: bs rule: flts.induct)
+        apply(simp) 
+       apply(simp) 
+      defer
+      apply(simp) 
+     apply(simp) 
+    apply(simp) 
+apply(simp) 
+  apply(rule ballI)
+  apply(simp)
+  done
+
+lemma flts_0a:
+  assumes "anonnested (AALTs bs  rs)"
+  shows "AZERO \<notin> set (flts rs)"
+  using assms
+  using flts_0 by blast 
+  
+lemma qqq1:
+  shows "AZERO \<notin> set (flts (map bsimp rs))"
+  by (metis ex_map_conv flts3 agood.simps(1) good1)
+
+
+fun nonazero :: "arexp \<Rightarrow> bool"
+  where
+  "nonazero AZERO = False"
+| "nonazero r = True"
+
+lemma flts_concat:
+  shows "flts rs = concat (map (\<lambda>r. flts [r]) rs)"
+  apply(induct rs)
+   apply(auto)
+  apply(subst k0)
+  apply(simp)
+  done
+
+lemma flts_single1:
+  assumes "anonalt r" "nonazero r"
+  shows "flts [r] = [r]"
+  using assms
+  apply(induct r)
+  apply(auto)
+  done
+
+lemma flts_qq:
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> agood y \<longrightarrow> bsimp y = y" 
+          "\<forall>r'\<in>set rs. agood r' \<and> anonalt r'"
+  shows "flts (map bsimp rs) = rs"
+  using assms
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(subgoal_tac "flts [bsimp a] =  [a]")
+   prefer 2
+   apply(drule_tac x="a" in spec)
+   apply(drule mp)
+    apply(simp)
+   apply(auto)[1]
+  using agood.simps(1) k0b apply blast
+  apply(auto)[1]  
+  done
+  
+lemma test:
+  assumes "agood r"
+  shows "bsimp r = r"
+  using assms
+  apply(induct r taking: "asize" rule: measure_induct)
+  apply(erule agood.elims)
+                      apply(simp_all)
+  apply(subst k0)
+  apply(subst (2) k0)
+                apply(subst flts_qq)
+                  apply(auto)[1]
+                 apply(auto)[1]
+  oops
+
+
+
+lemma bsimp_idem:
+  shows "bsimp (bsimp r) = bsimp r"
+  using test good1
+  oops
+
+
+lemma erase_preimage1:
+  assumes "anonalt r"
+  shows "erase r = ONE \<Longrightarrow> \<exists>bs. r = AONE bs"
+  apply(case_tac r)
+  apply simp+
+  using anonalt.simps(1) assms apply presburger
+  by fastforce
+
+lemma erase_preimage_char:
+  assumes "anonalt r"
+  shows "erase r = CH c \<Longrightarrow> \<exists>bs. r = ACHAR bs c"
+  apply(case_tac r)
+  apply simp+
+  using assms apply fastforce
+  by simp
+
+lemma erase_preimage_seq:
+  assumes "anonalt r"
+  shows "erase r = SEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> erase a1 = r1 \<and> erase a2 = r2"
+  apply(case_tac r)
+  apply simp+
+  using assms apply fastforce
+  by simp
+
+lemma rerase_preimage_seq:
+  assumes "anonalt r"
+  shows "rerase r = RSEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2 "
+  using rerase_preimage4 by presburger
+
+lemma seq_recursive_equality:
+  shows "\<lbrakk>r1 = a1; r2 = a2\<rbrakk> \<Longrightarrow> SEQ r1 r2 = SEQ a1 a2"
+  by meson
+
+lemma almost_identical_image:
+  assumes "agood r" "\<forall>r \<in> rset. agood r"
+  shows "erase r \<in> erase ` rset \<Longrightarrow> \<exists>r' \<in> rset. erase r' = erase r"
+  by auto
+
+lemma goodalts_never_change:
+  assumes "r = AALTs bs rs" "agood r"
+  shows "\<exists>r1 r2. erase r = ALT r1 r2"
+  by (metis agood.simps(4) agood.simps(5) assms(1) assms(2) bmkepss.cases erase.simps(6))
+
+
+fun shape_preserving :: "arexp \<Rightarrow> bool" where
+  "shape_preserving AZERO = True"
+| "shape_preserving (AONE bs) = True"
+| "shape_preserving (ACHAR bs c) = True"
+| "shape_preserving (AALTs bs []) = False"
+| "shape_preserving (AALTs bs [a]) = False"
+| "shape_preserving (AALTs bs (a1 # a2 # rs)) = (\<forall>r \<in> set (a1 # a2 # rs). shape_preserving r)"
+| "shape_preserving (ASEQ bs r1 r2) = (shape_preserving r1 \<and> shape_preserving r2)"
+| "shape_preserving (ASTAR bs r) = shape_preserving r"
+
+
+lemma good_shape_preserving:
+  assumes "\<nexists>bs r0. r = ASTAR bs r0"
+  shows "agood r \<Longrightarrow> shape_preserving r"
+  using assms
+
+  apply(induct r)
+  prefer 6
+  
+  apply blast
+      apply simp
+ 
+  oops
+
+
+
+
+
+lemma shadow_arexp_rerase_erase:
+  shows "\<lbrakk>agood r; agood r';  erase r = erase r'\<rbrakk> \<Longrightarrow> rerase r = rerase r'"
+  apply(induct r )
+       apply simp
+      apply(induct r')
+           apply simp+
+       apply (metis goodalts_never_change rexp.distinct(15))
+  apply simp+
+     apply (metis anonalt.elims(3) erase_preimage_char goodalts_never_change rerase.simps(3) rexp.distinct(21))
+    apply(induct r')
+         apply simp
+  apply simp
+  apply simp
+      apply(subgoal_tac "agood r1")
+  prefer 2
+  apply (metis SizeBound3.good_SEQ agood.simps(10) agood.simps(11) agood.simps(2) agood.simps(3) agood.simps(33) agood.simps(7) bsimp.cases)
+      apply(subgoal_tac "agood r2")
+       apply(subgoal_tac "agood r'1")
+        apply(subgoal_tac "agood r'2")
+         apply(subgoal_tac "rerase r'1 = rerase r1")
+  apply(subgoal_tac "rerase r'2 = rerase r2")
+  
+  using rerase.simps(5) apply presburger
+  sledgehammer
+
+
+lemma rerase_erase_good:
+  assumes "agood r" "\<forall>r \<in> rset. agood r"
+  shows "erase r \<in> erase ` rset \<Longrightarrow> rerase r \<in> rerase ` rset"
+  using assms
+  apply(case_tac r)
+       apply simp+
+  oops
+
+lemma rerase_erase_both:
+  assumes "\<forall>r \<in> rset. agood r" "agood r"
+  shows "(rerase r \<in> (rerase ` rset)) \<longleftrightarrow> (erase r \<in> (erase ` rset))"
+  using assms
+  apply(induct r )
+       apply force
+  apply simp
+      apply(case_tac "RONE \<in> rerase ` rset")
+       apply(subgoal_tac "\<exists>bs. (AONE bs) \<in> rset")
+        apply (metis erase.simps(2) rev_image_eqI)
+       apply (metis image_iff rerase_preimage2)
+      apply(subgoal_tac "\<nexists>bs. (AONE bs) \<in> rset")
+  apply(subgoal_tac "ONE \<notin> erase ` rset")
+  
+        apply blast
+  sledgehammer
+       apply (metis erase_preimage1 image_iff)
+      apply (metis rerase.simps(2) rev_image_eqI)
+     apply (smt (verit, best) erase.simps(3) erase_preimage_char image_iff rerase.simps(3) rerase_preimage3)
+(*    apply simp
+    apply(subgoal_tac "(RSEQ (rerase r1) (rerase r2) \<in> rerase ` rset) \<Longrightarrow>  (SEQ (erase r1) (erase r2) \<in> erase ` rset)")
+  prefer 2
+     apply(subgoal_tac "\<exists>bs a1 a2. (ASEQ bs a1 a2) \<in> rset \<and> rerase a1 = rerase r1 \<and> rerase a2 = rerase r2")
+      prefer 2
+  apply (metis (full_types) image_iff rerase_preimage4)
+     apply(erule exE)+
+     apply(subgoal_tac "erase (ASEQ bs a1 a2) \<in> (erase ` rset) ")
+      apply(subgoal_tac "SEQ (erase a1) (erase a2) \<in> (erase ` rset)")
+  apply(subgoal_tac "SEQ (erase a1) (erase a2) = SEQ (erase r1) (erase r2)")
+        apply metis
+       apply(erule conjE)+*)
+  apply(drule_tac x = "rset" in meta_spec)+
+  
+
+
+
+  oops
+
+
+lemma rerase_pushin1_general:
+  assumes "\<forall>r \<in> set rs. agood r"
+  shows "map rerase (distinctBy rs erase (erase ` rset)) = rdistinct (map rerase rs) (rerase ` rset)"
+  apply(induct rs arbitrary: rset)
+   apply simp+
+  apply(case_tac "erase a \<in> erase ` rset")
+   apply simp
+  
+
+
+  oops
+
+lemma rerase_erase:
+  assumes "\<forall>r \<in> set as. agood r \<and> anonalt r"
+  shows "rdistinct (map rerase as) (rerase ` rset) = map rerase (distinctBy as erase (erase ` rset))"
+  using assms
+  apply(induct as)
+   apply simp+
+
+  sorry
+
+
+lemma rerase_pushin1:
+  assumes "\<forall>r \<in> set rs. anonalt r \<and> agood r"
+  shows "map rerase (distinctBy rs erase {}) = rdistinct (map rerase rs) {}"
+  apply(insert rerase_erase)
+  by (metis assms image_empty)
+  
+
+
+
+
+
+
+lemma nonalt_flts : shows 
+  "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO"
+  using SizeBound3.qqq1 by force
+  
+
+
+
+lemma rerase_list_ders:
+  shows "\<And>x1 x2a.
+       (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> rerase (bsimp x2aa) = rsimp (rerase x2aa)) \<Longrightarrow>
+        (map rerase (distinctBy (flts (map bsimp x2a)) erase {})) =  (rdistinct (rflts (map (rsimp \<circ> rerase) x2a)) {})"
+  apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp x2a)). anonalt r ")
+  prefer 2
+  apply (metis SizeBound3.nn1b SizeBound3.nn1c ex_map_conv)
+  sledgehammer
+
+  sorry
+
+
+lemma simp_rerase:
+  shows "rerase (bsimp a) = rsimp (rerase a)"
+  apply(induct  a)
+  apply simp+
+  using rerase_bsimp_ASEQ apply presburger
+  apply simp
+   apply(subst rerase_bsimp_AALTs)
+  apply(subgoal_tac "map rerase (distinctBy (flts (map bsimp x2a)) erase {}) =  rdistinct (rflts (map (rsimp \<circ> rerase) x2a)) {}")  
+  apply simp
+  using rerase_list_ders apply blast
+  by simp
+
+lemma rders_simp_size:
+  shows " rders_simp (rerase r) s  = rerase (bders_simp r s)"
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply(subst rders_simp_append)
+  apply(subst bders_simp_append)
+  apply(subgoal_tac "rders_simp (rerase r ) xs = rerase (bders_simp r xs)")
+   apply(simp only:)
+   apply simp
+  apply (simp add: der_rerase2 simp_rerase)
+  by simp
+
+
+
+
+corollary aders_simp_finiteness:
+  assumes "\<exists>N. \<forall>s. rsize (rders_simp (rerase r) s) \<le> N"
+  shows " \<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"
+  using assms
+  apply(subgoal_tac "\<forall>s. asize (bders_simp r s) = rsize (rerase (bders_simp r s))")
+   apply(erule exE)
+   apply(rule_tac x = "N" in exI)
+  using rders_simp_size apply auto[1]
+  using asize_rsize by auto
+  
+theorem annotated_size_bound:
+  shows "\<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"
+  apply(insert aders_simp_finiteness)
+  by (simp add: rders_simp_bounded)
+
 end