--- 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.
--- 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 \<subseteq> 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. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n}
@@ -129,7 +129,7 @@
lemma lebesgueD: "A \<in> sets lebesgue \<Longrightarrow> (indicator A :: _ \<Rightarrow> real) integrable_on cube n"
unfolding sets_lebesgue by simp
-lemma emeasure_lebesgue:
+lemma emeasure_lebesgue:
assumes "A \<in> sets lebesgue"
shows "emeasure lebesgue A = (SUP n. ereal (integral (cube n) (indicator A)))"
(is "_ = ?\<mu> A")
@@ -231,6 +231,10 @@
finally show ?thesis .
qed
+lemma borel_measurable_lebesgueI:
+ "f \<in> borel_measurable borel \<Longrightarrow> f \<in> borel_measurable lebesgue"
+ unfolding measurable_def by simp
+
lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set"
assumes "negligible s" shows "s \<in> 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 \<in> 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 \<in> borel_measurable borel"
shows "integral\<^isup>P lebesgue f = integral\<^isup>P lborel f"
@@ -839,7 +850,7 @@
let ?E = "range (\<lambda>(a, b). {a..b} :: 'a set)"
show "?E \<subseteq> 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 \<subseteq> ?E" unfolding cube_def [abs_def] by auto
show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
{ fix x :: 'a have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
@@ -940,4 +951,122 @@
qed
qed simp
+lemma borel_cube[intro]: "cube n \<in> sets borel"
+ unfolding cube_def by auto
+
+lemma integrable_on_cmult_iff:
+ fixes c :: real assumes "c \<noteq> 0"
+ shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
+ using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
+ by auto
+
+lemma positive_integral_borel_has_integral:
+ fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
+ assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
+ assumes I: "(f has_integral I) UNIV"
+ shows "(\<integral>\<^isup>+x. f x \<partial>lborel) = I"
+proof -
+ from f_borel have "(\<lambda>x. ereal (f x)) \<in> borel_measurable borel" by auto
+ from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
+
+ have lebesgue_eq: "(\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue) = (\<integral>\<^isup>+ x. ereal (f x) \<partial>lborel)"
+ using f_borel by (intro lebesgue_positive_integral_eq_borel) auto
+ also have "\<dots> = (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 "\<dots> \<le> ereal I"
+ proof (rule SUP_least)
+ fix i :: nat
+
+ { fix z
+ from F(4)[of z] have "F i z \<le> 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) \<le> f z"
+ by (cases "F i z") simp_all }
+ note F_bound = this
+
+ { fix x :: ereal assume x: "x \<noteq> 0" "x \<in> range (F i)"
+ with F(3,5)[of i] have [simp]: "real x \<noteq> 0"
+ by (metis image_iff order_eq_iff real_of_ereal_le_0)
+ let ?s = "(\<lambda>n z. real x * indicator (F i -` {x} \<inter> cube n) z) :: nat \<Rightarrow> 'a \<Rightarrow> real"
+ have "(\<lambda>z::'a. real x * indicator (F i -` {x}) z) integrable_on UNIV"
+ proof (rule dominated_convergence(1))
+ fix n :: nat
+ have "(\<lambda>z. indicator (F i -` {x} \<inter> 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 "\<forall>x\<in>UNIV. norm (?s n x) \<le> f x"
+ using nonneg F(5) by (auto split: split_indicator)
+ next
+ show "\<forall>z\<in>UNIV. (\<lambda>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 (\<lambda>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 "(\<lambda>n. ?s n z) ----> real x * indicator (F i -` {x}) z"
+ by (rule Lim_eventually)
+ qed
+ qed
+ then have "(indicator (F i -` {x}) :: 'a \<Rightarrow> real) integrable_on UNIV"
+ by (simp add: integrable_on_cmult_iff) }
+ note F_finite = lmeasure_finite[OF this]
+
+ have "((\<lambda>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) \<subseteq> {0..<\<infinity>}"
+ using F(3,5)[of i] by (auto simp: image_iff) metis
+ next
+ fix x assume "x \<in> range (F i)" "emeasure lebesgue (F i -` {x} \<inter> UNIV) = \<infinity>"
+ with F_finite[of x] show "x = 0" by auto
+ qed
+ from this I have "real (integral\<^isup>S lebesgue (F i)) \<le> I"
+ by (rule has_integral_le) (intro ballI F_bound)
+ moreover
+ { fix x assume x: "x \<in> range (F i)"
+ with F(3,5)[of i] have "x = 0 \<or> (0 < x \<and> x \<noteq> \<infinity>)"
+ by (auto simp: image_iff le_less) metis
+ with F_finite[OF _ x] x have "x * emeasure lebesgue (F i -` {x} \<inter> UNIV) \<noteq> \<infinity>"
+ by auto }
+ then have "integral\<^isup>S lebesgue (F i) \<noteq> \<infinity>"
+ unfolding simple_integral_def setsum_Pinfty space_lebesgue by blast
+ moreover have "0 \<le> 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) \<le> ereal I"
+ by (cases "integral\<^isup>S lborel (F i)") auto
+ qed
+ also have "\<dots> < \<infinity>" by simp
+ finally have finite: "(\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue) \<noteq> \<infinity>" by simp
+ have borel: "(\<lambda>x. ereal (f x)) \<in> 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 (\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue)) UNIV"
+ using nonneg by (simp add: subset_eq)
+ with I have "I = real (\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue)"
+ by (rule has_integral_unique)
+ with finite positive_integral_positive[of _ "\<lambda>x. ereal (f x)"] show ?thesis
+ by (cases "\<integral>\<^isup>+ x. ereal (f x) \<partial>lborel") (auto simp: lebesgue_eq)
+qed
+
+lemma has_integral_iff_positive_integral:
+ fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
+ assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x"
+ shows "(f has_integral I) UNIV \<longleftrightarrow> 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
--- 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 \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')"
by (auto intro!: sigma_sets_subseteq)
-lemma in_extended_measure[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
+lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
by auto
section {* Constructing simple @{typ "'a measure"} *}
@@ -1029,7 +1029,7 @@
lemma measurable_iff_measure_of:
assumes "N \<subseteq> Pow \<Omega>" "f \<in> space M \<rightarrow> \<Omega>"
shows "f \<in> measurable M (measure_of \<Omega> N \<mu>) \<longleftrightarrow> (\<forall>A\<in>N. f -` A \<inter> space M \<in> 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 "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
--- 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))]
--- 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" ^
--- 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) =>
--- 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