--- 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