# HG changeset patch # User wenzelm # Date 1335362076 -7200 # Node ID af40c7e90c1e08bc2f22887fe493e251e46ba747 # Parent 5e6fe71e2390c0fef77be921b566e091da090bb7# Parent 8c37cb84065f0853e9f9e3c5a4a1ff7a7bef5dc5 merged diff -r 8c37cb84065f -r af40c7e90c1e NEWS --- a/NEWS Wed Apr 25 15:44:26 2012 +0200 +++ b/NEWS Wed Apr 25 15:54:36 2012 +0200 @@ -693,143 +693,143 @@ product_sigma_algebra Removed constants: + conditional_space distribution -> use distr measure, or distributed predicate + image_space joint_distribution -> use distr measure, or distributed predicate + pair_measure_generator product_prob_space.infprod_algebra -> use PiM subvimage - image_space - conditional_space - pair_measure_generator Replacement theorems: - sigma_algebra.measurable_sigma -> measurable_measure_of + finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite + finite_measure.empty_measure -> measure_empty + finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq + finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq + finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably + finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure + finite_measure.finite_measure -> finite_measure.emeasure_finite + finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton + finite_measure.positive_measure' -> measure_nonneg + finite_measure.real_measure -> finite_measure.emeasure_real + finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb + finite_product_sigma_algebra.in_P -> sets_PiM_I_finite + finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty + information_space.conditional_entropy_eq -> information_space.conditional_entropy_simple_distributed + information_space.conditional_entropy_positive -> information_space.conditional_entropy_nonneg_simple + information_space.conditional_mutual_information_eq_mutual_information -> information_space.conditional_mutual_information_eq_mutual_information_simple + information_space.conditional_mutual_information_generic_positive -> information_space.conditional_mutual_information_nonneg_simple + information_space.conditional_mutual_information_positive -> information_space.conditional_mutual_information_nonneg_simple + information_space.entropy_commute -> information_space.entropy_commute_simple + information_space.entropy_eq -> information_space.entropy_simple_distributed + information_space.entropy_generic_eq -> information_space.entropy_simple_distributed + information_space.entropy_positive -> information_space.entropy_nonneg_simple + information_space.entropy_uniform_max -> information_space.entropy_uniform + information_space.KL_eq_0_imp -> information_space.KL_eq_0_iff_eq + information_space.KL_eq_0 -> information_space.KL_same_eq_0 + information_space.KL_ge_0 -> information_space.KL_nonneg + information_space.mutual_information_eq -> information_space.mutual_information_simple_distributed + information_space.mutual_information_positive -> information_space.mutual_information_nonneg_simple + Int_stable_cuboids -> Int_stable_atLeastAtMost + Int_stable_product_algebra_generator -> positive_integral + measure_preserving -> equality "distr M N f = N" "f : measurable M N" measure_space.additive -> emeasure_additive - measure_space.measure_additive -> plus_emeasure - measure_space.measure_mono -> emeasure_mono - measure_space.measure_top -> emeasure_space - measure_space.measure_compl -> emeasure_compl - measure_space.measure_Diff -> emeasure_Diff - measure_space.measure_countable_increasing -> emeasure_countable_increasing + measure_space.AE_iff_null_set -> AE_iff_null + measure_space.almost_everywhere_def -> eventually_ae_filter + measure_space.almost_everywhere_vimage -> AE_distrD + measure_space.continuity_from_above -> INF_emeasure_decseq + measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq + measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq measure_space.continuity_from_below -> SUP_emeasure_incseq - measure_space.measure_incseq -> incseq_emeasure - measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq + measure_space_density -> emeasure_density + measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density + measure_space.integrable_vimage -> integrable_distr + measure_space.integral_translated_density -> integral_density + measure_space.integral_vimage -> integral_distr + measure_space.measure_additive -> plus_emeasure + measure_space.measure_compl -> emeasure_compl + measure_space.measure_countable_increasing -> emeasure_countable_increasing + measure_space.measure_countably_subadditive -> emeasure_subadditive_countably measure_space.measure_decseq -> decseq_emeasure - measure_space.continuity_from_above -> INF_emeasure_decseq - measure_space.measure_insert -> emeasure_insert - measure_space.measure_setsum -> setsum_emeasure - measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton - finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite - measure_space.measure_setsum_split -> setsum_emeasure_cover - measure_space.measure_subadditive -> subadditive - measure_space.measure_subadditive_finite -> emeasure_subadditive_finite + measure_space.measure_Diff -> emeasure_Diff + measure_space.measure_Diff_null_set -> emeasure_Diff_null_set measure_space.measure_eq_0 -> emeasure_eq_0 measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite - measure_space.measure_countably_subadditive -> emeasure_subadditive_countably - measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0 - measure_unique_Int_stable -> measure_eqI_generator_eq - measure_space.measure_Diff_null_set -> emeasure_Diff_null_set - measure_space.measure_Un_null_set -> emeasure_Un_null_set - measure_space.almost_everywhere_def -> eventually_ae_filter - measure_space.almost_everywhere_vimage -> AE_distrD + measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton + measure_space.measure_incseq -> incseq_emeasure + measure_space.measure_insert -> emeasure_insert + measure_space.measure_mono -> emeasure_mono + measure_space.measure_not_negative -> emeasure_not_MInf + measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq + measure_space.measure_setsum -> setsum_emeasure + measure_space.measure_setsum_split -> setsum_emeasure_cover measure_space.measure_space_vimage -> emeasure_distr - measure_space.AE_iff_null_set -> AE_iff_null - measure_space.real_measure_Union -> measure_Union - measure_space.real_measure_finite_Union -> measure_finite_Union - measure_space.real_measure_Diff -> measure_Diff - measure_space.real_measure_UNION -> measure_UNION - measure_space.real_measure_subadditive -> measure_subadditive - measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton - measure_space.real_continuity_from_below -> Lim_measure_incseq - measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq + measure_space.measure_subadditive_finite -> emeasure_subadditive_finite + measure_space.measure_subadditive -> subadditive + measure_space.measure_top -> emeasure_space + measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0 + measure_space.measure_Un_null_set -> emeasure_Un_null_set + measure_space.positive_integral_translated_density -> positive_integral_density + measure_space.positive_integral_vimage -> positive_integral_distr measure_space.real_continuity_from_above -> Lim_measure_decseq + measure_space.real_continuity_from_below -> Lim_measure_incseq measure_space.real_measure_countably_subadditive -> measure_subadditive_countably - finite_measure.finite_measure -> finite_measure.emeasure_finite - finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure - finite_measure.positive_measure' -> measure_nonneg - finite_measure.real_measure -> finite_measure.emeasure_real - finite_measure.empty_measure -> measure_empty - finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably - finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton - finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq - finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq - measure_space.simple_integral_vimage -> simple_integral_distr - measure_space.integrable_vimage -> integrable_distr - measure_space.positive_integral_translated_density -> positive_integral_density - measure_space.integral_translated_density -> integral_density - measure_space.integral_vimage -> integral_distr - measure_space_density -> emeasure_density - measure_space.positive_integral_vimage -> positive_integral_distr + measure_space.real_measure_Diff -> measure_Diff + measure_space.real_measure_finite_Union -> measure_finite_Union + measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton + measure_space.real_measure_subadditive -> measure_subadditive + measure_space.real_measure_Union -> measure_Union + measure_space.real_measure_UNION -> measure_UNION measure_space.simple_function_vimage -> simple_function_comp measure_space.simple_integral_vimage -> simple_integral_distr + measure_space.simple_integral_vimage -> simple_integral_distr + measure_unique_Int_stable -> measure_eqI_generator_eq + measure_unique_Int_stable_vimage -> measure_eqI_generator_eq pair_sigma_algebra.measurable_cut_fst -> sets_Pair1 pair_sigma_algebra.measurable_cut_snd -> sets_Pair2 pair_sigma_algebra.measurable_pair_image_fst -> measurable_Pair1 pair_sigma_algebra.measurable_pair_image_snd -> measurable_Pair2 pair_sigma_algebra.measurable_product_swap -> measurable_pair_swap_iff - pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1 - pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2 - measure_space.measure_not_negative -> emeasure_not_MInf - pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap - pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt - pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2 - pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times pair_sigma_algebra.pair_sigma_algebra_measurable -> measurable_pair_swap pair_sigma_algebra.pair_sigma_algebra_swap_measurable -> measurable_pair_swap' pair_sigma_algebra.sets_swap -> sets_pair_swap - finite_product_sigma_algebra.in_P -> sets_PiM_I_finite - Int_stable_product_algebra_generator -> positive_integral - product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge - product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton - product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge - finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty - product_algebra_generator_der -> prod_algebra_eq_finite - product_algebra_generator_into_space -> prod_algebra_sets_into_space - product_sigma_algebra.product_algebra_into_space -> space_closed - product_algebraE -> prod_algebraE_all - product_algebraI -> sets_PiM_I_finite - product_measure_exists -> product_sigma_finite.sigma_finite - sets_product_algebra -> sets_PiM - sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq - space_product_algebra -> space_PiM - Int_stable_cuboids -> Int_stable_atLeastAtMost - measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density - sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr - prob_space_unique_Int_stable -> measure_eqI_prob_space - sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint + pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1 + pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2 + pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap + pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2 + pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt + pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times + prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM + prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq prob_space.measure_space_1 -> prob_space.emeasure_space_1 prob_space.prob_space_vimage -> prob_space_distr prob_space.random_variable_restrict -> measurable_restrict - measure_preserving -> equality "distr M N f = N" "f : measurable M N" - measure_unique_Int_stable_vimage -> measure_eqI_generator_eq - measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq + prob_space_unique_Int_stable -> measure_eqI_prob_space + product_algebraE -> prod_algebraE_all + product_algebra_generator_der -> prod_algebra_eq_finite + product_algebra_generator_into_space -> prod_algebra_sets_into_space + product_algebraI -> sets_PiM_I_finite + product_measure_exists -> product_sigma_finite.sigma_finite product_prob_space.finite_index_eq_finite_product -> product_prob_space.sets_PiM_generator product_prob_space.finite_measure_infprod_emb_Pi -> product_prob_space.measure_PiM_emb - finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb product_prob_space.infprod_spec -> product_prob_space.emeasure_PiM_emb_not_empty product_prob_space.measurable_component -> measurable_component_singleton product_prob_space.measurable_emb -> measurable_prod_emb product_prob_space.measurable_into_infprod_algebra -> measurable_PiM_single product_prob_space.measurable_singleton_infprod -> measurable_component_singleton product_prob_space.measure_emb -> emeasure_prod_emb + product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict + product_sigma_algebra.product_algebra_into_space -> space_closed + product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge + product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton + product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge sequence_space.measure_infprod -> sequence_space.measure_PiM_countable - product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict - prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM - prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq - conditional_entropy_positive -> conditional_entropy_nonneg_simple - conditional_entropy_eq -> conditional_entropy_simple_distributed - conditional_mutual_information_eq_mutual_information -> conditional_mutual_information_eq_mutual_information_simple - conditional_mutual_information_generic_positive -> conditional_mutual_information_nonneg_simple - conditional_mutual_information_positive -> conditional_mutual_information_nonneg_simple - entropy_commute -> entropy_commute_simple - entropy_eq -> entropy_simple_distributed - entropy_generic_eq -> entropy_simple_distributed - entropy_positive -> entropy_nonneg_simple - entropy_uniform_max -> entropy_uniform - KL_eq_0 -> KL_same_eq_0 - KL_eq_0_imp -> KL_eq_0_iff_eq - KL_ge_0 -> KL_nonneg - mutual_information_eq -> mutual_information_simple_distributed - mutual_information_positive -> mutual_information_nonneg_simple + sets_product_algebra -> sets_PiM + sigma_algebra.measurable_sigma -> measurable_measure_of + sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint + sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr + sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq + space_product_algebra -> space_PiM * New "case_product" attribute to generate a case rule doing multiple case distinctions at the same time. E.g. diff -r 8c37cb84065f -r af40c7e90c1e src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Apr 25 15:44:26 2012 +0200 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Apr 25 15:54:36 2012 +0200 @@ -59,7 +59,7 @@ lemma cube_subset_Suc[intro]: "cube n \ cube (Suc n)" unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done -subsection {* Lebesgue measure *} +subsection {* Lebesgue measure *} definition lebesgue :: "'a::ordered_euclidean_space measure" where "lebesgue = measure_of UNIV {A. \n. (indicator A :: 'a \ real) integrable_on cube n} @@ -129,7 +129,7 @@ lemma lebesgueD: "A \ sets lebesgue \ (indicator A :: _ \ real) integrable_on cube n" unfolding sets_lebesgue by simp -lemma emeasure_lebesgue: +lemma emeasure_lebesgue: assumes "A \ sets lebesgue" shows "emeasure lebesgue A = (SUP n. ereal (integral (cube n) (indicator A)))" (is "_ = ?\ A") @@ -231,6 +231,10 @@ finally show ?thesis . qed +lemma borel_measurable_lebesgueI: + "f \ borel_measurable borel \ f \ borel_measurable lebesgue" + unfolding measurable_def by simp + lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set" assumes "negligible s" shows "s \ sets lebesgue" using assms by (force simp: cube_def integrable_on_def negligible_def intro!: lebesgueI) @@ -735,6 +739,13 @@ intro!: measurable_If) qed +lemma lebesgue_simple_integral_eq_borel: + assumes f: "f \ borel_measurable borel" + shows "integral\<^isup>S lebesgue f = integral\<^isup>S lborel f" + using f[THEN measurable_sets] + by (auto intro!: setsum_cong arg_cong2[where f="op *"] emeasure_lborel[symmetric] + simp: simple_integral_def) + lemma lebesgue_positive_integral_eq_borel: assumes f: "f \ borel_measurable borel" shows "integral\<^isup>P lebesgue f = integral\<^isup>P lborel f" @@ -839,7 +850,7 @@ let ?E = "range (\(a, b). {a..b} :: 'a set)" show "?E \ Pow UNIV" "sets lborel = sigma_sets UNIV ?E" "sets M = sigma_sets UNIV ?E" by (simp_all add: borel_eq_atLeastAtMost sets_eq) - + show "range cube \ ?E" unfolding cube_def [abs_def] by auto show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI) { fix x :: 'a have "\n. x \ cube n" using mem_big_cube[of x] by fastforce } @@ -940,4 +951,122 @@ qed qed simp +lemma borel_cube[intro]: "cube n \ sets borel" + unfolding cube_def by auto + +lemma integrable_on_cmult_iff: + fixes c :: real assumes "c \ 0" + shows "(\x. c * f x) integrable_on s \ f integrable_on s" + using integrable_cmul[of "\x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \ 0` + by auto + +lemma positive_integral_borel_has_integral: + fixes f :: "'a::ordered_euclidean_space \ real" + assumes f_borel: "f \ borel_measurable borel" and nonneg: "\x. 0 \ f x" + assumes I: "(f has_integral I) UNIV" + shows "(\\<^isup>+x. f x \lborel) = I" +proof - + from f_borel have "(\x. ereal (f x)) \ borel_measurable borel" by auto + from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this + + have lebesgue_eq: "(\\<^isup>+ x. ereal (f x) \lebesgue) = (\\<^isup>+ x. ereal (f x) \lborel)" + using f_borel by (intro lebesgue_positive_integral_eq_borel) auto + also have "\ = (SUP i. integral\<^isup>S lborel (F i))" + using F + by (subst positive_integral_monotone_convergence_simple) + (simp_all add: positive_integral_max_0 simple_function_def) + also have "\ \ ereal I" + proof (rule SUP_least) + fix i :: nat + + { fix z + from F(4)[of z] have "F i z \ ereal (f z)" + by (metis SUP_upper UNIV_I ereal_max_0 min_max.sup_absorb2 nonneg) + with F(5)[of i z] have "real (F i z) \ f z" + by (cases "F i z") simp_all } + note F_bound = this + + { fix x :: ereal assume x: "x \ 0" "x \ range (F i)" + with F(3,5)[of i] have [simp]: "real x \ 0" + by (metis image_iff order_eq_iff real_of_ereal_le_0) + let ?s = "(\n z. real x * indicator (F i -` {x} \ cube n) z) :: nat \ 'a \ real" + have "(\z::'a. real x * indicator (F i -` {x}) z) integrable_on UNIV" + proof (rule dominated_convergence(1)) + fix n :: nat + have "(\z. indicator (F i -` {x} \ cube n) z :: real) integrable_on cube n" + using x F(1)[of i] + by (intro lebesgueD) (auto simp: simple_function_def) + then have cube: "?s n integrable_on cube n" + by (simp add: integrable_on_cmult_iff) + show "?s n integrable_on UNIV" + by (rule integrable_on_superset[OF _ _ cube]) auto + next + show "f integrable_on UNIV" + unfolding integrable_on_def using I by auto + next + fix n from F_bound show "\x\UNIV. norm (?s n x) \ f x" + using nonneg F(5) by (auto split: split_indicator) + next + show "\z\UNIV. (\n. ?s n z) ----> real x * indicator (F i -` {x}) z" + proof + fix z :: 'a + from mem_big_cube[of z] guess j . + then have x: "eventually (\n. ?s n z = real x * indicator (F i -` {x}) z) sequentially" + by (auto intro!: eventually_sequentiallyI[where c=j] dest!: cube_subset split: split_indicator) + then show "(\n. ?s n z) ----> real x * indicator (F i -` {x}) z" + by (rule Lim_eventually) + qed + qed + then have "(indicator (F i -` {x}) :: 'a \ real) integrable_on UNIV" + by (simp add: integrable_on_cmult_iff) } + note F_finite = lmeasure_finite[OF this] + + have "((\x. real (F i x)) has_integral real (integral\<^isup>S lebesgue (F i))) UNIV" + proof (rule simple_function_has_integral[of "F i"]) + show "simple_function lebesgue (F i)" + using F(1) by (simp add: simple_function_def) + show "range (F i) \ {0..<\}" + using F(3,5)[of i] by (auto simp: image_iff) metis + next + fix x assume "x \ range (F i)" "emeasure lebesgue (F i -` {x} \ UNIV) = \" + with F_finite[of x] show "x = 0" by auto + qed + from this I have "real (integral\<^isup>S lebesgue (F i)) \ I" + by (rule has_integral_le) (intro ballI F_bound) + moreover + { fix x assume x: "x \ range (F i)" + with F(3,5)[of i] have "x = 0 \ (0 < x \ x \ \)" + by (auto simp: image_iff le_less) metis + with F_finite[OF _ x] x have "x * emeasure lebesgue (F i -` {x} \ UNIV) \ \" + by auto } + then have "integral\<^isup>S lebesgue (F i) \ \" + unfolding simple_integral_def setsum_Pinfty space_lebesgue by blast + moreover have "0 \ integral\<^isup>S lebesgue (F i)" + using F(1,5) by (intro simple_integral_positive) (auto simp: simple_function_def) + moreover have "integral\<^isup>S lebesgue (F i) = integral\<^isup>S lborel (F i)" + using F(1)[of i, THEN borel_measurable_simple_function] + by (rule lebesgue_simple_integral_eq_borel) + ultimately show "integral\<^isup>S lborel (F i) \ ereal I" + by (cases "integral\<^isup>S lborel (F i)") auto + qed + also have "\ < \" by simp + finally have finite: "(\\<^isup>+ x. ereal (f x) \lebesgue) \ \" by simp + have borel: "(\x. ereal (f x)) \ borel_measurable lebesgue" + using f_borel by (auto intro: borel_measurable_lebesgueI) + from positive_integral_has_integral[OF borel _ finite] + have "(f has_integral real (\\<^isup>+ x. ereal (f x) \lebesgue)) UNIV" + using nonneg by (simp add: subset_eq) + with I have "I = real (\\<^isup>+ x. ereal (f x) \lebesgue)" + by (rule has_integral_unique) + with finite positive_integral_positive[of _ "\x. ereal (f x)"] show ?thesis + by (cases "\\<^isup>+ x. ereal (f x) \lborel") (auto simp: lebesgue_eq) +qed + +lemma has_integral_iff_positive_integral: + fixes f :: "'a::ordered_euclidean_space \ real" + assumes f: "f \ borel_measurable borel" "\x. 0 \ f x" + shows "(f has_integral I) UNIV \ integral\<^isup>P lborel f = I" + using f positive_integral_borel_has_integral[of f I] positive_integral_has_integral[of f] + by (auto simp: subset_eq borel_measurable_lebesgueI lebesgue_positive_integral_eq_borel) + end diff -r 8c37cb84065f -r af40c7e90c1e src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Wed Apr 25 15:44:26 2012 +0200 +++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Apr 25 15:54:36 2012 +0200 @@ -877,7 +877,7 @@ "M \ Pow \ \ M' \ M \ sets (measure_of \ M' \) \ sets (measure_of \ M \')" by (auto intro!: sigma_sets_subseteq) -lemma in_extended_measure[intro, simp]: "M \ Pow \ \ A \ M \ A \ sets (measure_of \ M \)" +lemma in_measure_of[intro, simp]: "M \ Pow \ \ A \ M \ A \ sets (measure_of \ M \)" by auto section {* Constructing simple @{typ "'a measure"} *} @@ -1029,7 +1029,7 @@ lemma measurable_iff_measure_of: assumes "N \ Pow \" "f \ space M \ \" shows "f \ measurable M (measure_of \ N \) \ (\A\N. f -` A \ space M \ sets M)" - by (metis assms in_extended_measure measurable_measure_of assms measurable_sets) + by (metis assms in_measure_of measurable_measure_of assms measurable_sets) lemma measurable_cong: assumes "\ w. w \ space M \ f w = g w" diff -r 8c37cb84065f -r af40c7e90c1e src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Wed Apr 25 15:44:26 2012 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Wed Apr 25 15:54:36 2012 +0200 @@ -73,11 +73,13 @@ ("max_threads", "1"), ("batch_size", "10"), ("falsify", if null conjs then "false" else "true"), - (* ("debug", "true"), *) ("verbose", "true"), - (* ("overlord", "true"), *) +(* + ("debug", "true"), + ("overlord", "true"), +*) ("show_consts", "true"), - ("format", "1000"), + ("format", "1"), ("max_potential", "0"), ("timeout", string_of_int timeout), ("tac_timeout", string_of_int ((timeout + 49) div 50))] diff -r 8c37cb84065f -r af40c7e90c1e src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 25 15:44:26 2012 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 25 15:54:36 2012 +0200 @@ -667,6 +667,14 @@ ({free_names, sel_names, nonsel_names, rel_table, scope, ...} : problem_extension) = let + val _ = + print_t (fn () => + "% SZS status " ^ + (if genuine then + if falsify then "CounterSatisfiable" else "Satisfiable" + else + "Unknown") ^ "\n" ^ + "% SZS output start FiniteModel") val (reconstructed_model, codatatypes_ok) = reconstruct_hol_model {show_datatypes = show_datatypes, show_skolems = show_skolems, @@ -680,14 +688,7 @@ fun assms_prop () = Logic.mk_conjunction_list (neg_t :: def_assm_ts @ nondef_assm_ts) in - (print_t (fn () => - "% SZS status " ^ - (if genuine then - if falsify then "CounterSatisfiable" else "Satisfiable" - else - "Unknown") ^ "\n" ^ - "% SZS output start FiniteModel"); - pprint_a (Pretty.chunks + (pprint_a (Pretty.chunks [Pretty.blk (0, (pstrs ((if mode = Auto_Try then "Auto " else "") ^ "Nitpick found a" ^ diff -r 8c37cb84065f -r af40c7e90c1e src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Apr 25 15:44:26 2012 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Apr 25 15:54:36 2012 +0200 @@ -970,13 +970,8 @@ val u1' = aux table' false Neut u1 val u2' = aux table' false Neut u2 val R = - if is_opt_rep (rep_of u2') orelse - (pseudo_range_type T = bool_T andalso - not (is_Cst False (unrepify_nut_in_nut table false Neut - u1 u2))) then - opt_rep ofs T R - else - unopt_rep R + if is_opt_rep (rep_of u2') then opt_rep ofs T R + else unopt_rep R in s_op2 Lambda T R u1' u2' end | _ => raise NUT ("Nitpick_Nut.choose_reps_in_nut.aux", [u])) | Op2 (oper, T, _, u1, u2) => diff -r 8c37cb84065f -r af40c7e90c1e src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Apr 25 15:44:26 2012 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Apr 25 15:54:36 2012 +0200 @@ -564,21 +564,17 @@ else if is_positive_existential polar quant_s then let val j = length (!skolems) + 1 - val (js', (ss', Ts')) = - js ~~ (ss ~~ Ts) - |> filter (fn (j, _) => loose_bvar1 (t, j + 1)) - |> ListPair.unzip ||> ListPair.unzip in - if skolemizable andalso length js' <= skolem_depth then + if skolemizable andalso length js <= skolem_depth then let - val sko_s = skolem_prefix_for (length js') j ^ abs_s - val _ = Unsynchronized.change skolems (cons (sko_s, ss')) - val sko_t = list_comb (Const (sko_s, rev Ts' ---> abs_T), - map Bound (rev js')) + val sko_s = skolem_prefix_for (length js) j ^ abs_s + val _ = Unsynchronized.change skolems (cons (sko_s, ss)) + val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T), + map Bound (rev js)) val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) skolemizable polar t) in - if null js' then + if null js then s_betapply Ts (abs_t, sko_t) else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t