lexing: comparison thys2/SizeBound3.thy

equal deleted inserted replaced

-:61eff2abb0b6
+:1481f465e6ea
 | "erase (AALTs _ [r]) = (erase r)"
 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
 | "erase (ASTAR _ r) = STAR (erase r)"
+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)"
 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
 "fuse bs AZERO = AZERO"
 | "fuse bs (AONE cs) = AONE (bs @ cs)"
 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
 shows "nullable (erase r) = bnullable r"
 apply(induct r rule: erase.induct)
 apply(simp_all)
 done
+lemma rbnullable_correctness:
+shows "rnullable (rerase r) = bnullable r"
+apply(induct r rule: rerase.induct)
+apply simp+
+done
 lemma erase_fuse:
 shows "erase (fuse bs r) = erase r"
 apply(induct r rule: erase.induct)
 apply(simp_all)
 done
+lemma rerase_fuse:
+shows "rerase (fuse bs r) = rerase r"
+apply(induct r)
+apply simp+
+done
 lemma erase_intern [simp]:
 shows "erase (intern r) = r"
 apply(induct r)
 apply(simp_all add: erase_fuse)
 done
 lemma erase_bder [simp]:
 shows "erase (bder a r) = der a (erase r)"
 apply(induct r rule: erase.induct)
 apply(simp_all add: erase_fuse bnullable_correctness)
 done
 lemma erase_bders [simp]:
 shows "erase (bders r s) = ders s (erase r)"
 apply(induct s arbitrary: r )
 apply(simp_all)
 apply (metis (no_types, opaque_lifting) bmkepss.cases bnullable_correctness erase.simps(5) erase.simps(6) mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
 apply (metis r3)
 apply (metis (no_types, lifting) bmkepss.cases bnullable_correctness empty_iff erase.simps(6) list.set(1) mkeps.simps(3) retrieve.simps(4))
 apply (metis r3)
 done
 lemma bmkeps_retrieve:
 assumes "bnullable r"
 shows "bmkeps r = retrieve r (mkeps (erase r))"
 using assms
 apply(induct r)
 "bsimp_AALTs _ [] = AZERO"
 | "bsimp_AALTs bs1 [r] = fuse bs1 r"
 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"
 fun bsimp :: "arexp \<Rightarrow> arexp"
 where
 "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
-| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) "
+| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) rerase {}) "
 | "bsimp r = r"
 fun
 bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 "L (erase (ASEQ bs r1 r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
 apply(simp_all)
 by (metis erase_fuse fuse.simps(4))
+lemma RL_bsimp_ASEQ:
+"RL (rerase (ASEQ bs r1 r2)) = RL (rerase (bsimp_ASEQ bs r1 r2))"
+apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+apply simp+
+done
 lemma L_bsimp_AALTs:
 "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"
 apply(induct bs rs rule: bsimp_AALTs.induct)
 apply(simp_all add: erase_fuse)
 done
+lemma RL_bsimp_AALTs:
+"RL (rerase (AALTs bs rs)) = RL (rerase (bsimp_AALTs bs rs))"
+apply(induct bs rs rule: bsimp_AALTs.induct)
+apply(simp_all add: rerase_fuse)
+done
+lemma RL_rerase_AALTs:
+shows "RL (rerase (AALTs bs rs)) = \<Union> (RL ` rerase ` (set rs))"
+apply(induct rs)
+apply(simp)
+apply(simp)
+done
 lemma L_erase_AALTs:
 shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"
 apply(induct rs)
 apply(simp)
 apply(simp)
 apply(case_tac rs)
 apply(simp)
 apply(simp)
 done
 lemma L_erase_flts:
 shows "\<Union> (L ` erase ` (set (flts rs))) = \<Union> (L ` erase ` (set rs))"
 apply(induct rs rule: flts.induct)
 apply(simp_all)
 apply(auto)
 using L_erase_AALTs erase_fuse apply auto[1]
 by (simp add: L_erase_AALTs erase_fuse)
+lemma RL_erase_flts:
+shows "\<Union> (RL ` rerase ` (set (flts rs))) =
+\<Union> (RL ` rerase ` (set rs))"
+apply(induct rs rule: flts.induct)
+apply simp+
+apply auto
+apply (smt (verit) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6))
+by (smt (verit, best) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6))
 lemma L_erase_dB_acc:
 shows "(\<Union> (L ` acc) \<union> (\<Union> (L ` erase ` (set (distinctBy rs erase acc)))))
 = \<Union> (L ` acc) \<union>  \<Union> (L ` erase ` (set rs))"
 apply(induction rs arbitrary: acc)
 apply simp_all
 by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute)
+lemma RL_rerase_dB_acc:
+shows "(\<Union> (RL ` acc) \<union> (\<Union> (RL ` rerase ` (set (distinctBy rs rerase acc)))))
+= \<Union> (RL ` acc) \<union> \<Union> (RL ` rerase ` (set rs))"
+apply(induction rs arbitrary: acc)
+apply simp_all
+by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute)
 lemma L_erase_dB:
 shows "(\<Union> (L ` erase ` (set (distinctBy rs erase {})))) = \<Union> (L ` erase ` (set rs))"
 by (metis L_erase_dB_acc Un_commute Union_image_empty)
+lemma RL_rerase_dB:
+shows "(\<Union> (RL ` rerase ` (set (distinctBy rs rerase {})))) = \<Union> (RL ` rerase ` (set rs))"
+by (metis RL_rerase_dB_acc Un_commute Union_image_empty)
+(*
 lemma L_bsimp_erase:
 shows "L (erase r) = L (erase (bsimp r))"
 apply(induct r)
 apply(simp)
 apply(simp)
 apply(subst (2)L_erase_AALTs)
 apply(subst L_erase_dB)
 apply(subst L_erase_flts)
 apply (simp add: L_erase_AALTs)
 done
+*)
-lemma L_bders_simp:
-shows "L (erase (bders_simp r s)) = L (erase (bders r s))"
+lemma RL_bsimp_rerase:
+shows "RL (rerase r) = RL (rerase (bsimp r))"
+apply(induct r)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(auto simp add: Sequ_def)[1]
+apply(subst RL_bsimp_ASEQ[symmetric])
+apply(auto simp add: Sequ_def)[1]
+apply(subst (asm)  RL_bsimp_ASEQ[symmetric])
+apply(auto simp add: Sequ_def)[1]
+apply(simp)
+apply(subst RL_bsimp_AALTs[symmetric])
+defer
+apply(simp)
+using RL_erase_flts RL_rerase_dB by force
+lemma rder_correctness:
+shows "RL (rder c r) = Der c (RL r)"
+by (simp add: RL_rder)
+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 rder_bder_rerase:
+shows "rder c (rerase r ) = rerase (bder c r)"
+apply (induct r)
+apply simp+
+apply(case_tac "bnullable r1")
+apply simp
+apply (simp add: rb_nullability rerase_fuse)
+using rb_nullability apply presburger
+apply simp
+apply simp
+using rerase_fuse by presburger
+lemma RL_bder_preserved:
+shows "RL (rerase a1) = RL (rerase a2) \<Longrightarrow> RL (rerase (bder c a1 )) = RL (rerase (bder c a2))"
+by (metis rder_bder_rerase rder_correctness)
+lemma RL_bders_simp:
+shows "RL (rerase (bders_simp r s)) = RL (rerase (bders r s))"
 apply(induct s arbitrary: r rule: rev_induct)
 apply(simp)
-apply(simp)
+apply(simp add: bders_append)
-apply(simp add: ders_append)
 apply(simp add: bders_simp_append)
-apply(simp add: L_bsimp_erase[symmetric])
+apply(simp add: RL_bsimp_rerase[symmetric])
-by (simp add: der_correctness)
+using RL_bder_preserved by blast
 lemma bmkeps_fuse:
 assumes "bnullable r"
 shows "bmkeps (fuse bs r) = bs @ bmkeps r"
 lemma b4:
 shows "bnullable (bders_simp r s) = bnullable (bders r s)"
 proof -
-have "L (erase (bders_simp r s)) = L (erase (bders r s))"
+have "RL (rerase (bders_simp r s)) = RL (rerase (bders r s))"
-using L_bders_simp by force
+by (simp add: RL_bders_simp)
 then show "bnullable (bders_simp r s) = bnullable (bders r s)"
-using bnullable_correctness nullable_correctness by blast
+using RL_rnullable rb_nullability by blast
 qed
 lemma bder_fuse:
 shows "bder c (fuse bs a) = fuse bs  (bder c a)"
 | ss1:  "[] s\<leadsto> []"
 | ss2:  "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"
 | ss3:  "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"
 | ss4:  "(AZERO # rs) s\<leadsto> rs"
 | ss5:  "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"
-| ss6:  "erase a1 = erase a2 \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"
+| ss6:  "rerase a1 = rerase a2 \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"
 inductive
 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
 where
 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)"
 using assms
 by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)
 lemma ss6_stronger_aux:
-shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))"
+shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 rerase (set (map rerase rs1)))"
 apply(induct rs2 arbitrary: rs1)
 apply(auto)
 apply (smt (verit, best) append.assoc append.right_neutral append_Cons append_Nil split_list srewrite2(2) srewrites_trans ss6)
 apply(drule_tac x="rs1 @ [a]" in meta_spec)
 apply(simp)
 done
 lemma ss6_stronger:
-shows "rs1 s\<leadsto>* distinctBy rs1 erase {}"
+shows "rs1 s\<leadsto>* distinctBy rs1 rerase {}"
-using ss6_stronger_aux[of "[]" _] by auto
+by (metis append_Nil list.set(1) list.simps(8) ss6_stronger_aux)
 lemma rewrite_preserves_fuse:
 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3"
 and   "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3"
 by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps)
 next
 case (ss6 a1 a2 rsa rsb rsc)
 then show ?case
 apply(simp only: map_append)
-by (smt (verit, ccfv_threshold) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps)
+by (smt (verit, ccfv_threshold) rerase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps)
 qed (auto intro: rrewrite_srewrite.intros)
 lemma rewrites_fuse:
 assumes "r1 \<leadsto>* r2"
 lemma bnullable0:
 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2"
 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2"
 apply(induct rule: rrewrite_srewrite.inducts)
 apply(auto simp add:  bnullable_fuse)
 apply (meson UnCI bnullable_fuse imageI)
-by (metis bnullable_correctness)
+by (metis rb_nullability)
 lemma rewritesnullable:
 assumes "r1 \<leadsto>* r2"
 shows "bnullable r1 = bnullable r2"
 then show ?case
 by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)
 next
 case (ss6 a1 a2 rsa rsb rsc)
 then show ?case
-by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness)
+by (smt (z3) append_is_Nil_conv bmkepss1 bmkepss2 in_set_conv_decomp_first list.set_intros(1) rb_nullability set_ConsD)
 qed (auto)
 lemma rewrites_bmkeps:
 assumes "r1 \<leadsto>* r2" "bnullable r1"
 shows "bmkeps r1 = bmkeps r2"
 next
 case (2 bs1 rs)
 have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact
 then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites)
 also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites)
-also have "... s\<leadsto>* distinctBy (flts (map bsimp rs)) erase {}" by (simp add: ss6_stronger)
+also have "... s\<leadsto>* distinctBy (flts (map bsimp rs)) rerase {}" by (simp add: ss6_stronger)
-finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})"
+finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) rerase {})"
-using contextrewrites0 by blast
+using contextrewrites0 by auto
-also have "... \<leadsto>* bsimp_AALTs  bs1 (distinctBy (flts (map bsimp rs)) erase {})"
+also have "... \<leadsto>* bsimp_AALTs  bs1 (distinctBy (flts (map bsimp rs)) rerase {})"
 by (simp add: bsimp_AALTs_rewrites)
 finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp
 qed (simp_all)
 using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast
 next
 case (ss6 a1 a2 bs rsa rsb)
 then show ?case
 apply(simp only: map_append)
-by (smt (verit, best) erase_bder list.simps(8) list.simps(9) local.ss6 rrewrite_srewrite.ss6 srewrites.simps)
+by (smt (verit, best) rder_bder_rerase list.simps(8) list.simps(9) local.ss6 rrewrite_srewrite.ss6 srewrites.simps)
 qed
 lemma rewrites_preserves_bder:
 assumes "r1 \<leadsto>* r2"
 shows "bder c r1 \<leadsto>* bder c r2"
 theorem blexersimp_correctness:
 shows "lexer r s = blexer_simp r s"
 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)"
-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)
 "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 (AALTs cs (r1#r2#rs)) = (distinct (map rerase (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"
 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)"
+assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. anonalt r" "distinct (map rerase 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)
 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)))")
+apply(subgoal_tac "agood (AALTs bs1 (v # vb # vc)) = ((\<forall>r \<in> (set (v # vb # vc)). agood r \<and> anonalt r) \<and> distinct (map rerase (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)))")
+apply(subgoal_tac "((\<forall>r\<in>set (v # vb # vc). agood r \<and> anonalt r) \<and> distinct (map rerase (v # vb # vc))) = ((\<forall>r\<in>set (v # vb # vc). agood r) \<and> distinct (map rerase (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) ")
+apply(subgoal_tac "((\<forall>r \<in> set (v # vb # vc). agood r) \<and> distinct (map rerase (v # vb # vc))) = (\<forall> r \<in> set (v # vb # vc). agood r) ")
 prefer 2
-apply(subgoal_tac "distinct (map erase (v # vb # vc)) = True")
+apply(subgoal_tac "distinct (map rerase (v # vb # vc)) = True")
 prefer 2
+sledgehammer
 apply blast
 prefer 2
 apply force
 apply simp
 done
 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)"
+shows "(\<forall>r \<in> set rs. P r) \<longrightarrow> (\<forall>r \<in> set (distinctBy rs rerase 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))"
+shows "rerase a \<in> rset \<Longrightarrow> a \<notin> set (distinctBy rs rerase (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)))"
+shows "distinct (distinctBy rs rerase (insert (rerase a) rset)) \<Longrightarrow> distinct (a #  (distinctBy rs rerase (insert (rerase a) rset)))"
 using dB_filters_out by force
 lemma dB_does_the_job2:
-shows "distinct (distinctBy rs erase rset)"
+shows "distinct (distinctBy rs rerase rset)"
 apply(induct rs arbitrary: rset)
 apply simp
-apply(case_tac "erase a \<in> rset")
+apply(case_tac "rerase a \<in> rset")
 apply simp
-apply(drule_tac x = "insert (erase a) rset" in meta_spec)
+apply(drule_tac x = "insert (rerase a) rset" in meta_spec)
-apply(subgoal_tac "distinctBy (a # rs) erase rset = a # distinctBy rs erase (insert (erase a ) rset)")
+apply(subgoal_tac "distinctBy (a # rs) rerase rset = a # distinctBy rs rerase (insert (rerase 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))"
+shows "distinct (map rerase (distinctBy rs rerase rset))"
 apply(induct rs arbitrary:rset)
 apply simp
-apply(case_tac "erase a \<in> rset")
+apply(case_tac "rerase 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' = []"
+shows "rset \<subseteq> rset' \<Longrightarrow> distinctBy rs rerase rset = [] \<Longrightarrow> distinctBy rs rerase rset' = []"
 apply(induct rs arbitrary: rset rset')
 apply simp+
 by (meson in_mono list.discI)
 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")
+apply(subgoal_tac "\<forall>r \<in> set (distinctBy (flts (map bsimp x2a)) rerase {}). 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+
 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
+sledgehammer
 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
 lemma good1a:
-assumes "L (erase a) \<noteq> {}"
+assumes "RL (rerase a) \<noteq> {}"
 shows "agood (bsimp a)"
 using good1 assms
-using L_bsimp_erase by force
+using RL_bsimp_rerase by force
 lemma flts_append:
 "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
 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+
 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
+oops
 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"
 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_map_bsimp:
+assumes "\<And> r. r \<in> set x2a \<Longrightarrow> rerase (bsimp r) = (rsimp \<circ> rerase) r"
-lemma rerase_list_ders:
+shows "  map rerase (map bsimp x2a) =  map (rsimp \<circ> rerase) x2a "
-shows "\<And>x1 x2a.
+using assms
-(\<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(induct x2a)
-apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp x2a)). anonalt r ")
+apply simp
+apply(subgoal_tac "a \<in> set (a # x2a)")
 prefer 2
-apply (metis SizeBound3.nn1b SizeBound3.nn1c ex_map_conv)
+apply (meson list.set_intros(1))
-sledgehammer
+apply(subgoal_tac "rerase (bsimp a ) = (rsimp \<circ> rerase) a")
+apply simp
-sorry
+by presburger
+lemma rerase_flts:
+shows "map rerase (flts rs) = rflts (map rerase rs)"
+apply(induct rs)
+apply simp+
+apply(case_tac a)
+apply simp+
+apply(simp add: rerase_fuse)
+apply simp
+done
+lemma rerase_dB:
+shows "map rerase (distinctBy rs rerase acc) = rdistinct (map rerase rs) acc"
+apply(induct rs arbitrary: acc)
+apply simp+
+done
+lemma rerase_earlier_later_same:
+assumes " \<And>r. r \<in> set x2a \<Longrightarrow> rerase (bsimp r) = rsimp (rerase r)"
+shows " (map rerase (distinctBy (flts (map bsimp x2a)) rerase {})) =
+(rdistinct (rflts (map (rsimp \<circ> rerase) x2a)) {})"
+apply(subst rerase_dB)
+apply(subst rerase_flts)
+apply(subst rerase_map_bsimp)
+apply auto
+using assms
+apply simp
+done
 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(subgoal_tac "map rerase (distinctBy (flts (map bsimp x2a)) rerase {}) =  rdistinct (rflts (map (rsimp \<circ> rerase) x2a)) {}")
+apply simp
+using rerase_earlier_later_same apply presburger
 apply simp
-using rerase_list_ders apply blast
+done
-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

changeset 493	1481f465e6ea
parent 492	61eff2abb0b6
child 543	b2bea5968b89