--- a/thys2/SizeBound3.thy Tue Apr 19 09:08:01 2022 +0100
+++ b/thys2/SizeBound3.thy Thu Apr 21 14:58:51 2022 +0100
@@ -117,6 +117,16 @@
| "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"
@@ -236,12 +246,28 @@
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)
@@ -254,6 +280,10 @@
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 )
@@ -376,7 +406,8 @@
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))"
@@ -556,10 +587,12 @@
| "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"
@@ -587,12 +620,31 @@
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)
@@ -603,6 +655,8 @@
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)
@@ -611,6 +665,19 @@
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))"
@@ -618,11 +685,25 @@
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)
@@ -643,16 +724,81 @@
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: ders_append)
+ apply(simp add: bders_append)
apply(simp add: bders_simp_append)
- apply(simp add: L_bsimp_erase[symmetric])
- by (simp add: der_correctness)
+ apply(simp add: RL_bsimp_rerase[symmetric])
+ using RL_bder_preserved by blast
+
lemma bmkeps_fuse:
@@ -672,10 +818,10 @@
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))"
- using L_bders_simp by force
+ have "RL (rerase (bders_simp r s)) = RL (rerase (bders r s))"
+ 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
@@ -706,7 +852,7 @@
| 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
@@ -810,7 +956,7 @@
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)
@@ -819,8 +965,8 @@
done
lemma ss6_stronger:
- shows "rs1 s\<leadsto>* distinctBy rs1 erase {}"
- using ss6_stronger_aux[of "[]" _] by auto
+ shows "rs1 s\<leadsto>* distinctBy rs1 rerase {}"
+ by (metis append_Nil list.set(1) list.simps(8) ss6_stronger_aux)
lemma rewrite_preserves_fuse:
@@ -850,7 +996,7 @@
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)
@@ -924,8 +1070,8 @@
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)
+ apply (meson UnCI bnullable_fuse imageI)
+ by (metis rb_nullability)
lemma rewritesnullable:
@@ -956,7 +1102,7 @@
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:
@@ -1015,10 +1161,10 @@
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)
- finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})"
- using contextrewrites0 by blast
- also have "... \<leadsto>* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})"
+ 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)) rerase {})"
+ using contextrewrites0 by auto
+ 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)
@@ -1107,7 +1253,7 @@
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:
@@ -1160,36 +1306,6 @@
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"
@@ -1307,7 +1423,7 @@
| "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"
@@ -1383,7 +1499,7 @@
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)
@@ -1395,18 +1511,19 @@
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")
- prefer 2
+ apply(subgoal_tac "distinct (map rerase (v # vb # vc)) = True")
+ prefer 2
+ sledgehammer
apply blast
prefer 2
apply force
@@ -1628,13 +1745,13 @@
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")
@@ -1642,33 +1759,32 @@
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(subgoal_tac "distinctBy (a # rs) erase rset = a # distinctBy rs erase (insert (erase a ) rset)")
+ apply(drule_tac x = "insert (rerase a) rset" in meta_spec)
+ 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)
@@ -1692,12 +1808,11 @@
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
+ 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)
@@ -1761,6 +1876,8 @@
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
@@ -1820,10 +1937,10 @@
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
@@ -1940,7 +2057,7 @@
using test good1
oops
-
+(*
lemma erase_preimage1:
assumes "anonalt r"
shows "erase r = ONE \<Longrightarrow> \<exists>bs. r = AONE bs"
@@ -2036,7 +2153,8 @@
apply(subgoal_tac "rerase r'2 = rerase r2")
using rerase.simps(5) apply presburger
- sledgehammer
+ oops
+
lemma rerase_erase_good:
@@ -2114,7 +2232,7 @@
apply(insert rerase_erase)
by (metis assms image_empty)
-
+*)
@@ -2123,20 +2241,55 @@
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"
+ shows " map rerase (map bsimp x2a) = map (rsimp \<circ> rerase) x2a "
+ using assms
+
+ apply(induct x2a)
+ apply simp
+ apply(subgoal_tac "a \<in> set (a # x2a)")
+ prefer 2
+ apply (meson list.set_intros(1))
+ apply(subgoal_tac "rerase (bsimp a ) = (rsimp \<circ> rerase) a")
+ apply simp
+ 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_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
+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
- sorry
lemma simp_rerase:
@@ -2146,10 +2299,13 @@
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
- by simp
+ done
+
+
lemma rders_simp_size:
shows " rders_simp (rerase r) s = rerase (bders_simp r s)"