# HG changeset patch # User noschinl # Date 1429109304 -7200 # Node ID 2cd500d08c3080c626bb3bb6bc3c38333cda3e43 # Parent ef4fe30e9ef17d0764743bafaa2adc5cbd3292e6# Parent 019347f8dc88b532d5ed64d2b3d48f15576d3acd merged diff -r ef4fe30e9ef1 -r 2cd500d08c30 NEWS --- a/NEWS Wed Apr 15 15:10:01 2015 +0200 +++ b/NEWS Wed Apr 15 16:48:24 2015 +0200 @@ -77,6 +77,9 @@ * Old graph browser (Java/AWT 1.1) is superseded by improved graphview panel, which also produces PDF output without external tools. +* Improved scheduling for asynchronous print commands (e.g. provers +managed by the Sledgehammer panel) wrt. ongoing document processing. + *** Document preparation *** diff -r ef4fe30e9ef1 -r 2cd500d08c30 etc/options --- a/etc/options Wed Apr 15 15:10:01 2015 +0200 +++ b/etc/options Wed Apr 15 16:48:24 2015 +0200 @@ -101,6 +101,9 @@ public option ML_exception_trace : bool = false -- "ML exception trace for toplevel command execution" +public option ML_statistics : bool = true + -- "ML runtime system statistics" + section "Editor Reactivity" diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Complete_Partial_Order.thy --- a/src/HOL/Complete_Partial_Order.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Complete_Partial_Order.thy Wed Apr 15 16:48:24 2015 +0200 @@ -53,6 +53,20 @@ lemma chain_empty: "chain ord {}" by(simp add: chain_def) +lemma chain_equality: "chain op = A \ (\x\A. \y\A. x = y)" +by(auto simp add: chain_def) + +lemma chain_subset: + "\ chain ord A; B \ A \ + \ chain ord B" +by(rule chainI)(blast dest: chainD) + +lemma chain_imageI: + assumes chain: "chain le_a Y" + and mono: "\x y. \ x \ Y; y \ Y; le_a x y \ \ le_b (f x) (f y)" + shows "chain le_b (f ` Y)" +by(blast intro: chainI dest: chainD[OF chain] mono) + subsection {* Chain-complete partial orders *} text {* @@ -65,6 +79,12 @@ assumes ccpo_Sup_least: "\chain (op \) A; \x. x \ A \ x \ z\ \ Sup A \ z" begin +lemma chain_singleton: "Complete_Partial_Order.chain op \ {x}" +by(rule chainI) simp + +lemma ccpo_Sup_singleton [simp]: "\{x} = x" +by(rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton) + subsection {* Transfinite iteration of a function *} inductive_set iterates :: "('a \ 'a) \ 'a set" diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Extraction.thy Wed Apr 15 16:48:24 2015 +0200 @@ -31,7 +31,8 @@ induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq induct_atomize induct_atomize' induct_rulify induct_rulify' induct_rulify_fallback induct_trueI - True_implies_equals TrueE + True_implies_equals implies_True_equals TrueE + False_implies_equals lemmas [extraction_expand_def] = HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Library/Countable_Set.thy --- a/src/HOL/Library/Countable_Set.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Library/Countable_Set.thy Wed Apr 15 16:48:24 2015 +0200 @@ -247,6 +247,13 @@ shows "countable ((X ^^ i) `` Y)" using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X) +lemma countable_funpow: + fixes f :: "'a set \ 'a set" + assumes "\A. countable A \ countable (f A)" + and "countable A" + shows "countable ((f ^^ n) A)" +by(induction n)(simp_all add: assms) + lemma countable_rtrancl: "(\Y. countable Y \ countable (X `` Y)) \ countable Y \ countable (X^* `` Y)" unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow) @@ -276,6 +283,9 @@ "countable T \ countable {A. finite A \ A \ T}" unfolding Collect_finite_subset_eq_lists by auto +lemma countable_set_option [simp]: "countable (set_option x)" +by(cases x) auto + subsection {* Misc lemmas *} lemma countable_all: diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Library/Countable_Set_Type.thy --- a/src/HOL/Library/Countable_Set_Type.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Library/Countable_Set_Type.thy Wed Apr 15 16:48:24 2015 +0200 @@ -341,7 +341,30 @@ lemmas cin_mono = in_mono[Transfer.transferred] lemmas cLeast_mono = Least_mono[Transfer.transferred] lemmas cequalityI = equalityI[Transfer.transferred] - +lemmas cUnion_cimage_eq [simp] = Union_image_eq[Transfer.transferred] +lemmas cUN_iff [simp] = UN_iff[Transfer.transferred] +lemmas cUN_I [intro] = UN_I[Transfer.transferred] +lemmas cUN_E [elim!] = UN_E[Transfer.transferred] +lemmas cimage_eq_cUN = image_eq_UN[Transfer.transferred] +lemmas cUN_upper = UN_upper[Transfer.transferred] +lemmas cUN_least = UN_least[Transfer.transferred] +lemmas cUN_cinsert_distrib = UN_insert_distrib[Transfer.transferred] +lemmas cUN_empty [simp] = UN_empty[Transfer.transferred] +lemmas cUN_empty2 [simp] = UN_empty2[Transfer.transferred] +lemmas cUN_absorb = UN_absorb[Transfer.transferred] +lemmas cUN_cinsert [simp] = UN_insert[Transfer.transferred] +lemmas cUN_cUn [simp] = UN_Un[Transfer.transferred] +lemmas cUN_cUN_flatten = UN_UN_flatten[Transfer.transferred] +lemmas cUN_csubset_iff = UN_subset_iff[Transfer.transferred] +lemmas cUN_constant [simp] = UN_constant[Transfer.transferred] +lemmas cimage_cUnion = image_Union[Transfer.transferred] +lemmas cUNION_cempty_conv [simp] = UNION_empty_conv[Transfer.transferred] +lemmas cBall_cUN = ball_UN[Transfer.transferred] +lemmas cBex_cUN = bex_UN[Transfer.transferred] +lemmas cUn_eq_cUN = Un_eq_UN[Transfer.transferred] +lemmas cUN_mono = UN_mono[Transfer.transferred] +lemmas cimage_cUN = image_UN[Transfer.transferred] +lemmas cUN_csingleton [simp] = UN_singleton[Transfer.transferred] subsection {* Additional lemmas*} @@ -395,6 +418,11 @@ apply (rule equal_intr_rule) by (transfer, simp)+ +subsubsection {* @{const cUnion} *} + +lemma cUNION_cimage: "cUNION (cimage f A) g = cUNION A (g \ f)" +including cset.lifting by transfer auto + subsection {* Setup for Lifting/Transfer *} @@ -415,6 +443,14 @@ (\t. cin t b \ (\u. cin u a \ R u t))" by transfer(auto simp add: rel_set_def) +lemma rel_cset_cUNION: + "\ rel_cset Q A B; rel_fun Q (rel_cset R) f g \ + \ rel_cset R (cUNION A f) (cUNION B g)" +unfolding rel_fun_def by transfer(erule rel_set_UNION, simp add: rel_fun_def) + +lemma rel_cset_csingle_iff [simp]: "rel_cset R (csingle x) (csingle y) \ R x y" +by transfer(auto simp add: rel_set_def) + subsubsection {* Transfer rules for the Transfer package *} text {* Unconditional transfer rules *} diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Library/Extended_Real.thy Wed Apr 15 16:48:24 2015 +0200 @@ -298,6 +298,10 @@ end +lemma ereal_0_plus [simp]: "ereal 0 + x = x" + and plus_ereal_0 [simp]: "x + ereal 0 = x" +by(simp_all add: zero_ereal_def[symmetric]) + instance ereal :: numeral .. lemma real_of_ereal_0[simp]: "real (0::ereal) = 0" @@ -1286,6 +1290,9 @@ shows "real (a - b) = (if \a\ = \ \ \b\ = \ then 0 else real a - real b)" by (cases rule: ereal2_cases[of a b]) auto +lemma real_of_ereal_minus': "\x\ = \ \ \y\ = \ \ real x - real y = real (x - y :: ereal)" +by(subst real_of_ereal_minus) auto + lemma ereal_diff_positive: fixes a b :: ereal shows "a \ b \ 0 \ b - a" by (cases rule: ereal2_cases[of a b]) auto @@ -1428,6 +1435,14 @@ shows "0 < inverse x \ x \ \ \ 0 \ x" by (cases x) auto +lemma ereal_inverse_le_0_iff: + fixes x :: ereal + shows "inverse x \ 0 \ x < 0 \ x = \" + by(cases x) auto + +lemma ereal_divide_eq_0_iff: "x / y = 0 \ x = 0 \ \y :: ereal\ = \" +by(cases x y rule: ereal2_cases) simp_all + lemma ereal_mult_less_right: fixes a b c :: ereal assumes "b * a < c * a" @@ -1971,7 +1986,7 @@ assumes f: "\i. i \ I \ 0 \ f i" and c: "0 \ c" shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)" proof cases - assume "(SUP i:I. f i) = 0" + assume "(SUP i: I. f i) = 0" moreover then have "\i. i \ I \ f i = 0" by (metis SUP_upper f antisym) ultimately show ?thesis @@ -2646,6 +2661,38 @@ finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \ (SUP P:?F. INF x:Collect P. f x + g x)" . qed +lemma Sup_ereal_mult_right': + assumes nonempty: "Y \ {}" + and x: "x \ 0" + shows "(SUP i:Y. f i) * ereal x = (SUP i:Y. f i * ereal x)" (is "?lhs = ?rhs") +proof(cases "x = 0") + case True thus ?thesis by(auto simp add: nonempty zero_ereal_def[symmetric]) +next + case False + show ?thesis + proof(rule antisym) + show "?rhs \ ?lhs" + by(rule SUP_least)(simp add: ereal_mult_right_mono SUP_upper x) + next + have "?lhs / ereal x = (SUP i:Y. f i) * (ereal x / ereal x)" by(simp only: ereal_times_divide_eq) + also have "\ = (SUP i:Y. f i)" using False by simp + also have "\ \ ?rhs / x" + proof(rule SUP_least) + fix i + assume "i \ Y" + have "f i = f i * (ereal x / ereal x)" using False by simp + also have "\ = f i * x / x" by(simp only: ereal_times_divide_eq) + also from \i \ Y\ have "f i * x \ ?rhs" by(rule SUP_upper) + hence "f i * x / x \ ?rhs / x" using x False by simp + finally show "f i \ ?rhs / x" . + qed + finally have "(?lhs / x) * x \ (?rhs / x) * x" + by(rule ereal_mult_right_mono)(simp add: x) + also have "\ = ?rhs" using False ereal_divide_eq mult.commute by force + also have "(?lhs / x) * x = ?lhs" using False ereal_divide_eq mult.commute by force + finally show "?lhs \ ?rhs" . + qed +qed subsubsection {* Tests for code generator *} diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Library/document/root.tex --- a/src/HOL/Library/document/root.tex Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Library/document/root.tex Wed Apr 15 16:48:24 2015 +0200 @@ -2,7 +2,7 @@ \usepackage{ifthen} \usepackage[utf8]{inputenc} \usepackage[english]{babel} -\usepackage{isabelle,isabellesym,amssymb,stmaryrd,textcomp} +\usepackage{isabelle,isabellesym,amssymb,stmaryrd,textcomp,wasysym} \usepackage{pdfsetup} \urlstyle{rm} diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Lifting_Set.thy Wed Apr 15 16:48:24 2015 +0200 @@ -281,4 +281,9 @@ lemmas setsum_parametric = setsum.F_parametric lemmas setprod_parametric = setprod.F_parametric +lemma rel_set_UNION: + assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g" + shows "rel_set R (UNION A f) (UNION B g)" +by transfer_prover + end diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Map.thy --- a/src/HOL/Map.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Map.thy Wed Apr 15 16:48:24 2015 +0200 @@ -641,6 +641,8 @@ ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp qed +lemma ran_map_option: "ran (\x. map_option f (m x)) = f ` ran m" +by(auto simp add: ran_def) subsection {* @{text "map_le"} *} diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Partial_Function.thy --- a/src/HOL/Partial_Function.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Partial_Function.thy Wed Apr 15 16:48:24 2015 +0200 @@ -12,6 +12,40 @@ named_theorems partial_function_mono "monotonicity rules for partial function definitions" ML_file "Tools/Function/partial_function.ML" +lemma (in ccpo) in_chain_finite: + assumes "Complete_Partial_Order.chain op \ A" "finite A" "A \ {}" + shows "\A \ A" +using assms(2,1,3) +proof induction + case empty thus ?case by simp +next + case (insert x A) + note chain = `Complete_Partial_Order.chain op \ (insert x A)` + show ?case + proof(cases "A = {}") + case True thus ?thesis by simp + next + case False + from chain have chain': "Complete_Partial_Order.chain op \ A" + by(rule chain_subset) blast + hence "\A \ A" using False by(rule insert.IH) + show ?thesis + proof(cases "x \ \A") + case True + have "\insert x A \ \A" using chain + by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain']) + hence "\insert x A = \A" + by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain']) + with `\A \ A` show ?thesis by simp + next + case False + with chainD[OF chain, of x "\A"] `\A \ A` + have "\insert x A = x" + by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain]) + thus ?thesis by simp + qed + qed +qed subsection {* Axiomatic setup *} diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Wed Apr 15 16:48:24 2015 +0200 @@ -1056,6 +1056,13 @@ finally show ?thesis . qed +lemma measurable_pair_measure_countable1: + assumes "countable A" + and [measurable]: "\x. x \ A \ (\y. f (x, y)) \ measurable N K" + shows "f \ measurable (count_space A \\<^sub>M N) K" +using _ _ assms(1) +by(rule measurable_compose_countable'[where f="\a b. f (a, snd b)" and g=fst and I=A, simplified])simp_all + subsection {* Product of Borel spaces *} lemma borel_Times: diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Probability/Bochner_Integration.thy Wed Apr 15 16:48:24 2015 +0200 @@ -1875,6 +1875,15 @@ qed qed (simp add: integrable_restrict_space) +lemma integral_empty: + assumes "space M = {}" + shows "integral\<^sup>L M f = 0" +proof - + have "(\ x. f x \M) = (\ x. 0 \M)" + by(rule integral_cong)(simp_all add: assms) + thus ?thesis by simp +qed + subsection {* Measure spaces with an associated density *} lemma integrable_density: diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Probability/Embed_Measure.thy --- a/src/HOL/Probability/Embed_Measure.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Probability/Embed_Measure.thy Wed Apr 15 16:48:24 2015 +0200 @@ -110,13 +110,18 @@ "inj f \ embed_measure M f = distr M (embed_measure M f) f" by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD) +lemma nn_integral_embed_measure': + "inj_on f (space M) \ g \ borel_measurable (embed_measure M f) \ + nn_integral (embed_measure M f) g = nn_integral M (\x. g (f x))" + apply (subst embed_measure_eq_distr', simp) + apply (subst nn_integral_distr) + apply (simp_all add: measurable_embed_measure2') + done + lemma nn_integral_embed_measure: "inj f \ g \ borel_measurable (embed_measure M f) \ nn_integral (embed_measure M f) g = nn_integral M (\x. g (f x))" - apply (subst embed_measure_eq_distr, simp) - apply (subst nn_integral_distr) - apply (simp_all add: measurable_embed_measure2) - done + by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp lemma emeasure_embed_measure': assumes "inj_on f (space M)" "A \ sets (embed_measure M f)" @@ -167,18 +172,21 @@ qed qed -lemma embed_measure_count_space: - "inj f \ embed_measure (count_space A) f = count_space (f`A)" +lemma embed_measure_count_space': + "inj_on f A \ embed_measure (count_space A) f = count_space (f`A)" apply (subst distr_bij_count_space[of f A "f`A", symmetric]) apply (simp add: inj_on_def bij_betw_def) - apply (subst embed_measure_eq_distr) + apply (subst embed_measure_eq_distr') apply simp - apply (auto intro!: measure_eqI imageI simp: sets_embed_measure subset_image_iff) - apply blast + apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff) apply (subst (1 2) emeasure_distr) - apply (auto simp: space_embed_measure sets_embed_measure) + apply (auto simp: space_embed_measure sets_embed_measure') done +lemma embed_measure_count_space: + "inj f \ embed_measure (count_space A) f = count_space (f`A)" + by(rule embed_measure_count_space')(erule subset_inj_on, simp) + lemma sets_embed_measure_alt: "inj f \ sets (embed_measure M f) = (op`f) ` sets M" by (auto simp: sets_embed_measure) @@ -340,4 +348,33 @@ shows "(AE x in embed_measure M f. P x) \ (AE x in M. P (f x))" using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD) +lemma nn_integral_monotone_convergence_SUP_countable: + fixes f :: "'a \ 'b \ ereal" + assumes nonempty: "Y \ {}" + and chain: "Complete_Partial_Order.chain op \ (f ` Y)" + and countable: "countable B" + shows "(\\<^sup>+ x. (SUP i:Y. f i x) \count_space B) = (SUP i:Y. (\\<^sup>+ x. f i x \count_space B))" + (is "?lhs = ?rhs") +proof - + let ?f = "(\i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)" + have "?lhs = \\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \count_space B" + by(rule nn_integral_cong)(simp add: countable) + also have "\ = \\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \count_space (to_nat_on B ` B)" + by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1) + also have "\ = \\<^sup>+ x. (SUP i:Y. ?f i x) \count_space UNIV" + by(simp add: nn_integral_count_space_indicator ereal_indicator[symmetric] Sup_ereal_mult_right' nonempty) + also have "\ = (SUP i:Y. \\<^sup>+ x. ?f i x \count_space UNIV)" using nonempty + proof(rule nn_integral_monotone_convergence_SUP_nat) + show "Complete_Partial_Order.chain op \ (?f ` Y)" + by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD) + qed + also have "\ = (SUP i:Y. \\<^sup>+ x. f i (from_nat_into B x) \count_space (to_nat_on B ` B))" + by(simp add: nn_integral_count_space_indicator) + also have "\ = (SUP i:Y. \\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \count_space B)" + by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1) + also have "\ = ?rhs" + by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable) + finally show ?thesis . +qed + end diff -r ef4fe30e9ef1 -r 2cd500d08c30 src/HOL/Probability/Giry_Monad.thy --- a/src/HOL/Probability/Giry_Monad.thy Wed Apr 15 15:10:01 2015 +0200 +++ b/src/HOL/Probability/Giry_Monad.thy Wed Apr 15 16:48:24 2015 +0200 @@ -38,6 +38,12 @@ sublocale prob_space \ subprob_space by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty) +lemma subprob_space_sigma [simp]: "\ \ {} \ subprob_space (sigma \ X)" +by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv) + +lemma subprob_space_null_measure: "space M \ {} \ subprob_space (null_measure M)" +by(simp add: null_measure_def) + lemma (in subprob_space) subprob_space_distr: assumes f: "f \ measurable M M'" and "space M' \ {}" shows "subprob_space (distr M M' f)" proof (rule subprob_spaceI) @@ -324,6 +330,35 @@ finally show ?thesis . qed +lemma integral_measurable_subprob_algebra: + fixes f :: "_ \ real" + assumes f_measurable [measurable]: "f \ borel_measurable N" + and f_bounded: "\x. x \ space N \ \f x\ \ B" + shows "(\M. integral\<^sup>L M f) \ borel_measurable (subprob_algebra N)" +proof - + note [measurable] = nn_integral_measurable_subprob_algebra + have "?thesis \ (\M. real (\\<^sup>+ x. f x \M) - real (\\<^sup>+ x. - f x \M)) \ borel_measurable (subprob_algebra N)" + proof(rule measurable_cong) + fix M + assume "M \ space (subprob_algebra N)" + hence "subprob_space M" and M [measurable_cong]: "sets M = sets N" + by(simp_all add: space_subprob_algebra) + interpret subprob_space M by fact + have "(\\<^sup>+ x. ereal \f x\ \M) \ (\\<^sup>+ x. ereal B \M)" + by(rule nn_integral_mono)(simp add: sets_eq_imp_space_eq[OF M] f_bounded) + also have "\ = max B 0 * emeasure M (space M)" by(simp add: nn_integral_const_If max_def) + also have "\ \ ereal (max B 0) * 1" + by(rule ereal_mult_left_mono)(simp_all add: emeasure_space_le_1 zero_ereal_def) + finally have "(\\<^sup>+ x. ereal \f x\ \M) \ \" by(auto simp add: max_def) + then have "integrable M f" using f_measurable + by(auto intro: integrableI_bounded) + thus "(\ x. f x \M) = real (\\<^sup>+ x. f x \M) - real (\\<^sup>+ x. - f x \M)" + by(simp add: real_lebesgue_integral_def) + qed + also have "\" by measurable + finally show ?thesis . +qed + (* TODO: Rename. This name is too general -- Manuel *) lemma measurable_pair_measure: assumes f: "f \ measurable M (subprob_algebra N)" @@ -796,6 +831,163 @@ apply (auto simp: f) done +lemma measurable_join1: + "\ f \ measurable N K; sets M = sets (subprob_algebra N) \ + \ f \ measurable (join M) K" +by(simp add: measurable_def) + +lemma + fixes f :: "_ \ real" + assumes f_measurable [measurable]: "f \ borel_measurable N" + and f_bounded: "\x. x \ space N \ \f x\ \ B" + and M [measurable_cong]: "sets M = sets (subprob_algebra N)" + and fin: "finite_measure M" + and M_bounded: "AE M' in M. emeasure M' (space M') \ ereal B'" + shows integrable_join: "integrable (join M) f" (is ?integrable) + and integral_join: "integral\<^sup>L (join M) f = \ M'. integral\<^sup>L M' f \M" (is ?integral) +proof(case_tac [!] "space N = {}") + assume *: "space N = {}" + show ?integrable + using M * by(simp add: real_integrable_def measurable_def nn_integral_empty) + have "(\ M'. integral\<^sup>L M' f \M) = (\ M'. 0 \M)" + proof(rule integral_cong) + fix M' + assume "M' \ space M" + with sets_eq_imp_space_eq[OF M] have "space M' = space N" + by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) + with * show "(\ x. f x \M') = 0" by(simp add: integral_empty) + qed simp + then show ?integral + using M * by(simp add: integral_empty) +next + assume *: "space N \ {}" + + from * have B [simp]: "0 \ B" by(auto dest: f_bounded) + + have [measurable]: "f \ borel_measurable (join M)" using f_measurable M + by(rule measurable_join1) + + { fix f M' + assume [measurable]: "f \ borel_measurable N" + and f_bounded: "\x. x \ space N \ f x \ B" + and "M' \ space M" "emeasure M' (space M') \ ereal B'" + have "AE x in M'. ereal (f x) \ ereal B" + proof(rule AE_I2) + fix x + assume "x \ space M'" + with \M' \ space M\ sets_eq_imp_space_eq[OF M] + have "x \ space N" by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) + from f_bounded[OF this] show "ereal (f x) \ ereal B" by simp + qed + then have "(\\<^sup>+ x. ereal (f x) \M') \ (\\<^sup>+ x. ereal B \M')" + by(rule nn_integral_mono_AE) + also have "\ = ereal B * emeasure M' (space M')" by(simp) + also have "\ \ ereal B * ereal B'" by(rule ereal_mult_left_mono)(fact, simp) + also have "\ \ ereal B * ereal \B'\" by(rule ereal_mult_left_mono)(simp_all) + finally have "(\\<^sup>+ x. ereal (f x) \M') \ ereal (B * \B'\)" by simp } + note bounded1 = this + + have bounded: + "\f. \ f \ borel_measurable N; \x. x \ space N \ f x \ B \ + \ (\\<^sup>+ x. ereal (f x) \join M) \ \" + proof - + fix f + assume [measurable]: "f \ borel_measurable N" + and f_bounded: "\x. x \ space N \ f x \ B" + have "(\\<^sup>+ x. ereal (f x) \join M) = (\\<^sup>+ M'. \\<^sup>+ x. ereal (f x) \M' \M)" + by(rule nn_integral_join[OF _ M]) simp + also have "\ \ \\<^sup>+ M'. B * \B'\ \M" + using bounded1[OF \f \ borel_measurable N\ f_bounded] + by(rule nn_integral_mono_AE[OF AE_mp[OF M_bounded AE_I2], rule_format]) + also have "\ = B * \B'\ * emeasure M (space M)" by simp + also have "\ < \" by(simp add: finite_measure.finite_emeasure_space[OF fin]) + finally show "?thesis f" by simp + qed + have f_pos: "(\\<^sup>+ x. ereal (f x) \join M) \ \" + and f_neg: "(\\<^sup>+ x. ereal (- f x) \join M) \ \" + using f_bounded by(auto del: notI intro!: bounded simp add: abs_le_iff) + + show ?integrable using f_pos f_neg by(simp add: real_integrable_def) + + note [measurable] = nn_integral_measurable_subprob_algebra + + have "(\\<^sup>+ x. f x \join M) = (\\<^sup>+ x. max 0 (f x) \join M)" + by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) + also have "\ = \\<^sup>+ M'. \\<^sup>+ x. max 0 (f x) \M' \M" + by(simp add: nn_integral_join[OF _ M]) + also have "\ = \\<^sup>+ M'. \\<^sup>+ x. f x \M' \M" + by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) + finally have int_f: "(\\<^sup>+ x. f x \join M) = (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M)" . + + have "(\\<^sup>+ x. - f x \join M) = (\\<^sup>+ x. max 0 (- f x) \join M)" + by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) + also have "\ = \\<^sup>+ M'. \\<^sup>+ x. max 0 (- f x) \M' \M" + by(simp add: nn_integral_join[OF _ M]) + also have "\ = \\<^sup>+ M'. \\<^sup>+ x. - f x \M' \M" + by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) + finally have int_mf: "(\\<^sup>+ x. - f x \join M) = (\\<^sup>+ M'. \\<^sup>+ x. - f x \M' \M)" . + + have f_pos1: + "\M'. \ M' \ space M; emeasure M' (space M') \ ereal B' \ + \ (\\<^sup>+ x. ereal (f x) \M') \ ereal (B * \B'\)" + using f_measurable by(auto intro!: bounded1 dest: f_bounded) + have "AE M' in M. (\\<^sup>+ x. f x \M') \ \" + using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_pos1) + hence [simp]: "(\\<^sup>+ M'. ereal (real (\\<^sup>+ x. f x \M')) \M) = (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M)" + by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg) + from f_pos have [simp]: "integrable M (\M'. real (\