diff --git a/thys/Hahn_Jordan_Decomposition/Extended_Reals_Sums_Compl.thy b/thys/Hahn_Jordan_Decomposition/Extended_Reals_Sums_Compl.thy --- a/thys/Hahn_Jordan_Decomposition/Extended_Reals_Sums_Compl.thy +++ b/thys/Hahn_Jordan_Decomposition/Extended_Reals_Sums_Compl.thy @@ -1,232 +1,232 @@ theory Extended_Reals_Sums_Compl imports "HOL-Analysis.Analysis" begin lemma real_ereal_leq: fixes a::ereal and b::real assumes "real_of_ereal a \ b" and "a \ \" shows "a \ ereal b" - by (metis (mono_tags, hide_lams) MInfty_eq_minfinity assms eq_iff ereal_eq_0(2) ereal_le_real_iff + by (metis (mono_tags, opaque_lifting) MInfty_eq_minfinity assms eq_iff ereal_eq_0(2) ereal_le_real_iff ereal_less_eq(2) le_cases real_of_ereal.elims real_of_ereal.simps(1) zero_ereal_def) lemma ereal_sums_Pinfty: fixes f::"nat \ ereal" assumes "f sums \" and "\n. \f n\ \ \" shows "(\n. - f n) sums -\" proof - define rf where "rf = (\n. real_of_ereal (f n))" have "\n. f n = ereal (rf n)" unfolding rf_def using assms by (simp add: ereal_real') define g where "g = (\n. (\i \ {..< n}. rf i))" define gm where "gm = (\n. (\i \ {..< n}. - rf i))" have "\n. gm n = - g n" unfolding g_def gm_def by (simp add: sum_negf) hence "\n. ereal (gm n) = (\i \ {..< n}.- f i)" using \\n. f n = ereal (rf n)\ using gm_def by auto have "(\n. ereal (g n)) \ \" using assms \\n. f n = ereal (rf n)\ unfolding sums_def g_def by simp have "\M. \N. \n\ N. (gm n) \ M" proof fix M have "\N. \n\ N. ereal (-M) \ g n" using \g \ \\ Lim_PInfty by simp from this obtain N where "\n\ N. ereal (-M) \ g n" by auto hence "\n \ N. - (g n) \ M" by auto hence "\n \ N. gm n \ M" using \\n. gm n = - g n\ by simp thus "\N. \n \ N. gm n \ M" by auto qed hence "(\n. ereal (gm n)) \ -\" by (simp add: Lim_MInfty) thus ?thesis using \\n. ereal (gm n) = (\i \ {..< n}.- f i)\ unfolding sums_def by simp qed lemma ereal_sums_Minfty: fixes f::"nat \ ereal" assumes "f sums -\" and "\n. \f n\ \ \" shows "(\n. - f n) sums \" proof - define rf where "rf = (\n. real_of_ereal (f n))" have "\n. f n = ereal (rf n)" unfolding rf_def using assms by (simp add: ereal_real') define g where "g = (\n. (\i \ {..< n}. rf i))" define gm where "gm = (\n. (\i \ {..< n}. - rf i))" have "\n. gm n = - g n" unfolding g_def gm_def by (simp add: sum_negf) hence "\n. ereal (gm n) = (\i \ {..< n}.- f i)" using \\n. f n = ereal (rf n)\ using gm_def by auto have "(\n. ereal (g n)) \ -\" using assms \\n. f n = ereal (rf n)\ unfolding sums_def g_def by simp have "\M. \N. \n\ N. M \ (gm n)" proof fix M have "\N. \n\ N. g n \ ereal (-M)" using \g \ -\\ Lim_MInfty by simp from this obtain N where "\n\ N. g n \ ereal (-M)" by auto hence "\n \ N. M \ - (g n)" by auto hence "\n \ N. M \ gm n" using \\n. gm n = - g n\ by simp thus "\N. \n \ N. M \ gm n" by auto qed hence "(\n. ereal (gm n)) \ \" by (simp add: Lim_PInfty) thus ?thesis using \\n. ereal (gm n) = (\i \ {..< n}.- f i)\ unfolding sums_def by simp qed lemma mem_sums_Pinfty: assumes "((f i)::ereal) = \" shows "f sums \" proof - define g where "g = (\n. (\i \ {..< n}. f i))" have ginf: "\ j \ Suc i. g j = \" proof (intro allI impI) fix j assume "Suc i \ j" hence "i < j" by simp hence "i \ {..< j}" by auto thus "g j = \" unfolding g_def using sum_Pinfty[of f "{..< j}"] assms by blast qed have "\M. \N. \n\ N. M \ (g n)" proof fix M show "\N. \n\ N. M \ g n" using ginf by force qed hence "g \ \" by (simp add: Lim_PInfty) thus ?thesis unfolding sums_def g_def by simp qed lemma sum_Minfty: fixes f :: "nat \ ereal" shows "\i. finite P \ i \ P \ f i = - \ \ \ \ range f \ sum f P = -\" proof - fix i assume "finite P" and "i \ P" and "f i = -\" and "\ \ range f" thus "sum f P = -\" proof induct case empty then show ?case by simp next case (insert x F) then show ?case by (metis ereal_plus_eq_MInfty insert_iff rangeI sum.insert sum_Pinfty) qed qed lemma mem_sums_Minfty: assumes "((f i)::ereal) = -\" and "\ \ range f" shows "f sums -\" proof - define g where "g = (\n. (\i \ {..< n}. f i))" have ginf: "\ j \ Suc i. g j = -\" proof (intro allI impI) fix j assume "Suc i \ j" hence "i < j" by simp hence "i \ {..< j}" by auto thus "g j = -\" unfolding g_def using sum_Minfty[of "{..< j}"] assms by simp qed have "\M. \N. \n\ N. (g n) \ M" proof fix M show "\N. \n\ N. g n \ M" using ginf by force qed hence "g \ -\" by (simp add: Lim_MInfty) thus ?thesis unfolding sums_def g_def by simp qed lemma ereal_sums_not_infty: assumes "f sums (a::ereal)" and "\a\ \ \" shows "\n. \f n\ \ \" proof (rule ccontr) fix n assume "\\f n\ \ \" hence "\f n\ = \" by simp show False proof (cases "f n = \") case True hence "f sums \" using mem_sums_Pinfty by simp thus False using assms sums_unique2 by force next case False hence "f n = -\" using \\f n\ = \\ by blast show False proof (cases "\i. f i = \") case True from this obtain i where "f i = \" by auto hence "f sums \" using mem_sums_Pinfty by simp thus False using assms sums_unique2 by force next case False hence "\i. f i \ \" by simp hence "f sums -\" using mem_sums_Minfty \f n = -\\ by (metis MInfty_eq_minfinity image_iff) thus False using assms sums_unique2 by force qed qed qed lemma ereal_sums_not_infty_minus: assumes "f sums (a::ereal)" and "\a\ \ \" shows "(\n. - f n) sums -a" proof - have "\n. \f n\ \ \" using assms ereal_sums_not_infty by simp define g where "g = (\n. real_of_ereal (f n))" have "\n. f n = ereal (g n)" using \\n. \f n\ \ \\ by (simp add: ereal_real' g_def) hence "\n. - f n = ereal (-g n)" by simp have "\r. a = ereal (r)" using assms by auto from this obtain r where "a = ereal r" by auto hence "f sums (ereal r)" using assms by simp hence "(\n. ereal (g n)) sums (ereal r)" using \\n. f n = ereal (g n)\ sums_cong[of f "\n. ereal (g n)"] by simp hence "g sums r" by (simp add: sums_ereal) hence "(\n. -g n) sums -r" using sums_minus[of g] by simp hence "(\n. ereal (- g n)) sums ereal (-r)" by (simp add: sums_ereal) hence "(\n. - f n) sums (ereal (-r))" using \\n. - f n = ereal (-g n)\ sums_cong[of f "\n. ereal (g n)"] by simp thus ?thesis using \a = ereal r\ by simp qed lemma ereal_sums_minus: fixes f::"nat \ ereal" assumes "f sums a" and "\n. \f n\ \ \" shows "(\n. - f n) sums -a" proof (cases "\a\ = \") case False thus ?thesis using assms ereal_sums_not_infty_minus by simp next case True hence "a = \ \ a = - \" by auto thus ?thesis using assms ereal_sums_Pinfty ereal_sums_Minfty by auto qed lemma sums_minus': fixes f::"nat \ ereal" assumes "-\ \ range f \ \ \ range f" and "f sums a" shows "(\n. - f n) sums (- a)" proof (cases "\n. \f n\ \ \") case True thus ?thesis using ereal_sums_minus assms by simp next case False have "\n. \f n\ = \" using False by simp from this obtain n where "\f n\ = \" by meson show ?thesis proof (cases "\ \ range f") case True hence "\j. f j = \" by (metis image_iff) from this obtain j where "f j = \" by auto hence "a = \" using mem_sums_Pinfty assms(2) sums_unique2 by blast moreover have "-\ \ range f" using assms True by simp ultimately show ?thesis using mem_sums_Minfty[of "\n. - f n"] assms \f j = \\ using ereal_uminus_eq_reorder by fastforce next case False hence "f n = -\" using \\f n\ = \\ by (metis ereal_infinity_cases range_eqI) hence "a = -\" using mem_sums_Minfty False sums_unique2 assms(2) by blast thus ?thesis using mem_sums_Pinfty[of "\n. - f n"] assms by (metis MInfty_eq_minfinity \f n = - \\ ereal_uminus_uminus uminus_ereal.simps(3)) qed qed end \ No newline at end of file diff --git a/thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Decomposition.thy b/thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Decomposition.thy --- a/thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Decomposition.thy +++ b/thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Decomposition.thy @@ -1,2176 +1,2176 @@ section \Signed measures\ text \In this section we define signed measures. These are generalizations of measures that can also take negative values but cannot contain both $\infty$ and $-\infty$ in their range.\ subsection \Basic definitions\ theory Hahn_Jordan_Decomposition imports "HOL-Probability.Probability" Hahn_Jordan_Prelims begin definition signed_measure::"'a measure \ ('a set \ ereal) \ bool" where "signed_measure M \ \ \ {} = 0 \ (-\ \ range \ \ \ \ range \) \ (\A. range A \ sets M \ disjoint_family A \ \ (range A) \ sets M \ (\i. \ (A i)) sums \ (\ (range A))) \ (\A. range A \ sets M \ disjoint_family A \ \ (range A) \ sets M \ \\ (\ (range A))\ < \ \ summable (\i. real_of_ereal \\ (A i)\))" lemma signed_measure_empty: assumes "signed_measure M \" shows "\ {} = 0" using assms unfolding signed_measure_def by simp lemma signed_measure_sums: assumes "signed_measure M \" and "range A \ M" and "disjoint_family A" and "\ (range A) \ sets M" shows "(\i. \ (A i)) sums \ (\ (range A))" using assms unfolding signed_measure_def by simp lemma signed_measure_summable: assumes "signed_measure M \" and "range A \ M" and "disjoint_family A" and "\ (range A) \ sets M" and "\\ (\ (range A))\ < \" shows "summable (\i. real_of_ereal \\ (A i)\)" using assms unfolding signed_measure_def by simp lemma signed_measure_inf_sum: assumes "signed_measure M \" and "range A \ M" and "disjoint_family A" and "\ (range A) \ sets M" shows "(\i. \ (A i)) = \ (\ (range A))" using sums_unique assms signed_measure_sums by (metis) lemma signed_measure_abs_convergent: assumes "signed_measure M \" and "range A \ sets M" and "disjoint_family A" and "\ (range A) \ sets M" and "\\ (\ (range A))\ < \" shows "summable (\i. real_of_ereal \\ (A i)\)" using assms unfolding signed_measure_def by simp lemma signed_measure_additive: assumes "signed_measure M \" shows "additive M \" proof (auto simp add: additive_def) fix x y assume x: "x \ M" and y: "y \ M" and "x \ y = {}" hence "disjoint_family (binaryset x y)" by (auto simp add: disjoint_family_on_def binaryset_def) have "(\i. \ ((binaryset x y) i)) sums (\ x + \ y)" using binaryset_sums signed_measure_empty[of M \] assms by simp have "range (binaryset x y) = {x, y, {}}" using range_binaryset_eq by simp moreover have "{x, y, {}} \ M" using x y by auto moreover have "x\y \ sets M" using x y by simp moreover have "(\ (range (binaryset x y))) = x\ y" by (simp add: calculation(1)) ultimately have "(\i. \ ((binaryset x y) i)) sums \ (x \ y)" using assms x y signed_measure_empty[of M \] signed_measure_sums[of M \] \disjoint_family (binaryset x y)\ by (metis) then show "\ (x \ y) = \ x + \ y" using \(\i. \ ((binaryset x y) i)) sums (\ x + \ y)\ sums_unique2 by force qed lemma signed_measure_add: assumes "signed_measure M \" and "a\ sets M" and "b\ sets M" and "a\ b = {}" shows "\ (a\ b) = \ a + \ b" using additiveD[OF signed_measure_additive] assms by auto lemma signed_measure_disj_sum: shows "finite I \ signed_measure M \ \ disjoint_family_on A I \ (\i. i \ I \ A i \ sets M) \ \ (\ i\ I. A i) = (\ i\ I. \ (A i))" proof (induct rule:finite_induct) case empty then show ?case unfolding signed_measure_def by simp next case (insert x F) have "\ (\ (A ` insert x F)) = \ ((\ (A `F)) \ A x)" by (simp add: Un_commute) also have "... = \ (\ (A `F)) + \ (A x)" proof - have "(\ (A `F)) \ (A x) = {}" using insert by (metis disjoint_family_on_insert inf_commute) moreover have "\ (A `F) \ sets M" using insert by auto moreover have "A x \ sets M" using insert by simp ultimately show ?thesis by (meson insert.prems(1) signed_measure_add) qed also have "... = (\ i\ F. \ (A i)) + \ (A x)" using insert by (metis disjoint_family_on_insert insert_iff) also have "... = (\i\insert x F. \ (A i))" by (simp add: add.commute insert.hyps(1) insert.hyps(2)) finally show ?case . qed lemma pos_signed_measure_count_additive: assumes "signed_measure M \" and "\ E \ sets M. 0 \ \ E" shows "countably_additive (sets M) (\A. e2ennreal (\ A))" unfolding countably_additive_def proof (intro allI impI) fix A::"nat \ 'a set" assume "range A \ sets M" and "disjoint_family A" and "\ (range A) \ sets M" note Aprops = this have eq: "\i. \ (A i) = enn2ereal (e2ennreal (\ (A i)))" using assms enn2ereal_e2ennreal Aprops by simp have "(\n. \i\n. \ (A i)) \ \ (\ (range A))" using sums_def_le[of "\i. \ (A i)" "\ (\ (range A))"] assms signed_measure_sums[of M] Aprops by simp hence "((\n. e2ennreal (\i\n. \ (A i))) \ e2ennreal (\ (\ (range A)))) sequentially" using tendsto_e2ennrealI[of "(\n. \i\n. \ (A i))" "\ (\ (range A))"] by simp moreover have "\n. e2ennreal (\i\n. \ (A i)) = (\i\n. e2ennreal (\ (A i)))" using e2ennreal_finite_sum by (metis enn2ereal_nonneg eq finite_atMost) ultimately have "((\n. (\i\n. e2ennreal (\ (A i)))) \ e2ennreal (\ (\ (range A)))) sequentially" by simp hence "(\i. e2ennreal (\ (A i))) sums e2ennreal (\ (\ (range A)))" using sums_def_le[of "\i. e2ennreal (\ (A i))" "e2ennreal (\ (\ (range A)))"] by simp thus "(\i. e2ennreal (\ (A i))) = e2ennreal (\ (\ (range A)))" using sums_unique assms by (metis) qed lemma signed_measure_minus: assumes "signed_measure M \" shows "signed_measure M (\A. - \ A)" unfolding signed_measure_def proof (intro conjI) show "- \ {} = 0" using assms unfolding signed_measure_def by simp show "- \ \ range (\A. - \ A) \ \ \ range (\A. - \ A)" proof (cases "\ \ range \") case True hence "-\ \ range \" using assms unfolding signed_measure_def by simp hence "\ \ range (\A. - \ A)" using ereal_uminus_eq_reorder by blast thus "- \ \ range (\A. - \ A) \ \ \ range (\A. - \ A)" by simp next case False hence "-\ \ range (\A. - \ A)" using ereal_uminus_eq_reorder by (simp add: image_iff) thus "- \ \ range (\A. - \ A) \ \ \ range (\A. - \ A)" by simp qed show "\A. range A \ sets M \ disjoint_family A \ \ (range A) \ sets M \ \- \ (\ (range A))\ < \ \ summable (\i. real_of_ereal \- \ (A i)\)" proof (intro allI impI) fix A::"nat \ 'a set" assume "range A \ sets M" and "disjoint_family A" and "\ (range A) \ sets M" and "\- \ (\ (range A))\ < \" thus "summable (\i. real_of_ereal \- \ (A i)\)" using assms unfolding signed_measure_def by simp qed show "\A. range A \ sets M \ disjoint_family A \ \ (range A) \ sets M \ (\i. - \ (A i)) sums - \ (\ (range A))" proof - { fix A::"nat \ 'a set" assume "range A \ sets M" and "disjoint_family A" and "\ (range A) \ sets M" note Aprops = this have "- \ \ range (\i. \ (A i)) \ \ \ range (\i. \ (A i))" proof - have "range (\i. \ (A i)) \ range \" by auto thus ?thesis using assms unfolding signed_measure_def by auto qed moreover have "(\i. \ (A i)) sums \ (\ (range A))" using signed_measure_sums[of M] Aprops assms by simp ultimately have "(\i. - \ (A i)) sums - \ (\ (range A))" using sums_minus'[of "\i. \ (A i)"] by simp } thus ?thesis by auto qed qed locale near_finite_function = fixes \:: "'b set \ ereal" assumes inf_range: "- \ \ range \ \ \ \ range \" lemma (in near_finite_function) finite_subset: assumes "\\ E\ < \" and "A\ E" and "\ E = \ A + \ (E - A)" shows "\\ A\ < \" proof (cases "\ \ range \") case False show ?thesis proof (cases "0 < \ A") case True hence "\\ A\ = \ A" by simp also have "... < \" using False by (metis ereal_less_PInfty rangeI) finally show ?thesis . next case False hence "\\ A\ = -\ A" using not_less_iff_gr_or_eq by fastforce also have "... = \ (E - A) - \ E" proof - have "\ E = \ A + \ (E - A)" using assms by simp hence "\ E - \ A = \ (E - A)" by (metis abs_ereal_uminus assms(1) calculation ereal_diff_add_inverse ereal_infty_less(2) ereal_minus(5) ereal_minus_less_iff ereal_minus_less_minus ereal_uminus_uminus less_ereal.simps(2) minus_ereal_def plus_ereal.simps(3)) thus ?thesis using assms(1) ereal_add_uminus_conv_diff ereal_eq_minus by auto qed also have "... \ \ (E - A) + \\ E\" by (metis \- \ A = \ (E - A) - \ E\ abs_ereal_less0 abs_ereal_pos ereal_diff_le_self ereal_le_add_mono1 less_eq_ereal_def minus_ereal_def not_le_imp_less) also have "... < \" using assms \\ \ range \\ by (metis UNIV_I ereal_less_PInfty ereal_plus_eq_PInfty image_eqI) finally show ?thesis . qed next case True hence "-\ \ range \" using inf_range by simp hence "-\ < \ A" by (metis ereal_infty_less(2) rangeI) show ?thesis proof (cases "\ A < 0") case True hence "\\ A\ = -\ A" using not_less_iff_gr_or_eq by fastforce also have "... < \" using \-\ < \ A\ using ereal_uminus_less_reorder by blast finally show ?thesis . next case False hence "\\ A\ = \ A" by simp also have "... = \ E - \ (E - A)" proof - have "\ E = \ A + \ (E - A)" using assms by simp thus "\ A = \ E - \ (E - A)" by (metis add.right_neutral assms(1) add_diff_eq_ereal calculation ereal_diff_add_eq_diff_diff_swap ereal_diff_add_inverse ereal_infty_less(1) ereal_plus_eq_PInfty ereal_x_minus_x) qed also have "... \ \\ E\ - \ (E - A)" by (metis \\\ A\ = \ A\ \\ A = \ E - \ (E - A)\ abs_ereal_ge0 abs_ereal_pos abs_ereal_uminus antisym_conv ereal_0_le_uminus_iff ereal_abs_diff ereal_diff_le_mono_left ereal_diff_le_self le_cases less_eq_ereal_def minus_ereal_def) also have "... < \" proof - have "-\ < \ (E - A)" using \-\ \ range \\ by (metis ereal_infty_less(2) rangeI) hence "- \ (E - A) < \" using ereal_uminus_less_reorder by blast thus ?thesis using assms by (simp add: ereal_minus_eq_PInfty_iff ereal_uminus_eq_reorder) qed finally show ?thesis . qed qed locale signed_measure_space= fixes M::"'a measure" and \ assumes sgn_meas: "signed_measure M \" sublocale signed_measure_space \ near_finite_function proof (unfold_locales) show "- \ \ range \ \ \ \ range \" using sgn_meas unfolding signed_measure_def by simp qed context signed_measure_space begin lemma signed_measure_finite_subset: assumes "E \ sets M" and "\\ E\ < \" and "A\ sets M" and "A\ E" shows "\\ A\ < \" proof (rule finite_subset) show "\\ E\ < \" "A\ E" using assms by auto show "\ E = \ A + \ (E - A)" using assms sgn_meas signed_measure_add[of M \ A "E - A"] - by (simp add: \A \ sets M\ \E \ sets M\ sets.Diff sup.absorb_iff2) + by (metis Diff_disjoint Diff_partition sets.Diff) qed lemma measure_space_e2ennreal : assumes "measure_space (space M) (sets M) m \ (\E \ sets M. m E < \) \ (\E \ sets M. m E \ 0)" shows "\E \ sets M. e2ennreal (m E) < \" proof fix E assume "E \ sets M" show "e2ennreal (m E) < \" proof - have "m E < \" using assms \E \ sets M\ by blast then have "e2ennreal (m E) < \" using e2ennreal_less_top using \m E < \\ by auto thus ?thesis by simp qed qed subsection \Positive and negative subsets\ text \The Hahn decomposition theorem is based on the notions of positive and negative measurable sets. A measurable set is positive (resp. negative) if all its measurable subsets have a positive (resp. negative) measure by $\mu$. The decomposition theorem states that any measure space for a signed measure can be decomposed into a positive and a negative measurable set.\ definition pos_meas_set where "pos_meas_set E \ E \ sets M \ (\A \ sets M. A \ E \ 0 \ \ A)" definition neg_meas_set where "neg_meas_set E \ E \ sets M \ (\A \ sets M. A \ E \ \ A \ 0)" lemma pos_meas_setI: assumes "E \ sets M" and "\A. A \ sets M \ A \ E \ 0 \ \ A" shows "pos_meas_set E" unfolding pos_meas_set_def using assms by simp lemma pos_meas_setD1 : assumes "pos_meas_set E" shows "E \ sets M" using assms unfolding pos_meas_set_def by simp lemma neg_meas_setD1 : assumes "neg_meas_set E" shows "E \ sets M" using assms unfolding neg_meas_set_def by simp lemma neg_meas_setI: assumes "E \ sets M" and "\A. A \ sets M \ A \ E \ \ A \ 0" shows "neg_meas_set E" unfolding neg_meas_set_def using assms by simp lemma pos_meas_self: assumes "pos_meas_set E" shows "0 \ \ E" using assms unfolding pos_meas_set_def by simp lemma empty_pos_meas_set: shows "pos_meas_set {}" by (metis bot.extremum_uniqueI eq_iff pos_meas_set_def sets.empty_sets sgn_meas signed_measure_empty) lemma empty_neg_meas_set: shows "neg_meas_set {}" by (metis neg_meas_set_def order_refl sets.empty_sets sgn_meas signed_measure_empty subset_empty) lemma pos_measure_meas: assumes "pos_meas_set E" and "A\ E" and "A\ sets M" shows "0 \ \ A" using assms unfolding pos_meas_set_def by simp lemma pos_meas_subset: assumes "pos_meas_set A" and "B\ A" and "B\ sets M" shows "pos_meas_set B" using assms pos_meas_set_def by auto lemma neg_meas_subset: assumes "neg_meas_set A" and "B\ A" and "B\ sets M" shows "neg_meas_set B" using assms neg_meas_set_def by auto lemma pos_meas_set_Union: assumes "\(i::nat). pos_meas_set (A i)" and "\i. A i \ sets M" and "\\ (\ i. A i)\ < \" shows "pos_meas_set (\ i. A i)" proof (rule pos_meas_setI) show "\ (range A) \ sets M" using sigma_algebra.countable_UN assms by simp obtain B where "disjoint_family B" and "(\(i::nat). B i) = (\(i::nat). A i)" and "\i. B i \ sets M" and "\i. B i \ A i" using disj_Union2 assms by auto fix C assume "C \ sets M" and "C\ (\ i. A i)" hence "C = C \ (\ i. A i)" by auto also have "... = C \ (\ i. B i)" using \(\i. B i) = (\i. A i)\ by simp also have "... = (\ i. C \ B i)" by auto finally have "C = (\ i. C \ B i)" . hence "\ C = \ (\ i. C \ B i)" by simp also have "... = (\i. \ (C \ (B i)))" proof (rule signed_measure_inf_sum[symmetric]) show "signed_measure M \" using sgn_meas by simp show "disjoint_family (\i. C \ B i)" using \disjoint_family B\ by (meson Int_iff disjoint_family_subset subset_iff) show "range (\i. C \ B i) \ sets M" using \C\ sets M\ \\i. B i \ sets M\ by auto show "(\i. C \ B i) \ sets M" using \C = (\ i. C \ B i)\ \C\ sets M\ by simp qed also have "... \ 0" proof (rule suminf_nonneg) show "\n. 0 \ \ (C \ B n)" proof - fix n have "C\ B n \ A n" using \\i. B i \ A i\ by auto moreover have "C \ B n \ sets M" using \C\ sets M\ \\i. B i \ sets M\ by simp ultimately show "0 \ \ (C \ B n)" using assms pos_measure_meas[of "A n"] by simp qed have "summable (\i. real_of_ereal (\ (C \ B i)))" proof (rule summable_norm_cancel) have "\n. norm (real_of_ereal (\ (C \ B n))) = real_of_ereal \\ (C \ B n)\" by simp moreover have "summable (\i. real_of_ereal \\ (C \ B i)\)" proof (rule signed_measure_abs_convergent) show "signed_measure M \" using sgn_meas by simp show "range (\i. C \ B i) \ sets M" using \C\ sets M\ \\i. B i \ sets M\ by auto show "disjoint_family (\i. C \ B i)" using \disjoint_family B\ by (meson Int_iff disjoint_family_subset subset_iff) show "(\i. C \ B i) \ sets M" using \C = (\ i. C \ B i)\ \C\ sets M\ by simp have "\\ C\ < \" proof (rule signed_measure_finite_subset) show "(\ i. A i) \ sets M" using assms by simp show "\\ (\ (range A))\ < \" using assms by simp show "C \ sets M" using \C \ sets M\ . show "C \ \ (range A)" using \C \ \ (range A) \ . qed thus "\\ (\i. C \ B i)\ < \" using \C = (\ i. C \ B i)\ by simp qed ultimately show "summable (\n. norm (real_of_ereal (\ (C \ B n))))" by auto qed thus "summable (\i. \ (C \ B i))" by (simp add: \\n. 0 \ \ (C \ B n)\ summable_ereal_pos) qed finally show "0 \ \ C" . qed lemma pos_meas_set_pos_lim: assumes "\(i::nat). pos_meas_set (A i)" and "\i. A i \ sets M" shows "0 \ \ (\ i. A i)" proof - obtain B where "disjoint_family B" and "(\(i::nat). B i) = (\(i::nat). A i)" and "\i. B i \ sets M" and "\i. B i \ A i" using disj_Union2 assms by auto note Bprops = this have sums: "(\n. \ (B n)) sums \ (\i. B i)" proof (rule signed_measure_sums) show "signed_measure M \" using sgn_meas . show "range B \ sets M" using Bprops by auto show "disjoint_family B" using Bprops by simp show "\ (range B) \ sets M" using Bprops by blast qed hence "summable (\n. \ (B n))" using sums_summable[of "\n. \ (B n)"] by simp hence "suminf (\n. \ (B n)) = \ (\i. B i)" using sums sums_iff by auto thus ?thesis using suminf_nonneg by (metis Bprops(2) Bprops(3) Bprops(4) \summable (\n. \ (B n))\ assms(1) pos_measure_meas) qed lemma pos_meas_disj_union: assumes "pos_meas_set A" and "pos_meas_set B" and "A\ B = {}" shows "pos_meas_set (A \ B)" unfolding pos_meas_set_def proof (intro conjI ballI impI) show "A\ B \ sets M" by (metis assms(1) assms(2) pos_meas_set_def sets.Un) next fix C assume "C\ sets M" and "C\ A\ B" define DA where "DA = C\ A" define DB where "DB = C\ B" have "DA\ sets M" using DA_def \C \ sets M\ assms(1) pos_meas_set_def by blast have "DB\ sets M" using DB_def \C \ sets M\ assms(2) pos_meas_set_def by blast have "DA \ DB = {}" unfolding DA_def DB_def using assms by auto have "C = DA \ DB" unfolding DA_def DB_def using \C\ A\ B\ by auto have "0 \ \ DB" using assms unfolding DB_def pos_meas_set_def by (metis DB_def Int_lower2\DB \ sets M\) also have "... \ \ DA + \ DB" using assms unfolding pos_meas_set_def by (metis DA_def Diff_Diff_Int Diff_subset Int_commute \DA \ sets M\ ereal_le_add_self2) also have "... = \ C" using signed_measure_add sgn_meas \DA \ sets M\ \DB \ sets M\ \DA \ DB = {}\ \C = DA \ DB\ by metis finally show "0 \ \ C" . qed lemma pos_meas_set_union: assumes "pos_meas_set A" and "pos_meas_set B" shows "pos_meas_set (A \ B)" proof - define C where "C = B - A" have "A\ C = A\ B" unfolding C_def by auto moreover have "pos_meas_set (A\ C)" proof (rule pos_meas_disj_union) show "pos_meas_set C" unfolding C_def by (meson Diff_subset assms(1) assms(2) sets.Diff signed_measure_space.pos_meas_set_def signed_measure_space.pos_meas_subset signed_measure_space_axioms) show "pos_meas_set A" using assms by simp show "A \ C = {}" unfolding C_def by auto qed ultimately show ?thesis by simp qed lemma neg_meas_disj_union: assumes "neg_meas_set A" and "neg_meas_set B" and "A\ B = {}" shows "neg_meas_set (A \ B)" unfolding neg_meas_set_def proof (intro conjI ballI impI) show "A\ B \ sets M" by (metis assms(1) assms(2) neg_meas_set_def sets.Un) next fix C assume "C\ sets M" and "C\ A\ B" define DA where "DA = C\ A" define DB where "DB = C\ B" have "DA\ sets M" using DA_def \C \ sets M\ assms(1) neg_meas_set_def by blast have "DB\ sets M" using DB_def \C \ sets M\ assms(2) neg_meas_set_def by blast have "DA \ DB = {}" unfolding DA_def DB_def using assms by auto have "C = DA \ DB" unfolding DA_def DB_def using \C\ A\ B\ by auto have "\ C = \ DA + \ DB" using signed_measure_add sgn_meas \DA \ sets M\ \DB \ sets M\ \DA \ DB = {}\ \C = DA \ DB\ by metis also have "... \ \ DB" using assms unfolding neg_meas_set_def by (metis DA_def Int_lower2 \DA \ sets M\ add_decreasing dual_order.refl) also have "... \ 0" using assms unfolding DB_def neg_meas_set_def by (metis DB_def Int_lower2\DB \ sets M\) finally show "\ C \ 0" . qed lemma neg_meas_set_union: assumes "neg_meas_set A" and "neg_meas_set B" shows "neg_meas_set (A \ B)" proof - define C where "C = B - A" have "A\ C = A\ B" unfolding C_def by auto moreover have "neg_meas_set (A\ C)" proof (rule neg_meas_disj_union) show "neg_meas_set C" unfolding C_def by (meson Diff_subset assms(1) assms(2) sets.Diff neg_meas_set_def neg_meas_subset signed_measure_space_axioms) show "neg_meas_set A" using assms by simp show "A \ C = {}" unfolding C_def by auto qed ultimately show ?thesis by simp qed lemma neg_meas_self : assumes "neg_meas_set E" shows "\ E \ 0" using assms unfolding neg_meas_set_def by simp lemma pos_meas_set_opp: assumes "signed_measure_space.pos_meas_set M (\ A. - \ A) A" shows "neg_meas_set A" proof - have m_meas_pos : "signed_measure M (\ A. - \ A)" using assms signed_measure_space_def by (simp add: sgn_meas signed_measure_minus) thus ?thesis by (metis assms ereal_0_le_uminus_iff neg_meas_setI signed_measure_space.intro signed_measure_space.pos_meas_set_def) qed lemma neg_meas_set_opp: assumes "signed_measure_space.neg_meas_set M (\ A. - \ A) A" shows "pos_meas_set A" proof - have m_meas_neg : "signed_measure M (\ A. - \ A)" using assms signed_measure_space_def by (simp add: sgn_meas signed_measure_minus) thus ?thesis by (metis assms ereal_uminus_le_0_iff m_meas_neg pos_meas_setI signed_measure_space.intro signed_measure_space.neg_meas_set_def) qed end lemma signed_measure_inter: assumes "signed_measure M \" and "A \ sets M" shows "signed_measure M (\E. \ (E \ A))" unfolding signed_measure_def proof (intro conjI) show "\ ({} \ A) = 0" using assms(1) signed_measure_empty by auto show "- \ \ range (\E. \ (E \ A)) \ \ \ range (\E. \ (E \ A))" proof (rule ccontr) assume "\ (- \ \ range (\E. \ (E \ A)) \ \ \ range (\E. \ (E \ A)))" hence "- \ \ range (\E. \ (E \ A)) \ \ \ range (\E. \ (E \ A))" by simp hence "- \ \ range \ \ \ \ range \" by auto thus False using assms unfolding signed_measure_def by simp qed show "\E. range E \ sets M \ disjoint_family E \ \ (range E) \ sets M \ (\i. \ (E i \ A)) sums \ (\ (range E) \ A)" proof (intro allI impI) fix E::"nat \ 'a set" assume "range E \ sets M" and "disjoint_family E" and "\ (range E) \ sets M" note Eprops = this define F where "F = (\i. E i \ A)" have "(\i. \ (F i)) sums \ (\ (range F))" proof (rule signed_measure_sums) show "signed_measure M \" using assms by simp show "range F \ sets M" using Eprops F_def assms by blast show "disjoint_family F" using Eprops F_def assms by (metis disjoint_family_subset inf.absorb_iff2 inf_commute inf_right_idem) show "\ (range F) \ sets M" using Eprops assms unfolding F_def by (simp add: Eprops assms countable_Un_Int(1) sets.Int) qed moreover have "\ (range F) = A \ \ (range E)" unfolding F_def by auto ultimately show "(\i. \ (E i \ A)) sums \ (\ (range E) \ A)" unfolding F_def by simp qed show "\E. range E \ sets M \ disjoint_family E \ \ (range E) \ sets M \ \\ (\ (range E) \ A)\ < \ \ summable (\i. real_of_ereal \\ (E i \ A)\)" proof (intro allI impI) fix E::"nat \ 'a set" assume "range E \ sets M" and "disjoint_family E" and "\ (range E) \ sets M" and "\\ (\ (range E) \ A)\ < \" note Eprops = this show "summable (\i. real_of_ereal \\ (E i \ A)\)" proof (rule signed_measure_summable) show "signed_measure M \" using assms by simp show "range (\i. E i \ A) \ sets M" using Eprops assms by blast show "disjoint_family (\i. E i \ A)" using Eprops assms disjoint_family_subset inf.absorb_iff2 inf_commute inf_right_idem by fastforce show "(\i. E i \ A) \ sets M" using Eprops assms by (simp add: Eprops assms countable_Un_Int(1) sets.Int) show "\\ (\i. E i \ A)\ < \" using Eprops by auto qed qed qed context signed_measure_space begin lemma pos_signed_to_meas_space : assumes "pos_meas_set M1" and "m1 = (\A. \ (A \ M1))" shows "measure_space (space M) (sets M) m1" unfolding measure_space_def proof (intro conjI) show "sigma_algebra (space M) (sets M)" by (simp add: sets.sigma_algebra_axioms) show "positive (sets M) m1" using assms unfolding pos_meas_set_def by (metis Sigma_Algebra.positive_def Un_Int_eq(4) e2ennreal_neg neg_meas_self sup_bot_right empty_neg_meas_set) show "countably_additive (sets M) m1" proof (rule pos_signed_measure_count_additive) show "\E\sets M. 0 \ m1 E" by (metis assms inf.cobounded2 pos_meas_set_def sets.Int) show "signed_measure M m1" using assms pos_meas_set_def signed_measure_inter[of M \ M1] sgn_meas by blast qed qed lemma neg_signed_to_meas_space : assumes "neg_meas_set M2" and "m2 = (\A. -\ (A \ M2))" shows "measure_space (space M) (sets M) m2" unfolding measure_space_def proof (intro conjI) show "sigma_algebra (space M) (sets M)" by (simp add: sets.sigma_algebra_axioms) show "positive (sets M) m2" using assms unfolding neg_meas_set_def by (metis Sigma_Algebra.positive_def e2ennreal_neg ereal_uminus_zero inf.absorb_iff2 inf.orderE inf_bot_right neg_meas_self pos_meas_self empty_neg_meas_set empty_pos_meas_set) show "countably_additive (sets M) m2" proof (rule pos_signed_measure_count_additive) show "\E\sets M. 0 \ m2 E" by (metis assms ereal_uminus_eq_reorder ereal_uminus_le_0_iff inf.cobounded2 neg_meas_set_def sets.Int) have "signed_measure M (\A. \ (A \ M2))" using assms neg_meas_set_def signed_measure_inter[of M \ M2] sgn_meas by blast thus "signed_measure M m2" using signed_measure_minus assms by simp qed qed lemma pos_part_meas_nul_neg_set : assumes "pos_meas_set M1" and "neg_meas_set M2" and "m1 = (\A. \ (A \ M1))" and "E \ sets M" and "E \ M2" shows "m1 E = 0" proof - have "m1 E \ 0" using assms unfolding pos_meas_set_def by (simp add: \E \ sets M\ sets.Int) have "\ E \ 0" using \E \ M2\ assms unfolding neg_meas_set_def using \E \ sets M\ by blast then have "m1 E \ 0" using \\ E \ 0\ assms by (metis Int_Un_eq(1) Un_subset_iff \E \ sets M\ \E \ M2\ pos_meas_setD1 sets.Int signed_measure_space.neg_meas_set_def signed_measure_space_axioms) thus "m1 E = 0" using \m1 E \ 0\ \m1 E \ 0\ by auto qed lemma neg_part_meas_nul_pos_set : assumes "pos_meas_set M1" and "neg_meas_set M2" and "m2 = (\A. -\ (A \ M2))" and "E \ sets M" and "E \ M1" shows "m2 E = 0" proof - have "m2 E \ 0" using assms unfolding neg_meas_set_def by (simp add: \E \ sets M\ sets.Int) have "\ E \ 0" using assms unfolding pos_meas_set_def by blast then have "m2 E \ 0" using \\ E \ 0\ assms by (metis \E \ sets M\ \E \ M1\ ereal_0_le_uminus_iff ereal_uminus_uminus inf_sup_ord(1) neg_meas_setD1 pos_meas_set_def pos_meas_subset sets.Int) thus "m2 E = 0" using \m2 E \ 0\ \m2 E \ 0\ by auto qed definition pos_sets where "pos_sets = {A. A \ sets M \ pos_meas_set A}" definition pos_img where "pos_img = {\ A|A. A\ pos_sets}" subsection \Essential uniqueness\ text \In this part, under the assumption that a measure space for a signed measure admits a decomposition into a positive and a negative set, we prove that this decomposition is essentially unique; in other words, that if two such decompositions $(P,N)$ and $(X,Y)$ exist, then any measurable subset of $(P\triangle X) \cup (N \triangle Y)$ has a null measure.\ definition hahn_space_decomp where "hahn_space_decomp M1 M2 \ (pos_meas_set M1) \ (neg_meas_set M2) \ (space M = M1 \ M2) \ (M1 \ M2 = {})" lemma pos_neg_null_set: assumes "pos_meas_set A" and "neg_meas_set A" shows "\ A = 0" using assms pos_meas_self[of A] neg_meas_self[of A] by simp lemma pos_diff_neg_meas_set: assumes "(pos_meas_set M1)" and "(neg_meas_set N2)" and "(space M = N1 \ N2)" and "N1 \ sets M" shows "neg_meas_set ((M1 - N1) \ space M)" using assms neg_meas_subset by (metis Diff_subset_conv Int_lower2 pos_meas_setD1 sets.Diff sets.Int_space_eq2) lemma neg_diff_pos_meas_set: assumes "(neg_meas_set M2)" and "(pos_meas_set N1)" and "(space M = N1 \ N2)" and "N2 \ sets M" shows "pos_meas_set ((M2 - N2) \ space M)" proof - have "(M2 - N2) \ space M \ N1" using assms by auto thus ?thesis using assms pos_meas_subset neg_meas_setD1 by blast qed lemma pos_sym_diff_neg_meas_set: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp N1 N2" shows "neg_meas_set ((sym_diff M1 N1) \ space M)" using assms unfolding hahn_space_decomp_def by (metis Int_Un_distrib2 neg_meas_set_union pos_meas_setD1 pos_diff_neg_meas_set) lemma neg_sym_diff_pos_meas_set: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp N1 N2" shows "pos_meas_set ((sym_diff M2 N2) \ space M)" using assms neg_diff_pos_meas_set unfolding hahn_space_decomp_def by (metis (no_types, lifting) Int_Un_distrib2 neg_meas_setD1 pos_meas_set_union) lemma pos_meas_set_diff: assumes "pos_meas_set A" and "B\ sets M" shows "pos_meas_set ((A - B) \ (space M))" using pos_meas_subset by (metis Diff_subset assms(1) assms(2) pos_meas_setD1 sets.Diff sets.Int_space_eq2) lemma pos_meas_set_sym_diff: assumes "pos_meas_set A" and "pos_meas_set B" shows "pos_meas_set ((sym_diff A B) \ space M)" using pos_meas_set_diff by (metis Int_Un_distrib2 assms(1) assms(2) pos_meas_setD1 pos_meas_set_union) lemma neg_meas_set_diff: assumes "neg_meas_set A" and "B\ sets M" shows "neg_meas_set ((A - B) \ (space M))" using neg_meas_subset by (metis Diff_subset assms(1) assms(2) neg_meas_setD1 sets.Diff sets.Int_space_eq2) lemma neg_meas_set_sym_diff: assumes "neg_meas_set A" and "neg_meas_set B" shows "neg_meas_set ((sym_diff A B) \ space M)" using neg_meas_set_diff by (metis Int_Un_distrib2 assms(1) assms(2) neg_meas_setD1 neg_meas_set_union) lemma hahn_decomp_space_diff: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp N1 N2" shows "pos_meas_set ((sym_diff M1 N1 \ sym_diff M2 N2) \ space M)" "neg_meas_set ((sym_diff M1 N1 \ sym_diff M2 N2) \ space M)" proof - show "pos_meas_set ((sym_diff M1 N1 \ sym_diff M2 N2) \ space M)" by (metis Int_Un_distrib2 assms(1) assms(2) hahn_space_decomp_def neg_sym_diff_pos_meas_set pos_meas_set_sym_diff pos_meas_set_union) show "neg_meas_set ((sym_diff M1 N1 \ sym_diff M2 N2) \ space M)" by (metis Int_Un_distrib2 assms(1) assms(2) hahn_space_decomp_def neg_meas_set_sym_diff neg_meas_set_union pos_sym_diff_neg_meas_set) qed lemma hahn_decomp_ess_unique: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp N1 N2" and "C \ sym_diff M1 N1 \ sym_diff M2 N2" and "C\ sets M" shows "\ C = 0" proof - have "C\ (sym_diff M1 N1 \ sym_diff M2 N2) \ space M" using assms by (simp add: sets.sets_into_space) thus ?thesis using assms hahn_decomp_space_diff pos_neg_null_set by (meson neg_meas_subset pos_meas_subset) qed section \Existence of a positive subset\ text \The goal of this part is to prove that any measurable set of finite and positive measure must contain a positive subset with a strictly positive measure.\ subsection \A sequence of negative subsets\ definition inf_neg where "inf_neg A = (if (A \ sets M \ pos_meas_set A) then (0::nat) else Inf {n|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal(-1/n))})" lemma inf_neg_ne: assumes "A \ sets M" and "\ pos_meas_set A" shows "{n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal (-1/n))} \ {}" proof - define N where "N = {n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal (-1/n))}" have "\B \ sets M. B\ A \ \ B < 0" using assms unfolding pos_meas_set_def by auto from this obtain B where "B\ sets M" and "B\ A" and "\ B < 0" by auto hence "\n::nat. (1::nat) \ n \ \ B < ereal (-1/n)" proof (cases "\ B = -\") case True hence "\ B < -1/(2::nat)" by simp thus ?thesis using numeral_le_real_of_nat_iff one_le_numeral by blast next case False hence "real_of_ereal (\ B) < 0" using \\ B < 0\ by (metis Infty_neq_0(3) ereal_mult_eq_MInfty ereal_zero_mult less_eq_ereal_def less_eq_real_def less_ereal.simps(2) real_of_ereal_eq_0 real_of_ereal_le_0) hence "\n::nat. Suc 0 \ n \ real_of_ereal (\ B) < -1/n" proof - define nw where "nw = Suc (nat (floor (-1/ (real_of_ereal (\ B)))))" have "Suc 0 \ nw" unfolding nw_def by simp have "0 < -1/ (real_of_ereal (\ B))" using \real_of_ereal (\ B) < 0\ by simp have "-1/ (real_of_ereal (\ B)) < nw" unfolding nw_def by linarith hence "1/nw < 1/(-1/ (real_of_ereal (\ B)))" using \0 < -1/ (real_of_ereal (\ B))\ by (metis frac_less2 le_eq_less_or_eq of_nat_1 of_nat_le_iff zero_less_one) also have "... = - (real_of_ereal (\ B))" by simp finally have "1/nw < - (real_of_ereal (\ B))" . hence "real_of_ereal (\ B) < -1/nw" by simp thus ?thesis using \Suc 0 \ nw\ by auto qed from this obtain n1::nat where "Suc 0 \ n1" and "real_of_ereal (\ B) < -1/n1" by auto hence "ereal (real_of_ereal (\ B)) < -1/n1" using real_ereal_leq[of "\ B"] \\ B < 0\ by simp moreover have "\ B = real_of_ereal (\ B)" using \\ B < 0\ False by (metis less_ereal.simps(2) real_of_ereal.elims zero_ereal_def) ultimately show ?thesis using \Suc 0 \ n1\ by auto qed from this obtain n0::nat where "(1::nat) \ n0" and "\ B < -1/n0" by auto hence "n0 \ {n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal(-1/n))}" using \B\ sets M\ \B\ A\ by auto thus ?thesis by auto qed lemma inf_neg_ge_1: assumes "A \ sets M" and "\ pos_meas_set A" shows "(1::nat) \ inf_neg A" proof - define N where "N = {n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal (-1/n))}" have "N \ {}" unfolding N_def using assms inf_neg_ne by auto moreover have "\n. n\ N \ (1::nat) \ n" unfolding N_def by simp ultimately show "1 \ inf_neg A" unfolding inf_neg_def N_def using Inf_nat_def1 assms(1) assms(2) by presburger qed lemma inf_neg_pos: assumes "A \ sets M" and "\ pos_meas_set A" shows "\ B \ sets M. B\ A \ \ B < -1/(inf_neg A)" proof - define N where "N = {n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal (-1/n))}" have "N \ {}" unfolding N_def using assms inf_neg_ne by auto hence "Inf N \ N" using Inf_nat_def1[of N] by simp hence "inf_neg A \ N" unfolding N_def inf_neg_def using assms by auto thus ?thesis unfolding N_def by auto qed definition rep_neg where "rep_neg A = (if (A \ sets M \ pos_meas_set A) then {} else SOME B. B \ sets M \ B \ A \ \ B \ ereal (-1 / (inf_neg A)))" lemma g_rep_neg: assumes "A\ sets M" and "\ pos_meas_set A" shows "rep_neg A \ sets M" "rep_neg A \ A" "\ (rep_neg A) \ ereal (-1 / (inf_neg A))" proof - have "\ B. B \ sets M \ B\ A \ \ B \ -1 / (inf_neg A)" using assms inf_neg_pos[of A] by auto from someI_ex[OF this] show "rep_neg A \ sets M" "rep_neg A \ A" "\ (rep_neg A) \ -1 / (inf_neg A)" unfolding rep_neg_def using assms by auto qed lemma rep_neg_sets: shows "rep_neg A \ sets M" proof (cases "A \ sets M \ pos_meas_set A") case True then show ?thesis unfolding rep_neg_def by simp next case False then show ?thesis using g_rep_neg(1) by blast qed lemma rep_neg_subset: shows "rep_neg A \ A" proof (cases "A \ sets M \ pos_meas_set A") case True then show ?thesis unfolding rep_neg_def by simp next case False then show ?thesis using g_rep_neg(2) by blast qed lemma rep_neg_less: assumes "A\ sets M" and "\ pos_meas_set A" shows "\ (rep_neg A) \ ereal (-1 / (inf_neg A))" using assms g_rep_neg(3) by simp lemma rep_neg_leq: shows "\ (rep_neg A) \ 0" proof (cases "A \ sets M \ pos_meas_set A") case True hence "rep_neg A = {}" unfolding rep_neg_def by simp then show ?thesis using sgn_meas signed_measure_empty by force next case False then show ?thesis using rep_neg_less by (metis le_ereal_le minus_divide_left neg_le_0_iff_le of_nat_0 of_nat_le_iff zero_ereal_def zero_le zero_le_divide_1_iff) qed subsection \Construction of the positive subset\ fun pos_wtn where pos_wtn_base: "pos_wtn E 0 = E"| pos_wtn_step: "pos_wtn E (Suc n) = pos_wtn E n - rep_neg (pos_wtn E n)" lemma pos_wtn_subset: shows "pos_wtn E n \ E" proof (induct n) case 0 then show ?case using pos_wtn_base by simp next case (Suc n) hence "rep_neg (pos_wtn E n) \ pos_wtn E n" using rep_neg_subset by simp then show ?case using Suc by auto qed lemma pos_wtn_sets: assumes "E\ sets M" shows "pos_wtn E n \ sets M" proof (induct n) case 0 then show ?case using assms by simp next case (Suc n) then show ?case using pos_wtn_step rep_neg_sets by auto qed definition neg_wtn where "neg_wtn E (n::nat) = rep_neg (pos_wtn E n)" lemma neg_wtn_neg_meas: shows "\ (neg_wtn E n) \ 0" unfolding neg_wtn_def using rep_neg_leq by simp lemma neg_wtn_sets: shows "neg_wtn E n \ sets M" unfolding neg_wtn_def using rep_neg_sets by simp lemma neg_wtn_subset: shows "neg_wtn E n \ E" unfolding neg_wtn_def using pos_wtn_subset[of E n] rep_neg_subset[of "pos_wtn E n"] by simp lemma neg_wtn_union_subset: shows "(\ i \ n. neg_wtn E i) \ E" using neg_wtn_subset by auto lemma pos_wtn_Suc: shows "pos_wtn E (Suc n) = E - (\ i \ n. neg_wtn E i)" unfolding neg_wtn_def proof (induct n) case 0 then show ?case using pos_wtn_base pos_wtn_step by simp next case (Suc n) have "pos_wtn E (Suc (Suc n)) = pos_wtn E (Suc n) - rep_neg (pos_wtn E (Suc n))" using pos_wtn_step by simp also have "... = (E - (\ i \ n. rep_neg (pos_wtn E i))) - rep_neg (pos_wtn E (Suc n))" using Suc by simp also have "... = E - (\ i \ (Suc n). rep_neg (pos_wtn E i))" using diff_union[of E "\i. rep_neg (pos_wtn E i)" n] by auto finally show "pos_wtn E (Suc (Suc n)) = E - (\ i \ (Suc n). rep_neg (pos_wtn E i))" . qed definition pos_sub where "pos_sub E = (\ n. pos_wtn E n)" lemma pos_sub_sets: assumes "E\ sets M" shows "pos_sub E \ sets M" unfolding pos_sub_def using pos_wtn_sets assms by auto lemma pos_sub_subset: shows "pos_sub E \ E" unfolding pos_sub_def using pos_wtn_subset by blast lemma pos_sub_infty: assumes "E \ sets M" and "\\ E\ < \" shows "\\ (pos_sub E)\ < \" using signed_measure_finite_subset assms pos_sub_sets pos_sub_subset by simp lemma neg_wtn_djn: shows "disjoint_family (\n. neg_wtn E n)" unfolding disjoint_family_on_def proof - { fix n fix m::nat assume "n < m" hence "\p. m = Suc p" using old.nat.exhaust by auto from this obtain p where "m = Suc p" by auto have "neg_wtn E m \ pos_wtn E m" unfolding neg_wtn_def by (simp add: rep_neg_subset) also have "... = E - (\ i \ p. neg_wtn E i)" using pos_wtn_Suc \m = Suc p\ by simp finally have "neg_wtn E m \ E - (\ i \ p. neg_wtn E i)" . moreover have "neg_wtn E n \ (\ i \ p. neg_wtn E i)" using \n < m\ \m = Suc p\ by (simp add: UN_upper) ultimately have "neg_wtn E n \ neg_wtn E m = {}" by auto } thus "\m\UNIV. \n\UNIV. m \ n \ neg_wtn E m \ neg_wtn E n = {}" by (metis inf_commute linorder_neqE_nat) qed end lemma disjoint_family_imp_on: assumes "disjoint_family A" shows "disjoint_family_on A S" using assms disjoint_family_on_mono subset_UNIV by blast context signed_measure_space begin lemma neg_wtn_union_neg_meas: shows "\ (\ i \ n. neg_wtn E i) \ 0" proof - have "\ (\ i \ n. neg_wtn E i) = (\i\{.. n}. \ (neg_wtn E i))" proof (rule signed_measure_disj_sum, simp+) show "signed_measure M \" using sgn_meas . show "disjoint_family_on (neg_wtn E) {..n}" using neg_wtn_djn disjoint_family_imp_on[of "neg_wtn E"] by simp show "\i. i \ {..n} \ neg_wtn E i \ sets M" using neg_wtn_sets by simp qed also have "... \ 0" using neg_wtn_neg_meas by (simp add: sum_nonpos) finally show ?thesis . qed lemma pos_wtn_meas_gt: assumes "0 < \ E" and "E\ sets M" shows "0 < \ (pos_wtn E n)" proof (cases "n = 0") case True then show ?thesis using assms by simp next case False hence "\m. n = Suc m" by (simp add: not0_implies_Suc) from this obtain m where "n = Suc m" by auto hence eq: "pos_wtn E n = E - (\ i \ m. neg_wtn E i)" using pos_wtn_Suc by simp hence "pos_wtn E n \ (\ i \ m. neg_wtn E i) = {}" by auto moreover have "E = pos_wtn E n \ (\ i \ m. neg_wtn E i)" using eq neg_wtn_union_subset[of E m] by auto ultimately have "\ E = \ (pos_wtn E n) + \ (\ i \ m. neg_wtn E i)" using signed_measure_add[of M \ "pos_wtn E n" "\ i \ m. neg_wtn E i"] pos_wtn_sets neg_wtn_sets assms sgn_meas by auto hence "0 < \ (pos_wtn E n) + \ (\ i \ m. neg_wtn E i)" using assms by simp thus ?thesis using neg_wtn_union_neg_meas by (metis add.right_neutral add_mono not_le) qed definition union_wit where "union_wit E = (\ n. neg_wtn E n)" lemma union_wit_sets: shows "union_wit E \ sets M" unfolding union_wit_def proof (intro sigma_algebra.countable_nat_UN) show "sigma_algebra (space M) (sets M)" by (simp add: sets.sigma_algebra_axioms) show "range (neg_wtn E) \ sets M" proof - { fix n have "neg_wtn E n \ sets M" unfolding neg_wtn_def by (simp add: rep_neg_sets) } thus ?thesis by auto qed qed lemma union_wit_subset: shows "union_wit E \ E" proof - { fix n have "neg_wtn E n \ E" unfolding neg_wtn_def using pos_wtn_subset rep_neg_subset[of "pos_wtn E n"] by auto } thus ?thesis unfolding union_wit_def by auto qed lemma pos_sub_diff: shows "pos_sub E = E - union_wit E" proof show "pos_sub E \ E - union_wit E" proof - have "pos_sub E \ E" using pos_sub_subset by simp moreover have "pos_sub E \ union_wit E = {}" proof (rule ccontr) assume "pos_sub E \ union_wit E \ {}" hence "\ a. a\ pos_sub E \ union_wit E" by auto from this obtain a where "a\ pos_sub E \ union_wit E" by auto hence "a\ union_wit E" by simp hence "\n. a \ rep_neg (pos_wtn E n)" unfolding union_wit_def neg_wtn_def by auto from this obtain n where "a \ rep_neg (pos_wtn E n)" by auto have "a \ pos_wtn E (Suc n)" using \a\ pos_sub E \ union_wit E\ unfolding pos_sub_def by blast hence "a\ rep_neg (pos_wtn E n)" using pos_wtn_step by simp thus False using \a \ rep_neg (pos_wtn E n)\ by simp qed ultimately show ?thesis by auto qed next show "E - union_wit E \ pos_sub E" proof fix a assume "a \ E - union_wit E" show "a \ pos_sub E" unfolding pos_sub_def proof fix n show "a \ pos_wtn E n" proof (cases "n = 0") case True thus ?thesis using pos_wtn_base \a\ E - union_wit E\ by simp next case False hence "\m. n = Suc m" by (simp add: not0_implies_Suc) from this obtain m where "n = Suc m" by auto have "(\ i \ m. rep_neg (pos_wtn E i)) \ (\ n. (rep_neg (pos_wtn E n)))" by auto hence "a \ E - (\ i \ m. rep_neg (pos_wtn E i))" using \a \ E - union_wit E\ unfolding union_wit_def neg_wtn_def by auto thus "a\ pos_wtn E n" using pos_wtn_Suc \n = Suc m\ unfolding neg_wtn_def by simp qed qed qed qed definition num_wtn where "num_wtn E n = inf_neg (pos_wtn E n)" lemma num_wtn_geq: shows "\ (neg_wtn E n) \ ereal (-1/(num_wtn E n))" proof (cases "(pos_wtn E n) \ sets M \ pos_meas_set (pos_wtn E n)") case True hence "neg_wtn E n = {}" unfolding neg_wtn_def rep_neg_def by simp moreover have "num_wtn E n = 0" using True unfolding num_wtn_def inf_neg_def by simp ultimately show ?thesis using sgn_meas signed_measure_empty by force next case False then show ?thesis using g_rep_neg(3)[of "pos_wtn E n"] unfolding neg_wtn_def num_wtn_def by simp qed lemma neg_wtn_infty: assumes "E \ sets M" and "\\ E\ < \" shows "\\ (neg_wtn E i)\ < \" proof (rule signed_measure_finite_subset) show "E \ sets M" "\\ E\ < \" using assms by auto show "neg_wtn E i \ sets M" proof (cases "pos_wtn E i \ sets M \ pos_meas_set (pos_wtn E i)") case True then show ?thesis unfolding neg_wtn_def rep_neg_def by simp next case False then show ?thesis unfolding neg_wtn_def using g_rep_neg(1)[of "pos_wtn E i"] by simp qed show "neg_wtn E i \ E" unfolding neg_wtn_def using pos_wtn_subset[of E] rep_neg_subset[of "pos_wtn E i"] by auto qed lemma union_wit_infty: assumes "E \ sets M" and "\\ E\ < \" shows "\\ (union_wit E)\ < \" using union_wit_subset union_wit_sets signed_measure_finite_subset assms unfolding union_wit_def by simp lemma neg_wtn_summable: assumes "E \ sets M" and "\\ E\ < \" shows "summable (\i. - real_of_ereal (\ (neg_wtn E i)))" proof - have "signed_measure M \" using sgn_meas . moreover have "range (neg_wtn E) \ sets M" unfolding neg_wtn_def using rep_neg_sets by auto moreover have "disjoint_family (neg_wtn E)" using neg_wtn_djn by simp moreover have "\ (range (neg_wtn E)) \ sets M" using union_wit_sets unfolding union_wit_def by simp moreover have "\\ (\ (range (neg_wtn E)))\ < \" using union_wit_subset signed_measure_finite_subset union_wit_sets assms unfolding union_wit_def by simp ultimately have "summable (\i. real_of_ereal \\ (neg_wtn E i)\)" using signed_measure_abs_convergent[of M ] by simp moreover have "\i. \\ (neg_wtn E i)\ = -(\ (neg_wtn E i))" proof - fix i have "\ (neg_wtn E i) \ 0" using rep_neg_leq[of "pos_wtn E i"] unfolding neg_wtn_def . thus "\\ (neg_wtn E i)\ = -\ (neg_wtn E i)" using less_eq_ereal_def by auto qed ultimately show ?thesis by simp qed lemma inv_num_wtn_summable: assumes "E \ sets M" and "\\ E\ < \" shows "summable (\n. 1/(num_wtn E n))" proof (rule summable_bounded) show "\i. 0 \ 1 / real (num_wtn E i)" by simp show "\i. 1 / real (num_wtn E i) \ (\n. -real_of_ereal (\ (neg_wtn E n))) i" proof - fix i have "\\ (neg_wtn E i)\ < \" using assms neg_wtn_infty by simp have "ereal (1/(num_wtn E i)) \ -\ (neg_wtn E i)" using num_wtn_geq[of E i] ereal_minus_le_minus by fastforce also have "... = ereal(- real_of_ereal (\ (neg_wtn E i)))" using \\\ (neg_wtn E i)\ < \\ ereal_real' by auto finally have "ereal (1/(num_wtn E i)) \ ereal(- real_of_ereal (\ (neg_wtn E i)))" . thus "1 / real (num_wtn E i) \ -real_of_ereal (\ (neg_wtn E i))" by simp qed show "summable (\i. - real_of_ereal (\ (neg_wtn E i)))" using assms neg_wtn_summable by simp qed lemma inv_num_wtn_shift_summable: assumes "E \ sets M" and "\\ E\ < \" shows "summable (\n. 1/(num_wtn E n - 1))" proof (rule sum_shift_denum) show "summable (\n. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable by simp qed lemma neg_wtn_meas_sums: assumes "E \ sets M" and "\\ E\ < \" shows "(\i. - (\ (neg_wtn E i))) sums suminf (\i. - real_of_ereal (\ (neg_wtn E i)))" proof - have "(\i. ereal (- real_of_ereal (\ (neg_wtn E i)))) sums suminf (\i. - real_of_ereal (\ (neg_wtn E i)))" proof (rule sums_ereal[THEN iffD2]) have "summable (\i. - real_of_ereal (\ (neg_wtn E i)))" using neg_wtn_summable assms by simp thus "(\x. - real_of_ereal (\ (neg_wtn E x))) sums (\i. - real_of_ereal (\ (neg_wtn E i)))" by auto qed moreover have "\i. \ (neg_wtn E i) = ereal (real_of_ereal (\ (neg_wtn E i)))" proof - fix i show "\ (neg_wtn E i) = ereal (real_of_ereal (\ (neg_wtn E i)))" using assms(1) assms(2) ereal_real' neg_wtn_infty by auto qed ultimately show ?thesis by (metis (no_types, lifting) sums_cong uminus_ereal.simps(1)) qed lemma neg_wtn_meas_suminf_le: assumes "E \ sets M" and "\\ E\ < \" shows "suminf (\i. \ (neg_wtn E i)) \ - suminf (\n. 1/(num_wtn E n))" proof - have "suminf (\n. 1/(num_wtn E n)) \ suminf (\i. -real_of_ereal (\ (neg_wtn E i)))" proof (rule suminf_le) show "summable (\n. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable[of E] summable_minus[of "\n. 1 / real (num_wtn E n)"] by simp show "summable (\i. -real_of_ereal (\ (neg_wtn E i)))" using neg_wtn_summable assms summable_minus[of "\i. real_of_ereal (\ (neg_wtn E i))"] by (simp add: summable_minus_iff) show "\n. 1 / real (num_wtn E n) \ -real_of_ereal (\ (neg_wtn E n))" proof - fix n have "\ (neg_wtn E n) \ ereal (- 1 / real (num_wtn E n))" using num_wtn_geq by simp hence "ereal (1/ real (num_wtn E n)) \ - \ (neg_wtn E n)" by (metis add.inverse_inverse eq_iff ereal_uminus_le_reorder linear minus_divide_left uminus_ereal.simps(1)) have "real_of_ereal (ereal (1 / real (num_wtn E n))) \ real_of_ereal (- \ (neg_wtn E n))" proof (rule real_of_ereal_positive_mono) show "0 \ ereal (1 / real (num_wtn E n))" by simp show "ereal (1 / real (num_wtn E n)) \ - \ (neg_wtn E n)" using \ereal (1 / real (num_wtn E n)) \ - \ (neg_wtn E n)\ . show "- \ (neg_wtn E n) \ \" using neg_wtn_infty[of E n] assms by auto qed thus "(1 / real (num_wtn E n)) \ -real_of_ereal ( \ (neg_wtn E n))" by simp qed qed also have "... = - suminf (\i. real_of_ereal (\ (neg_wtn E i)))" proof (rule suminf_minus) show "summable (\n. real_of_ereal (\ (neg_wtn E n)))" using neg_wtn_summable assms summable_minus[of "\i. real_of_ereal (\ (neg_wtn E i))"] by (simp add: summable_minus_iff) qed finally have "suminf (\n. 1/(num_wtn E n)) \ - suminf (\i. real_of_ereal (\ (neg_wtn E i)))" . hence a: "suminf (\i. real_of_ereal (\ (neg_wtn E i))) \ - suminf (\n. 1/(num_wtn E n))" by simp show "suminf (\i. (\ (neg_wtn E i))) \ ereal (-suminf (\n. 1/(num_wtn E n)))" proof - have sumeq: "suminf (\i. ereal (real_of_ereal (\ (neg_wtn E i)))) = suminf (\i. (real_of_ereal (\ (neg_wtn E i))))" proof (rule sums_suminf_ereal) have "summable (\i. -real_of_ereal (\ (neg_wtn E i)))" using neg_wtn_summable assms summable_minus[of "\i. real_of_ereal (\ (neg_wtn E i))"] by (simp add: summable_minus_iff) thus "(\i. real_of_ereal (\ (neg_wtn E i))) sums (\i. real_of_ereal (\ (neg_wtn E i)))" using neg_wtn_summable[of E] assms summable_minus_iff by blast qed hence "suminf (\i. \ (neg_wtn E i)) = suminf (\i. (real_of_ereal (\ (neg_wtn E i))))" proof - have "\i. ereal (real_of_ereal (\ (neg_wtn E i))) = \ (neg_wtn E i)" proof - fix i show "ereal (real_of_ereal (\ (neg_wtn E i))) = \ (neg_wtn E i)" using neg_wtn_infty[of E] assms by (simp add: ereal_real') qed thus ?thesis using sumeq by auto qed thus ?thesis using a by simp qed qed lemma union_wit_meas_le: assumes "E \ sets M" and "\\ E\ < \" shows "\ (union_wit E) \ - suminf (\n. 1 / real (num_wtn E n))" proof - have "\ (union_wit E) = \ (\ (range (neg_wtn E)))" unfolding union_wit_def by simp also have "... = (\i. \ (neg_wtn E i))" proof (rule signed_measure_inf_sum[symmetric]) show "signed_measure M \" using sgn_meas . show "range (neg_wtn E) \ sets M" by (simp add: image_subset_iff neg_wtn_def rep_neg_sets) show "disjoint_family (neg_wtn E)" using neg_wtn_djn by simp show "\ (range (neg_wtn E)) \ sets M" using union_wit_sets unfolding union_wit_def by simp qed also have "... \ - suminf (\n. 1 / real (num_wtn E n))" using assms neg_wtn_meas_suminf_le by simp finally show ?thesis . qed lemma pos_sub_pos_meas: assumes "E \ sets M" and "\\ E\ < \" and "0 < \ E" and "\ pos_meas_set E" shows "0 < \ (pos_sub E)" proof - have "0 < \ E" using assms by simp also have "... = \ (pos_sub E) + \ (union_wit E)" proof - have "E = pos_sub E \ (union_wit E)" using pos_sub_diff[of E] union_wit_subset by force moreover have "pos_sub E \ union_wit E = {}" using pos_sub_diff by auto ultimately show ?thesis using signed_measure_add[of M \ "pos_sub E" "union_wit E"] pos_sub_sets union_wit_sets assms sgn_meas by simp qed also have "... \ \ (pos_sub E) + (- suminf (\n. 1 / real (num_wtn E n)))" proof - have "\ (union_wit E) \ - suminf (\n. 1 / real (num_wtn E n))" using union_wit_meas_le[of E] assms by simp thus ?thesis using union_wit_infty assms using add_left_mono by blast qed also have "... = \ (pos_sub E) - suminf (\n. 1 / real (num_wtn E n))" by (simp add: minus_ereal_def) finally have "0 < \ (pos_sub E) - suminf (\n. 1 / real (num_wtn E n))" . moreover have "0 < suminf (\n. 1 / real (num_wtn E n))" proof (rule suminf_pos2) show "0 < 1 / real (num_wtn E 0)" using inf_neg_ge_1[of E] assms pos_wtn_base unfolding num_wtn_def by simp show "\n. 0 \ 1 / real (num_wtn E n)" by simp show "summable (\n. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable by simp qed ultimately show ?thesis using pos_sub_infty assms by fastforce qed lemma num_wtn_conv: assumes "E \ sets M" and "\\ E\ < \" shows "(\n. 1/(num_wtn E n)) \ 0" proof (rule summable_LIMSEQ_zero) show "summable (\n. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable by simp qed lemma num_wtn_shift_conv: assumes "E \ sets M" and "\\ E\ < \" shows "(\n. 1/(num_wtn E n - 1)) \ 0" proof (rule summable_LIMSEQ_zero) show "summable (\n. 1 / real (num_wtn E n - 1))" using assms inv_num_wtn_shift_summable by simp qed lemma inf_neg_E_set: assumes "0 < inf_neg E" shows "E \ sets M" using assms unfolding inf_neg_def by presburger lemma inf_neg_pos_meas: assumes "0 < inf_neg E" shows "\ pos_meas_set E" using assms unfolding inf_neg_def by presburger lemma inf_neg_mem: assumes "0 < inf_neg E" shows "inf_neg E \ {n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ E \ \ B < ereal (-1/n))}" proof - have "E \ sets M" using assms unfolding inf_neg_def by presburger moreover have "\ pos_meas_set E" using assms unfolding inf_neg_def by presburger ultimately have "{n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ E \ \ B < ereal (-1/n))} \ {}" using inf_neg_ne[of E] by simp thus ?thesis unfolding inf_neg_def by (meson Inf_nat_def1 \E \ sets M\ \\ pos_meas_set E\) qed lemma prec_inf_neg_pos: assumes "0 < inf_neg E - 1" and "B \ sets M" and "B\ E" shows "-1/(inf_neg E - 1) \ \ B" proof (rule ccontr) define S where "S = {p::nat|p. (1::nat) \ p \ (\B \ sets M. B \ E \ \ B < ereal (-1/p))}" assume "\ ereal (- 1 / real (inf_neg E - 1)) \ \ B" hence "\ B < -1/(inf_neg E - 1)" by auto hence "inf_neg E - 1\ S" unfolding S_def using assms by auto have "Suc 0 < inf_neg E" using assms by simp hence "inf_neg E \ S" unfolding S_def using inf_neg_mem[of E] by simp hence "S \ {}" by auto have "inf_neg E = Inf S" unfolding S_def inf_neg_def using assms inf_neg_E_set inf_neg_pos_meas by auto have "inf_neg E - 1 < inf_neg E" using assms by simp hence "inf_neg E -1 \ S" using cInf_less_iff[of S] \S \ {}\ \inf_neg E = Inf S\ by auto thus False using \inf_neg E - 1 \ S\ by simp qed lemma pos_wtn_meas_ge: assumes "E \ sets M" and "\\ E\ < \" and "C\ sets M" and "\n. C\ pos_wtn E n" and "\n. 0 < num_wtn E n" shows "\N. \n\ N. - 1/ (num_wtn E n - 1) \ \ C" proof - have "\N. \n\ N. 1/(num_wtn E n) < 1/2" using num_wtn_conv[of E] conv_0_half[of "\n. 1 / real (num_wtn E n)"] assms by simp from this obtain N where "\n\ N. 1/(num_wtn E n) < 1/2" by auto { fix n assume "N \ n" hence "1/(num_wtn E n) < 1/2" using \\n\ N. 1/(num_wtn E n) < 1/2\ by simp have "1/(1/2) < 1/(1/(num_wtn E n))" proof (rule frac_less2, auto) show "2 / real (num_wtn E n) < 1" using \1/(num_wtn E n) < 1/2\ by linarith show "0 < num_wtn E n" unfolding num_wtn_def using inf_neg_ge_1 assms by (simp add: num_wtn_def) qed hence "2 < (num_wtn E n)" by simp hence "Suc 0 < num_wtn E n - 1" unfolding num_wtn_def by simp hence "- 1/ (num_wtn E n - 1) \ \ C" using assms prec_inf_neg_pos unfolding num_wtn_def by simp } thus ?thesis by auto qed lemma pos_sub_pos_meas_subset: assumes "E \ sets M" and "\\ E\ < \" and "C\ sets M" and "C\ (pos_sub E)" and "\n. 0 < num_wtn E n" shows "0 \ \ C" proof - have "\n. C \ pos_wtn E n" using assms unfolding pos_sub_def by auto hence "\N. \n\ N. - 1/ (num_wtn E n - 1) \ \ C" using assms pos_wtn_meas_ge[of E C] by simp from this obtain N where Nprop: "\n\ N. - 1/ (num_wtn E n - 1) \ \ C" by auto show "0 \ \ C" proof (rule lim_mono) show "\n. N \ n \ - 1/ (num_wtn E n - 1) \ (\n. \ C) n" using Nprop by simp have "(\n. ( 1 / real (num_wtn E n - 1))) \ 0" using assms num_wtn_shift_conv[of E] by simp hence "(\n. (- 1 / real (num_wtn E n - 1))) \ 0" using tendsto_minus[of "\n. 1 / real (num_wtn E n - 1)" 0] by simp thus "(\n. ereal (- 1 / real (num_wtn E n - 1))) \ 0" by (simp add: zero_ereal_def) show "(\n. \ C) \ \ C" by simp qed qed lemma pos_sub_pos_meas': assumes "E \ sets M" and "\\ E\ < \" and "0 < \ E" and "\n. 0 < num_wtn E n" shows "0 < \ (pos_sub E)" proof - have "0 < \ E" using assms by simp also have "... = \ (pos_sub E) + \ (union_wit E)" proof - have "E = pos_sub E \ (union_wit E)" using pos_sub_diff[of E] union_wit_subset by force moreover have "pos_sub E \ union_wit E = {}" using pos_sub_diff by auto ultimately show ?thesis using signed_measure_add[of M \ "pos_sub E" "union_wit E"] pos_sub_sets union_wit_sets assms sgn_meas by simp qed also have "... \ \ (pos_sub E) + (- suminf (\n. 1 / real (num_wtn E n)))" proof - have "\ (union_wit E) \ - suminf (\n. 1 / real (num_wtn E n))" using union_wit_meas_le[of E] assms by simp thus ?thesis using union_wit_infty assms using add_left_mono by blast qed also have "... = \ (pos_sub E) - suminf (\n. 1 / real (num_wtn E n))" by (simp add: minus_ereal_def) finally have "0 < \ (pos_sub E) - suminf (\n. 1 / real (num_wtn E n))" . moreover have "0 < suminf (\n. 1 / real (num_wtn E n))" proof (rule suminf_pos2) show "0 < 1 / real (num_wtn E 0)" using assms by simp show "\n. 0 \ 1 / real (num_wtn E n)" by simp show "summable (\n. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable by simp qed ultimately show ?thesis using pos_sub_infty assms by fastforce qed text \We obtain the main result of this part on the existence of a positive subset.\ lemma exists_pos_meas_subset: assumes "E \ sets M" and "\\ E\ < \" and "0 < \ E" shows "\A. A \ E \ pos_meas_set A \ 0 < \ A" proof (cases "\n. 0 < num_wtn E n") case True have "pos_meas_set (pos_sub E)" proof (rule pos_meas_setI) show "pos_sub E \ sets M" by (simp add: assms(1) pos_sub_sets) fix A assume "A \ sets M" and "A\ pos_sub E" thus "0 \ \ A" using assms True pos_sub_pos_meas_subset[of E] by simp qed moreover have "0 < \ (pos_sub E)" using pos_sub_pos_meas'[of E] True assms by simp ultimately show ?thesis using pos_meas_set_def by (metis pos_sub_subset) next case False hence "\n. num_wtn E n = 0" by simp from this obtain n where "num_wtn E n = 0" by auto hence "pos_wtn E n \ sets M \ pos_meas_set (pos_wtn E n)" using inf_neg_ge_1 unfolding num_wtn_def by fastforce hence "pos_meas_set (pos_wtn E n)" using assms by (simp add: \E \ sets M\ pos_wtn_sets) moreover have "0 < \ (pos_wtn E n)" using pos_wtn_meas_gt assms by simp ultimately show ?thesis using pos_meas_set_def by (meson pos_wtn_subset) qed section \The Hahn decomposition theorem\ definition seq_meas where "seq_meas = (SOME f. incseq f \ range f \ pos_img \ \ pos_img = \ range f)" lemma seq_meas_props: shows "incseq seq_meas \ range seq_meas \ pos_img \ \ pos_img = \ range seq_meas" proof - have ex: "\f. incseq f \ range f \ pos_img \ \ pos_img = \ range f" proof (rule Extended_Real.Sup_countable_SUP) show "pos_img \ {}" proof - have "{} \ pos_sets" using empty_pos_meas_set unfolding pos_sets_def by simp hence "\ {} \ pos_img" unfolding pos_img_def by auto thus ?thesis by auto qed qed let ?V = "SOME f. incseq f \ range f \ pos_img \ \ pos_img = \ range f" have vprop: "incseq ?V \ range ?V \ pos_img \ \ pos_img = \ range ?V" using someI_ex[of "\f. incseq f \ range f \ pos_img \ \ pos_img = \ range f"] ex by blast show ?thesis using seq_meas_def vprop by presburger qed definition seq_meas_rep where "seq_meas_rep n = (SOME A. A\ pos_sets \ seq_meas n = \ A)" lemma seq_meas_rep_ex: shows "seq_meas_rep n \ pos_sets \ \ (seq_meas_rep n) = seq_meas n" proof - have ex: "\A. A \ pos_sets \ seq_meas n = \ A" using seq_meas_props by (smt (z3) UNIV_I image_subset_iff mem_Collect_eq pos_img_def) let ?V = "SOME A. A\ pos_sets \ seq_meas n = \ A" have vprop: "?V\ pos_sets \ seq_meas n = \ ?V" using someI_ex[of "\A. A\ pos_sets \ seq_meas n = \ A"] using ex by blast show ?thesis using seq_meas_rep_def vprop by fastforce qed lemma seq_meas_rep_pos: assumes "\E \ sets M. \ E < \" shows "pos_meas_set (\ i. seq_meas_rep i)" proof (rule pos_meas_set_Union) show " \i. pos_meas_set (seq_meas_rep i)" using seq_meas_rep_ex signed_measure_space.pos_sets_def signed_measure_space_axioms by auto then show "\i. seq_meas_rep i \ sets M" by (simp add: pos_meas_setD1) show "\\ (\ (range seq_meas_rep))\ < \" proof - have "(\ (range seq_meas_rep)) \ sets M" proof (rule sigma_algebra.countable_Union) show "sigma_algebra (space M) (sets M)" by (simp add: sets.sigma_algebra_axioms) show "countable (range seq_meas_rep)" by simp show "range seq_meas_rep \ sets M" by (simp add: \\i. seq_meas_rep i \ sets M\ image_subset_iff) qed hence "\ (\ (range seq_meas_rep)) \ 0 " using \\i. pos_meas_set (seq_meas_rep i)\ \\i. seq_meas_rep i \ sets M\ signed_measure_space.pos_meas_set_pos_lim signed_measure_space_axioms by blast thus ?thesis using assms \\ (range seq_meas_rep) \ sets M\ abs_ereal_ge0 by simp qed qed lemma sup_seq_meas_rep: assumes "\E \ sets M. \ E < \" and "S = (\ pos_img)" and "A = (\ i. seq_meas_rep i)" shows "\ A = S" proof - have pms: "pos_meas_set (\ i. seq_meas_rep i)" using assms seq_meas_rep_pos by simp hence "\ A \ S" by (metis (mono_tags, lifting) Sup_upper \S = \ pos_img\ mem_Collect_eq pos_img_def pos_meas_setD1 pos_sets_def assms(2) assms(3)) have "\n. (\ A = \ (A - seq_meas_rep n) + \ (seq_meas_rep n))" proof fix n have "A = (A - seq_meas_rep n) \ seq_meas_rep n " using \A = \ (range seq_meas_rep)\ by blast hence "\ A = \ ((A - seq_meas_rep n) \ seq_meas_rep n)" by simp also have "... = \ (A - seq_meas_rep n) + \ (seq_meas_rep n)" proof (rule signed_measure_add) show "signed_measure M \" using sgn_meas by simp show "seq_meas_rep n \ sets M" using pos_sets_def seq_meas_rep_ex by auto then show "A - seq_meas_rep n \ sets M" by (simp add: assms pms pos_meas_setD1 sets.Diff) show "(A - seq_meas_rep n) \ seq_meas_rep n = {}" by auto qed finally show "\ A = \ (A - seq_meas_rep n) + \ (seq_meas_rep n)". qed have "\n. \ A \ \ (seq_meas_rep n)" proof fix n have "\ A \ 0" using pms assms unfolding pos_meas_set_def by auto have "(A - seq_meas_rep n) \ A" by simp hence "pos_meas_set (A - seq_meas_rep n)" proof - have "(A - seq_meas_rep n) \ sets M" using pms assms pos_meas_setD1 pos_sets_def seq_meas_rep_ex by auto thus ?thesis using pms assms unfolding pos_meas_set_def by auto qed hence "\ (A - seq_meas_rep n) \ 0" unfolding pos_meas_set_def by auto thus "\ (seq_meas_rep n) \ \ A" using \\n. (\ A = \ (A - seq_meas_rep n) + \ (seq_meas_rep n))\ by (metis ereal_le_add_self2) qed hence "\ A \ (\ range seq_meas)" by (simp add: Sup_le_iff seq_meas_rep_ex) moreover have "S = (\ range seq_meas)" using seq_meas_props \S = (\ pos_img)\ by simp ultimately have "\ A \ S" by simp thus "\ A = S" using \\ A \ S\ by simp qed lemma seq_meas_rep_compl: assumes "\E \ sets M. \ E < \" and "A = (\ i. seq_meas_rep i)" shows "neg_meas_set ((space M) - A)" unfolding neg_meas_set_def proof (rule ccontr) assume asm: "\ (space M - A \ sets M \ (\Aa\sets M. Aa \ space M - A \ \ Aa \ 0))" define S where "S = (\ pos_img)" have "pos_meas_set A" using assms seq_meas_rep_pos by simp have "\ A = S" using sup_seq_meas_rep assms S_def by simp hence "S < \" using assms \pos_meas_set A\ pos_meas_setD1 by blast have "(space M - A \ sets M)" by (simp add: \pos_meas_set A\ pos_meas_setD1 sets.compl_sets) hence " \(\Aa\sets M. Aa \ space M - A \ \ Aa \ 0)" using asm by blast hence "\ E \ sets M. E \ ((space M) - A) \ \ E > 0" by (metis less_eq_ereal_def linear) from this obtain E where "E \ sets M" and "E \ ((space M) - A)" and "\ E > 0" by auto have "\ A0 \ E. pos_meas_set A0 \ \ A0 > 0" proof (rule exists_pos_meas_subset) show "E \ sets M" using \E \ sets M\ by simp show "0 < \ E" using \\ E > 0\ by simp show "\\ E\ < \" proof - have "\ E < \" using assms \E \ sets M\ by simp moreover have "- \ < \ E" using \0 < \ E\ by simp ultimately show ?thesis by (meson ereal_infty_less(1) not_inftyI) qed qed from this obtain A0 where "A0 \ E" and "pos_meas_set A0" and " \ A0 > 0" by auto have "pos_meas_set (A \ A0)" using pos_meas_set_union \pos_meas_set A0\ \pos_meas_set A\ by simp have "\ (A \ A0) = \ A + \ A0" proof (rule signed_measure_add) show "signed_measure M \" using sgn_meas by simp show "A \ sets M" using \pos_meas_set A\ unfolding pos_meas_set_def by simp show "A0 \ sets M" using \pos_meas_set A0\ unfolding pos_meas_set_def by simp show "(A \ A0) = {}" using \A0 \ E\ \E \ ((space M) - A)\ by auto qed then have "\ (A \ A0) > S" using \\ A = S\ \\ A0 > 0\ by (metis \S < \\ \pos_meas_set (A \ A0)\ abs_ereal_ge0 ereal_between(2) not_inftyI not_less_iff_gr_or_eq pos_meas_self) have "(A \ A0) \ pos_sets" proof - have " (A \ A0) \ sets M" using sigma_algebra.countable_Union by (simp add: \pos_meas_set (A \ A0)\ pos_meas_setD1) moreover have "pos_meas_set (A \ A0)" using \pos_meas_set (A \ A0)\ by simp ultimately show ?thesis unfolding pos_sets_def by simp qed then have "\ (A \ A0) \ pos_img" unfolding pos_img_def by auto show False using \\ (A \ A0) > S\ \\ (A \ A0) \ pos_img\ \S = (\ pos_img)\ by (metis Sup_upper sup.absorb_iff2 sup.strict_order_iff) qed lemma hahn_decomp_finite: assumes "\E \ sets M. \ E < \" shows "\ M1 M2. hahn_space_decomp M1 M2" unfolding hahn_space_decomp_def proof - define S where "S = (\ pos_img)" define A where "A = (\ i. seq_meas_rep i)" have "pos_meas_set A" unfolding A_def using assms seq_meas_rep_pos by simp have "neg_meas_set ((space M) - A)" using seq_meas_rep_compl assms unfolding A_def by simp show "\M1 M2. pos_meas_set M1 \ neg_meas_set M2 \ space M = M1 \ M2 \ M1 \ M2 = {}" proof (intro exI conjI) show "pos_meas_set A" using \pos_meas_set A\ . show "neg_meas_set (space M - A)" using \neg_meas_set (space M - A)\ . show "space M = A \ (space M - A)" by (metis Diff_partition \pos_meas_set A\ inf.absorb_iff2 pos_meas_setD1 sets.Int_space_eq1) show "A \ (space M - A) = {}" by auto qed qed theorem hahn_decomposition: shows "\ M1 M2. hahn_space_decomp M1 M2" proof (cases "\E \ sets M. \ E < \") case True thus ?thesis using hahn_decomp_finite by simp next case False define m where "m = (\A . - \ A)" have "\ M1 M2. signed_measure_space.hahn_space_decomp M m M1 M2" proof (rule signed_measure_space.hahn_decomp_finite) show "signed_measure_space M m" using signed_measure_minus sgn_meas \m = (\A . - \ A)\ by (unfold_locales, simp) show "\E\sets M. m E < \" proof fix E assume "E \ sets M" show "m E < \" proof show "m E \ \" proof (rule ccontr) assume "\ m E \ \" have "m E = \" using \\ m E \ \\ by auto have "signed_measure M m" using \signed_measure_space M m\ signed_measure_space_def by auto moreover have "m E = - \ E" using \m = (\A . - \ A)\ by auto then have "\ \ range m" using \signed_measure M m\ by (metis (no_types, lifting) False ereal_less_PInfty ereal_uminus_eq_reorder image_iff inf_range m_def rangeI) show False using \m E = \\ \\ \ range m\ by (metis rangeI) qed qed qed qed hence "\ M1 M2. (neg_meas_set M1) \ (pos_meas_set M2) \ (space M = M1 \ M2) \ (M1 \ M2 = {})" using pos_meas_set_opp neg_meas_set_opp unfolding m_def by (metis sgn_meas signed_measure_minus signed_measure_space_def signed_measure_space.hahn_space_decomp_def) thus ?thesis using hahn_space_decomp_def by (metis inf_commute sup_commute) qed section \The Jordan decomposition theorem\ definition jordan_decomp where "jordan_decomp m1 m2 \ ((measure_space (space M) (sets M) m1) \ (measure_space (space M) (sets M) m2) \ (\A\ sets M. 0 \ m1 A) \ (\ A\ sets M. 0 \ m2 A) \ (\A \ sets M. \ A = (m1 A) - (m2 A)) \ (\ P N A. hahn_space_decomp P N \ (A \ sets M \ A \ P \ (m2 A) = 0) \ (A \ sets M \ A \ N \ (m1 A) = 0)) \ ((\A \ sets M. m1 A < \) \ (\A \ sets M. m2 A < \)))" lemma jordan_decomp_pos_meas: assumes "jordan_decomp m1 m2" and "hahn_space_decomp P N" and "A \ sets M" shows "m1 A = \ (A \ P)" proof - have "A\P \ sets M" using assms unfolding hahn_space_decomp_def by (simp add: pos_meas_setD1 sets.Int) have "A\ N \ sets M" using assms unfolding hahn_space_decomp_def by (simp add: neg_meas_setD1 sets.Int) have "(A \ P) \ (A\ N) = {}" using assms unfolding hahn_space_decomp_def by auto have "A = (A \ P) \ (A\ N)" using assms unfolding hahn_space_decomp_def by (metis Int_Un_distrib sets.Int_space_eq2) hence "m1 A = m1 ((A \ P) \ (A\ N))" by simp also have "... = m1 (A \ P) + m1 (A \ N)" using assms pos_e2ennreal_additive[of M m1] \A\P \ sets M\ \A\N \ sets M\ \A \ P \ (A \ N) = {}\ unfolding jordan_decomp_def additive_def by simp also have "... = m1 (A \ P)" using assms unfolding jordan_decomp_def by (metis Int_lower2 \A \ N \ sets M\ add.right_neutral) also have "... = m1 (A \ P) - m2 (A \ P)" using assms unfolding jordan_decomp_def by (metis Int_subset_iff \A \ P \ sets M\ ereal_minus(7) local.pos_wtn_base pos_wtn_subset) also have "... = \ (A \ P)" using assms \A \ P \ sets M\ unfolding jordan_decomp_def by simp finally show ?thesis . qed lemma jordan_decomp_neg_meas: assumes "jordan_decomp m1 m2" and "hahn_space_decomp P N" and "A \ sets M" shows "m2 A = -\ (A \ N)" proof - have "A\P \ sets M" using assms unfolding hahn_space_decomp_def by (simp add: pos_meas_setD1 sets.Int) have "A\ N \ sets M" using assms unfolding hahn_space_decomp_def by (simp add: neg_meas_setD1 sets.Int) have "(A \ P) \ (A\ N) = {}" using assms unfolding hahn_space_decomp_def by auto have "A = (A \ P) \ (A\ N)" using assms unfolding hahn_space_decomp_def by (metis Int_Un_distrib sets.Int_space_eq2) hence "m2 A = m2 ((A \ P) \ (A\ N))" by simp also have "... = m2 (A \ P) + m2 (A \ N)" using pos_e2ennreal_additive[of M m2] assms \A\P \ sets M\ \A\N \ sets M\ \A \ P \ (A \ N) = {}\ unfolding jordan_decomp_def additive_def by simp also have "... = m2 (A \ N)" using assms unfolding jordan_decomp_def by (metis Int_lower2 \A \ P \ sets M\ add.commute add.right_neutral) also have "... = m2 (A \ N) - m1 (A \ N)" using assms unfolding jordan_decomp_def by (metis Int_lower2 \A \ N \ sets M\ ereal_minus(7)) also have "... = -\ (A \ N)" using assms \A \ P \ sets M\ unfolding jordan_decomp_def by (metis Diff_cancel Diff_eq_empty_iff Int_Un_eq(2) \A \ N \ sets M\ \m2 (A \ N) = m2 (A \ N) - m1 (A \ N)\ ereal_minus(8) ereal_uminus_eq_reorder sup.bounded_iff) finally show ?thesis . qed lemma pos_inter_neg_0: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp P N" and "A \ sets M" and "A \ N" shows "\ (A \ M1) = 0" proof - have "\ (A \ M1) = \ (A \ ((M1 \ P) \ (M1 \ (sym_diff M1 P))))" by (metis Diff_subset_conv Int_Un_distrib Un_upper1 inf.orderE) also have "... = \ ((A \ (M1 \ P)) \ (A \ (M1 \ (sym_diff M1 P))))" by (simp add: Int_Un_distrib) also have "... = \ (A \ (M1 \ P)) + \ (A \ (M1 \ (sym_diff M1 P)))" proof (rule signed_measure_add) show "signed_measure M \" using sgn_meas . show "A \ (M1 \ P) \ sets M" by (meson assms(1) assms(2) assms(3) hahn_space_decomp_def sets.Int signed_measure_space.pos_meas_setD1 signed_measure_space_axioms) show "A \ (M1 \ sym_diff M1 P) \ sets M" by (meson Diff_subset assms(1) assms(2) assms(3) hahn_space_decomp_def pos_meas_setD1 pos_meas_set_union pos_meas_subset sets.Diff sets.Int) show "A \ (M1 \ P) \ (A \ (M1 \ sym_diff M1 P)) = {}" by auto qed also have "... = \ (A \ (M1 \ (sym_diff M1 P)))" proof - have "A \ (M1 \ P) = {}" using assms hahn_space_decomp_def by auto thus ?thesis using signed_measure_empty[OF sgn_meas] by simp qed also have "... = 0" proof (rule hahn_decomp_ess_unique[OF assms(1) assms(2)]) show "A \ (M1 \ sym_diff M1 P) \ sym_diff M1 P \ sym_diff M2 N" by auto show "A \ (M1 \ sym_diff M1 P) \ sets M" proof - have "sym_diff M1 P \ sets M" using assms by (meson hahn_space_decomp_def sets.Diff sets.Un signed_measure_space.pos_meas_setD1 signed_measure_space_axioms) hence "M1 \ sym_diff M1 P \ sets M" by (meson assms(1) hahn_space_decomp_def pos_meas_setD1 sets.Int) thus ?thesis by (simp add: assms sets.Int) qed qed finally show ?thesis . qed lemma neg_inter_pos_0: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp P N" and "A \ sets M" and "A \ P" shows "\ (A \ M2) = 0" proof - have "\ (A \ M2) = \ (A \ ((M2 \ N) \ (M2 \ (sym_diff M2 N))))" by (metis Diff_subset_conv Int_Un_distrib Un_upper1 inf.orderE) also have "... = \ ((A \ (M2 \ N)) \ (A \ (M2 \ (sym_diff M2 N))))" by (simp add: Int_Un_distrib) also have "... = \ (A \ (M2 \ N)) + \ (A \ (M2 \ (sym_diff M2 N)))" proof (rule signed_measure_add) show "signed_measure M \" using sgn_meas . show "A \ (M2 \ N) \ sets M" by (meson assms(1) assms(2) assms(3) hahn_space_decomp_def sets.Int signed_measure_space.neg_meas_setD1 signed_measure_space_axioms) show "A \ (M2 \ sym_diff M2 N) \ sets M" by (meson Diff_subset assms(1) assms(2) assms(3) hahn_space_decomp_def neg_meas_setD1 neg_meas_set_union neg_meas_subset sets.Diff sets.Int) show "A \ (M2 \ N) \ (A \ (M2 \ sym_diff M2 N)) = {}" by auto qed also have "... = \ (A \ (M2 \ (sym_diff M2 N)))" proof - have "A \ (M2 \ N) = {}" using assms hahn_space_decomp_def by auto thus ?thesis using signed_measure_empty[OF sgn_meas] by simp qed also have "... = 0" proof (rule hahn_decomp_ess_unique[OF assms(1) assms(2)]) show "A \ (M2 \ sym_diff M2 N) \ sym_diff M1 P \ sym_diff M2 N" by auto show "A \ (M2 \ sym_diff M2 N) \ sets M" proof - have "sym_diff M2 N \ sets M" using assms by (meson hahn_space_decomp_def sets.Diff sets.Un signed_measure_space.neg_meas_setD1 signed_measure_space_axioms) hence "M2 \ sym_diff M2 N \ sets M" by (meson assms(1) hahn_space_decomp_def neg_meas_setD1 sets.Int) thus ?thesis by (simp add: assms sets.Int) qed qed finally show ?thesis . qed lemma jordan_decomposition : shows "\ m1 m2. jordan_decomp m1 m2" proof - have "\ M1 M2. hahn_space_decomp M1 M2" using hahn_decomposition unfolding hahn_space_decomp_def by simp from this obtain M1 M2 where "hahn_space_decomp M1 M2" by auto note Mprops = this define m1 where "m1 = (\A. \ (A \ M1))" define m2 where "m2 = (\A. -\ (A \ M2))" show ?thesis unfolding jordan_decomp_def proof (intro exI allI impI conjI ballI) show "measure_space (space M) (sets M) (\x. e2ennreal (m1 x))" using pos_signed_to_meas_space Mprops m1_def unfolding hahn_space_decomp_def by auto next show "measure_space (space M) (sets M) (\x. e2ennreal (m2 x))" using neg_signed_to_meas_space Mprops m2_def unfolding hahn_space_decomp_def by auto next fix A assume "A\ sets M" thus "0 \ m1 A" unfolding m1_def using Mprops unfolding hahn_space_decomp_def by (meson inf_sup_ord(2) pos_meas_setD1 sets.Int signed_measure_space.pos_measure_meas signed_measure_space_axioms) next fix A assume "A\ sets M" thus "0 \ m2 A" unfolding m2_def using Mprops unfolding hahn_space_decomp_def by (metis ereal_0_le_uminus_iff inf_sup_ord(2) neg_meas_self neg_meas_setD1 neg_meas_subset sets.Int) next fix A assume "A \ sets M" have "\ A = \ ((A \ M1) \ (A \ M2))" using Mprops unfolding hahn_space_decomp_def by (metis Int_Un_distrib \A \ sets M\ sets.Int_space_eq2) also have "... = \ (A \ M1) + \ (A \ M2)" proof (rule signed_measure_add) show "signed_measure M \" using sgn_meas . show "A \ M1 \ sets M" using Mprops \A \ sets M\ unfolding hahn_space_decomp_def by (simp add: pos_meas_setD1 sets.Int) show "A \ M2 \ sets M" using Mprops \A \ sets M\ unfolding hahn_space_decomp_def by (simp add: neg_meas_setD1 sets.Int) show "A \ M1 \ (A \ M2) = {}" using Mprops unfolding hahn_space_decomp_def by auto qed also have "... = m1 A - m2 A" using m1_def m2_def by simp finally show "\ A = m1 A - m2 A" . next fix P N A assume "hahn_space_decomp P N" and "A \ sets M" and "A \ N" note hn = this have "\ (A \ M1) = 0" proof (rule pos_inter_neg_0[OF _ hn]) show "hahn_space_decomp M1 M2" using Mprops unfolding hahn_space_decomp_def by simp qed thus "m1 A = 0" unfolding m1_def by simp next fix P N A assume "hahn_space_decomp P N" and "A \ sets M" and "A \ P" note hp = this have "\ (A \ M2) = 0" proof (rule neg_inter_pos_0[OF _ hp]) show "hahn_space_decomp M1 M2" using Mprops unfolding hahn_space_decomp_def by simp qed thus "m2 A = 0" unfolding m2_def by simp next show "(\E\sets M. m1 E < \) \ (\E\sets M. m2 E < \)" proof (cases "\ E \ sets M. m1 E < \") case True thus ?thesis by simp next case False have "\ E \ sets M. m2 E < \" proof fix E assume "E \ sets M" show "m2 E < \" proof - have "(m2 E) = -\ (E \ M2)" using m2_def by simp also have "... \ \" using False sgn_meas inf_range by (metis ereal_less_PInfty ereal_uminus_uminus m1_def rangeI) finally have "m2 E \ \" . thus ?thesis by (simp add: top.not_eq_extremum) qed qed thus ?thesis by simp qed qed qed lemma jordan_decomposition_unique : assumes "jordan_decomp m1 m2" and "jordan_decomp n1 n2" and "A \ sets M" shows "m1 A = n1 A" "m2 A = n2 A" proof - have "\ M1 M2. hahn_space_decomp M1 M2" using hahn_decomposition by simp from this obtain M1 M2 where "hahn_space_decomp M1 M2" by auto note mprop = this have "m1 A = \ (A \ M1)" using assms jordan_decomp_pos_meas mprop by simp also have "... = n1 A" using assms jordan_decomp_pos_meas[of n1] mprop by simp finally show "m1 A = n1 A" . have "m2 A = -\ (A \ M2)" using assms jordan_decomp_neg_meas mprop by simp also have "... = n2 A" using assms jordan_decomp_neg_meas[of n1] mprop by simp finally show "m2 A = n2 A" . qed end end diff --git a/thys/Van_Emde_Boas_Trees/Imperative_HOL_Time/Array_Time.thy b/thys/Van_Emde_Boas_Trees/Imperative_HOL_Time/Array_Time.thy --- a/thys/Van_Emde_Boas_Trees/Imperative_HOL_Time/Array_Time.thy +++ b/thys/Van_Emde_Boas_Trees/Imperative_HOL_Time/Array_Time.thy @@ -1,511 +1,511 @@ (* Title: Imperative_HOL_Time/Array_Time.thy Author: Maximilian P. L. Haslbeck & Bohua Zhan, TU Muenchen *) section \Monadic arrays\ text \This theory is an adaptation of \HOL/Imperative_HOL/Array_Time.thy\, adding time bookkeeping.\ theory Array_Time imports Heap_Time_Monad begin subsection \Primitives\ definition present :: "heap \ 'a::heap array \ bool" where "present h a \ addr_of_array a < lim h" definition get :: "heap \ 'a::heap array \ 'a list" where "get h a = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" definition set :: "'a::heap array \ 'a list \ heap \ heap" where "set a x = arrays_update (\h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" definition alloc :: "'a list \ heap \ 'a::heap array \ heap" where "alloc xs h = (let l = lim h; r = Array l; h'' = set r xs (h\lim := l + 1\) in (r, h''))" definition length :: "heap \ 'a::heap array \ nat" where "length h a = List.length (get h a)" definition update :: "'a::heap array \ nat \ 'a \ heap \ heap" where "update a i x h = set a ((get h a)[i:=x]) h" definition noteq :: "'a::heap array \ 'b::heap array \ bool" (infix "=!!=" 70) where "r =!!= s \ TYPEREP('a) \ TYPEREP('b) \ addr_of_array r \ addr_of_array s" subsection \Monad operations\ definition new :: "nat \ 'a::heap \ 'a array Heap" where [code del]: "new n x = Heap_Time_Monad.heap (%h. let (r,h') = alloc (replicate n x) h in (r,h',n+1))" definition of_list :: "'a::heap list \ 'a array Heap" where [code del]: "of_list xs = Heap_Time_Monad.heap (%h. let (r,h') = alloc xs h in (r,h',1+List.length xs))" definition make :: "nat \ (nat \ 'a::heap) \ 'a array Heap" where [code del]: "make n f = Heap_Time_Monad.heap (%h. let (r,h') = alloc (map f [0 ..< n]) h in (r,h',n+1))" definition len :: "'a::heap array \ nat Heap" where [code del]: "len a = Heap_Time_Monad.tap (\h. length h a)" definition nth :: "'a::heap array \ nat \ 'a Heap" where [code del]: "nth a i = Heap_Time_Monad.guard (\h. i < length h a) (\h. (get h a ! i, h, 1))" definition upd :: "nat \ 'a \ 'a::heap array \ 'a::heap array Heap" where [code del]: "upd i x a = Heap_Time_Monad.guard (\h. i < length h a) (\h. (a, update a i x h, 1))" definition map_entry :: "nat \ ('a::heap \ 'a) \ 'a array \ 'a array Heap" where [code del]: "map_entry i f a = Heap_Time_Monad.guard (\h. i < length h a) (\h. (a, update a i (f (get h a ! i)) h, 2))" definition swap :: "nat \ 'a \ 'a::heap array \ 'a Heap" where [code del]: "swap i x a = Heap_Time_Monad.guard (\h. i < length h a) (\h. (get h a ! i, update a i x h, 2 ))" (* questionable *) definition freeze :: "'a::heap array \ 'a list Heap" where [code del]: "freeze a = Heap_Time_Monad.heap (\h. (get h a, h, 1+length h a)) " subsection \Properties\ text \FIXME: Does there exist a "canonical" array axiomatisation in the literature?\ text \Primitives\ lemma noteq_sym: "a =!!= b \ b =!!= a" and unequal [simp]: "a \ a' \ a =!!= a'" unfolding noteq_def by auto lemma noteq_irrefl: "r =!!= r \ False" unfolding noteq_def by auto lemma present_alloc_noteq: "present h a \ a =!!= fst (alloc xs h)" by (simp add: present_def noteq_def alloc_def Let_def) lemma get_set_eq [simp]: "get (set r x h) r = x" by (simp add: get_def set_def o_def) lemma get_set_neq [simp]: "r =!!= s \ get (set s x h) r = get h r" by (simp add: noteq_def get_def set_def) lemma set_same [simp]: "set r x (set r y h) = set r x h" by (simp add: set_def) lemma set_set_swap: "r =!!= r' \ set r x (set r' x' h) = set r' x' (set r x h)" by (simp add: Let_def fun_eq_iff noteq_def set_def) lemma get_update_eq [simp]: "get (update a i v h) a = (get h a) [i := v]" by (simp add: update_def) lemma nth_update_neq [simp]: "a =!!= b \ get (update b j v h) a ! i = get h a ! i" by (simp add: update_def noteq_def) lemma get_update_elem_neqIndex [simp]: "i \ j \ get (update a j v h) a ! i = get h a ! i" by simp lemma length_update [simp]: "length (update b i v h) = length h" by (simp add: update_def length_def set_def get_def fun_eq_iff) lemma update_swap_neq: "a =!!= a' \ update a i v (update a' i' v' h) = update a' i' v' (update a i v h)" apply (unfold update_def) apply simp apply (subst set_set_swap, assumption) apply (subst get_set_neq) apply (erule noteq_sym) apply simp done lemma update_swap_neqIndex: "\ i \ i' \ \ update a i v (update a i' v' h) = update a i' v' (update a i v h)" by (auto simp add: update_def set_set_swap list_update_swap) lemma get_alloc: "get (snd (alloc xs h)) (fst (alloc ys h)) = xs" by (simp add: Let_def split_def alloc_def) lemma length_alloc: "length (snd (alloc (xs :: 'a::heap list) h)) (fst (alloc (ys :: 'a list) h)) = List.length xs" by (simp add: Array_Time.length_def get_alloc) lemma set: "set (fst (alloc ls h)) new_ls (snd (alloc ls h)) = snd (alloc new_ls h)" by (simp add: Let_def split_def alloc_def) lemma present_update [simp]: "present (update b i v h) = present h" by (simp add: update_def present_def set_def get_def fun_eq_iff) lemma present_alloc [simp]: "present (snd (alloc xs h)) (fst (alloc xs h))" by (simp add: present_def alloc_def set_def Let_def) lemma not_present_alloc [simp]: "\ present h (fst (alloc xs h))" by (simp add: present_def alloc_def Let_def) text \Monad operations\ lemma execute_new [execute_simps]: "execute (new n x) h = Some (let (r,h') = alloc (replicate n x) h in (r,h',n+1))" by (simp add: new_def execute_simps) lemma success_newI [success_intros]: "success (new n x) h" by (auto intro: success_intros simp add: new_def) lemma effect_newI [effect_intros]: assumes "(a, h') = alloc (replicate n x) h" shows "effect (new n x) h h' a (n+1)" apply (rule effectI) apply (simp add: assms execute_simps) by (metis assms case_prod_conv) lemma effect_newE [effect_elims]: assumes "effect (new n x) h h' r n'" obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)" "get h' r = replicate n x" "present h' r" "\ present h r" "n+1=n'" using assms apply (rule effectE) using case_prod_beta get_alloc execute_new by (metis (mono_tags, lifting) fst_conv not_present_alloc option.sel present_alloc sndI) (* apply (si mp add: case_prod_beta get_alloc execute_simps) refactor proof *) lemma execute_of_list [execute_simps]: "execute (of_list xs) h = Some (let (r,h') = alloc xs h in (r,h',1 + List.length xs))" by (simp add: of_list_def execute_simps) lemma success_of_listI [success_intros]: "success (of_list xs) h" by (auto intro: success_intros simp add: of_list_def) lemma effect_of_listI [effect_intros]: assumes "(a, h') = alloc xs h" shows "effect (of_list xs) h h' a (1 + List.length xs)" by (rule effectI, simp add: assms execute_simps, metis assms case_prod_conv) lemma effect_of_listE [effect_elims]: assumes "effect (of_list xs) h h' r n'" obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)" "get h' r = xs" "present h' r" "\ present h r" "n' = 1 + List.length xs" using assms apply (rule effectE) apply (simp add: get_alloc execute_of_list) by (simp add: case_prod_unfold) lemma execute_make [execute_simps]: "execute (make n f) h = Some (let (r,h') = alloc (map f [0 ..< n]) h in (r,h',n+1))" by (simp add: make_def execute_simps) lemma success_makeI [success_intros]: "success (make n f) h" by (auto intro: success_intros simp add: make_def) lemma effect_makeI [effect_intros]: assumes "(a, h') = alloc (map f [0 ..< n]) h" shows "effect (make n f) h h' a (n+1)" by (rule effectI) (simp add: assms execute_simps, metis assms case_prod_conv) lemma effect_makeE [effect_elims]: assumes "effect (make n f) h h' r n'" obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)" "get h' r = map f [0 ..< n]" "present h' r" "\ present h r" "n+1=n'" using assms apply (rule effectE) using get_alloc - by (metis (mono_tags, hide_lams) effectE effect_makeI not_present_alloc present_alloc prod.collapse) + by (metis (mono_tags, opaque_lifting) effectE effect_makeI not_present_alloc present_alloc prod.collapse) (* apply (si mp add: get_alloc execute_make) by (s imp add: case_prod_unfold) *) lemma execute_len [execute_simps]: "execute (len a) h = Some (length h a, h, 1)" by (simp add: len_def execute_simps) lemma success_lenI [success_intros]: "success (len a) h" by (auto intro: success_intros simp add: len_def) lemma effect_lengthI [effect_intros]: assumes "h' = h" "r = length h a" "n=1" shows "effect (len a) h h' r n" by (rule effectI) (simp add: assms execute_simps) lemma effect_lengthE [effect_elims]: assumes "effect (len a) h h' r n" obtains "r = length h' a" "h' = h" "n=1" using assms by (rule effectE) (simp add: execute_simps) lemma execute_nth [execute_simps]: "i < length h a \ execute (nth a i) h = Some (get h a ! i, h,1)" "i \ length h a \ execute (nth a i) h = None" by (simp_all add: nth_def execute_simps) lemma success_nthI [success_intros]: "i < length h a \ success (nth a i) h" by (auto intro: success_intros simp add: nth_def) lemma effect_nthI [effect_intros]: assumes "i < length h a" "h' = h" "r = get h a ! i" "n=1" shows "effect (nth a i) h h' r n" by (rule effectI) (insert assms, simp add: execute_simps) lemma effect_nthE [effect_elims]: assumes "effect (nth a i) h h' r n" obtains "i < length h a" "r = get h a ! i" "h' = h" "n=1" using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE) lemma execute_upd [execute_simps]: "i < length h a \ execute (upd i x a) h = Some (a, update a i x h, 1)" "i \ length h a \ execute (upd i x a) h = None" by (simp_all add: upd_def execute_simps) lemma success_updI [success_intros]: "i < length h a \ success (upd i x a) h" by (auto intro: success_intros simp add: upd_def) lemma effect_updI [effect_intros]: assumes "i < length h a" "h' = update a i v h" "n=1" shows "effect (upd i v a) h h' a n" by (rule effectI) (insert assms, simp add: execute_simps) lemma effect_updE [effect_elims]: assumes "effect (upd i v a) h h' r n" obtains "r = a" "h' = update a i v h" "i < length h a" "n=1" using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE) lemma execute_map_entry [execute_simps]: "i < length h a \ execute (map_entry i f a) h = Some (a, update a i (f (get h a ! i)) h, 2)" "i \ length h a \ execute (map_entry i f a) h = None" by (simp_all add: map_entry_def execute_simps) lemma success_map_entryI [success_intros]: "i < length h a \ success (map_entry i f a) h" by (auto intro: success_intros simp add: map_entry_def) lemma effect_map_entryI [effect_intros]: assumes "i < length h a" "h' = update a i (f (get h a ! i)) h" "r = a" "n=2" shows "effect (map_entry i f a) h h' r n" by (rule effectI) (insert assms, simp add: execute_simps) lemma effect_map_entryE [effect_elims]: assumes "effect (map_entry i f a) h h' r n" obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a" "n=2" using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE) lemma execute_swap [execute_simps]: "i < length h a \ execute (swap i x a) h = Some (get h a ! i, update a i x h, 2)" "i \ length h a \ execute (swap i x a) h = None" by (simp_all add: swap_def execute_simps) lemma success_swapI [success_intros]: "i < length h a \ success (swap i x a) h" by (auto intro: success_intros simp add: swap_def) lemma effect_swapI [effect_intros]: assumes "i < length h a" "h' = update a i x h" "r = get h a ! i" "n=2" shows "effect (swap i x a) h h' r n" by (rule effectI) (insert assms, simp add: execute_simps) lemma effect_swapE [effect_elims]: assumes "effect (swap i x a) h h' r n" obtains "r = get h a ! i" "h' = update a i x h" "i < length h a" "n=2" using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE) lemma execute_freeze [execute_simps]: "execute (freeze a) h = Some (get h a, h, 1+length h a)" by (simp add: freeze_def execute_simps) lemma success_freezeI [success_intros]: "success (freeze a) h" by (auto intro: success_intros simp add: freeze_def) lemma effect_freezeI [effect_intros]: assumes "h' = h" "r = get h a" "n=length h a" shows "effect (freeze a) h h' r (n+1)" by (rule effectI) (insert assms, simp add: execute_simps) lemma effect_freezeE [effect_elims]: assumes "effect (freeze a) h h' r n" obtains "h' = h" "r = get h a" "n=length h a+1" using assms by (rule effectE) (simp add: execute_simps) lemma upd_ureturn: "upd i x a \ ureturn a = upd i x a " by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps) lemma array_make: "new n x = make n (\_. x)" by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps) lemma array_of_list_make [code]: "of_list xs = make (List.length xs) (\n. xs ! n)" by (rule Heap_eqI) (simp add: map_nth execute_simps) hide_const (open) present get set alloc length update noteq new of_list make len nth upd map_entry swap freeze subsection \Code generator setup\ subsubsection \Logical intermediate layer\ definition new' where [code del]: "new' = Array_Time.new o nat_of_integer" lemma [code]: "Array_Time.new = new' o of_nat" by (simp add: new'_def o_def) definition make' where [code del]: "make' i f = Array_Time.make (nat_of_integer i) (f o of_nat)" lemma [code]: "Array_Time.make n f = make' (of_nat n) (f o nat_of_integer)" by (simp add: make'_def o_def) definition len' where [code del]: "len' a = Array_Time.len a \ (\n. ureturn (of_nat n))" lemma [code]: "Array_Time.len a = len' a \ (\i. ureturn (nat_of_integer i))" by (simp add: len'_def execute_simps) definition nth' where [code del]: "nth' a = Array_Time.nth a o nat_of_integer" lemma [code]: "Array_Time.nth a n = nth' a (of_nat n)" by (simp add: nth'_def) definition upd' where [code del]: "upd' a i x = Array_Time.upd (nat_of_integer i) x a \ ureturn ()" lemma [code]: "Array_Time.upd i x a = upd' a (of_nat i) x \ ureturn a" by (simp add: upd'_def upd_ureturn execute_simps) lemma [code]: "Array_Time.map_entry i f a = do { x \ Array_Time.nth a i; Array_Time.upd i (f x) a }" by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps) lemma [code]: "Array_Time.swap i x a = do { y \ Array_Time.nth a i; Array_Time.upd i x a; ureturn y }" by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps) (* lemma [code]: "Array_Time.freeze a = do { n \ Array_Time.len a; Heap_Monad.fold_map (\i. Array_Time.nth a i) [0..x. fst (the (if x < Array_Time.length h a then Some (Array_Time.get h a ! x, h) else None))) [0.. Array_Time.len a; Heap_Monad.fold_map (Array_Time.nth a) [0.. Array_Time.len a; Heap_Monad.fold_map (Array_Time.nth a) [0..SML\ code_printing type_constructor array \ (SML) "_/ array" code_printing constant Array \ (SML) "raise/ (Fail/ \"bare Array\")" code_printing constant Array_Time.new' \ (SML) "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))" code_printing constant Array_Time.of_list \ (SML) "(fn/ ()/ =>/ Array.fromList/ _)" code_printing constant Array_Time.make' \ (SML) "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))" code_printing constant Array_Time.len' \ (SML) "(fn/ ()/ =>/ Array.length/ _)" code_printing constant Array_Time.nth' \ (SML) "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))" code_printing constant Array_Time.upd' \ (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))" code_printing constant "HOL.equal :: 'a array \ 'a array \ bool" \ (SML) infixl 6 "=" code_reserved SML Array text \OCaml\ code_printing type_constructor array \ (OCaml) "_/ array" code_printing constant Array \ (OCaml) "failwith/ \"bare Array\"" code_printing constant Array_Time.new' \ (OCaml) "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)" code_printing constant Array_Time.of_list \ (OCaml) "(fun/ ()/ ->/ Array.of'_list/ _)" code_printing constant Array_Time.make' \ (OCaml) "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/ (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))" code_printing constant Array_Time.len' \ (OCaml) "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))" code_printing constant Array_Time.nth' \ (OCaml) "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))" code_printing constant Array_Time.upd' \ (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)" code_printing constant "HOL.equal :: 'a array \ 'a array \ bool" \ (OCaml) infixl 4 "=" code_reserved OCaml Array text \Haskell\ code_printing type_constructor array \ (Haskell) "Heap.STArray/ Heap.RealWorld/ _" code_printing constant Array \ (Haskell) "error/ \"bare Array\"" code_printing constant Array_Time.new' \ (Haskell) "Heap.newArray" code_printing constant Array_Time.of_list \ (Haskell) "Heap.newListArray" code_printing constant Array_Time.make' \ (Haskell) "Heap.newFunArray" code_printing constant Array_Time.len' \ (Haskell) "Heap.lengthArray" code_printing constant Array_Time.nth' \ (Haskell) "Heap.readArray" code_printing constant Array_Time.upd' \ (Haskell) "Heap.writeArray" code_printing constant "HOL.equal :: 'a array \ 'a array \ bool" \ (Haskell) infix 4 "==" code_printing class_instance array :: HOL.equal \ (Haskell) - text \Scala\ code_printing type_constructor array \ (Scala) "!collection.mutable.ArraySeq[_]" code_printing constant Array \ (Scala) "!sys.error(\"bare Array\")" code_printing constant Array_Time.new' \ (Scala) "('_: Unit)/ => / Array.alloc((_))((_))" code_printing constant Array_Time.make' \ (Scala) "('_: Unit)/ =>/ Array.make((_))((_))" code_printing constant Array_Time.len' \ (Scala) "('_: Unit)/ =>/ Array.len((_))" code_printing constant Array_Time.nth' \ (Scala) "('_: Unit)/ =>/ Array.nth((_), (_))" code_printing constant Array_Time.upd' \ (Scala) "('_: Unit)/ =>/ Array.upd((_), (_), (_))" code_printing constant Array_Time.freeze \ (Scala) "('_: Unit)/ =>/ Array.freeze((_))" code_printing constant "HOL.equal :: 'a array \ 'a array \ bool" \ (Scala) infixl 5 "==" end diff --git a/thys/Van_Emde_Boas_Trees/VEBT_InsertCorrectness.thy b/thys/Van_Emde_Boas_Trees/VEBT_InsertCorrectness.thy --- a/thys/Van_Emde_Boas_Trees/VEBT_InsertCorrectness.thy +++ b/thys/Van_Emde_Boas_Trees/VEBT_InsertCorrectness.thy @@ -1,1091 +1,1091 @@ (*by Ammer*) theory VEBT_InsertCorrectness imports VEBT_Member VEBT_Insert begin context VEBT_internal begin section \Correctness of the Insert Operation\ subsection \Validness Preservation\ theorem valid_pres_insert: "invar_vebt t n \ x< 2^n \ invar_vebt (vebt_insert t x) n" proof(induction t n arbitrary: x rule: invar_vebt.induct) case (1 a b) then show ?case using vebt_insert.simps(1)[of a b x] by (simp add: invar_vebt.intros(1)) next case (2 treeList n summary m deg) hence 0: " ( \ t \ set treeList. invar_vebt t n) " and 1:" invar_vebt summary n" and 2:" length treeList = 2^n" and 3:" deg = 2*n" and 4:" (\ i. both_member_options summary i)" and 5:" (\ t \ set treeList. \ x. both_member_options t x) " and 6: "n\ 1" using "2.prems" by (auto simp add: Suc_leI deg_not_0) let ?t = "Node None deg treeList summary" let ?tnew = "vebt_insert ?t x" have 6:"?tnew = (Node (Some (x,x)) deg treeList summary)" using vebt_insert.simps(4)[of "deg-2" treeList summary x] by (metis "1" "2.hyps"(3) "2.hyps"(4) add_2_eq_Suc add_diff_inverse_nat add_self_div_2 deg_not_0 div_less gr_implies_not0) have 7:"(x = x \ (\ t \ set treeList. \ x. both_member_options t x))" using \\t\set treeList. \x. both_member_options t x\ by blast have 8:"x \ x" by simp have 9:" x < 2^deg" by (simp add: "2.prems") have 10:"(x \ x \ (\ i < 2^(2^n). (high x deg = i \ both_member_options (treeList ! i) (low x deg)) \ (\ y. (high y deg = i \ both_member_options (treeList ! i) (low y deg) ) \ x < y \ y \ x) ))" by simp then show ?case using 0 1 2 3 4 5 6 7 8 9 10 invar_vebt.intros(4)[of treeList n summary m deg x x] by (metis "2.hyps"(3) "2.hyps"(4) nth_mem) next case (3 treeList n summary m deg) hence 0: " ( \ t \ set treeList. invar_vebt t n) " and 1:" invar_vebt summary m" and 2:" length treeList = 2^m" and 3:" deg = n+m" and 4:" (\ i. both_member_options summary i)" and 5:" (\ t \ set treeList. \ x. both_member_options t x) " and 6: "n\ 1" and 7: "Suc n = m" using "3.prems" apply auto by (metis "3.hyps"(2) One_nat_def set_n_deg_not_0) let ?t = "Node None deg treeList summary" let ?tnew = "vebt_insert ?t x" have 6:"?tnew = (Node (Some (x,x)) deg treeList summary)" using vebt_insert.simps(4)[of "deg-2" treeList summary x] by (smt "3" "3.hyps"(3) "6" Nat.add_diff_assoc One_nat_def Suc_le_mono add_diff_inverse_nat add_gr_0 add_numeral_left diff_is_0_eq' not_less not_less_iff_gr_or_eq numeral_2_eq_2 numerals(1) plus_1_eq_Suc semiring_norm(2)) have 7:"(x = x \ (\ t \ set treeList. \ x. both_member_options t x))" using \\t\set treeList. \x. both_member_options t x\ by blast have 8:"x \ x" by simp have 9:" x < 2^deg" by (simp add: "3.prems") have 10:"(x \ x \ (\ i < 2^(2^n). (high x deg = i \ both_member_options (treeList ! i) (low x deg)) \ (\ y. (high y deg = i \ both_member_options (treeList ! i) (low y deg) ) \ x < y \ y \ x) ))" by simp then show ?case using 0 1 2 3 4 5 6 7 8 9 10 invar_vebt.intros(5)[of treeList n summary m deg x x] "3.hyps"(3) nth_mem by force next case (4 treeList n summary m deg mi ma) hence myIHs: "x \ set treeList \ invar_vebt x n \ xa < 2 ^ n \ invar_vebt (vebt_insert x xa) n" for x xa by simp hence 0: "( \ t \ set treeList. invar_vebt t n)" and 1: " invar_vebt summary m" and 2:"length treeList = 2^m" and 3:" deg = n+m" and 4: "(\ i < 2^m. (\ y. both_member_options (treeList ! i) y) \ ( both_member_options summary i))" and 5: "(mi = ma \ (\ t \ set treeList. \ y. both_member_options t y))" and 6:"mi \ ma \ ma < 2^deg" and 7: "(mi \ ma \ (\ i < 2^m. (high ma n = i \ both_member_options (treeList ! i) (low ma n)) \ (\ y. (high y n = i \ both_member_options (treeList ! i) (low y n) ) \ mi < y \ y \ ma)))" and 8: "n = m" and 9: "deg div 2 = n" using "4" add_self_div_2 by blast+ then show ?case proof(cases "x = mi \ x = ma") case True then show ?thesis using insert_simp_mima[of x mi ma deg treeList summary] invar_vebt.intros(4)[of treeList n summary m deg mi ma] by (smt "0" "1" "2" "3" "4" "4.hyps"(3) "4.hyps"(7) "4.hyps"(8) "5" "7" "9" deg_not_0 div_greater_zero_iff) next case False hence mimaxrel: "x \ mi \ x \ ma" by simp then show ?thesis proof(cases "mi < x") case True hence abcdef: "mi < x" by simp let ?h = "high x n" and ?l="low x n" have highlowprop: "high x n < 2^m \ low x n < 2^n" using "1" "3" "4.hyps"(3) "4.prems" deg_not_0 exp_split_high_low(1) exp_split_high_low(2) by blast have 10:"vebt_insert (Node (Some (mi,ma)) deg treeList summary) x = Node (Some (mi, max x ma)) deg (treeList[?h:=vebt_insert (treeList ! ?h) ?l]) (if minNull (treeList ! ?h) then vebt_insert summary ?h else summary) " using "2" "3" False True \high x n < 2 ^ m \ low x n < 2 ^ n\ insert_simp_norm by (metis "1" "4.hyps"(3) "9" deg_not_0 div_greater_zero_iff) let ?maxnew = "max x ma" and ?nextTreeList = "(take ?h treeList @ [vebt_insert (treeList ! ?h) ?l] @ drop (?h+1) treeList)" and ?nextSummary = "(if minNull (treeList ! ?h) then vebt_insert summary ?h else summary)" have 11: "( \ t \ set ?nextTreeList. invar_vebt t n)" proof fix t assume " t \ set ?nextTreeList" hence 111:"t \ set (take ?h treeList) \ t \ set ([vebt_insert (treeList ! ?h) ?l] @ drop (?h+1) treeList)" by auto show "invar_vebt t n" proof(cases "t \ set (take ?h treeList) ") case True then show ?thesis by (meson "0" in_set_takeD) next case False hence 1110: "t = vebt_insert (treeList ! ?h) ?l \ t \ set ( drop (?h+1) treeList)" using "111" by auto then show ?thesis proof(cases "t = vebt_insert (treeList ! ?h) ?l") case True have 11110: "invar_vebt (treeList ! ?h) n" by (simp add: "2" "4.IH"(1) highlowprop) have 11111: "?l < 2^n" by (simp add: low_def) then show ?thesis using myIHs[of "treeList ! ?h"] by (simp add: "11110" "2" True highlowprop) next case False then show ?thesis by (metis "0" "1110" append_assoc append_take_drop_id in_set_conv_decomp) qed qed qed have 12: "invar_vebt ?nextSummary n" proof(cases "minNull (treeList ! high x n)") case True then show ?thesis using "4.IH"(2) "8" highlowprop by auto next case False then show ?thesis by (simp add: "1" "8") qed have 13: "\ i < 2^m. (\ y. both_member_options (?nextTreeList ! i) y) \ ( both_member_options ?nextSummary i)" proof fix i show "i < 2 ^ m \ (\y. both_member_options ((?nextTreeList) ! i) y) = both_member_options (?nextSummary) i " proof assume "i< 2^m" show "(\y. both_member_options ((?nextTreeList) ! i) y) = both_member_options (?nextSummary) i " proof(cases "minNull (treeList ! high x n)") case True hence tc: "minNull (treeList ! high x n)" by simp hence nsprop: "?nextSummary = vebt_insert summary ?h" by simp have insprop:"?nextTreeList ! ?h = vebt_insert (treeList ! ?h) ?l" by (metis "2" Suc_eq_plus1 append_Cons highlowprop nth_list_update_eq self_append_conv2 upd_conv_take_nth_drop) then show ?thesis proof(cases "i = ?h") case True have 161:"\ y. vebt_member (treeList ! ?h) y" by (simp add: min_Null_member tc) hence 162:"\ y. both_member_options (treeList ! ?h) y" by (metis "2" "4.IH"(1) highlowprop nth_mem valid_member_both_member_options) hence 163:"\ both_member_options summary i" using "11" "2" "4" True \i < 2 ^ m\ by blast have 164:"?nextTreeList ! i = vebt_insert (treeList ! ?h) ?l" using True insprop by simp have 165:"invar_vebt (vebt_insert (treeList ! ?h) ?l) n" by (simp add: "11") have 166:"both_member_options (vebt_insert (treeList ! ?h) ?l) ?l" using myIHs[of "treeList ! ?h" ?l] by (metis "0" "2" highlowprop nth_mem valid_insert_both_member_options_add) have 167:"\ y. both_member_options ((?nextTreeList) ! i) y " using "164" "166" by auto then show ?thesis using "1" "11" "2" True nsprop valid_insert_both_member_options_add highlowprop by auto next case False have "?nextTreeList ! i = treeList ! i" by (metis "2" False \i < 2 ^ m\ highlowprop nth_repl) have fstprop:"both_member_options ((?nextTreeList) ! i) y \ both_member_options (?nextSummary) i " for y using "1" "4" \(take (high x n) treeList @ [VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] @ drop (high x n + 1) treeList) ! i = treeList ! i\ \i < 2 ^ m\ highlowprop valid_insert_both_member_options_pres by auto moreover have" both_member_options (?nextSummary) i \ \ y . both_member_options ((?nextTreeList) ! i) y " proof- assume "both_member_options (?nextSummary) i " have "i \ high x n" by (simp add: False) hence "both_member_options summary i" by (smt (z3) "1" "12" \both_member_options (if minNull (treeList ! high x n) then VEBT_Insert.vebt_insert summary (high x n) else summary) i\ \i < 2 ^ m\ both_member_options_equiv_member highlowprop post_member_pre_member) hence "\ y. both_member_options (treeList ! i) y" by (simp add: "4" \i < 2 ^ m\) then show ?thesis using \(take (high x n) treeList @ [VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] @ drop (high x n + 1) treeList) ! i = treeList ! i\ by presburger qed ultimately show ?thesis by auto qed next case False hence "?nextSummary = summary" by simp hence "\ y. both_member_options (treeList ! high x n) y" using not_min_Null_member False by blast hence "both_member_options summary (high x n)" using "4" highlowprop by blast hence " both_member_options (?nextTreeList ! high x n) ?l" by (metis "0" "2" Suc_eq_plus1 append_Cons append_Nil highlowprop nth_list_update_eq nth_mem upd_conv_take_nth_drop valid_insert_both_member_options_add) then show ?thesis by (smt (verit, best) "2" "4" False \both_member_options summary (high x n)\ \i < 2 ^ m\ highlowprop nth_repl) qed qed qed have 14: "(mi = max ma x \ (\ t \ set ?nextTreeList. \ y. both_member_options t y))" using True max_less_iff_conj by blast have 15: "mi \ max ma x \ max ma x < 2^deg" using "4.hyps"(8) "4.prems" abcdef by auto have 16: "(mi \ max ma x \ (\ i < 2^m. (high (max ma x) n = i \ both_member_options (?nextTreeList ! i) (low (max ma x) n)) \ (\ y. (high y n = i \ both_member_options (?nextTreeList ! i) (low y n) ) \ mi < y \ y \ max ma x)))" proof assume "mi \ max ma x" show "(\ i < 2^m. (high (max ma x) n = i \ both_member_options (?nextTreeList ! i) (low (max ma x) n)) \ (\ y. (high y n = i \ both_member_options (?nextTreeList ! i) (low y n) ) \ mi < y \ y \ max ma x))" proof fix i::nat show "i < 2 ^ m\ (high (max ma x) n = i \ both_member_options (?nextTreeList ! i) (low (max ma x) n)) \ (\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ mi < y \ y \ max ma x)" proof assume "i < 2^m" show " (high (max ma x) n = i \ both_member_options (?nextTreeList ! i) (low (max ma x) n)) \ (\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ mi < y \ y \ max ma x)" proof show "(high (max ma x) n = i \ both_member_options (?nextTreeList ! i) (low (max ma x) n))" proof assume "high (max ma x) n = i" show "both_member_options (?nextTreeList ! i) (low (max ma x) n)" proof(cases "high x n = high ma n") case True have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence "?nextTreeList ! i = vebt_insert (treeList ! i) (low x n)" using concat_inth[of "take (high x n) treeList" "vebt_insert (treeList ! i) (low x n)" "drop (high x n + 1) treeList"] "2" True \high (max ma x) n = i\ \i < 2 ^ m\ concat_inth length_take max_def by (metis Suc_eq_plus1 append_Cons append_Nil nth_list_update_eq upd_conv_take_nth_drop) hence "vebt_member (?nextTreeList ! i) (low x n)" using Un_iff \i < 2 ^ m\ \invar_vebt (treeList ! i) n\ both_member_options_equiv_member highlowprop list.set_intros(1) set_append valid_insert_both_member_options_add by (metis "11" True \high (max ma x) n = i\ max_def) then show ?thesis proof(cases "mi = ma") case True then show ?thesis by (metis \(take (high x n) treeList @ [VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] @ drop (high x n + 1) treeList) ! i = VEBT_Insert.vebt_insert (treeList ! i) (low x n)\ \mi \ max ma x\ \invar_vebt (treeList ! i) n\ highlowprop max_def valid_insert_both_member_options_add) next case False hence "vebt_member (treeList ! i) (low ma n)" - using "7" True \high (max ma x) n = i\ \i < 2 ^ m\ \invar_vebt (treeList ! i) n\ both_member_options_equiv_member by auto + by (metis "7" True \high (max ma x) n = i\ \invar_vebt (treeList ! i) n\ both_member_options_equiv_member highlowprop linorder_cases max.absorb3 max.absorb4 mimaxrel) hence "vebt_member (?nextTreeList ! i) (low ma n) \ (low ma n = low x n)" using post_member_pre_member[of " (treeList ! i)" n "low x n" "low ma n" ] by (metis "2" "4.IH"(1) \(take (high x n) treeList @ [VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] @ drop (high x n + 1) treeList) ! i = VEBT_Insert.vebt_insert (treeList ! i) (low x n)\ \i < 2 ^ m\ both_member_options_equiv_member highlowprop member_bound nth_mem valid_insert_both_member_options_pres) then show ?thesis by (metis "2" "4.IH"(1) True \(take (high x n) treeList @ [VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] @ drop (high x n + 1) treeList) ! i = VEBT_Insert.vebt_insert (treeList ! i) (low x n)\ \high (max ma x) n = i\ both_member_options_equiv_member highlowprop max_def nth_mem valid_insert_both_member_options_add) qed next case False then show ?thesis proof(cases "x < ma") case True then show ?thesis by (metis "2" "7" False \high (max ma x) n = i\ \i < 2 ^ m\ abcdef highlowprop less_trans max.strict_order_iff nth_repl) next case False hence "x > ma" using mimaxrel nat_neq_iff by blast then show ?thesis by (metis "2" "4.IH"(1) One_nat_def \high (max ma x) n = i\ add.right_neutral add_Suc_right append_Cons highlowprop max.commute max.strict_order_iff nth_list_update_eq nth_mem self_append_conv2 upd_conv_take_nth_drop valid_insert_both_member_options_add) qed qed qed show "(\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ mi < y \ y \ max ma x)" proof fix y show "high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ mi < y \ y \ max ma x" proof assume bb:"high y n = i \ both_member_options (?nextTreeList ! i) (low y n)" show " mi < y \ y \ max ma x" proof(cases "i = high x n") case True hence cc:" i = high x n" by simp have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence aa:"?nextTreeList ! i = vebt_insert (treeList ! i) (low x n)" using concat_inth[of "take (high x n) treeList" "vebt_insert (treeList ! i) (low x n)" "drop (high x n + 1) treeList"] by (metis "2" Suc_eq_plus1 append_Cons append_self_conv2 cc highlowprop nth_list_update_eq upd_conv_take_nth_drop) hence "invar_vebt (?nextTreeList ! i) n" by (simp add: "11" True) hence "vebt_member (treeList ! i) (low y n) \ (low y n) = (low x n)" by (metis \invar_vebt (treeList ! i) n\ aa bb highlowprop member_bound post_member_pre_member valid_member_both_member_options) then show ?thesis proof(cases "low y n = low x n") case True hence "high x n = high y n \ low y n = low x n" by (simp add: bb cc) hence "x = y" by (metis bit_split_inv) then show ?thesis using abcdef by auto next case False hence "vebt_member (treeList ! i) (low y n)" using \vebt_member (treeList ! i) (low y n) \ low y n = low x n\ by blast hence "mi \ ma " using 5 inthall by (metis "2" \i < 2 ^ m\ min_Null_member not_min_Null_member) then show ?thesis using "7" \i < 2 ^ m\ \vebt_member (treeList ! i) (low y n)\ \invar_vebt (treeList ! i) n\ bb both_member_options_equiv_member max.coboundedI1 by blast qed next case False have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence aa:"?nextTreeList ! i = (treeList ! i)" by (metis "2" False \i < 2 ^ m\ highlowprop nth_repl) hence "both_member_options (treeList !i) (low y n)" using bb by auto hence "mi \ ma " using 5 "2" \i < 2 ^ m\ by force then show ?thesis using 7 using \both_member_options (treeList ! i) (low y n)\ \i < 2 ^ m\ bb max.coboundedI1 by blast qed qed qed qed qed qed qed then show ?thesis using invar_vebt.intros(4)[of ?nextTreeList n ?nextSummary m deg mi "max ma x"] by (smt (z3) "10" "11" "12" "13" "15" "2" "3" "8" One_nat_def abcdef add.right_neutral add_Suc_right append_Cons highlowprop leD max.cobounded2 max.commute pos_n_replace self_append_conv2 upd_conv_take_nth_drop) next case False hence abcdef: "x < mi" using antisym_conv3 mimaxrel by blast let ?h = "high mi n" and ?l="low mi n" have highlowprop: "high mi n < 2^m \ low mi n < 2^n" using "1" "3" "4.hyps"(3) "4.hyps"(7) "4.hyps"(8) deg_not_0 exp_split_high_low(1) exp_split_high_low(2) le_less_trans by blast have 10:"vebt_insert (Node (Some (mi,ma)) deg treeList summary) x = Node (Some (x, max mi ma)) deg (treeList[?h:=vebt_insert (treeList ! ?h) ?l]) (if minNull (treeList ! ?h) then vebt_insert summary ?h else summary) " by (metis "1" "2" "4.hyps"(3) "9" abcdef deg_not_0 div_greater_zero_iff highlowprop insert_simp_excp mimaxrel) let ?maxnew = "max mi ma" and ?nextTreeList = "(treeList[ ?h :=vebt_insert (treeList ! ?h) ?l])" and ?nextSummary = "(if minNull (treeList ! ?h) then vebt_insert summary ?h else summary)" have 11: "( \ t \ set ?nextTreeList. invar_vebt t n)" proof fix t assume " t \ set ?nextTreeList" then obtain i where "?nextTreeList ! i = t \ i < 2^m" by (metis "2" in_set_conv_nth length_list_update) show "invar_vebt t n" by (metis "2" "4.IH"(1) \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = t \ i < 2 ^ m\ highlowprop nth_list_update_eq nth_list_update_neq nth_mem) qed have 12: "invar_vebt ?nextSummary n" using "1" "4.IH"(2) "8" highlowprop by presburger have 13: "\ i < 2^m. (\ y. both_member_options (?nextTreeList ! i) y) \ ( both_member_options ?nextSummary i)" proof fix i show "i < 2 ^ m \ (\y. both_member_options ((?nextTreeList) ! i) y) = both_member_options (?nextSummary) i " proof assume "i< 2^m" show "(\y. both_member_options ((?nextTreeList) ! i) y) = both_member_options (?nextSummary) i " proof(cases "minNull (treeList ! high mi n)") case True hence tc: "minNull (treeList ! high mi n)" by simp hence nsprop: "?nextSummary = vebt_insert summary ?h" by simp have insprop:"?nextTreeList ! ?h = vebt_insert (treeList ! ?h) ?l" by (simp add: "2" highlowprop) then show ?thesis proof(cases "i = ?h") case True have 161:"\ y. vebt_member (treeList ! ?h) y" by (simp add: min_Null_member tc) hence 162:"\ y. both_member_options (treeList ! ?h) y" by (metis "2" "4.IH"(1) highlowprop nth_mem valid_member_both_member_options) hence 163:"\ both_member_options summary i" using "11" "2" "4" True \i < 2 ^ m\ by blast have 164:"?nextTreeList ! i = vebt_insert (treeList ! ?h) ?l" using True insprop by simp have 165:"invar_vebt (vebt_insert (treeList ! ?h) ?l) n" by (simp add: "2" "4.IH"(1) highlowprop) have 166:"both_member_options (vebt_insert (treeList ! ?h) ?l) ?l" using myIHs[of "treeList ! ?h" ?l] by (metis "0" "2" highlowprop in_set_member inthall valid_insert_both_member_options_add) have 167:"\ y. both_member_options ((?nextTreeList) ! i) y " using "164" "166" by auto then show ?thesis using "1" "11" "2" True nsprop valid_insert_both_member_options_add highlowprop by auto next case False have "?nextTreeList ! i = treeList ! i" using False by fastforce have fstprop:"both_member_options ((?nextTreeList) ! i) y \ both_member_options (?nextSummary) i " for y using "1" "4" \i < 2 ^ m\ \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = treeList ! i\ highlowprop valid_insert_both_member_options_pres by auto moreover have" both_member_options (?nextSummary) i \ \ y . both_member_options ((?nextTreeList) ! i) y " proof- assume "both_member_options (?nextSummary) i " have "i \ high mi n" by (simp add: False) hence "both_member_options summary i" by (smt (z3) "1" "12" \both_member_options (if minNull (treeList ! high mi n) then VEBT_Insert.vebt_insert summary (high mi n) else summary) i\ \i < 2 ^ m\ both_member_options_equiv_member highlowprop post_member_pre_member) hence "\ y. both_member_options (treeList ! i) y" by (simp add: "4" \i < 2 ^ m\) then show ?thesis by (simp add: \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = treeList ! i\) qed ultimately show ?thesis by auto qed next case False hence "?nextSummary = summary" by simp hence "\ y. both_member_options (treeList ! high mi n) y" using not_min_Null_member False by blast hence "both_member_options summary (high mi n)" using "4" highlowprop by blast hence " both_member_options (?nextTreeList ! high mi n) ?l" by (metis "0" "2" highlowprop nth_list_update_eq nth_mem valid_insert_both_member_options_add) then show ?thesis - by (metis (full_types, hide_lams) "4" False \both_member_options summary (high mi n)\ \i < 2 ^ m\ nth_list_update_neq) + by (metis (full_types, opaque_lifting) "4" False \both_member_options summary (high mi n)\ \i < 2 ^ m\ nth_list_update_neq) qed qed qed have 14: "(x = max ma mi \ (\ t \ set ?nextTreeList. \ y. both_member_options t y))" using mimaxrel by linarith have 15: "x \ max ma mi \ max ma mi < 2^deg" using "6" abcdef by linarith have 16: "(x \ max ma mi \ (\ i < 2^m. (high (max ma mi) n = i \ both_member_options (?nextTreeList ! i) (low (max ma mi) n)) \ (\ y. (high y n = i \ both_member_options (?nextTreeList ! i) (low y n) ) \ x < y \ y \ max ma mi)))" proof assume "x \ max ma mi" show "(\ i < 2^m. (high (max ma mi) n = i \ both_member_options (?nextTreeList ! i) (low (max ma mi) n)) \ (\ y. (high y n = i \ both_member_options (?nextTreeList ! i) (low y n) ) \ x < y \ y \ max ma mi))" proof fix i::nat show "i < 2 ^ m\ (high (max ma mi) n = i \ both_member_options (?nextTreeList ! i) (low (max ma mi) n)) \ (\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ x < y \ y \ max ma mi)" proof assume "i < 2^m" show " (high (max ma mi) n = i \ both_member_options (?nextTreeList ! i) (low (max ma mi) n)) \ (\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ x < y \ y \ max ma mi)" proof show "(high (max ma mi) n = i \ both_member_options (?nextTreeList ! i) (low (max ma mi) n))" proof assume "high (max ma mi) n = i" show "both_member_options (?nextTreeList ! i) (low (max ma mi) n)" proof(cases "high mi n = high ma n") case True have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence "?nextTreeList ! i = vebt_insert (treeList ! i) (low mi n)" using concat_inth[of "take (high x n) treeList" "vebt_insert (treeList ! i) (low x n)" "drop (high x n + 1) treeList"] by (metis "2" True \high (max ma mi) n = i\ highlowprop max_def nth_list_update_eq) hence "vebt_member (?nextTreeList ! i) (low mi n)" by (metis "11" "2" True \high (max ma mi) n = i\ \invar_vebt (treeList ! i) n\ highlowprop max_def set_update_memI valid_insert_both_member_options_add valid_member_both_member_options) then show ?thesis proof(cases "mi = ma") case True then show ?thesis using \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = VEBT_Insert.vebt_insert (treeList ! i) (low mi n)\ \invar_vebt (treeList ! i) n\ highlowprop valid_insert_both_member_options_add by force next case False hence "vebt_member (treeList ! i) (low ma n)" using "6" "7" \high (max ma mi) n = i\ \i < 2 ^ m\ \invar_vebt (treeList ! i) n\ both_member_options_equiv_member by auto hence "vebt_member (?nextTreeList ! i) (low ma n) \ (low ma n = low mi n)" using post_member_pre_member[of " (treeList ! i)" n "low mi n" "low ma n" ] by (metis "11" "2" "7" True \high (max ma mi) n = i\ \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = VEBT_Insert.vebt_insert (treeList ! i) (low mi n)\ \invar_vebt (treeList ! i) n\ highlowprop max_def member_bound set_update_memI valid_insert_both_member_options_pres valid_member_both_member_options) then show ?thesis by (metis "11" "2" "4.hyps"(7) "7" False True \high (max ma mi) n = i\ \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = VEBT_Insert.vebt_insert (treeList ! i) (low mi n)\ both_member_options_equiv_member highlowprop less_irrefl max.commute max_def set_update_memI) qed next case False hence "?nextTreeList ! i = treeList ! i" by (metis "4.hyps"(7) \high (max ma mi) n = i\ max.commute max_def nth_list_update_neq) then show ?thesis by (metis "4.hyps"(7) "7" False \high (max ma mi) n = i\ \i < 2 ^ m\ max.orderE) qed qed show "(\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ x < y \ y \ max ma mi)" proof fix y show "high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ x < y \ y \ max ma mi" proof assume bb:"high y n = i \ both_member_options (?nextTreeList ! i) (low y n)" show " x < y \ y \ max ma mi" proof(cases "i = high mi n") case True hence cc:" i = high mi n" by simp have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence aa:"?nextTreeList ! i = vebt_insert (treeList ! i) (low mi n)" using concat_inth[of "take (high x n) treeList" "vebt_insert (treeList ! i) (low x n)" "drop (high x n + 1) treeList"] by (simp add: cc highlowprop) hence "invar_vebt (?nextTreeList ! i) n" by (simp add: "2" "4.IH"(1) cc highlowprop) hence "vebt_member (treeList ! i) (low y n) \ (low y n) = (low mi n)" by (metis \invar_vebt (treeList ! i) n\ aa bb both_member_options_equiv_member highlowprop member_bound post_member_pre_member) then show ?thesis proof(cases "low y n = low mi n") case True hence "high mi n = high y n \ low y n = low mi n" by (simp add: bb cc) hence "mi = y" by (metis bit_split_inv) then show ?thesis using abcdef by auto next case False hence "vebt_member (treeList ! i) (low y n)" using \vebt_member (treeList ! i) (low y n) \ low y n = low mi n\ by blast hence "mi \ ma " using 5 inthall by (metis "2" \i < 2 ^ m\ min_Null_member not_min_Null_member) then show ?thesis using "7" by (metis \i < 2 ^ m\ \vebt_member (treeList ! i) (low y n)\ \invar_vebt (treeList ! i) n\ abcdef bb both_member_options_equiv_member max.absorb1 max.strict_order_iff max_less_iff_conj) qed next case False have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence aa:"?nextTreeList ! i = (treeList ! i)" using False by auto hence "both_member_options (treeList ! i) (low y n)" using bb by auto hence "mi \ ma " using 5 "2" \i < 2 ^ m\ by force then show ?thesis using 7 by (metis \both_member_options (treeList ! i) (low y n)\ \i < 2 ^ m\ abcdef bb max.absorb1 max.strict_order_iff max_less_iff_conj) qed qed qed qed qed qed qed then show ?thesis using invar_vebt.intros(4)[of ?nextTreeList n ?nextSummary m deg x "max ma mi"] by (smt (z3) "10" "11" "12" "13" "14" "15" "2" "3" "4.hyps"(3) "4.hyps"(7) length_list_update max.absorb1 max.absorb2) qed qed next case (5 treeList n summary m deg mi ma) hence myIHs: "x \ set treeList \ invar_vebt x n \ xa < 2 ^ n \ invar_vebt (vebt_insert x xa) n" for x xa by simp hence 0: "( \ t \ set treeList. invar_vebt t n)" and 1: " invar_vebt summary m" and 2:"length treeList = 2^m" and 3:" deg = n+m" and 4: "(\ i < 2^m. (\ y. both_member_options (treeList ! i) y) \ ( both_member_options summary i))" and 5: "(mi = ma \ (\ t \ set treeList. \ y. both_member_options t y))" and 6:"mi \ ma \ ma < 2^deg" and 7: "(mi \ ma \ (\ i < 2^m. (high ma n = i \ both_member_options (treeList ! i) (low ma n)) \ (\ y. (high y n = i \ both_member_options (treeList ! i) (low y n) ) \ mi < y \ y \ ma)))" and 8: "Suc n = m" and 9: "deg div 2 = n" using "5" add_self_div_2 apply blast+ by (simp add: "5.hyps"(3) "5.hyps"(4)) then show ?case proof(cases "x = mi \ x = ma") case True then show ?thesis using insert_simp_mima[of x mi ma deg treeList summary] invar_vebt.intros(5)[of treeList n summary m deg mi ma] by (smt "0" "1" "2" "3" "4" "5" "5.hyps"(3) "5.hyps"(7) "5.hyps"(8) "7" "9" div_less not_less not_one_le_zero set_n_deg_not_0) next case False hence mimaxrel: "x \ mi \ x \ ma" by simp then show ?thesis proof(cases "mi < x") case True hence abcdef: "mi < x" by simp let ?h = "high x n" and ?l="low x n" have highlowprop: "high x n < 2^m \ low x n < 2^n" by (metis "1" "2" "3" "5.IH"(1) "5.prems" Euclidean_Division.div_eq_0_iff add_nonneg_eq_0_iff deg_not_0 div_exp_eq exp_split_high_low(2) high_def not_one_le_zero one_add_one power_not_zero set_n_deg_not_0 zero_le_one zero_neq_one) have 10:"vebt_insert (Node (Some (mi,ma)) deg treeList summary) x = Node (Some (mi, max x ma)) deg (treeList[?h :=vebt_insert (treeList ! ?h) ?l]) (if minNull (treeList ! ?h) then vebt_insert summary ?h else summary) " using "2" "3" False True \high x n < 2 ^ m \ low x n < 2 ^ n\ insert_simp_norm by (smt "5.IH"(1) "9" div_greater_zero_iff div_if less_Suc_eq_0_disj not_one_le_zero set_n_deg_not_0) let ?maxnew = "max x ma" and ?nextTreeList = "(treeList[ ?h :=vebt_insert (treeList ! ?h) ?l])" and ?nextSummary = "(if minNull (treeList ! ?h) then vebt_insert summary ?h else summary)" have 11: "( \ t \ set ?nextTreeList. invar_vebt t n)" proof fix t assume " t \ set ?nextTreeList" then obtain i where "i <2^m \ ?nextTreeList ! i = t" by (metis "2" in_set_conv_nth length_list_update) show "invar_vebt t n" by (metis "2" "5.IH"(1) \i < 2 ^ m \ treeList[high x n := VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] ! i = t\ highlowprop nth_list_update_eq nth_list_update_neq nth_mem) qed have 12: "invar_vebt ?nextSummary m" by (simp add: "1" "5.IH"(2) highlowprop) have 13: "\ i < 2^m. (\ y. both_member_options (?nextTreeList ! i) y) \ ( both_member_options ?nextSummary i)" proof fix i show "i < 2 ^ m \ (\y. both_member_options ((?nextTreeList) ! i) y) = both_member_options (?nextSummary) i " proof assume "i< 2^m" show "(\y. both_member_options ((?nextTreeList) ! i) y) = both_member_options (?nextSummary) i " proof(cases "minNull (treeList ! high x n)") case True hence tc: "minNull (treeList ! high x n)" by simp hence nsprop: "?nextSummary = vebt_insert summary ?h" by simp have insprop:"?nextTreeList ! ?h = vebt_insert (treeList ! ?h) ?l" by (simp add: "2" highlowprop) then show ?thesis proof(cases "i = ?h") case True have 161:"\ y. vebt_member (treeList ! ?h) y" by (simp add: min_Null_member tc) hence 162:"\ y. both_member_options (treeList ! ?h) y" by (metis "0" "2" highlowprop nth_mem valid_member_both_member_options) hence 163:"\ both_member_options summary i" using "11" "2" "4" True \i < 2 ^ m\ by blast have 164:"?nextTreeList ! i = vebt_insert (treeList ! ?h) ?l" using True insprop by simp have 165:"invar_vebt (vebt_insert (treeList ! ?h) ?l) n" by (simp add: "11" "2" highlowprop set_update_memI) have 166:"both_member_options (vebt_insert (treeList ! ?h) ?l) ?l" using myIHs[of "treeList ! ?h" ?l] by (metis "0" "2" highlowprop in_set_member inthall valid_insert_both_member_options_add) have 167:"\ y. both_member_options ((?nextTreeList) ! i) y " using "164" "166" by auto then show ?thesis using "1" "11" "2" True nsprop valid_insert_both_member_options_add highlowprop by auto next case False have "?nextTreeList ! i = treeList ! i" using False by auto have fstprop:"both_member_options ((?nextTreeList) ! i) y \ both_member_options (?nextSummary) i " for y using "1" "4" \i < 2 ^ m\ \treeList[high x n := VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] ! i = treeList ! i\ highlowprop valid_insert_both_member_options_pres by auto moreover have" both_member_options (?nextSummary) i \ \ y . both_member_options ((?nextTreeList) ! i) y " proof- assume "both_member_options (?nextSummary) i " have "i \ high x n" by (simp add: False) hence "both_member_options summary i" by (smt "1" "12" \both_member_options (if minNull (treeList ! high x n) then vebt_insert summary (high x n) else summary) i\ \i < 2 ^ m\ both_member_options_equiv_member highlowprop post_member_pre_member) hence "\ y. both_member_options (treeList ! i) y" by (simp add: "4" \i < 2 ^ m\) then show ?thesis by (simp add: \treeList[high x n := VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] ! i = treeList ! i\) qed ultimately show ?thesis by auto qed next case False hence "?nextSummary = summary" by simp hence "\ y. both_member_options (treeList ! high x n) y" using not_min_Null_member False by blast hence "both_member_options summary (high x n)" using "4" highlowprop by blast hence " both_member_options (?nextTreeList ! high x n) ?l" by (metis "0" "2" highlowprop nth_list_update_eq nth_mem valid_insert_both_member_options_add) then show ?thesis by (metis (full_types) "4" False \both_member_options summary (high x n)\ \i < 2 ^ m\ nth_list_update_neq) qed qed qed have 14: "(mi = max ma x \ (\ t \ set ?nextTreeList. \ y. both_member_options t y))" using True max_less_iff_conj by blast have 15: "mi \ max ma x \ max ma x < 2^deg" using "5.hyps"(8) "5.prems" abcdef by auto have 16: "(mi \ max ma x \ (\ i < 2^m. (high (max ma x) n = i \ both_member_options (?nextTreeList ! i) (low (max ma x) n)) \ (\ y. (high y n = i \ both_member_options (?nextTreeList ! i) (low y n) ) \ mi < y \ y \ max ma x)))" proof assume "mi \ max ma x" show "(\ i < 2^m. (high (max ma x) n = i \ both_member_options (?nextTreeList ! i) (low (max ma x) n)) \ (\ y. (high y n = i \ both_member_options (?nextTreeList ! i) (low y n) ) \ mi < y \ y \ max ma x))" proof fix i::nat show "i < 2 ^ m\ (high (max ma x) n = i \ both_member_options (?nextTreeList ! i) (low (max ma x) n)) \ (\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ mi < y \ y \ max ma x)" proof assume "i < 2^m" show " (high (max ma x) n = i \ both_member_options (?nextTreeList ! i) (low (max ma x) n)) \ (\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ mi < y \ y \ max ma x)" proof show "(high (max ma x) n = i \ both_member_options (?nextTreeList ! i) (low (max ma x) n))" proof assume "high (max ma x) n = i" show "both_member_options (?nextTreeList ! i) (low (max ma x) n)" proof(cases "high x n = high ma n") case True have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence "?nextTreeList ! i = vebt_insert (treeList ! i) (low x n)" using concat_inth[of "take (high x n) treeList" "vebt_insert (treeList ! i) (low x n)" "drop (high x n + 1) treeList"] by (metis "2" False True \high (max ma x) n = i\ highlowprop linorder_neqE_nat max.commute max.strict_order_iff nth_list_update_eq) hence "vebt_member (?nextTreeList ! i) (low x n)" by (metis "11" "2" True \high (max ma x) n = i\ \invar_vebt (treeList ! i) n\ highlowprop max_def set_update_memI valid_insert_both_member_options_add valid_member_both_member_options) then show ?thesis proof(cases "mi = ma") case True then show ?thesis by (metis \treeList[high x n := VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] ! i = VEBT_Insert.vebt_insert (treeList ! i) (low x n)\ \invar_vebt (treeList ! i) n\ abcdef highlowprop max.commute max.strict_order_iff valid_insert_both_member_options_add) next case False hence "vebt_member (treeList ! i) (low ma n)" by (metis "7" True \high (max ma x) n = i\ \invar_vebt (treeList ! i) n\ highlowprop max_def valid_member_both_member_options) hence "vebt_member (?nextTreeList ! i) (low ma n) \ (low ma n = low x n)" using post_member_pre_member[of " (treeList ! i)" n "low x n" "low ma n" ] by (metis "1" "11" "2" "3" "5.hyps"(8) "7" False True \treeList[high x n := VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] ! i = VEBT_Insert.vebt_insert (treeList ! i) (low x n)\ \invar_vebt (treeList ! i) n\ deg_not_0 exp_split_high_low(2) highlowprop nth_list_update_neq set_update_memI valid_insert_both_member_options_pres valid_member_both_member_options) then show ?thesis by (metis "11" "2" True \high (max ma x) n = i\ \treeList[high x n := VEBT_Insert.vebt_insert (treeList ! high x n) (low x n)] ! i = VEBT_Insert.vebt_insert (treeList ! i) (low x n)\ \invar_vebt (treeList ! i) n\ both_member_options_equiv_member highlowprop max_def set_update_memI valid_insert_both_member_options_add) qed next case False then show ?thesis by (metis "0" "2" "7" \high (max ma x) n = i\ \i < 2 ^ m\ \mi \ max ma x\ highlowprop max_def nth_list_update_eq nth_list_update_neq nth_mem valid_insert_both_member_options_add) qed qed show "(\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ mi < y \ y \ max ma x)" proof fix y show "high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ mi < y \ y \ max ma x" proof assume bb:"high y n = i \ both_member_options (?nextTreeList ! i) (low y n)" show " mi < y \ y \ max ma x" proof(cases "i = high x n") case True hence cc:" i = high x n" by simp have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence aa:"?nextTreeList ! i = vebt_insert (treeList ! i) (low x n)" using concat_inth[of "take (high x n) treeList" "vebt_insert (treeList ! i) (low x n)" "drop (high x n + 1) treeList"] by (simp add: cc highlowprop) hence "invar_vebt (?nextTreeList ! i) n" by (simp add: "2" "5.IH"(1) cc highlowprop) hence "vebt_member (treeList ! i) (low y n) \ (low y n) = (low x n)" by (metis \high y n = i \ both_member_options ((treeList[?h:=vebt_insert (treeList ! high x n) (low x n)]) ! i) (low y n)\ \invar_vebt (treeList ! i) n\ aa highlowprop member_bound post_member_pre_member valid_member_both_member_options) then show ?thesis proof(cases "low y n = low x n") case True hence "high x n = high y n \ low y n = low x n" by (simp add: bb cc) hence "x = y" by (metis bit_split_inv) then show ?thesis using abcdef by auto next case False hence "vebt_member (treeList ! i) (low y n)" using \vebt_member (treeList ! i) (low y n) \ low y n = low x n\ by blast hence "mi \ ma " using 5 inthall by (metis "2" \i < 2 ^ m\ min_Null_member not_min_Null_member) then show ?thesis using "7" \i < 2 ^ m\ \vebt_member (treeList ! i) (low y n)\ \invar_vebt (treeList ! i) n\ bb both_member_options_equiv_member max.coboundedI1 by blast qed next case False have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence aa:"?nextTreeList ! i = (treeList ! i)" using False by auto hence "both_member_options (treeList ! i) (low y n)" using bb by auto hence "mi \ ma " using 5 using "2" \i < 2 ^ m\ by fastforce then show ?thesis using 7 using \both_member_options (treeList ! i) (low y n)\ \i < 2 ^ m\ bb max.coboundedI1 by blast qed qed qed qed qed qed qed then show ?thesis using invar_vebt.intros(5)[of ?nextTreeList n ?nextSummary m deg mi "max ma x"] by (smt (z3) "10" "11" "12" "13" "14" "15" "2" "3" "8" length_list_update max.commute) next case False hence abcdef: "x < mi" using antisym_conv3 mimaxrel by blast let ?h = "high mi n" and ?l="low mi n" have highlowprop: "high mi n < 2^m \ low mi n < 2^n" by (metis (full_types) "1" "2" "3" "5.IH"(1) "5.hyps"(7) "5.hyps"(8) deg_not_0 exp_split_high_low(1) exp_split_high_low(2) le_less_trans not_one_le_zero set_n_deg_not_0) have 10:"vebt_insert (Node (Some (mi,ma)) deg treeList summary) x = Node (Some (x, max mi ma)) deg (treeList[ ?h :=vebt_insert (treeList ! ?h) ?l]) (if minNull (treeList ! ?h) then vebt_insert summary ?h else summary) " by (metis "0" "2" "9" abcdef div_less highlowprop insert_simp_excp mimaxrel not_less not_one_le_zero set_n_deg_not_0) let ?maxnew = "max mi ma" and ?nextTreeList = "(treeList[ ?h:=vebt_insert (treeList ! ?h) ?l])" and ?nextSummary = "(if minNull (treeList ! ?h) then vebt_insert summary ?h else summary)" have 11: "( \ t \ set ?nextTreeList. invar_vebt t n)" proof fix t assume " t \ set ?nextTreeList" then obtain i where "i < 2^m \ ?nextTreeList ! i = t" by (metis "2" in_set_conv_nth length_list_update) thus "invar_vebt t n" by (metis "2" "5.IH"(1) highlowprop nth_list_update_eq nth_list_update_neq nth_mem) qed have 12: "invar_vebt ?nextSummary m" by (simp add: "1" "5.IH"(2) highlowprop) have 13: "\ i < 2^m. (\ y. both_member_options (?nextTreeList ! i) y) \ ( both_member_options ?nextSummary i)" proof fix i show "i < 2 ^ m \ (\y. both_member_options ((?nextTreeList) ! i) y) = both_member_options (?nextSummary) i " proof assume "i< 2^m" show "(\y. both_member_options ((?nextTreeList) ! i) y) = both_member_options (?nextSummary) i " proof(cases "minNull (treeList ! high mi n)") case True hence tc: "minNull (treeList ! high mi n)" by simp hence nsprop: "?nextSummary = vebt_insert summary ?h" by simp have insprop:"?nextTreeList ! ?h = vebt_insert (treeList ! ?h) ?l" by (simp add: "2" highlowprop) then show ?thesis proof(cases "i = ?h") case True have 161:"\ y. vebt_member (treeList ! ?h) y" by (simp add: min_Null_member tc) hence 162:"\ y. both_member_options (treeList ! ?h) y" by (metis "0" "2" highlowprop nth_mem valid_member_both_member_options) hence 163:"\ both_member_options summary i" using "11" "2" "4" True \i < 2 ^ m\ by blast have 164:"?nextTreeList ! i = vebt_insert (treeList ! ?h) ?l" using True insprop by simp have 165:"invar_vebt (vebt_insert (treeList ! ?h) ?l) n" by (simp add: "11" "2" highlowprop set_update_memI) have 166:"both_member_options (vebt_insert (treeList ! ?h) ?l) ?l" using myIHs[of "treeList ! ?h" ?l] by (metis "0" "2" highlowprop in_set_member inthall valid_insert_both_member_options_add) have 167:"\ y. both_member_options ((?nextTreeList) ! i) y " using "164" "166" by auto then show ?thesis using "1" "11" "2" True nsprop valid_insert_both_member_options_add highlowprop by auto next case False have "?nextTreeList ! i = treeList ! i" by (metis False nth_list_update_neq) have fstprop:"both_member_options ((?nextTreeList) ! i) y \ both_member_options (?nextSummary) i " for y using "1" "4" \i < 2 ^ m\ \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = treeList ! i\ highlowprop valid_insert_both_member_options_pres by auto moreover have" both_member_options (?nextSummary) i \ \ y . both_member_options ((?nextTreeList) ! i) y " proof- assume "both_member_options (?nextSummary) i " have "i \ high mi n" by (simp add: False) hence "both_member_options summary i" by (smt (z3) "1" "12" \both_member_options (if minNull (treeList ! high mi n) then VEBT_Insert.vebt_insert summary (high mi n) else summary) i\ \i < 2 ^ m\ both_member_options_equiv_member highlowprop post_member_pre_member) hence "\ y. both_member_options (treeList ! i) y" by (simp add: "4" \i < 2 ^ m\) then show ?thesis by (simp add: \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = treeList ! i\) qed ultimately show ?thesis by auto qed next case False hence "?nextSummary = summary" by simp hence "\ y. both_member_options (treeList ! high mi n) y" using not_min_Null_member False by blast hence "both_member_options summary (high mi n)" using "4" highlowprop by blast hence " both_member_options (?nextTreeList ! high mi n) ?l" by (metis "0" "2" highlowprop nth_list_update_eq nth_mem valid_insert_both_member_options_add) then show ?thesis by (metis (full_types) "4" False \both_member_options summary (high mi n)\ \i < 2 ^ m\ nth_list_update_neq) qed qed qed have 14: "(x = max ma mi \ (\ t \ set ?nextTreeList. \ y. both_member_options t y))" using mimaxrel by linarith have 15: "x \ max ma mi \ max ma mi < 2^deg" using "6" abcdef by linarith have 16: "(x \ max ma mi \ (\ i < 2^m. (high (max ma mi) n = i \ both_member_options (?nextTreeList ! i) (low (max ma mi) n)) \ (\ y. (high y n = i \ both_member_options (?nextTreeList ! i) (low y n) ) \ x < y \ y \ max ma mi)))" proof assume "x \ max ma mi" show "(\ i < 2^m. (high (max ma mi) n = i \ both_member_options (?nextTreeList ! i) (low (max ma mi) n)) \ (\ y. (high y n = i \ both_member_options (?nextTreeList ! i) (low y n) ) \ x < y \ y \ max ma mi))" proof fix i::nat show "i < 2 ^ m\ (high (max ma mi) n = i \ both_member_options (?nextTreeList ! i) (low (max ma mi) n)) \ (\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ x < y \ y \ max ma mi)" proof assume "i < 2^m" show " (high (max ma mi) n = i \ both_member_options (?nextTreeList ! i) (low (max ma mi) n)) \ (\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ x < y \ y \ max ma mi)" proof show "(high (max ma mi) n = i \ both_member_options (?nextTreeList ! i) (low (max ma mi) n))" proof assume "high (max ma mi) n = i" show "both_member_options (?nextTreeList ! i) (low (max ma mi) n)" proof(cases "high mi n = high ma n") case True have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence "?nextTreeList ! i = vebt_insert (treeList ! i) (low mi n)" using concat_inth[of "take (high x n) treeList" "vebt_insert (treeList ! i) (low x n)" "drop (high x n + 1) treeList"] by (metis "2" "5.hyps"(7) True \high (max ma mi) n = i\ highlowprop max.orderE nth_list_update_eq) hence "vebt_member (?nextTreeList ! i) (low mi n)" by (metis "11" "2" True \high (max ma mi) n = i\ \invar_vebt (treeList ! i) n\ highlowprop max_def set_update_memI valid_insert_both_member_options_add valid_member_both_member_options) then show ?thesis proof(cases "mi = ma") case True then show ?thesis using \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = VEBT_Insert.vebt_insert (treeList ! i) (low mi n)\ \invar_vebt (treeList ! i) n\ highlowprop valid_insert_both_member_options_add by auto next case False hence "vebt_member (treeList ! i) (low ma n)" using "6" "7" \high (max ma mi) n = i\ \i < 2 ^ m\ \invar_vebt (treeList ! i) n\ both_member_options_equiv_member by auto hence "vebt_member (?nextTreeList ! i) (low ma n) \ (low ma n = low mi n)" using post_member_pre_member[of " (treeList ! i)" n "low mi n" "low ma n" ] by (metis "1" "11" "2" "3" "5.hyps"(8) "7" True \high (max ma mi) n = i\ \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = VEBT_Insert.vebt_insert (treeList ! i) (low mi n)\ \invar_vebt (treeList ! i) n\ deg_not_0 exp_split_high_low(2) highlowprop max_def set_update_memI valid_insert_both_member_options_pres valid_member_both_member_options) then show ?thesis by (metis "5.hyps"(7) "7" False \high (max ma mi) n = i\ \i < 2 ^ m\ \vebt_member (treeList ! i) (low ma n)\ \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = VEBT_Insert.vebt_insert (treeList ! i) (low mi n)\ \invar_vebt (treeList ! i) n\ highlowprop max.absorb1 member_bound valid_insert_both_member_options_pres) qed next case False hence "?nextTreeList ! i = treeList ! i" by (metis "5.hyps"(7) \high (max ma mi) n = i\ max.commute max_def nth_list_update_neq) then show ?thesis proof(cases "mi < ma") case True then show ?thesis by (metis "5.hyps"(7) "7" False \high (max ma mi) n = i\ \i < 2 ^ m\ \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = treeList ! i\ max.commute max_def) next case False hence "mi \ ma " by simp hence "mi = ma" by (simp add: "6" eq_iff) hence "\both_member_options (treeList ! i) (low (max ma mi) n)" using 5 "2" \i < 2 ^ m\ by auto then show ?thesis by (metis "11" "2" \high (max ma mi) n = i\ \mi = ma\ \treeList[high mi n := VEBT_Insert.vebt_insert (treeList ! high mi n) (low mi n)] ! i = treeList ! i\ highlowprop max.idem nth_list_update_eq set_update_memI valid_insert_both_member_options_add) qed qed qed show "(\y. high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ x < y \ y \ max ma mi)" proof fix y show "high y n = i \ both_member_options (?nextTreeList ! i) (low y n) \ x < y \ y \ max ma mi" proof assume bb:"high y n = i \ both_member_options (?nextTreeList ! i) (low y n)" show " x < y \ y \ max ma mi" proof(cases "i = high mi n") case True hence cc:" i = high mi n" by simp have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence aa:"?nextTreeList ! i = vebt_insert (treeList ! i) (low mi n)" using concat_inth[of "take (high x n) treeList" "vebt_insert (treeList ! i) (low x n)" "drop (high x n + 1) treeList"] by (simp add: cc highlowprop) hence "invar_vebt (?nextTreeList ! i) n" by (simp add: "2" "5.IH"(1) \i < 2 ^ m\ highlowprop) hence "vebt_member (treeList ! i) (low y n) \ (low y n) = (low mi n)" by (metis \invar_vebt (treeList ! i) n\ aa bb both_member_options_equiv_member highlowprop member_bound post_member_pre_member) then show ?thesis proof(cases "low y n = low mi n") case True hence "high mi n = high y n \ low y n = low mi n" by (simp add: bb cc) hence "mi = y" by (metis bit_split_inv) then show ?thesis using abcdef by auto next case False hence "vebt_member (treeList ! i) (low y n)" using \vebt_member (treeList ! i) (low y n) \ low y n = low mi n\ by blast hence "mi \ ma " using 5 inthall by (metis "2" \i < 2 ^ m\ min_Null_member not_min_Null_member) then show ?thesis using "7" by (metis \i < 2 ^ m\ \vebt_member (treeList ! i) (low y n)\ \invar_vebt (treeList ! i) n\ abcdef bb both_member_options_equiv_member max.absorb1 max.strict_order_iff max_less_iff_conj) qed next case False have "invar_vebt (treeList ! i ) n" by (metis "0" "2" \i < 2 ^ m\ in_set_member inthall) have "length ?nextTreeList = 2^m" using "2" highlowprop by auto hence aa:"?nextTreeList ! i = (treeList ! i)" using False by auto hence "both_member_options (treeList ! i) (low y n)" using bb by auto hence "mi \ ma " using 5 "2" \i < 2 ^ m\ by fastforce then show ?thesis using 7 by (metis \both_member_options (treeList ! i) (low y n)\ \i < 2 ^ m\ abcdef bb max.absorb1 max.strict_order_iff max_less_iff_conj) qed qed qed qed qed qed qed then show ?thesis using invar_vebt.intros(5)[of ?nextTreeList n ?nextSummary m deg x "max ma mi"] by (smt (z3) "10" "11" "12" "13" "14" "15" "2" "3" "5.hyps"(7) "8" length_list_update max.absorb2 max.orderE) qed qed qed subsection \Correctness with Respect to Set Interpretation\ theorem insert_corr: assumes "invar_vebt t n " and "x < 2^n " shows " set_vebt' t \ {x} = set_vebt' (vebt_insert t x) " proof show "set_vebt' t \ {x} \ set_vebt' (vebt_insert t x)" proof fix y assume "y \ set_vebt' t \ {x}" show "y \set_vebt' (vebt_insert t x)" proof(cases "x=y") case True then show ?thesis by (metis (full_types) assms(1) assms(2) both_member_options_equiv_member mem_Collect_eq set_vebt'_def valid_insert_both_member_options_add valid_pres_insert) next case False have "vebt_member t y" using False \y \ set_vebt' t \ {x}\ set_vebt'_def by auto hence "vebt_member (vebt_insert t x) y" by (meson assms(1) assms(2) both_member_options_equiv_member member_bound valid_insert_both_member_options_pres valid_pres_insert) then show ?thesis by (simp add: set_vebt'_def) qed qed show " set_vebt' (vebt_insert t x) \ set_vebt' t \ {x} " proof fix y assume "y \ set_vebt' (vebt_insert t x)" show "y \set_vebt' t \ {x}" proof(cases "x=y") case True then show ?thesis by simp next case False hence "vebt_member t y \ x=y" using post_member_pre_member using \y \ set_vebt' (vebt_insert t x)\ assms(1) assms(2) set_vebt'_def member_bound valid_pres_insert by fastforce hence "vebt_member t y" by (simp add: False) hence "y \ set_vebt' t" by (simp add: set_vebt'_def) then show ?thesis by simp qed qed qed corollary insert_correct: assumes "invar_vebt t n " and "x < 2^n " shows " set_vebt t \ {x} = set_vebt (vebt_insert t x) " using assms(1) assms(2) insert_corr set_vebt_set_vebt'_valid valid_pres_insert by blast fun insert'::"VEBT \ nat \ VEBT" where "insert' (Leaf a b) x = vebt_insert (Leaf a b) x"| "insert' (Node info deg treeList summary) x = (if x \ 2^deg then (Node info deg treeList summary ) else vebt_insert (Node info deg treeList summary) x)" theorem insert'_pres_valid: assumes "invar_vebt t n" shows "invar_vebt (insert' t x) n" using assms apply cases apply (metis One_nat_def deg1Leaf insert'.simps(1) vebt_insert.simps(1)) apply (metis assms insert'.simps(2) leI valid_pres_insert)+ done theorem insert'_correct: assumes "invar_vebt t n" shows "set_vebt (insert' t x) = (set_vebt t \ {x})\{0..2^n-1}" proof(cases t) case (Node x11 x12 x13 x14) then show ?thesis proof(cases "x < 2^n") case True hence "set_vebt (insert' t x) = set_vebt(vebt_insert t x)" by (metis Node assms deg_deg_n insert'.simps(2) leD) moreover hence "set_vebt(vebt_insert t x) = set_vebt t \ {x}" using True assms insert_correct by auto moreover hence "set_vebt t \ {x} = (set_vebt t \ {x})\{0..2^n-1} " by (metis Diff_Diff_Int True assms calculation(1) inf_le1 inrange le_inf_iff order_refl subset_antisym set_vebt'_def set_vebt_def set_vebt_set_vebt'_valid valid_pres_insert) ultimately show ?thesis by simp next case False hence "set_vebt (insert' t x) = set_vebt t" by (metis Node assms deg_deg_n insert'.simps(2) leI) moreover hence "set_vebt t = (set_vebt t \ {x})\{0..2^n-1} " by (smt (z3) False Int_commute Int_insert_right_if0 Un_Int_assoc_eq assms atLeastAtMost_iff boolean_algebra_cancel.sup0 inf_bot_right inrange le_add_diff_inverse le_imp_less_Suc one_le_numeral one_le_power plus_1_eq_Suc sup_commute set_vebt_set_vebt'_valid) ultimately show ?thesis by simp qed next case (Leaf x21 x22) then show ?thesis apply(auto simp add: insert'.simps vebt_insert.simps set_vebt_def both_member_options_def) using assms apply cases apply simp+ using assms apply cases apply simp+ using assms apply cases apply simp+ using assms apply cases apply simp+ done qed end end diff --git a/thys/Van_Emde_Boas_Trees/VEBT_List_Assn.thy b/thys/Van_Emde_Boas_Trees/VEBT_List_Assn.thy --- a/thys/Van_Emde_Boas_Trees/VEBT_List_Assn.thy +++ b/thys/Van_Emde_Boas_Trees/VEBT_List_Assn.thy @@ -1,327 +1,333 @@ (*by Lammich and Ammer*) theory VEBT_List_Assn imports "Separation_Logic_Imperative_HOL/Sep_Main" "HOL-Library.Rewrite" begin subsection "Lists" fun list_assn :: "('a \ 'c \ assn) \ 'a list \ 'c list \ assn" where "list_assn P [] [] = emp" | "list_assn P (a#as) (c#cs) = P a c * list_assn P as cs" | "list_assn _ _ _ = false" lemma list_assn_aux_simps[simp]: "list_assn P [] l' = (\(l'=[]))" "list_assn P l [] = (\(l=[]))" apply (cases l') apply simp apply simp apply (cases l) apply simp apply simp done lemma list_assn_aux_append[simp]: "length l1=length l1' \ list_assn P (l1@l2) (l1'@l2') = list_assn P l1 l1' * list_assn P l2 l2'" apply (induct rule: list_induct2) apply simp apply (simp add: star_assoc) done lemma list_assn_aux_ineq_len: "length l \ length li \ list_assn A l li = false" proof (induction l arbitrary: li) case (Cons x l li) thus ?case by (cases li; auto) qed simp lemma list_assn_aux_append2[simp]: assumes "length l2=length l2'" shows "list_assn P (l1@l2) (l1'@l2') = list_assn P l1 l1' * list_assn P l2 l2'" apply (cases "length l1 = length l1'") apply (erule list_assn_aux_append) apply (simp add: list_assn_aux_ineq_len assms) done lemma list_assn_simps[simp]: "(list_assn P) [] [] = emp" "(list_assn P) (a#as) (c#cs) = P a c * (list_assn P) as cs" "(list_assn P) (a#as) [] = false" "(list_assn P) [] (c#cs) = false" apply simp_all done lemma list_assn_mono: "\\x x'. P x x'\\<^sub>AP' x x'\ \ list_assn P l l' \\<^sub>A list_assn P' l l'" apply (induct P l l' rule: list_assn.induct) by (auto intro: ent_star_mono) lemma list_assn_cong[fundef_cong]: assumes "xs=xs'" "xsi=xsi'" assumes "\x xi. x\set xs' \ xi\set xsi' \ A x xi = A' x xi" shows "list_assn A xs xsi = list_assn A' xs' xsi'" using assms apply (induct A\A xs' xsi' arbitrary: xs xsi rule: list_assn.induct) apply simp_all done term prod_list definition "listI_assn I A xs xsi \ \(length xsi=length xs \ I\{0..i a. a * A (xs!i) (xsi!i)) 1 I" +lemmas comp_fun_commute_fold_insert = + comp_fun_commute_on.fold_insert[where S=UNIV, folded comp_fun_commute_def', simplified] + + lemma aux: "Finite_Set.fold (\i aa. aa * P ((a # as) ! i) ((c # cs) ! i)) emp {0..i aa. aa * P (as ! i) (cs ! i)) emp {0..i x. P (Suc i) x = Q i x" and "comp_fun_commute P" and "comp_fun_commute Q" for P Q n using that apply (induction n arbitrary: a) subgoal by simp - apply (simp add: comp_fun_commute.fold_insert) + thm comp_fun_commute_on.fold_insert + apply (simp add: comp_fun_commute_fold_insert) apply (subst 2) apply (subst 3) - apply (simp add: comp_fun_commute.fold_insert) + apply (simp add: comp_fun_commute_fold_insert) done show ?thesis apply (simp add: 1) - apply (subst comp_fun_commute.fold_insert_remove) + apply (subst comp_fun_commute_fold_insert) subgoal apply unfold_locales apply (auto simp: fun_eq_iff algebra_simps) done subgoal by simp + subgoal by simp apply simp apply (rewrite at "\ = _*_" mult.commute) apply (rule arg_cong[where f="\x. P _ _ * x"]) apply (rule A) subgoal by auto subgoal apply unfold_locales apply (auto simp: fun_eq_iff algebra_simps) done subgoal apply unfold_locales apply (auto simp: fun_eq_iff algebra_simps) done done qed lemma list_assn_conv_idx: "list_assn A xs xsi = listI_assn {0.. listI_assn {0.. listI_assn {0..finite I \ listI_assn I A xs xsi = false" using subset_eq_atLeast0_lessThan_finite by (auto simp: listI_assn_def) find_theorems Finite_Set.fold name: cong lemma mult_fun_commute: "comp_fun_commute (\i (a::assn). a * f i)" apply unfold_locales apply (auto simp: fun_eq_iff mult_ac) done lemma listI_assn_weak_cong: assumes I: "I=I'" "A=A'" "length xs=length xs'" "length xsi=length xsi'" assumes A: "\i. \i\I; i \ xs!i = xs'!i \ xsi!i = xsi'!i" shows "listI_assn I A xs xsi = listI_assn I' A' xs' xsi'" unfolding listI_assn_def apply (simp add: I) apply (cases "length xsi' = length xs' \ I' \ {0..i. \i\I; i \ xs!i = xs'!i \ xsi!i = xsi'!i \ A (xs!i) (xsi!i) = A' (xs'!i) (xsi'!i)" shows "listI_assn I A xs xsi = listI_assn I' A' xs' xsi'" unfolding listI_assn_def apply (simp add: I) apply (cases "length xsi' = length xs' \ I' \ {0..I \ i listI_assn (insert i I) A xs xsi = A (xs!i) (xsi!i) * listI_assn I A xs xsi" apply (cases "finite I"; simp?) unfolding listI_assn_def - apply (subst comp_fun_commute.fold_insert) + apply (subst comp_fun_commute_fold_insert) subgoal apply unfold_locales apply (auto simp: fun_eq_iff algebra_simps) done subgoal by simp subgoal by simp subgoal by (auto simp: algebra_simps) done lemma listI_assn_extract: assumes "i\I" "i\<^sub>A A (xs!i) (xsi!i) * listI_assn (I-{i}) A xs xsi * F" assumes "iI" assumes "listI_assn I A xs xsi * F \\<^sub>A Q" shows "P \\<^sub>A Q" proof - show ?thesis apply (rule ent_trans[OF assms(1)]) apply (subst listI_assn_extract[symmetric]) subgoal by fact subgoal by fact subgoal by fact done qed lemma listI_assn_reinsert_upd: fixes xs xsi :: "_ list" assumes "P \\<^sub>A A x xi * listI_assn (I-{i}) A xs xsi * F" assumes "iI" assumes "listI_assn I A (xs[i:=x]) (xsi[i:=xi]) * F \\<^sub>A Q" shows "P \\<^sub>A Q" proof (cases "length xs = length xsi") case True have 1: "listI_assn (I-{i}) A xs xsi = listI_assn (I-{i}) A (xs[i:=x]) (xsi[i:=xi])" by (rule listI_assn_cong) auto have 2: "A x xi = A ((xs[i:=x])!i) ((xsi[i:=xi])!i)" using \i True by auto from assms[unfolded 1 2] show ?thesis apply (rule_tac listI_assn_reinsert) apply assumption apply simp_all done next case False with assms(1) have "P \\<^sub>A false" by (simp add: listI_assn_def) thus ?thesis using ent_false_iff entailsI by blast qed lemma listI_assn_reinsert': assumes "P \\<^sub>A A (xs!i) (xsi!i) * listI_assn (I-{i}) A xs xsi * F" assumes "iI" assumes "c" shows "

c" proof - show ?thesis apply (rule cons_pre_rule[OF assms(1)]) apply (subst listI_assn_extract[symmetric]) subgoal by fact subgoal by fact subgoal by fact done qed lemma listI_assn_reinsert_upd': fixes xs xsi :: "_ list" assumes "P \\<^sub>A A x xi * listI_assn (I-{i}) A xs xsi * F" assumes "iI" assumes " c " shows "

c " by (meson assms(1) assms(2) assms(3) assms(4) cons_pre_rule ent_refl listI_assn_reinsert_upd) lemma subst_not_in: assumes "i\I " " iI "" i list_assn A xs xsi \ length xsi = length xs" by (metis list_assn_aux_ineq_len mod_false) method unwrap_idx for i ::nat = (rewrite in "<\>_<_>" list_assn_conv_idx), (rewrite in "<\>_<_>" listI_assn_extract[where i="i"]), (simp split: if_splits; fail), (simp split: if_splits; fail) method wrap_idx uses R = (rule R), frame_inference, (simp split: if_splits; fail), (simp split: if_splits; fail), (subst listI_assn_conv, (simp; fail)) method extract_pre_pure uses dest = (rule hoare_triple_preI | drule asm_rl[of "_\_"]), (determ \elim mod_starE dest[elim_format]\)?, ((determ \thin_tac "_ \ _"\)+)?, (simp (no_asm) only: triv_forall_equality)? lemma rule_at_index: assumes 1:"P \\<^sub>A list_assn A xs xsi * F" and 2[simp]:"i < length xs" and 3:" c " and 4: "\ r. Q' r \\<^sub>A A (xs ! i) (xsi ! i) * listI_assn ({0..c <\ r. list_assn A xs xsi * F' r> " apply(rule cons_pre_rule[OF 1]) apply(unwrap_idx i) apply(rule cons_post_rule) apply(rule 3) apply(rule ent_trans[OF 4]) apply(wrap_idx R: listI_assn_reinsert_upd) apply simp done end diff --git a/thys/Van_Emde_Boas_Trees/VEBT_Member.thy b/thys/Van_Emde_Boas_Trees/VEBT_Member.thy --- a/thys/Van_Emde_Boas_Trees/VEBT_Member.thy +++ b/thys/Van_Emde_Boas_Trees/VEBT_Member.thy @@ -1,525 +1,525 @@ (*by Ammer*) theory VEBT_Member imports VEBT_Definitions begin section \Member Function\ context begin interpretation VEBT_internal . fun vebt_member :: "VEBT \ nat \ bool" where "vebt_member (Leaf a b) x = (if x = 0 then a else if x = 1 then b else False)"| "vebt_member (Node None _ _ _) x = False"| "vebt_member (Node _ 0 _ _) x = False"| "vebt_member (Node _ (Suc 0) _ _) x = False"| "vebt_member (Node (Some (mi, ma)) deg treeList summary) x = ( if x = mi then True else if x = ma then True else if x < mi then False else if x > ma then False else ( let h = high x (deg div 2); l = low x (deg div 2) in( if h < length treeList then vebt_member (treeList ! h) l else False))) " end context VEBT_internal begin lemma member_inv: assumes "vebt_member (Node (Some (mi, ma)) deg treeList summary) x " shows "deg \ 2 \ (x = mi \ x = ma \ (x < ma \ x > mi \ high x (deg div 2) < length treeList \ vebt_member (treeList ! ( high x (deg div 2))) (low x (deg div 2))))" proof(cases deg) case 0 then show ?thesis using vebt_member.simps(3)[of "(mi, ma)" treeList summary x] using assms by blast next case (Suc nat) hence "deg = Suc nat" by simp then show ?thesis proof(cases nat) case 0 then show ?thesis using Suc assms by auto next case (Suc nata) hence "deg \ 2" by (simp add: \deg = Suc nat\) then show ?thesis by (metis vebt_member.simps(5) Suc \deg = Suc nat\ assms linorder_neqE_nat) qed qed definition bit_concat::"nat \ nat \ nat \ nat" where "bit_concat h l d = h*2^d + l" lemma bit_split_inv: "bit_concat (high x d) (low x d) d = x" unfolding bit_concat_def high_def low_def by presburger definition set_vebt'::"VEBT \ nat set" where "set_vebt' t = {x. vebt_member t x}" lemma Leaf_0_not: assumes "invar_vebt (Leaf a b) 0 "shows " False" proof- from assms show ?thesis proof(cases) qed qed lemma valid_0_not: "invar_vebt t 0 \ False" proof(induction t) case (Node info deg treeList summary) from this(3) have "length treeList > 0" apply cases apply auto done then obtain t where "t \ set treeList" by fastforce from Node(3) obtain n where "invar_vebt t n" apply cases using Node.IH(2) apply auto done from Node(3) have "n \ 0" apply cases using Node.IH(2) apply auto done hence "n = 0" by blast then show ?case using Node.IH(1) \t \ set treeList\ \invar_vebt t n\ by blast next case (Leaf x1 x2) then show ?case using Leaf_0_not by blast qed theorem valid_tree_deg_neq_0: "(\ invar_vebt t 0)" using valid_0_not by blast lemma deg_1_Leafy: "invar_vebt t n \ n = 1 \ \ a b. t = Leaf a b" apply(induction rule: invar_vebt.induct) apply simp apply presburger apply (metis (full_types) Suc_eq_plus1 add_cancel_right_left in_set_replicate list.map_cong0 map_replicate_const nat_neq_iff not_add_less2 numeral_1_eq_Suc_0 numeral_2_eq_2 numerals(1) order_less_irrefl power_eq_0_iff valid_tree_deg_neq_0 zero_less_numeral) apply (metis odd_add odd_one) by (metis Suc_eq_plus1 add_cancel_right_left in_set_replicate list.map_cong0 map_replicate_const nat_neq_iff not_add_less2 numeral_2_eq_2 power_eq_0_iff valid_tree_deg_neq_0) lemma deg_1_Leaf: "invar_vebt t 1 \ \ a b. t = Leaf a b" using deg_1_Leafy by blast corollary deg1Leaf: "invar_vebt t 1 \ (\ a b. t = Leaf a b)" using deg_1_Leaf invar_vebt.intros(1) by auto lemma deg_SUcn_Node: assumes "invar_vebt tree (Suc (Suc n)) " shows " \ info treeList s. tree = Node info (Suc (Suc n)) treeList s" proof- from assms show ?thesis apply(cases) apply blast+ done qed lemma "invar_vebt (Node info deg treeList summary) deg \ deg > 1" by (metis VEBT.simps(4) deg_1_Leafy less_one linorder_neqE_nat valid_tree_deg_neq_0) lemma deg_deg_n: assumes "invar_vebt (Node info deg treeList summary) n "shows" deg = n" proof- from assms show ?thesis proof(cases) qed blast+ qed lemma member_valid_both_member_options: "invar_vebt tree n \ vebt_member tree x \ (naive_member tree x \ membermima tree x)" proof(induction tree n arbitrary: x rule: invar_vebt.induct) case (1 a b) then show ?case using vebt_member.simps(1) naive_member.simps(1) by blast next case (2 treeList n summary m deg) then show ?case by simp next case (3 treeList n summary m deg) then show ?case using vebt_member.simps(2) by blast next case (4 treeList n summary m deg mi ma) hence "deg \ 2" by (metis Euclidean_Division.div_eq_0_iff add_self_div_2 le_less_linear valid_tree_deg_neq_0) then show ?case proof(cases "x = mi \ x = ma") case True then show ?thesis by (metis (full_types) "4"(12) vebt_member.simps(3) membermima.simps(4) old.nat.exhaust) next case False hence 1:"mi < x \ x < ma \ (high x (deg div 2 )) < length treeList \ vebt_member (treeList ! (high x (deg div 2))) (low x (deg div 2))" using member_inv[of mi ma deg treeList summary x] "4"(12) by blast hence " (treeList ! (high x (deg div 2))) \ set treeList" by (metis in_set_member inthall) hence "both_member_options (treeList ! (high x (deg div 2))) (low x (deg div 2))" using "1" "4.IH"(1) both_member_options_def by blast then show ?thesis by (smt "1" "4"(1) "4"(6) \treeList ! high x (deg div 2) \ set treeList\ membermima.simps(4) naive_member.simps(3) old.nat.exhaust valid_tree_deg_neq_0 zero_eq_add_iff_both_eq_0) qed next case (5 treeList n summary m deg mi ma) hence "deg \ 2" using member_inv by presburger then show ?case proof(cases "x = mi \ x = ma") case True then show ?thesis by (metis (full_types) "5"(12) vebt_member.simps(3) membermima.simps(4) old.nat.exhaust) next case False hence 1:"mi < x \ x < ma \ (high x (deg div 2 )) < length treeList \ vebt_member (treeList ! (high x (deg div 2))) (low x (deg div 2))" using member_inv[of mi ma deg treeList summary x] "5"(12) by blast hence " (treeList ! (high x (deg div 2))) \ set treeList" by (metis in_set_member inthall) hence "both_member_options (treeList ! (high x (deg div 2))) (low x (deg div 2))" using "1" "5.IH"(1) both_member_options_def by blast then show ?thesis by (smt "1" "5"(1) "5"(6) \treeList ! high x (deg div 2) \ set treeList\ membermima.simps(4) naive_member.simps(3) old.nat.exhaust valid_tree_deg_neq_0 zero_eq_add_iff_both_eq_0) qed qed lemma member_bound: "vebt_member tree x \ invar_vebt tree n \ x < 2^n" proof(induction tree x arbitrary: n rule: vebt_member.induct) case (1 a b x) then show ?case by (metis vebt_member.simps(1) One_nat_def le_neq_implies_less nat_power_eq_Suc_0_iff numeral_eq_iff numerals(1) one_le_numeral one_le_power semiring_norm(85) valid_tree_deg_neq_0 zero_less_numeral zero_less_power) next case (2 uu uv uw x) then show ?case by simp next case (3 v uy uz x) then show ?case by simp next case (4 v vb vc x) then show ?case by simp next case (5 mi ma va treeList summary x) hence 111: "n = Suc (Suc va)" using deg_deg_n by fastforce hence "ma < 2^n" using "5.prems"(2) mi_ma_2_deg by blast then show ?case by (metis "5.prems"(1) "5.prems"(2) le_less_trans less_imp_le_nat member_inv mi_ma_2_deg) qed theorem inrange: assumes "invar_vebt t n" shows " set_vebt' t \ {0..2^n-1}" proof fix x assume "x \ set_vebt' t" hence "vebt_member t x" using set_vebt'_def by auto hence "x < 2^n" using assms member_bound by blast then show "x \ {0..2^n-1}" by simp qed theorem buildup_gives_empty: "set_vebt' (vebt_buildup n) = {}" unfolding set_vebt'_def by (metis Collect_empty_eq vebt_member.simps(1) vebt_member.simps(2) vebt_buildup.elims) fun minNull::"VEBT \ bool" where "minNull (Leaf False False) = True"| "minNull (Leaf _ _ ) = False"| "minNull (Node None _ _ _) = True"| "minNull (Node (Some _) _ _ _) = False" lemma min_Null_member: "minNull t \ \ vebt_member t x" apply(induction t) using vebt_member.simps(2) minNull.elims(2) apply blast apply auto done lemma not_min_Null_member: "\ minNull t \ \ y. both_member_options t y" proof(induction t) case (Node info deg treeList summary) obtain mi ma where "info = Some(mi , ma)" by (metis Node.prems minNull.simps(4) not_None_eq surj_pair) then show ?case by (metis (full_types) both_member_options_def membermima.simps(3) membermima.simps(4) not0_implies_Suc) next case (Leaf x1 x2) then show ?case by (metis (full_types) both_member_options_def minNull.simps(1) naive_member.simps(1) zero_neq_one) qed lemma valid_member_both_member_options: "invar_vebt t n \ both_member_options t x \ vebt_member t x" proof(induction t n arbitrary: x rule: invar_vebt.induct) case (1 a b) then show ?case by (simp add: both_member_options_def) next case (2 treeList n summary m deg) hence 0: " ( \ t \ set treeList. invar_vebt t n) " and 1:" invar_vebt summary n" and 2:" length treeList = 2^n" and 3:" deg = 2*n" and 4:" (\ i. both_member_options summary i)" and 5:" (\ t \ set treeList. \ y. both_member_options t y) " and 6: "n> 0" apply blast+ apply (auto simp add: "2.hyps"(3) "2.hyps") using "2.hyps"(1) "2.hyps"(3) neq0_conv valid_tree_deg_neq_0 by blast have "both_member_options (Node None deg treeList summary) x \ False" proof- assume "both_member_options (Node None deg treeList summary) x" hence "naive_member (Node None deg treeList summary) x \ membermima (Node None deg treeList summary) x" unfolding both_member_options_def by simp then show False proof(cases "naive_member (Node None deg treeList summary) x") case True hence "high x n < length treeList \ naive_member (treeList ! (high x n)) (low x n)" by (metis "1" "2.hyps"(3) "2.hyps"(4) add_cancel_right_left add_self_div_2 naive_member.simps(3) old.nat.exhaust valid_tree_deg_neq_0) then show ?thesis by (metis "5" both_member_options_def in_set_member inthall) next case False hence "membermima (Node None deg treeList summary) x" using \naive_member (Node None deg treeList summary) x \ membermima (Node None deg treeList summary) x\ by blast moreover have "Suc (deg-1) =deg" by (simp add: "2.hyps"(4) "6") moreover hence "(let pos = high x (deg div 2) in if pos < length treeList then membermima (treeList ! pos) (low x (Suc (deg - 1) div 2)) else False)" using calculation(1) membermima.simps(5) by metis moreover hence " if high x (deg div 2) < length treeList then membermima (treeList ! ( high x (deg div 2))) (low x(deg div 2)) else False" using calculation(2) by metis ultimately have " high x (deg div 2) < length treeList \ membermima (treeList ! (high x n)) (low x n)" by (metis "2.hyps"(3) "2.hyps"(4) add_self_div_2) then show ?thesis using "2.IH" "5" both_member_options_def in_set_member inthall by (metis "2.hyps"(3) "2.hyps"(4) add_self_div_2) qed qed then show ?case by (simp add: "2.prems") next case (3 treeList n summary m deg) hence 0: " ( \ t \ set treeList. invar_vebt t n) " and 1:" invar_vebt summary m" and 2:" length treeList = 2^m" and 3:" deg = n+m" and 4:" (\ i. both_member_options summary i)" and 5:" (\ t \ set treeList. \ y. both_member_options t y) " and 6: "n> 0" and 7: "m> 0" and 8: "n+1 = m" apply blast+ apply (metis (full_types) "3.IH"(1) "3.hyps"(2) in_set_member inthall neq0_conv power_eq_0_iff valid_tree_deg_neq_0 zero_neq_numeral) apply (simp add: "3.hyps"(3)) by (simp add: "3.hyps"(3)) have "both_member_options (Node None deg treeList summary) x \ False" proof- assume "both_member_options (Node None deg treeList summary) x" hence "naive_member (Node None deg treeList summary) x \ membermima (Node None deg treeList summary) x" unfolding both_member_options_def by simp then show False proof(cases "naive_member (Node None deg treeList summary) x") case True hence "high x n < length treeList \ naive_member (treeList ! (high x n)) (low x n)" by (metis "3" "3.hyps"(3) add_Suc_right add_self_div_2 even_Suc_div_two naive_member.simps(3) odd_add) then show ?thesis by (metis "5" both_member_options_def in_set_member inthall) next case False hence "membermima (Node None deg treeList summary) x" using \naive_member (Node None deg treeList summary) x \ membermima (Node None deg treeList summary) x\ by blast moreover have "Suc (deg-1) =deg" by (simp add: "3" "3.hyps"(3)) moreover hence "(let pos = high x (deg div 2) in if pos < length treeList then membermima (treeList ! pos) (low x (Suc (deg - 1) div 2)) else False)" using calculation(1) membermima.simps(5) by metis moreover hence 11:" if high x (deg div 2) < length treeList then membermima (treeList ! ( high x (deg div 2))) (low x(deg div 2)) else False" using calculation(2) by metis ultimately have " high x (deg div 2) < length treeList \ membermima (treeList ! (high x n)) (low x n)" by (metis "3" "3.hyps"(3) add_Suc_right add_self_div_2 even_Suc_div_two odd_add) then show ?thesis using "3.IH" "5" both_member_options_def in_set_member inthall 11 by metis qed qed then show ?case using "3.prems" by blast next case (4 treeList n summary m deg mi ma) hence 0: "( \ t \ set treeList. invar_vebt t n)" and 1: " invar_vebt summary n" and 2:"length treeList = 2^n" and 3:" deg = n+m" and "n=m" and 4: "(\ i < 2^n. (\ y. both_member_options (treeList ! i) y) \ ( both_member_options summary i))" and 5: "(mi = ma \ (\ t \ set treeList. \ y. both_member_options t y))" and 6:"mi \ ma \ ma < 2^deg" and 7: "(mi \ ma \ (\ i < 2^m. (high ma n = i \ both_member_options (treeList ! i) (low ma n)) \ (\ y. (high y n = i \ both_member_options (treeList ! i) (low y n) ) \ mi < y \ y \ ma)))" using "4.prems" by auto hence "n>0" by (metis neq0_conv valid_tree_deg_neq_0) then show ?case proof(cases "x = mi \ x = ma") case True hence xmimastmt: "x = mi \ x=ma" by simp then show ?thesis using vebt_member.simps(5)[of mi ma "deg-2" treeList summary x] by (metis "3" "4.hyps"(3) \0 < n\ add_diff_inverse_nat add_numeral_left add_self_div_2 div_if nat_neq_iff numerals(1) plus_1_eq_Suc semiring_norm(2)) next case False hence xmimastmt: "x \ mi \ x\ma" by simp hence "mi = ma \ False" proof- assume "mi = ma" hence astmt: "(\ t \ set treeList. \ y. both_member_options t y)" using 5 by simp have bstmt: "both_member_options (Node (Some (mi, ma)) deg treeList summary) x" by (simp add: "4.prems") then show False proof(cases "naive_member (Node (Some (mi, ma)) deg treeList summary) x") case True hence "high x n < length treeList \ naive_member (treeList ! (high x n)) (low x n)" - by (metis (no_types, hide_lams) "3" "4.hyps"(1) "4.hyps"(3) add_self_div_2 naive_member.simps(3) old.nat.exhaust valid_0_not zero_eq_add_iff_both_eq_0) + by (metis (no_types, opaque_lifting) "3" "4.hyps"(1) "4.hyps"(3) add_self_div_2 naive_member.simps(3) old.nat.exhaust valid_0_not zero_eq_add_iff_both_eq_0) then show ?thesis by (metis "5" \mi = ma\ both_member_options_def in_set_member inthall) next case False hence "membermima (Node (Some (mi, ma)) deg treeList summary) x" using bstmt unfolding both_member_options_def by blast hence " x = mi \ x = ma \ (if high x n < length treeList then membermima (treeList ! (high x n)) (low x n) else False)" using membermima.simps(4)[of mi ma "deg-1" treeList summary x] by (metis "3" "4.hyps"(3) One_nat_def Suc_diff_Suc \0 < n\ add_gr_0 add_self_div_2 diff_zero) hence " high x n < length treeList \ membermima (treeList ! (high x n)) (low x n)" using xmimastmt by presburger then show ?thesis using both_member_options_def in_set_member inthall membermima.simps(4)[of mi ma n treeList summary x] astmt by metis qed qed hence "mi \ ma " by blast hence followstmt: "(\ i < 2^m. (high ma n = i \ both_member_options (treeList ! i) (low ma n)) \ (\ y. (high y n = i \ both_member_options (treeList ! i) (low y n) ) \ mi < y \ y \ ma))" using 7 by simp have 10:"high x n < length treeList \ (naive_member (treeList ! (high x n)) (low x n) \ membermima (treeList ! (high x n)) (low x n) )" by (smt "3" "4.hyps"(3) "4.prems" False One_nat_def Suc_leI \0 < n\ add_gr_0 add_self_div_2 both_member_options_def le_add_diff_inverse membermima.simps(4) naive_member.simps(3) plus_1_eq_Suc) hence 11:"both_member_options (treeList ! (high x n)) (low x n)" by (simp add: both_member_options_def) have 12:"high x n< 2^m" using "10" "4.hyps"(2) by auto hence "mi < x \ x < ma" proof- have "(\ y. (high y n = (high x n) \ both_member_options (treeList ! (high y n)) (low y n) ) \ mi < y \ y \ ma)" using "12" followstmt by auto then show ?thesis using "11" False order.not_eq_order_implies_strict by blast qed have "vebt_member (treeList ! (high x n)) (low x n)" by (metis"10" "11" "4.IH"(1) in_set_member inthall) then show ?thesis by (smt "10" "11" "12" "3" "4.hyps"(3) vebt_member.simps(5) One_nat_def Suc_leI \0 < n\ add_Suc_right add_self_div_2 followstmt le_add_diff_inverse le_imp_less_Suc not_less_eq not_less_iff_gr_or_eq plus_1_eq_Suc) qed next case (5 treeList n summary m deg mi ma) hence 0: "( \ t \ set treeList. invar_vebt t n)" and 1: " invar_vebt summary m" and 2:"length treeList = 2^m" and 3:" deg = n+m" and "Suc n=m" and 4: "(\ i < 2^m. (\ y. both_member_options (treeList ! i) y) \ ( both_member_options summary i))" and 5: "(mi = ma \ (\ t \ set treeList. \ y. both_member_options t y))" and 6:"mi \ ma \ ma < 2^deg" and 7: "(mi \ ma \ (\ i < 2^m. (high ma n = i \ both_member_options (treeList ! i) (low ma n)) \ (\ y. (high y n = i \ both_member_options (treeList ! i) (low y n) ) \ mi < y \ y \ ma)))" using "5.prems" by auto hence "n>0" by (metis "5.hyps"(3) in_set_member inthall neq0_conv power_Suc0_right valid_tree_deg_neq_0 zero_neq_numeral) then show ?case proof(cases "x = mi \ x = ma") case True hence xmimastmt: "x = mi \ x=ma" by simp then show ?thesis using vebt_member.simps(5)[of mi ma "deg-2" treeList summary x] using "3" "5.hyps"(3) \0 < n\ by auto next case False hence xmimastmt: "x \ mi \ x\ma" by simp hence "mi = ma \ False" proof- assume "mi = ma" hence astmt: "(\ t \ set treeList. \ y. both_member_options t y)" using 5 by simp have bstmt: "both_member_options (Node (Some (mi, ma)) deg treeList summary) x" by (simp add: "5.prems") then show False proof(cases "naive_member (Node (Some (mi, ma)) deg treeList summary) x") case True hence "high x n < length treeList \ naive_member (treeList ! (high x n)) (low x n)" by (metis "3" "5.hyps"(3) add_Suc_right add_self_div_2 even_Suc_div_two naive_member.simps(3) odd_add) then show ?thesis by (metis "5" \mi = ma\ both_member_options_def in_set_member inthall) next case False hence "membermima (Node (Some (mi, ma)) deg treeList summary) x" using bstmt unfolding both_member_options_def by blast hence " x = mi \ x = ma \ (if high x n < length treeList then membermima (treeList ! (high x n)) (low x n) else False)" using membermima.simps(4)[of mi ma "deg-1" treeList summary x] using "3" "5.hyps"(3) by auto hence " high x n < length treeList \ membermima (treeList ! (high x n)) (low x n)" using xmimastmt by presburger then show ?thesis using both_member_options_def in_set_member inthall membermima.simps(4)[of mi ma n treeList summary x] astmt by metis qed qed hence "mi \ ma " by blast hence followstmt: "(\ i < 2^m. (high ma n = i \ both_member_options (treeList ! i) (low ma n)) \ (\ y. (high y n = i \ both_member_options (treeList ! i) (low y n) ) \ mi < y \ y \ ma))" using 7 by simp have 10:"high x n < length treeList \ (naive_member (treeList ! (high x n)) (low x n) \ membermima (treeList ! (high x n)) (low x n) )" by (smt "3" "5.hyps"(3) "5.prems" False add_Suc_right add_self_div_2 both_member_options_def even_Suc_div_two membermima.simps(4) naive_member.simps(3) odd_add) hence 11:"both_member_options (treeList ! (high x n)) (low x n)" by (simp add: both_member_options_def) have 12:"high x n< 2^m" using "10" "5.hyps"(2) by auto hence "mi < x \ x < ma" proof- have "(\ y. (high y n = (high x n) \ both_member_options (treeList ! (high y n)) (low y n) ) \ mi < y \ y \ ma)" using "12" followstmt by auto then show ?thesis using "11" False order.not_eq_order_implies_strict by blast qed have "vebt_member (treeList ! (high x n)) (low x n)" by (metis "10" "11" "5.IH"(1) in_set_member inthall) then show ?thesis by (smt "10" "11" "12" "3" "5.hyps"(3) vebt_member.simps(5) Suc_pred \0 < n\ add_Suc_right add_self_div_2 even_Suc_div_two followstmt le_neq_implies_less not_less_iff_gr_or_eq odd_add) qed qed corollary both_member_options_equiv_member: assumes "invar_vebt t n" shows "both_member_options t x \ vebt_member t x" using assms both_member_options_def member_valid_both_member_options valid_member_both_member_options by blast lemma member_correct: "invar_vebt t n \ vebt_member t x \ x \ set_vebt t " using both_member_options_equiv_member set_vebt_def by auto corollary set_vebt_set_vebt'_valid: assumes "invar_vebt t n" shows "set_vebt t =set_vebt' t" unfolding set_vebt_def set_vebt'_def apply auto using assms valid_member_both_member_options apply auto[1] using assms both_member_options_equiv_member by auto lemma set_vebt_finite: "invar_vebt t n \ finite (set_vebt' t)" using finite_subset inrange by blast lemma mi_eq_ma_no_ch:assumes "invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg " and " mi = ma " shows "(\ t \ set treeList. \ x. both_member_options t x ) \ (\ x. both_member_options summary x)" proof- from assms(1) show ?thesis proof(cases) case (4 n m) have 0:"\t\set treeList. \ Ex (both_member_options t)" by (simp add: "4"(7) assms(2)) moreover have "both_member_options summary x \ False" for x proof- assume "both_member_options summary x " hence "vebt_member summary x" using "4"(2) valid_member_both_member_options by auto moreover hence "x < 2^m" using "4"(2) member_bound by auto ultimately have "\ y. both_member_options (treeList ! (high x n)) y" using "0" "4"(3) "4"(4) "4"(6) \both_member_options summary x\ inthall by (metis nth_mem) then show ?thesis by (metis "0" "4"(3) "4"(4) Euclidean_Division.div_eq_0_iff \x < 2 ^ m\ high_def nth_mem zero_less_numeral zero_less_power) qed then show ?thesis using calculation by blast next case (5 n m) have 0:"\t\set treeList. \ Ex (both_member_options t)" using "5"(7) assms(2) by blast moreover have "both_member_options summary x \ False" for x proof- assume "both_member_options summary x " hence "vebt_member summary x" using "5"(2) valid_member_both_member_options by auto moreover hence "x < 2^m" using "5"(2) member_bound by auto ultimately have "\ y. both_member_options (treeList ! (high x n)) y" using "0" "5"(3) "5"(4) "5"(6) \both_member_options summary x\ inthall by (metis nth_mem) then show ?thesis by (metis "0" "5"(3) "5"(6) \both_member_options summary x\ \x < 2 ^ m\ nth_mem) qed then show ?thesis using calculation by blast qed qed end end diff --git a/thys/Van_Emde_Boas_Trees/VEBT_MinMax.thy b/thys/Van_Emde_Boas_Trees/VEBT_MinMax.thy --- a/thys/Van_Emde_Boas_Trees/VEBT_MinMax.thy +++ b/thys/Van_Emde_Boas_Trees/VEBT_MinMax.thy @@ -1,326 +1,326 @@ (*by Ammer*) theory VEBT_MinMax imports VEBT_Member begin section \The Minimum and Maximum Operation\ fun vebt_mint :: "VEBT \ nat option" where "vebt_mint (Leaf a b) = (if a then Some 0 else if b then Some 1 else None)"| "vebt_mint (Node None _ _ _) = None"| "vebt_mint (Node (Some (mi,ma)) _ _ _ ) = Some mi" fun vebt_maxt :: "VEBT \ nat option" where "vebt_maxt (Leaf a b) = (if b then Some 1 else if a then Some 0 else None)"| "vebt_maxt (Node None _ _ _) = None"| "vebt_maxt (Node (Some (mi,ma)) _ _ _ ) = Some ma" context VEBT_internal begin fun option_shift::"('a\'a\'a) \'a option \'a option\ 'a option" where "option_shift _ None _ = None"| "option_shift _ _ None = None"| "option_shift f (Some a) (Some b) = Some (f a b)" definition power::"nat option \ nat option \ nat option" (infixl"^\<^sub>o" 81) where "power= option_shift (^)" definition add::"nat option \ nat option \ nat option" (infixl"+\<^sub>o" 79) where "add= option_shift (+)" definition mul::"nat option \ nat option \ nat option" (infixl"*\<^sub>o" 80) where "mul = option_shift (*)" fun option_comp_shift::"('a \ 'a \ bool) \ 'a option \ 'a option \ bool" where "option_comp_shift _ None _ = False"| "option_comp_shift _ _ None = False"| "option_comp_shift f (Some x) (Some y) = f x y" fun less::"nat option \ nat option \ bool" (infixl"<\<^sub>o" 80) where "less x y= option_comp_shift (<) x y" fun lesseq::"nat option \ nat option \ bool" (infixl"\\<^sub>o" 80) where "lesseq x y = option_comp_shift (\) x y" fun greater::"nat option \ nat option \ bool" (infixl">\<^sub>o" 80) where "greater x y = option_comp_shift (>) x y" lemma add_shift:"x+y = z \ Some x +\<^sub>o Some y = Some z" by (simp add: add_def) lemma mul_shift:"x*y = z \ Some x *\<^sub>o Some y = Some z" by (simp add: mul_def) lemma power_shift:"x^y = z \ Some x ^\<^sub>o Some y = Some z" by (simp add: power_def) lemma less_shift: "x < y \ Some x <\<^sub>o Some y" by simp lemma lesseq_shift: "x \ y \ Some x \\<^sub>o Some y" by simp lemma greater_shift: "x > y \ Some x >\<^sub>o Some y" by simp definition max_in_set :: "nat set \ nat \ bool" where "max_in_set xs x \ (x \ xs \ (\ y \ xs. y \ x))" lemma maxt_member: "invar_vebt t n \ vebt_maxt t = Some maxi \ vebt_member t maxi" proof(induction t n arbitrary: maxi rule: invar_vebt.induct) case (1 a b) then show ?case by (metis VEBT_Member.vebt_member.simps(1) vebt_maxt.simps(1) option.distinct(1) option.inject zero_neq_one) next case (2 treeList n summary m deg) then show ?case by simp next case (3 treeList n summary m deg) then show ?case by simp next case (4 treeList n summary m deg mi ma) hence "deg \ 2" by (metis One_nat_def Suc_le_eq add_mono deg_not_0 numeral_2_eq_2 plus_1_eq_Suc) then show ?case by (metis "4.prems" VEBT_Member.vebt_member.simps(5) Suc_diff_Suc Suc_pred lessI less_le_trans vebt_maxt.simps(3) numeral_2_eq_2 option.inject zero_less_Suc) next case (5 treeList n summary m deg mi ma) hence "deg \ 2" by (metis Suc_leI le_add2 less_add_same_cancel2 less_le_trans not_less_iff_gr_or_eq not_one_le_zero numeral_2_eq_2 plus_1_eq_Suc set_n_deg_not_0) then show ?case by (metis "5.prems" VEBT_Member.vebt_member.simps(5) add_2_eq_Suc le_add_diff_inverse vebt_maxt.simps(3) option.inject) qed lemma maxt_corr_help: "invar_vebt t n \ vebt_maxt t = Some maxi \ vebt_member t x \ maxi \ x " by (smt VEBT_Member.vebt_member.simps(1) le_less vebt_maxt.elims member_inv mi_ma_2_deg option.simps(1) option.simps(3) zero_le_one) lemma maxt_corr_help_empty: "invar_vebt t n \ vebt_maxt t = None \ set_vebt' t = {}" by (metis (full_types) VEBT_Member.vebt_member.simps(1) empty_Collect_eq vebt_maxt.elims minNull.simps(4) min_Null_member option.distinct(1) set_vebt'_def) theorem maxt_corr:assumes "invar_vebt t n" and "vebt_maxt t = Some x" shows "max_in_set (set_vebt' t) x" unfolding set_vebt'_def Max_def max_in_set_def using assms(1) assms(2) maxt_corr_help maxt_member by blast theorem maxt_sound:assumes "invar_vebt t n" and "max_in_set (set_vebt' t) x" shows "vebt_maxt t = Some x" - by (metis (no_types, hide_lams) assms(1) assms(2) empty_Collect_eq le_less max_in_set_def + by (metis (no_types, opaque_lifting) assms(1) assms(2) empty_Collect_eq le_less max_in_set_def maxt_corr_help maxt_corr_help_empty maxt_member mem_Collect_eq not_le option.exhaust set_vebt'_def) definition min_in_set :: "nat set \ nat \ bool" where "min_in_set xs x \ (x \ xs \ (\ y \ xs. y \ x))" lemma mint_member: "invar_vebt t n \ vebt_mint t = Some maxi \ vebt_member t maxi" proof(induction t n arbitrary: maxi rule: invar_vebt.induct) case (1 a b) then show ?case by (metis VEBT_Member.vebt_member.simps(1) vebt_mint.simps(1) option.distinct(1) option.inject zero_neq_one) next case (2 treeList n summary m deg) then show ?case by simp next case (3 treeList n summary m deg) then show ?case by simp next case (4 treeList n summary m deg mi ma) hence "deg \ 2" by (metis One_nat_def Suc_le_eq add_mono deg_not_0 numeral_2_eq_2 plus_1_eq_Suc) then show ?case by (metis "4.prems" VEBT_Member.vebt_member.simps(5) One_nat_def Suc_diff_Suc Suc_pred dual_order.strict_trans1 le_imp_less_Suc le_numeral_extra(4) vebt_mint.simps(3) numeral_2_eq_2 option.inject zero_le_one) next case (5 treeList n summary m deg mi ma) hence "deg \ 2" by (metis Suc_leI le_add2 less_add_same_cancel2 less_le_trans not_less_iff_gr_or_eq not_one_le_zero numeral_2_eq_2 plus_1_eq_Suc set_n_deg_not_0) then show ?case using "5.prems" VEBT_Member.vebt_member.simps(5) add_2_eq_Suc le_add_diff_inverse vebt_mint.simps(3) by (metis option.inject) qed lemma mint_corr_help: "invar_vebt t n \ vebt_mint t = Some mini \ vebt_member t x \ mini \ x " by (smt VEBT_Member.vebt_member.simps(1) eq_iff option.inject less_imp_le_nat member_inv mi_ma_2_deg vebt_mint.elims of_nat_0 of_nat_0_le_iff of_nat_le_iff option.simps(3)) lemma mint_corr_help_empty: "invar_vebt t n \ vebt_mint t = None \ set_vebt' t = {}" by (metis VEBT_internal.maxt_corr_help_empty option.distinct(1) vebt_maxt.simps(1) vebt_maxt.simps(2) vebt_mint.elims) theorem mint_corr:assumes "invar_vebt t n" and "vebt_mint t = Some x" shows "min_in_set (set_vebt' t) x" using assms(1) assms(2) min_in_set_def mint_corr_help mint_member set_vebt'_def by auto theorem mint_sound:assumes "invar_vebt t n" and "min_in_set (set_vebt' t) x" shows "vebt_mint t = Some x" by (metis assms(1) assms(2) empty_Collect_eq eq_iff mem_Collect_eq min_in_set_def mint_corr_help mint_corr_help_empty mint_member option.exhaust set_vebt'_def) lemma summaxma:assumes "invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg" and "mi \ ma" shows "the (vebt_maxt summary) = high ma (deg div 2)" proof- from assms(1) show ?thesis proof(cases) case (4 n m) have "both_member_options summary (high ma n)" using "4"(10) "4"(2) "4"(4) "4"(5) "4"(6) "4"(9) assms(2) deg_not_0 exp_split_high_low(1) by blast have "high ma n \ the (vebt_maxt summary)" using "4"(2) \both_member_options summary (high ma n)\ empty_Collect_eq option.inject maxt_corr_help maxt_corr_help_empty not_None_eq set_vebt'_def valid_member_both_member_options by (metis option.exhaust_sel) have "high ma n < the (vebt_maxt summary) \ False" proof- assume "high ma n < the (vebt_maxt summary)" obtain maxs where "Some maxs = vebt_maxt summary" by (metis "4"(2) \both_member_options summary (high ma n)\ empty_Collect_eq maxt_corr_help_empty not_None_eq set_vebt'_def valid_member_both_member_options) hence "\ x. both_member_options (treeList ! maxs) x" by (metis "4"(2) "4"(6) both_member_options_equiv_member maxt_member member_bound) then obtain x where "both_member_options (treeList ! maxs) x" by auto hence "vebt_member (treeList ! maxs) x" by (metis "4"(1) "4"(2) "4"(3) \Some maxs = vebt_maxt summary\ maxt_member member_bound nth_mem valid_member_both_member_options) have "maxs < 2^m" by (metis "4"(2) \Some maxs = vebt_maxt summary\ maxt_member member_bound) have "invar_vebt (treeList ! maxs) n" by (metis "4"(1) "4"(3) \maxs < 2 ^ m\ inthall member_def) hence "x < 2^n" using \vebt_member (treeList ! maxs) x\ member_bound by auto let ?X = "2^n*maxs + x" have "high ?X n = maxs" by (simp add: \x < 2 ^ n\ high_inv mult.commute) hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) (2^n*maxs + x)" by (metis "4"(3) "4"(4) "4"(5) One_nat_def Suc_leI \both_member_options (treeList ! maxs) x\ \maxs < 2 ^ m\ \x < 2 ^ n\ add_self_div_2 assms(1) both_member_options_from_chilf_to_complete_tree deg_not_0 low_inv mult.commute) hence "vebt_member (Node (Some (mi, ma)) deg treeList summary) ?X" using assms(1) both_member_options_equiv_member by auto have "high ?X n> high ma n" by (metis \Some maxs = vebt_maxt summary\ \high (2 ^ n * maxs + x) n = maxs\ \high ma n < the (vebt_maxt summary)\ option.exhaust_sel option.inject option.simps(3)) hence "?X > ma" by (metis div_le_mono high_def not_le) then show ?thesis by (metis "4"(8) \vebt_member (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)\ leD member_inv not_less_iff_gr_or_eq) qed then show ?thesis using "4"(4) "4"(5) \high ma n \ the (vebt_maxt summary)\ by fastforce next case (5 n m) have "both_member_options summary (high ma n)" by (metis "5"(10) "5"(5) "5"(6) "5"(9) Euclidean_Division.div_eq_0_iff assms(2) div_exp_eq high_def nat.simps(3) numerals(2) power_not_zero) have "high ma n \ the (vebt_maxt summary)" by (metis "5"(2) VEBT_Member.vebt_member.simps(2) \both_member_options summary (high ma n)\ vebt_maxt.elims maxt_corr_help minNull.simps(1) min_Null_member option.exhaust_sel option.simps(3) valid_member_both_member_options) have "high ma n < the (vebt_maxt summary) \ False" proof- assume "high ma n < the (vebt_maxt summary)" obtain maxs where "Some maxs = vebt_maxt summary" by (metis "5"(2) \both_member_options summary (high ma n)\ empty_Collect_eq maxt_corr_help_empty not_None_eq set_vebt'_def valid_member_both_member_options) hence "\ x. both_member_options (treeList ! maxs) x" by (metis "5"(2) "5"(6) both_member_options_equiv_member maxt_member member_bound) then obtain x where "both_member_options (treeList ! maxs) x" by auto hence "vebt_member (treeList ! maxs) x" by (metis "5"(1) "5"(2) "5"(3) \Some maxs = vebt_maxt summary\ both_member_options_equiv_member maxt_member member_bound nth_mem) have "maxs < 2^m" by (metis "5"(2) \Some maxs = vebt_maxt summary\ maxt_member member_bound) have "invar_vebt (treeList ! maxs) n" by (metis "5"(1) "5"(3) \maxs < 2 ^ m\ inthall member_def) hence "x < 2^n" using \vebt_member (treeList ! maxs) x\ member_bound by auto let ?X = "2^n*maxs + x" have "high ?X n = maxs" by (simp add: \x < 2 ^ n\ high_inv mult.commute) hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) (2^n*maxs + x)" by (smt (z3) "5"(3) "5"(4) "5"(5) \both_member_options (treeList ! maxs) x\ \maxs < 2 ^ m\ \x < 2 ^ n\ add_Suc_right add_self_div_2 both_member_options_from_chilf_to_complete_tree even_Suc_div_two le_add1 low_inv mult.commute odd_add plus_1_eq_Suc) hence "vebt_member (Node (Some (mi, ma)) deg treeList summary) ?X" using assms(1) both_member_options_equiv_member by auto have "high ?X n> high ma n" by (metis \Some maxs = vebt_maxt summary\ \high (2 ^ n * maxs + x) n = maxs\ \high ma n < the (vebt_maxt summary)\ option.sel) hence "?X > ma" by (metis div_le_mono high_def not_le) then show ?thesis by (metis "5"(8) \vebt_member (Node (Some (mi, ma)) deg treeList summary) (2 ^ n * maxs + x)\ leD member_inv not_less_iff_gr_or_eq) qed then show ?thesis using "5"(4) "5"(5) \high ma n \ the(vebt_maxt summary)\ by fastforce qed qed lemma maxbmo: "vebt_maxt t = Some x \ both_member_options t x" apply(induction t rule: vebt_maxt.induct) apply auto apply (metis both_member_options_def naive_member.simps(1) option.distinct(1) option.sel zero_neq_one) by (metis One_nat_def Suc_le_D both_member_options_def div_by_1 div_greater_zero_iff membermima.simps(3) membermima.simps(4) not_gr0) lemma misiz:"invar_vebt t n \ Some m = vebt_mint t \ m < 2^n" by (metis member_bound mint_member) lemma mintlistlength: assumes "invar_vebt (Node (Some (mi, ma)) deg treeList summary) n " " mi \ ma " shows " ma > mi \ (\ m. Some m = vebt_mint summary \ m < 2^(n - n div 2))" using assms(1) proof cases case (4 n m) hence "both_member_options (treeList ! high ma n) (low ma n)" by (metis assms(2) high_bound_aux) moreover hence "both_member_options summary (high ma n)" using "4"(10) "4"(6) "4"(7) high_bound_aux by blast moreover then obtain mini where "Some mini = vebt_mint summary" by (metis "4"(3) empty_Collect_eq mint_corr_help_empty option.exhaust_sel set_vebt'_def valid_member_both_member_options) moreover hence "mini < 2^m" by (metis "4"(3) mint_member member_bound) moreover have "m = (deg - deg div 2)" using 4(6) 4(5) by auto ultimately show ?thesis using 4(1) assms 4(9) by auto next case (5 n m) hence "both_member_options (treeList ! high ma n) (low ma n)" by (metis assms(2) high_bound_aux) moreover hence "both_member_options summary (high ma n)" using "5"(10) "5"(6) "5"(7) high_bound_aux by blast moreover then obtain mini where "Some mini = vebt_mint summary" by (metis "5"(3) empty_Collect_eq mint_corr_help_empty option.exhaust_sel set_vebt'_def valid_member_both_member_options) moreover hence "mini < 2^m" by (metis "5"(3) mint_member member_bound) moreover have "m = (deg - deg div 2)" using 5(6) 5(5) by auto ultimately show ?thesis using 5(1) assms 5(9) by auto qed lemma power_minus_is_div: "b \ a \ (2 :: nat) ^ (a - b) = 2 ^ a div 2 ^ b" apply (induct a arbitrary: b) apply simp apply (erule le_SucE) apply (clarsimp simp:Suc_diff_le le_iff_add power_add) apply simp done lemma nested_mint:assumes "invar_vebt (Node (Some (mi, ma)) deg treeList summary) n " "n = Suc (Suc va) "" \ ma < mi "" ma \ mi " shows " high (the (vebt_mint summary) * (2 * 2 ^ (va div 2)) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (Suc (va div 2)) < length treeList" proof- have setprop: "t \ set treeList \ invar_vebt t (n div 2 )" for t using assms(1) by (cases) simp+ have listlength: "length treeList = 2^(n - n div 2)" using assms(1) by (cases) simp+ have sumprop: "invar_vebt summary (n - n div 2)" using assms(1) by (cases) simp+ have mimaxprop: "mi \ ma \ ma \ 2^n" using assms(1) by cases simp+ hence xbound: "mi \ x \ x \ ma \ high x (n div 2) \ length treeList " for x using div_le_dividend div_le_mono high_def listlength power_minus_is_div by auto have contcong:"i < length treeList \ \ x. both_member_options (treeList ! i) x \ both_member_options summary i " for i using assms(1)by cases auto+ obtain m where " Some m = vebt_mint summary \ m < 2^(n - n div 2)" using assms(1) assms(4) mintlistlength by blast then obtain miny where "(vebt_mint (treeList ! the (vebt_mint summary))) =Some miny" by (metis both_member_options_equiv_member contcong empty_Collect_eq listlength mint_corr_help_empty mint_member nth_mem option.exhaust_sel option.sel setprop sumprop set_vebt'_def) hence "miny < 2^(n div 2)" by (metis \\thesis. (\m. Some m = vebt_mint summary \ m < 2 ^ (n - n div 2) \ thesis) \ thesis\ listlength misiz nth_mem option.sel setprop) then show ?thesis by (metis \\thesis. (\m. Some m = vebt_mint summary \ m < 2 ^ (n - n div 2) \ thesis) \ thesis\ \vebt_mint (treeList ! the (vebt_mint summary)) = Some miny\ assms(2) div2_Suc_Suc high_inv listlength option.sel power_Suc) qed lemma minminNull: "vebt_mint t = None \ minNull t" by (metis minNull.simps(1) minNull.simps(4) vebt_mint.elims option.distinct(1)) lemma minNullmin: "minNull t \ vebt_mint t = None" by (metis minNull.elims(2) vebt_mint.simps(1) vebt_mint.simps(2)) end end