use measurability prover
authorhoelzl
Fri Nov 02 14:23:54 2012 +0100 (2012-11-02)
changeset 500038c213922ed49
parent 50002 ce0d316b5b44
child 50004 c96e8e40d789
use measurability prover
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4    "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
     1.5    unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
     1.6  
     1.7 -lemma pair_measureI[intro, simp]:
     1.8 +lemma pair_measureI[intro, simp, measurable]:
     1.9    "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^isub>M B)"
    1.10    by (auto simp: sets_pair_measure)
    1.11  
    1.12 @@ -61,7 +61,11 @@
    1.13    unfolding pair_measure_def using 1 2
    1.14    by (intro measurable_measure_of) (auto dest: sets_into_space)
    1.15  
    1.16 -lemma measurable_Pair:
    1.17 +lemma measurable_split_replace[measurable (raw)]:
    1.18 +  "(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. split (f x) (g x)) \<in> measurable M N"
    1.19 +  unfolding split_beta' .
    1.20 +
    1.21 +lemma measurable_Pair[measurable (raw)]:
    1.22    assumes f: "f \<in> measurable M M1" and g: "g \<in> measurable M M2"
    1.23    shows "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
    1.24  proof (rule measurable_pair_measureI)
    1.25 @@ -75,34 +79,38 @@
    1.26    finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" .
    1.27  qed
    1.28  
    1.29 +lemma measurable_Pair_compose_split[measurable_dest]:
    1.30 +  assumes f: "split f \<in> measurable (M1 \<Otimes>\<^isub>M M2) N"
    1.31 +  assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2"
    1.32 +  shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N"
    1.33 +  using measurable_compose[OF measurable_Pair f, OF g h] by simp
    1.34 +
    1.35  lemma measurable_pair:
    1.36    assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
    1.37    shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
    1.38    using measurable_Pair[OF assms] by simp
    1.39  
    1.40 -lemma measurable_fst[intro!, simp]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
    1.41 +lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
    1.42    by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
    1.43  
    1.44 -lemma measurable_snd[intro!, simp]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
    1.45 +lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
    1.46    by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
    1.47  
    1.48 -lemma measurable_fst': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. fst (f x)) \<in> measurable M N"
    1.49 -  using measurable_comp[OF _ measurable_fst] by (auto simp: comp_def)
    1.50 -
    1.51 -lemma measurable_snd': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. snd (f x)) \<in> measurable M P"
    1.52 -    using measurable_comp[OF _ measurable_snd] by (auto simp: comp_def)
    1.53 +lemma 
    1.54 +  assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^isub>M P)" 
    1.55 +  shows measurable_fst': "(\<lambda>x. fst (f x)) \<in> measurable M N"
    1.56 +    and measurable_snd': "(\<lambda>x. snd (f x)) \<in> measurable M P"
    1.57 +  by simp_all
    1.58  
    1.59 -lemma measurable_fst'': "f \<in> measurable M N \<Longrightarrow> (\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^isub>M P) N"
    1.60 -  using measurable_comp[OF measurable_fst _] by (auto simp: comp_def)
    1.61 -
    1.62 -lemma measurable_snd'': "f \<in> measurable M N \<Longrightarrow> (\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^isub>M M) N"
    1.63 -  using measurable_comp[OF measurable_snd _] by (auto simp: comp_def)
    1.64 +lemma
    1.65 +  assumes f[measurable]: "f \<in> measurable M N"
    1.66 +  shows measurable_fst'': "(\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^isub>M P) N"
    1.67 +    and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^isub>M M) N"
    1.68 +  by simp_all
    1.69  
    1.70  lemma measurable_pair_iff:
    1.71    "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
    1.72 -  using measurable_pair[of f M M1 M2]
    1.73 -  using [[simproc del: measurable]] (* the measurable method is nonterminating when using measurable_pair *)
    1.74 -  by auto
    1.75 +  by (auto intro: measurable_pair[of f M M1 M2]) 
    1.76  
    1.77  lemma measurable_split_conv:
    1.78    "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"
    1.79 @@ -117,16 +125,13 @@
    1.80  
    1.81  lemma measurable_pair_swap_iff:
    1.82    "f \<in> measurable (M2 \<Otimes>\<^isub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) M"
    1.83 -  using measurable_pair_swap[of "\<lambda>(x,y). f (y, x)"]
    1.84 -  by (auto intro!: measurable_pair_swap)
    1.85 -
    1.86 -lemma measurable_ident[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
    1.87 -  unfolding measurable_def by auto
    1.88 +  by (auto dest: measurable_pair_swap)
    1.89  
    1.90  lemma measurable_Pair1': "x \<in> space M1 \<Longrightarrow> Pair x \<in> measurable M2 (M1 \<Otimes>\<^isub>M M2)"
    1.91 -  by (auto intro!: measurable_Pair)
    1.92 +  by simp
    1.93  
    1.94 -lemma sets_Pair1: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
    1.95 +lemma sets_Pair1[measurable (raw)]:
    1.96 +  assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
    1.97  proof -
    1.98    have "Pair x -` A = (if x \<in> space M1 then Pair x -` A \<inter> space M2 else {})"
    1.99      using A[THEN sets_into_space] by (auto simp: space_pair_measure)
   1.100 @@ -163,8 +168,11 @@
   1.101    unfolding Int_stable_def
   1.102    by safe (auto simp add: times_Int_times)
   1.103  
   1.104 +lemma disjoint_family_vimageI: "disjoint_family F \<Longrightarrow> disjoint_family (\<lambda>i. f -` F i)"
   1.105 +  by (auto simp: disjoint_family_on_def)
   1.106 +
   1.107  lemma (in finite_measure) finite_measure_cut_measurable:
   1.108 -  assumes "Q \<in> sets (N \<Otimes>\<^isub>M M)"
   1.109 +  assumes [measurable]: "Q \<in> sets (N \<Otimes>\<^isub>M M)"
   1.110    shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N"
   1.111      (is "?s Q \<in> _")
   1.112    using Int_stable_pair_measure_generator pair_measure_closed assms
   1.113 @@ -179,11 +187,10 @@
   1.114      by (auto intro!: measurable_If simp: space_pair_measure)
   1.115  next
   1.116    case (union F)
   1.117 -  moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
   1.118 -    unfolding sets_pair_measure[symmetric]
   1.119 -    by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
   1.120 +  moreover then have *: "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
   1.121 +    by (simp add: suminf_emeasure disjoint_family_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])
   1.122    ultimately show ?case
   1.123 -    by (auto simp: vimage_UN)
   1.124 +    unfolding sets_pair_measure[symmetric] by simp
   1.125  qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
   1.126  
   1.127  lemma (in sigma_finite_measure) measurable_emeasure_Pair:
   1.128 @@ -226,6 +233,17 @@
   1.129      by auto
   1.130  qed
   1.131  
   1.132 +lemma (in sigma_finite_measure) measurable_emeasure[measurable (raw)]:
   1.133 +  assumes space: "\<And>x. x \<in> space N \<Longrightarrow> A x \<subseteq> space M"
   1.134 +  assumes A: "{x\<in>space (N \<Otimes>\<^isub>M M). snd x \<in> A (fst x)} \<in> sets (N \<Otimes>\<^isub>M M)"
   1.135 +  shows "(\<lambda>x. emeasure M (A x)) \<in> borel_measurable N"
   1.136 +proof -
   1.137 +  from space have "\<And>x. x \<in> space N \<Longrightarrow> Pair x -` {x \<in> space (N \<Otimes>\<^isub>M M). snd x \<in> A (fst x)} = A x"
   1.138 +    by (auto simp: space_pair_measure)
   1.139 +  with measurable_emeasure_Pair[OF A] show ?thesis
   1.140 +    by (auto cong: measurable_cong)
   1.141 +qed
   1.142 +
   1.143  lemma (in sigma_finite_measure) emeasure_pair_measure:
   1.144    assumes "X \<in> sets (N \<Otimes>\<^isub>M M)"
   1.145    shows "emeasure (N \<Otimes>\<^isub>M M) X = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator X (x, y) \<partial>M \<partial>N)" (is "_ = ?\<mu> X")
   1.146 @@ -476,7 +494,7 @@
   1.147  
   1.148  lemma measurable_compose_Pair1:
   1.149    "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^isub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
   1.150 -  by (rule measurable_compose[OF measurable_Pair]) auto
   1.151 +  by simp
   1.152  
   1.153  lemma (in sigma_finite_measure) borel_measurable_positive_integral_fst':
   1.154    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M)" "\<And>x. 0 \<le> f x"
   1.155 @@ -527,9 +545,13 @@
   1.156      positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
   1.157    unfolding positive_integral_max_0 by auto
   1.158  
   1.159 -lemma (in sigma_finite_measure) borel_measurable_positive_integral:
   1.160 -  "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M) \<in> borel_measurable M1"
   1.161 -  using positive_integral_fst_measurable(1)[of "split f" M1] by simp
   1.162 +lemma (in sigma_finite_measure) borel_measurable_positive_integral[measurable (raw)]:
   1.163 +  "split f \<in> borel_measurable (N \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M) \<in> borel_measurable N"
   1.164 +  using positive_integral_fst_measurable(1)[of "split f" N] by simp
   1.165 +
   1.166 +lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
   1.167 +  "split f \<in> borel_measurable (N \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral> y. f x y \<partial>M) \<in> borel_measurable N"
   1.168 +  by (simp add: lebesgue_integral_def)
   1.169  
   1.170  lemma (in pair_sigma_finite) positive_integral_snd_measurable:
   1.171    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.172 @@ -650,29 +672,6 @@
   1.173      by simp
   1.174  qed
   1.175  
   1.176 -lemma (in pair_sigma_finite) positive_integral_fst_measurable':
   1.177 -  assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.178 -  shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
   1.179 -  using M2.positive_integral_fst_measurable(1)[OF f] by simp
   1.180 -
   1.181 -lemma (in pair_sigma_finite) integral_fst_measurable:
   1.182 -  "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral> y. f x y \<partial>M2) \<in> borel_measurable M1"
   1.183 -  by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_fst_measurable')
   1.184 -
   1.185 -lemma (in pair_sigma_finite) positive_integral_snd_measurable':
   1.186 -  assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.187 -  shows "(\<lambda>y. \<integral>\<^isup>+ x. f x y \<partial>M1) \<in> borel_measurable M2"
   1.188 -proof -
   1.189 -  interpret Q: pair_sigma_finite M2 M1 ..
   1.190 -  show ?thesis
   1.191 -    using measurable_pair_swap[OF f]
   1.192 -    by (intro Q.positive_integral_fst_measurable') (simp add: split_beta')
   1.193 -qed
   1.194 -
   1.195 -lemma (in pair_sigma_finite) integral_snd_measurable:
   1.196 -  "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>y. \<integral> x. f x y \<partial>M1) \<in> borel_measurable M2"
   1.197 -  by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_snd_measurable')
   1.198 -
   1.199  lemma (in pair_sigma_finite) Fubini_integral:
   1.200    assumes f: "integrable (M1 \<Otimes>\<^isub>M M2) f"
   1.201    shows "(\<integral>y. (\<integral>x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1)"
   1.202 @@ -739,48 +738,21 @@
   1.203  lemma pair_measure_density:
   1.204    assumes f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x"
   1.205    assumes g: "g \<in> borel_measurable M2" "AE x in M2. 0 \<le> g x"
   1.206 -  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
   1.207 -  assumes "sigma_finite_measure (density M1 f)" "sigma_finite_measure (density M2 g)"
   1.208 +  assumes "sigma_finite_measure M2" "sigma_finite_measure (density M2 g)"
   1.209    shows "density M1 f \<Otimes>\<^isub>M density M2 g = density (M1 \<Otimes>\<^isub>M M2) (\<lambda>(x,y). f x * g y)" (is "?L = ?R")
   1.210  proof (rule measure_eqI)
   1.211 -  interpret M1: sigma_finite_measure M1 by fact
   1.212    interpret M2: sigma_finite_measure M2 by fact
   1.213 -  interpret D1: sigma_finite_measure "density M1 f" by fact
   1.214    interpret D2: sigma_finite_measure "density M2 g" by fact
   1.215 -  interpret L: pair_sigma_finite "density M1 f" "density M2 g" ..
   1.216 -  interpret R: pair_sigma_finite M1 M2 ..
   1.217  
   1.218    fix A assume A: "A \<in> sets ?L"
   1.219 -  then have indicator_eq: "\<And>x y. indicator A (x, y) = indicator (Pair x -` A) y"
   1.220 -   and Pair_A: "\<And>x. Pair x -` A \<in> sets M2"
   1.221 -    by (auto simp: indicator_def sets_Pair1)
   1.222 -  have f_fst: "(\<lambda>p. f (fst p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.223 -    using measurable_comp[OF measurable_fst f(1)] by (simp add: comp_def)
   1.224 -  have g_snd: "(\<lambda>p. g (snd p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.225 -    using measurable_comp[OF measurable_snd g(1)] by (simp add: comp_def)
   1.226 -  have "(\<lambda>x. \<integral>\<^isup>+ y. g (snd (x, y)) * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1"
   1.227 -    using g_snd Pair_A A by (intro M2.positive_integral_fst_measurable) auto
   1.228 -  then have int_g: "(\<lambda>x. \<integral>\<^isup>+ y. g y * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1"
   1.229 -    by simp
   1.230 -
   1.231 -  show "emeasure ?L A = emeasure ?R A"
   1.232 -    apply (subst D2.emeasure_pair_measure[OF A])
   1.233 -    apply (subst emeasure_density)
   1.234 -        using f_fst g_snd apply (simp add: split_beta')
   1.235 -      using A apply simp
   1.236 -    apply (subst positive_integral_density[OF g])
   1.237 -      apply (simp add: indicator_eq Pair_A)
   1.238 -    apply (subst positive_integral_density[OF f])
   1.239 -      apply (rule int_g)
   1.240 -    apply (subst M2.positive_integral_fst_measurable(2)[symmetric])
   1.241 -      using f g A Pair_A f_fst g_snd
   1.242 -      apply (auto intro!: positive_integral_cong_AE R.measurable_emeasure_Pair1
   1.243 -                  simp: positive_integral_cmult indicator_eq split_beta')
   1.244 -    apply (intro AE_I2 impI)
   1.245 -    apply (subst mult_assoc)
   1.246 -    apply (subst positive_integral_cmult)
   1.247 -          apply auto
   1.248 -    done
   1.249 +  with f g have "(\<integral>\<^isup>+ x. f x * \<integral>\<^isup>+ y. g y * indicator A (x, y) \<partial>M2 \<partial>M1) =
   1.250 +    (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. f x * g y * indicator A (x, y) \<partial>M2 \<partial>M1)"
   1.251 +    by (intro positive_integral_cong_AE)
   1.252 +       (auto simp add: positive_integral_cmult[symmetric] ac_simps)
   1.253 +  with A f g show "emeasure ?L A = emeasure ?R A"
   1.254 +    by (simp add: D2.emeasure_pair_measure emeasure_density positive_integral_density
   1.255 +                  M2.positive_integral_fst_measurable(2)[symmetric]
   1.256 +             cong: positive_integral_cong)
   1.257  qed simp
   1.258  
   1.259  lemma sigma_finite_measure_distr:
   1.260 @@ -792,7 +764,7 @@
   1.261    show ?thesis
   1.262    proof (unfold_locales, intro conjI exI allI)
   1.263      show "range (\<lambda>i. f -` A i \<inter> space M) \<subseteq> sets M"
   1.264 -      using A f by (auto intro!: measurable_sets)
   1.265 +      using A f by auto
   1.266      show "(\<Union>i. f -` A i \<inter> space M) = space M"
   1.267        using A(1) A(2)[symmetric] f by (auto simp: measurable_def Pi_def)
   1.268      fix i show "emeasure M (f -` A i \<inter> space M) \<noteq> \<infinity>"
   1.269 @@ -800,47 +772,19 @@
   1.270    qed
   1.271  qed
   1.272  
   1.273 -lemma measurable_cong':
   1.274 -  assumes sets: "sets M = sets M'" "sets N = sets N'"
   1.275 -  shows "measurable M N = measurable M' N'"
   1.276 -  using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def)
   1.277 -
   1.278  lemma pair_measure_distr:
   1.279    assumes f: "f \<in> measurable M S" and g: "g \<in> measurable N T"
   1.280 -  assumes "sigma_finite_measure (distr M S f)" "sigma_finite_measure (distr N T g)"
   1.281 +  assumes "sigma_finite_measure (distr N T g)"
   1.282    shows "distr M S f \<Otimes>\<^isub>M distr N T g = distr (M \<Otimes>\<^isub>M N) (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). (f x, g y))" (is "?P = ?D")
   1.283  proof (rule measure_eqI)
   1.284 -  show "sets ?P = sets ?D"
   1.285 -    by simp
   1.286 -  interpret S: sigma_finite_measure "distr M S f" by fact
   1.287    interpret T: sigma_finite_measure "distr N T g" by fact
   1.288 -  interpret ST: pair_sigma_finite "distr M S f"  "distr N T g" ..
   1.289 -  interpret M: sigma_finite_measure M by (rule sigma_finite_measure_distr) fact+
   1.290    interpret N: sigma_finite_measure N by (rule sigma_finite_measure_distr) fact+
   1.291 -  interpret MN: pair_sigma_finite M N ..
   1.292 -  interpret SN: pair_sigma_finite "distr M S f" N ..
   1.293 -  have [simp]: 
   1.294 -    "\<And>f g. fst \<circ> (\<lambda>(x, y). (f x, g y)) = f \<circ> fst" "\<And>f g. snd \<circ> (\<lambda>(x, y). (f x, g y)) = g \<circ> snd"
   1.295 -    by auto
   1.296 -  then have fg: "(\<lambda>(x, y). (f x, g y)) \<in> measurable (M \<Otimes>\<^isub>M N) (S \<Otimes>\<^isub>M T)"
   1.297 -    using measurable_comp[OF measurable_fst f] measurable_comp[OF measurable_snd g]
   1.298 -    by (auto simp: measurable_pair_iff)
   1.299 +
   1.300    fix A assume A: "A \<in> sets ?P"
   1.301 -  then have "emeasure ?P A = (\<integral>\<^isup>+x. emeasure (distr N T g) (Pair x -` A) \<partial>distr M S f)"
   1.302 -    by (rule T.emeasure_pair_measure_alt)
   1.303 -  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair x -` A) \<inter> space N) \<partial>distr M S f)"
   1.304 -    using g A by (simp add: sets_Pair1 emeasure_distr)
   1.305 -  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair (f x) -` A) \<inter> space N) \<partial>M)"
   1.306 -    using f g A ST.measurable_emeasure_Pair1[OF A]
   1.307 -    by (intro positive_integral_distr) (auto simp add: sets_Pair1 emeasure_distr)
   1.308 -  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (Pair x -` ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))) \<partial>M)"
   1.309 -    by (intro positive_integral_cong arg_cong2[where f=emeasure]) (auto simp: space_pair_measure)
   1.310 -  also have "\<dots> = emeasure (M \<Otimes>\<^isub>M N) ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))"
   1.311 -    using fg by (intro N.emeasure_pair_measure_alt[symmetric] measurable_sets[OF _ A])
   1.312 -                (auto cong: measurable_cong')
   1.313 -  also have "\<dots> = emeasure ?D A"
   1.314 -    using fg A by (subst emeasure_distr) auto
   1.315 -  finally show "emeasure ?P A = emeasure ?D A" .
   1.316 -qed
   1.317 +  with f g show "emeasure ?P A = emeasure ?D A"
   1.318 +    by (auto simp add: N.emeasure_pair_measure_alt space_pair_measure emeasure_distr
   1.319 +                       T.emeasure_pair_measure_alt positive_integral_distr
   1.320 +             intro!: positive_integral_cong arg_cong[where f="emeasure N"])
   1.321 +qed simp
   1.322  
   1.323  end
   1.324 \ No newline at end of file
     2.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:23:40 2012 +0100
     2.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:23:54 2012 +0100
     2.3 @@ -36,14 +36,14 @@
     2.4  lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
     2.5    unfolding borel_def pred_def by auto
     2.6  
     2.7 -lemma borel_open[simp, measurable (raw generic)]:
     2.8 +lemma borel_open[measurable (raw generic)]:
     2.9    assumes "open A" shows "A \<in> sets borel"
    2.10  proof -
    2.11    have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
    2.12    thus ?thesis unfolding borel_def by auto
    2.13  qed
    2.14  
    2.15 -lemma borel_closed[simp, measurable (raw generic)]:
    2.16 +lemma borel_closed[measurable (raw generic)]:
    2.17    assumes "closed A" shows "A \<in> sets borel"
    2.18  proof -
    2.19    have "space borel - (- A) \<in> sets borel"
    2.20 @@ -51,11 +51,11 @@
    2.21    thus ?thesis by simp
    2.22  qed
    2.23  
    2.24 -lemma borel_insert[measurable]:
    2.25 -  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t2_space measure)"
    2.26 +lemma borel_singleton[measurable]:
    2.27 +  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
    2.28    unfolding insert_def by (rule Un) auto
    2.29  
    2.30 -lemma borel_comp[intro, simp, measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
    2.31 +lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
    2.32    unfolding Compl_eq_Diff_UNIV by simp
    2.33  
    2.34  lemma borel_measurable_vimage:
    2.35 @@ -74,19 +74,11 @@
    2.36      using assms[of S] by simp
    2.37  qed
    2.38  
    2.39 -lemma borel_singleton[simp, intro]:
    2.40 -  fixes x :: "'a::t1_space"
    2.41 -  shows "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets borel"
    2.42 -  proof (rule insert_in_sets)
    2.43 -    show "{x} \<in> sets borel"
    2.44 -      using closed_singleton[of x] by (rule borel_closed)
    2.45 -  qed simp
    2.46 -
    2.47 -lemma borel_measurable_const[simp, intro, measurable (raw)]:
    2.48 +lemma borel_measurable_const[measurable (raw)]:
    2.49    "(\<lambda>x. c) \<in> borel_measurable M"
    2.50    by auto
    2.51  
    2.52 -lemma borel_measurable_indicator[simp, intro!]:
    2.53 +lemma borel_measurable_indicator:
    2.54    assumes A: "A \<in> sets M"
    2.55    shows "indicator A \<in> borel_measurable M"
    2.56    unfolding indicator_def [abs_def] using A
    2.57 @@ -137,7 +129,7 @@
    2.58    "(f :: 'a \<Rightarrow> 'b::euclidean_space) \<in> borel_measurable M \<Longrightarrow>(\<lambda>x. f x $$ i) \<in> borel_measurable M"
    2.59    by simp
    2.60  
    2.61 -lemma [simp, intro, measurable]:
    2.62 +lemma [measurable]:
    2.63    fixes a b :: "'a\<Colon>ordered_euclidean_space"
    2.64    shows lessThan_borel: "{..< a} \<in> sets borel"
    2.65      and greaterThan_borel: "{a <..} \<in> sets borel"
    2.66 @@ -151,13 +143,13 @@
    2.67    by (blast intro: borel_open borel_closed)+
    2.68  
    2.69  lemma 
    2.70 -  shows hafspace_less_borel[simp, intro]: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
    2.71 -    and hafspace_greater_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
    2.72 -    and hafspace_less_eq_borel[simp, intro]: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
    2.73 -    and hafspace_greater_eq_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
    2.74 +  shows hafspace_less_borel: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
    2.75 +    and hafspace_greater_borel: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
    2.76 +    and hafspace_less_eq_borel: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
    2.77 +    and hafspace_greater_eq_borel: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
    2.78    by simp_all
    2.79  
    2.80 -lemma borel_measurable_less[simp, intro, measurable]:
    2.81 +lemma borel_measurable_less[measurable]:
    2.82    fixes f :: "'a \<Rightarrow> real"
    2.83    assumes f: "f \<in> borel_measurable M"
    2.84    assumes g: "g \<in> borel_measurable M"
    2.85 @@ -169,7 +161,7 @@
    2.86      by simp
    2.87  qed
    2.88  
    2.89 -lemma [simp, intro]:
    2.90 +lemma
    2.91    fixes f :: "'a \<Rightarrow> real"
    2.92    assumes f[measurable]: "f \<in> borel_measurable M"
    2.93    assumes g[measurable]: "g \<in> borel_measurable M"
    2.94 @@ -633,7 +625,7 @@
    2.95    using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
    2.96    by (simp add: comp_def)
    2.97  
    2.98 -lemma borel_measurable_uminus[simp, intro, measurable (raw)]:
    2.99 +lemma borel_measurable_uminus[measurable (raw)]:
   2.100    fixes g :: "'a \<Rightarrow> real"
   2.101    assumes g: "g \<in> borel_measurable M"
   2.102    shows "(\<lambda>x. - g x) \<in> borel_measurable M"
   2.103 @@ -644,7 +636,7 @@
   2.104    shows "x $$ i = (if i < DIM('a) then fst x $$ i else snd x $$ (i - DIM('a)))"
   2.105    unfolding euclidean_component_def basis_prod_def inner_prod_def by auto
   2.106  
   2.107 -lemma borel_measurable_Pair[simp, intro, measurable (raw)]:
   2.108 +lemma borel_measurable_Pair[measurable (raw)]:
   2.109    fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   2.110    assumes f: "f \<in> borel_measurable M"
   2.111    assumes g: "g \<in> borel_measurable M"
   2.112 @@ -675,8 +667,8 @@
   2.113  
   2.114  lemma borel_measurable_continuous_Pair:
   2.115    fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   2.116 -  assumes [simp]: "f \<in> borel_measurable M"
   2.117 -  assumes [simp]: "g \<in> borel_measurable M"
   2.118 +  assumes [measurable]: "f \<in> borel_measurable M"
   2.119 +  assumes [measurable]: "g \<in> borel_measurable M"
   2.120    assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
   2.121    shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
   2.122  proof -
   2.123 @@ -685,7 +677,7 @@
   2.124      unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
   2.125  qed
   2.126  
   2.127 -lemma borel_measurable_add[simp, intro, measurable (raw)]:
   2.128 +lemma borel_measurable_add[measurable (raw)]:
   2.129    fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   2.130    assumes f: "f \<in> borel_measurable M"
   2.131    assumes g: "g \<in> borel_measurable M"
   2.132 @@ -694,7 +686,7 @@
   2.133    by (rule borel_measurable_continuous_Pair)
   2.134       (auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
   2.135  
   2.136 -lemma borel_measurable_setsum[simp, intro, measurable (raw)]:
   2.137 +lemma borel_measurable_setsum[measurable (raw)]:
   2.138    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   2.139    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   2.140    shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
   2.141 @@ -703,14 +695,14 @@
   2.142    thus ?thesis using assms by induct auto
   2.143  qed simp
   2.144  
   2.145 -lemma borel_measurable_diff[simp, intro, measurable (raw)]:
   2.146 +lemma borel_measurable_diff[measurable (raw)]:
   2.147    fixes f :: "'a \<Rightarrow> real"
   2.148    assumes f: "f \<in> borel_measurable M"
   2.149    assumes g: "g \<in> borel_measurable M"
   2.150    shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   2.151 -  unfolding diff_minus using assms by fast
   2.152 +  unfolding diff_minus using assms by simp
   2.153  
   2.154 -lemma borel_measurable_times[simp, intro, measurable (raw)]:
   2.155 +lemma borel_measurable_times[measurable (raw)]:
   2.156    fixes f :: "'a \<Rightarrow> real"
   2.157    assumes f: "f \<in> borel_measurable M"
   2.158    assumes g: "g \<in> borel_measurable M"
   2.159 @@ -724,7 +716,7 @@
   2.160    shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
   2.161    unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
   2.162  
   2.163 -lemma borel_measurable_dist[simp, intro, measurable (raw)]:
   2.164 +lemma borel_measurable_dist[measurable (raw)]:
   2.165    fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
   2.166    assumes f: "f \<in> borel_measurable M"
   2.167    assumes g: "g \<in> borel_measurable M"
   2.168 @@ -769,7 +761,7 @@
   2.169    "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M"
   2.170    using affine_borel_measurable_vector[of f M a 1] by simp
   2.171  
   2.172 -lemma borel_measurable_setprod[simp, intro, measurable (raw)]:
   2.173 +lemma borel_measurable_setprod[measurable (raw)]:
   2.174    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   2.175    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   2.176    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
   2.177 @@ -778,53 +770,36 @@
   2.178    thus ?thesis using assms by induct auto
   2.179  qed simp
   2.180  
   2.181 -lemma borel_measurable_inverse[simp, intro, measurable (raw)]:
   2.182 +lemma borel_measurable_inverse[measurable (raw)]:
   2.183    fixes f :: "'a \<Rightarrow> real"
   2.184    assumes f: "f \<in> borel_measurable M"
   2.185    shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
   2.186  proof -
   2.187 -  have *: "\<And>x::real. inverse x = (if x \<in> UNIV - {0} then inverse x else 0)" by auto
   2.188 -  show ?thesis
   2.189 -    apply (subst *)
   2.190 -    apply (rule borel_measurable_continuous_on_open)
   2.191 -    apply (auto intro!: f continuous_on_inverse continuous_on_id)
   2.192 -    done
   2.193 +  have "(\<lambda>x::real. if x \<in> UNIV - {0} then inverse x else 0) \<in> borel_measurable borel"
   2.194 +    by (intro borel_measurable_continuous_on_open' continuous_on_inverse continuous_on_id) auto
   2.195 +  also have "(\<lambda>x::real. if x \<in> UNIV - {0} then inverse x else 0) = inverse" by (intro ext) auto
   2.196 +  finally show ?thesis using f by simp
   2.197  qed
   2.198  
   2.199 -lemma borel_measurable_divide[simp, intro, measurable (raw)]:
   2.200 -  fixes f :: "'a \<Rightarrow> real"
   2.201 -  assumes "f \<in> borel_measurable M"
   2.202 -  and "g \<in> borel_measurable M"
   2.203 -  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
   2.204 -  unfolding field_divide_inverse
   2.205 -  by (rule borel_measurable_inverse borel_measurable_times assms)+
   2.206 +lemma borel_measurable_divide[measurable (raw)]:
   2.207 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. f x / g x::real) \<in> borel_measurable M"
   2.208 +  by (simp add: field_divide_inverse)
   2.209  
   2.210 -lemma borel_measurable_max[intro, simp, measurable (raw)]:
   2.211 -  fixes f g :: "'a \<Rightarrow> real"
   2.212 -  assumes "f \<in> borel_measurable M"
   2.213 -  assumes "g \<in> borel_measurable M"
   2.214 -  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
   2.215 -  unfolding max_def by (auto intro!: assms measurable_If)
   2.216 +lemma borel_measurable_max[measurable (raw)]:
   2.217 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: real) \<in> borel_measurable M"
   2.218 +  by (simp add: max_def)
   2.219  
   2.220 -lemma borel_measurable_min[intro, simp, measurable (raw)]:
   2.221 -  fixes f g :: "'a \<Rightarrow> real"
   2.222 -  assumes "f \<in> borel_measurable M"
   2.223 -  assumes "g \<in> borel_measurable M"
   2.224 -  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
   2.225 -  unfolding min_def by (auto intro!: assms measurable_If)
   2.226 +lemma borel_measurable_min[measurable (raw)]:
   2.227 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: real) \<in> borel_measurable M"
   2.228 +  by (simp add: min_def)
   2.229  
   2.230 -lemma borel_measurable_abs[simp, intro, measurable (raw)]:
   2.231 -  assumes "f \<in> borel_measurable M"
   2.232 -  shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
   2.233 -proof -
   2.234 -  have *: "\<And>x. \<bar>f x\<bar> = max 0 (f x) + max 0 (- f x)" by (simp add: max_def)
   2.235 -  show ?thesis unfolding * using assms by auto
   2.236 -qed
   2.237 +lemma borel_measurable_abs[measurable (raw)]:
   2.238 +  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
   2.239 +  unfolding abs_real_def by simp
   2.240  
   2.241 -lemma borel_measurable_nth[simp, intro, measurable (raw)]:
   2.242 +lemma borel_measurable_nth[measurable (raw)]:
   2.243    "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
   2.244 -  using borel_measurable_euclidean_component'
   2.245 -  unfolding nth_conv_component by auto
   2.246 +  by (simp add: nth_conv_component)
   2.247  
   2.248  lemma convex_measurable:
   2.249    fixes a b :: real
   2.250 @@ -843,7 +818,7 @@
   2.251    finally show ?thesis .
   2.252  qed
   2.253  
   2.254 -lemma borel_measurable_ln[simp, intro, measurable (raw)]:
   2.255 +lemma borel_measurable_ln[measurable (raw)]:
   2.256    assumes f: "f \<in> borel_measurable M"
   2.257    shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
   2.258  proof -
   2.259 @@ -864,7 +839,7 @@
   2.260    finally show ?thesis .
   2.261  qed
   2.262  
   2.263 -lemma borel_measurable_log[simp, intro, measurable (raw)]:
   2.264 +lemma borel_measurable_log[measurable (raw)]:
   2.265    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
   2.266    unfolding log_def by auto
   2.267  
   2.268 @@ -902,17 +877,17 @@
   2.269  lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
   2.270    by simp
   2.271  
   2.272 -lemma borel_measurable_real_natfloor[intro, simp]:
   2.273 +lemma borel_measurable_real_natfloor:
   2.274    "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
   2.275    by simp
   2.276  
   2.277  subsection "Borel space on the extended reals"
   2.278  
   2.279 -lemma borel_measurable_ereal[simp, intro, measurable (raw)]:
   2.280 +lemma borel_measurable_ereal[measurable (raw)]:
   2.281    assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
   2.282    using continuous_on_ereal f by (rule borel_measurable_continuous_on)
   2.283  
   2.284 -lemma borel_measurable_real_of_ereal[simp, intro, measurable (raw)]:
   2.285 +lemma borel_measurable_real_of_ereal[measurable (raw)]:
   2.286    fixes f :: "'a \<Rightarrow> ereal" 
   2.287    assumes f: "f \<in> borel_measurable M"
   2.288    shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
   2.289 @@ -937,10 +912,10 @@
   2.290  qed
   2.291  
   2.292  lemma
   2.293 -  fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M"
   2.294 -  shows borel_measurable_ereal_abs[intro, simp, measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
   2.295 -    and borel_measurable_ereal_inverse[simp, intro, measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
   2.296 -    and borel_measurable_uminus_ereal[intro, measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
   2.297 +  fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M"
   2.298 +  shows borel_measurable_ereal_abs[measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
   2.299 +    and borel_measurable_ereal_inverse[measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
   2.300 +    and borel_measurable_uminus_ereal[measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
   2.301    by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
   2.302  
   2.303  lemma borel_measurable_uminus_eq_ereal[simp]:
   2.304 @@ -968,15 +943,18 @@
   2.305      by (subst *) (simp del: space_borel split del: split_if)
   2.306  qed
   2.307  
   2.308 -lemma
   2.309 +lemma [measurable]:
   2.310    fixes f g :: "'a \<Rightarrow> ereal"
   2.311    assumes f: "f \<in> borel_measurable M"
   2.312    assumes g: "g \<in> borel_measurable M"
   2.313 -  shows borel_measurable_ereal_le[intro,simp,measurable(raw)]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
   2.314 -    and borel_measurable_ereal_less[intro,simp,measurable(raw)]: "{x \<in> space M. f x < g x} \<in> sets M"
   2.315 -    and borel_measurable_ereal_eq[intro,simp,measurable(raw)]: "{w \<in> space M. f w = g w} \<in> sets M"
   2.316 -    and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
   2.317 -  using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg)
   2.318 +  shows borel_measurable_ereal_le: "{x \<in> space M. f x \<le> g x} \<in> sets M"
   2.319 +    and borel_measurable_ereal_less: "{x \<in> space M. f x < g x} \<in> sets M"
   2.320 +    and borel_measurable_ereal_eq: "{w \<in> space M. f w = g w} \<in> sets M"
   2.321 +  using f g by (simp_all add: set_Collect_ereal2)
   2.322 +
   2.323 +lemma borel_measurable_ereal_neq:
   2.324 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> {w \<in> space M. f w \<noteq> (g w :: ereal)} \<in> sets M"
   2.325 +  by simp
   2.326  
   2.327  lemma borel_measurable_ereal_iff:
   2.328    shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
   2.329 @@ -1102,24 +1080,24 @@
   2.330      and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
   2.331    using f by auto
   2.332  
   2.333 -lemma [intro, simp, measurable(raw)]:
   2.334 +lemma [measurable(raw)]:
   2.335    fixes f :: "'a \<Rightarrow> ereal"
   2.336 -  assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   2.337 +  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   2.338    shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
   2.339      and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
   2.340      and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
   2.341      and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
   2.342 -  by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def)
   2.343 +  by (simp_all add: borel_measurable_ereal2 min_def max_def)
   2.344  
   2.345 -lemma [simp, intro, measurable(raw)]:
   2.346 +lemma [measurable(raw)]:
   2.347    fixes f g :: "'a \<Rightarrow> ereal"
   2.348    assumes "f \<in> borel_measurable M"
   2.349    assumes "g \<in> borel_measurable M"
   2.350    shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   2.351      and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
   2.352 -  unfolding minus_ereal_def divide_ereal_def using assms by auto
   2.353 +  using assms by (simp_all add: minus_ereal_def divide_ereal_def)
   2.354  
   2.355 -lemma borel_measurable_ereal_setsum[simp, intro,measurable (raw)]:
   2.356 +lemma borel_measurable_ereal_setsum[measurable (raw)]:
   2.357    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   2.358    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   2.359    shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
   2.360 @@ -1129,7 +1107,7 @@
   2.361      by induct auto
   2.362  qed simp
   2.363  
   2.364 -lemma borel_measurable_ereal_setprod[simp, intro,measurable (raw)]:
   2.365 +lemma borel_measurable_ereal_setprod[measurable (raw)]:
   2.366    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   2.367    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   2.368    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
   2.369 @@ -1138,7 +1116,7 @@
   2.370    thus ?thesis using assms by induct auto
   2.371  qed simp
   2.372  
   2.373 -lemma borel_measurable_SUP[simp, intro,measurable (raw)]:
   2.374 +lemma borel_measurable_SUP[measurable (raw)]:
   2.375    fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
   2.376    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   2.377    shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
   2.378 @@ -1151,7 +1129,7 @@
   2.379      using assms by auto
   2.380  qed
   2.381  
   2.382 -lemma borel_measurable_INF[simp, intro,measurable (raw)]:
   2.383 +lemma borel_measurable_INF[measurable (raw)]:
   2.384    fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
   2.385    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   2.386    shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
   2.387 @@ -1164,13 +1142,45 @@
   2.388      using assms by auto
   2.389  qed
   2.390  
   2.391 -lemma [simp, intro, measurable (raw)]:
   2.392 +lemma [measurable (raw)]:
   2.393    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   2.394    assumes "\<And>i. f i \<in> borel_measurable M"
   2.395    shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   2.396      and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
   2.397    unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
   2.398  
   2.399 +lemma sets_Collect_eventually_sequientially[measurable]:
   2.400 +  "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
   2.401 +  unfolding eventually_sequentially by simp
   2.402 +
   2.403 +lemma convergent_ereal:
   2.404 +  fixes X :: "nat \<Rightarrow> ereal"
   2.405 +  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
   2.406 +  using ereal_Liminf_eq_Limsup_iff[of sequentially]
   2.407 +  by (auto simp: convergent_def)
   2.408 +
   2.409 +lemma convergent_ereal_limsup:
   2.410 +  fixes X :: "nat \<Rightarrow> ereal"
   2.411 +  shows "convergent X \<Longrightarrow> limsup X = lim X"
   2.412 +  by (auto simp: convergent_def limI lim_imp_Limsup)
   2.413 +
   2.414 +lemma sets_Collect_ereal_convergent[measurable]: 
   2.415 +  fixes f :: "nat \<Rightarrow> 'a => ereal"
   2.416 +  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   2.417 +  shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
   2.418 +  unfolding convergent_ereal by auto
   2.419 +
   2.420 +lemma borel_measurable_extreal_lim[measurable (raw)]:
   2.421 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   2.422 +  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
   2.423 +  shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
   2.424 +proof -
   2.425 +  have "\<And>x. lim (\<lambda>i. f i x) = (if convergent (\<lambda>i. f i x) then limsup (\<lambda>i. f i x) else (THE i. False))"
   2.426 +    using convergent_ereal_limsup by (simp add: lim_def convergent_def)
   2.427 +  then show ?thesis
   2.428 +    by simp
   2.429 +qed
   2.430 +
   2.431  lemma borel_measurable_ereal_LIMSEQ:
   2.432    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   2.433    assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
   2.434 @@ -1179,17 +1189,14 @@
   2.435  proof -
   2.436    have "\<And>x. x \<in> space M \<Longrightarrow> u' x = liminf (\<lambda>n. u n x)"
   2.437      using u' by (simp add: lim_imp_Liminf[symmetric])
   2.438 -  then show ?thesis by (simp add: u cong: measurable_cong)
   2.439 +  with u show ?thesis by (simp cong: measurable_cong)
   2.440  qed
   2.441  
   2.442 -lemma borel_measurable_psuminf[simp, intro, measurable (raw)]:
   2.443 +lemma borel_measurable_extreal_suminf[measurable (raw)]:
   2.444    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   2.445 -  assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x"
   2.446 +  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
   2.447    shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
   2.448 -  apply (subst measurable_cong)
   2.449 -  apply (subst suminf_ereal_eq_SUPR)
   2.450 -  apply (rule pos)
   2.451 -  using assms by auto
   2.452 +  unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
   2.453  
   2.454  section "LIMSEQ is borel measurable"
   2.455  
     3.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
     3.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
     3.3 @@ -56,7 +56,7 @@
     3.4  
     3.5  lemma merge_commute:
     3.6    "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)"
     3.7 -  by (auto simp: merge_def intro!: ext)
     3.8 +  by (force simp: merge_def)
     3.9  
    3.10  lemma Pi_cancel_merge_range[simp]:
    3.11    "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
    3.12 @@ -430,7 +430,7 @@
    3.13      by (auto simp add: sets_PiM intro!: sigma_sets_top)
    3.14  next
    3.15    assume "J \<noteq> {}" with assms show ?thesis
    3.16 -    by (auto simp add: sets_PiM prod_algebra_def intro!: sigma_sets.Basic)
    3.17 +    by (force simp add: sets_PiM prod_algebra_def)
    3.18  qed
    3.19  
    3.20  lemma measurable_PiM:
    3.21 @@ -475,24 +475,12 @@
    3.22    finally show "f -` A \<inter> space N \<in> sets N" .
    3.23  qed (auto simp: space)
    3.24  
    3.25 -lemma sets_PiM_I_finite[simp, intro]:
    3.26 +lemma sets_PiM_I_finite[measurable]:
    3.27    assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
    3.28    shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
    3.29    using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto
    3.30  
    3.31 -lemma measurable_component_update:
    3.32 -  assumes "x \<in> space (Pi\<^isub>M I M)" and "i \<notin> I"
    3.33 -  shows "(\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \<in> _")
    3.34 -proof (intro measurable_PiM_single)
    3.35 -  fix j A assume "j \<in> insert i I" "A \<in> sets (M j)"
    3.36 -  moreover have "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} =
    3.37 -    (if i = j then space (M i) \<inter> A else if x j \<in> A then space (M i) else {})"
    3.38 -    by auto
    3.39 -  ultimately show "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} \<in> sets (M i)"
    3.40 -    by auto
    3.41 -qed (insert sets_into_space assms, auto simp: space_PiM)
    3.42 -
    3.43 -lemma measurable_component_singleton:
    3.44 +lemma measurable_component_singleton[measurable (raw)]:
    3.45    assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
    3.46  proof (unfold measurable_def, intro CollectI conjI ballI)
    3.47    fix A assume "A \<in> sets (M i)"
    3.48 @@ -503,7 +491,7 @@
    3.49      using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
    3.50  qed (insert `i \<in> I`, auto simp: space_PiM)
    3.51  
    3.52 -lemma measurable_add_dim:
    3.53 +lemma measurable_add_dim[measurable]:
    3.54    "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
    3.55      (is "?f \<in> measurable ?P ?I")
    3.56  proof (rule measurable_PiM_single)
    3.57 @@ -517,7 +505,11 @@
    3.58    finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
    3.59  qed (auto simp: space_pair_measure space_PiM)
    3.60  
    3.61 -lemma measurable_merge:
    3.62 +lemma measurable_component_update:
    3.63 +  "x \<in> space (Pi\<^isub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)"
    3.64 +  by simp
    3.65 +
    3.66 +lemma measurable_merge[measurable]:
    3.67    "merge I J \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
    3.68      (is "?f \<in> measurable ?P ?U")
    3.69  proof (rule measurable_PiM_single)
    3.70 @@ -531,7 +523,7 @@
    3.71    finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
    3.72  qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
    3.73  
    3.74 -lemma measurable_restrict:
    3.75 +lemma measurable_restrict[measurable (raw)]:
    3.76    assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
    3.77    shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^isub>M I M)"
    3.78  proof (rule measurable_PiM_single)
    3.79 @@ -542,6 +534,31 @@
    3.80      using A X by (auto intro!: measurable_sets)
    3.81  qed (insert X, auto dest: measurable_space)
    3.82  
    3.83 +lemma sets_in_Pi_aux:
    3.84 +  "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
    3.85 +  {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
    3.86 +  by (simp add: subset_eq Pi_iff)
    3.87 +
    3.88 +lemma sets_in_Pi[measurable (raw)]:
    3.89 +  "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
    3.90 +  (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
    3.91 +  Sigma_Algebra.pred N (\<lambda>x. f x \<in> Pi I F)"
    3.92 +  unfolding pred_def
    3.93 +  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
    3.94 +
    3.95 +lemma sets_in_extensional_aux:
    3.96 +  "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
    3.97 +proof -
    3.98 +  have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
    3.99 +    by (auto simp add: extensional_def space_PiM)
   3.100 +  then show ?thesis by simp
   3.101 +qed
   3.102 +
   3.103 +lemma sets_in_extensional[measurable (raw)]:
   3.104 +  "f \<in> measurable N (PiM I M) \<Longrightarrow> Sigma_Algebra.pred N (\<lambda>x. f x \<in> extensional I)"
   3.105 +  unfolding pred_def
   3.106 +  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
   3.107 +
   3.108  locale product_sigma_finite =
   3.109    fixes M :: "'i \<Rightarrow> 'a measure"
   3.110    assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
   3.111 @@ -665,7 +682,7 @@
   3.112    qed (auto intro!: setprod_cong)
   3.113    with insert show ?case
   3.114      by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
   3.115 -qed (simp add: emeasure_PiM_empty)
   3.116 +qed simp
   3.117  
   3.118  lemma (in product_sigma_finite) sigma_finite: 
   3.119    assumes "finite I"
   3.120 @@ -759,18 +776,18 @@
   3.121      show "emeasure ?P (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
   3.122    next
   3.123      fix A assume A: "A \<in> prod_algebra (I \<union> J) M"
   3.124 -    with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>I \<union> J. F i \<in> sets (M i)"
   3.125 +    with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>J. F i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
   3.126        by (auto simp add: prod_algebra_eq_finite)
   3.127      let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M"
   3.128      let ?X = "?g -` A \<inter> space ?B"
   3.129      have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)"
   3.130 -      using F[rule_format, THEN sets_into_space] by (auto simp: space_PiM)
   3.131 +      using F[rule_format, THEN sets_into_space] by (force simp: space_PiM)+
   3.132      then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
   3.133        unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
   3.134      have "emeasure ?D A = emeasure ?B ?X"
   3.135        using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
   3.136      also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
   3.137 -      using `finite J` `finite I` F X
   3.138 +      using `finite J` `finite I` F unfolding X
   3.139        by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
   3.140      also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
   3.141        using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
   3.142 @@ -1013,8 +1030,7 @@
   3.143  
   3.144  lemma sets_Collect_single:
   3.145    "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^isub>M I M). x i \<in> A } \<in> sets (Pi\<^isub>M I M)"
   3.146 -  unfolding sets_PiM_single
   3.147 -  by (auto intro!: sigma_sets.Basic exI[of _ i] exI[of _ A]) (auto simp: space_PiM)
   3.148 +  by simp
   3.149  
   3.150  lemma sigma_prod_algebra_sigma_eq_infinite:
   3.151    fixes E :: "'i \<Rightarrow> 'a set set"
   3.152 @@ -1127,7 +1143,7 @@
   3.153      by (simp add: P_closed)
   3.154    show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
   3.155      using `finite I`
   3.156 -    by (auto intro!: sigma_sets_subset simp: E_generates P_def)
   3.157 +    by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
   3.158  qed
   3.159  
   3.160  end
     4.1 --- a/src/HOL/Probability/Independent_Family.thy	Fri Nov 02 14:23:40 2012 +0100
     4.2 +++ b/src/HOL/Probability/Independent_Family.thy	Fri Nov 02 14:23:54 2012 +0100
     4.3 @@ -1004,6 +1004,9 @@
     4.4    "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
     4.5    using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def)
     4.6  
     4.7 +lemma measurable_id_prod[measurable (raw)]: "i = j \<Longrightarrow> (\<lambda>x. x) \<in> measurable (M i) (M j)"
     4.8 +  by simp
     4.9 +
    4.10  lemma (in product_sigma_finite) distr_component:
    4.11    "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
    4.12  proof (intro measure_eqI[symmetric])
    4.13 @@ -1015,15 +1018,10 @@
    4.14    fix A assume A: "A \<in> sets ?P"
    4.15    then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)" 
    4.16      by simp
    4.17 -  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) x \<partial>M i)" 
    4.18 -    apply (subst product_positive_integral_singleton[symmetric])
    4.19 -    apply (force intro!: measurable_restrict measurable_sets A)
    4.20 -    apply (auto intro!: positive_integral_cong simp: space_PiM indicator_def simp: eq)
    4.21 -    done
    4.22 -  also have "\<dots> = emeasure (M i) ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i))"
    4.23 -    by (force intro!: measurable_restrict measurable_sets A positive_integral_indicator)
    4.24 +  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)" 
    4.25 +    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
    4.26    also have "\<dots> = emeasure ?D A"
    4.27 -    using A by (auto intro!: emeasure_distr[symmetric] measurable_restrict) 
    4.28 +    using A by (simp add: product_positive_integral_singleton emeasure_distr)
    4.29    finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
    4.30  qed simp
    4.31  
     5.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
     5.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
     5.3 @@ -99,7 +99,8 @@
     5.4    
     5.5    fix X assume "X \<in> ?J"
     5.6    then obtain E where [simp]: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
     5.7 -  with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)" by auto
     5.8 +  with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)"
     5.9 +    by simp
    5.10  
    5.11    have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
    5.12      using E by (simp add: J.measure_times)
    5.13 @@ -190,7 +191,7 @@
    5.14        unfolding sets_PiM
    5.15      proof (safe intro!: sigma_sets_subseteq)
    5.16        fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
    5.17 -        by (auto intro!: generatorI' elim!: prod_algebraE)
    5.18 +        by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
    5.19      qed
    5.20    qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
    5.21  qed
    5.22 @@ -242,10 +243,8 @@
    5.23  qed
    5.24  
    5.25  lemma (in product_prob_space) merge_sets:
    5.26 -  assumes "J \<inter> K = {}" and A: "A \<in> sets (Pi\<^isub>M (J \<union> K) M)" and x: "x \<in> space (Pi\<^isub>M J M)"
    5.27 -  shows "(\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
    5.28 -  by (rule measurable_sets[OF _ A] measurable_compose[OF measurable_Pair measurable_merge]  
    5.29 -           measurable_const x measurable_ident)+
    5.30 +  "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
    5.31 +  by simp
    5.32  
    5.33  lemma (in product_prob_space) merge_emb:
    5.34    assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M J M)"
    5.35 @@ -622,7 +621,7 @@
    5.36      then show "emb I J (Pi\<^isub>E J X) \<in> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
    5.37        by (auto simp: Pi_iff prod_emb_def dest: sets_into_space)
    5.38      have "emb I J (Pi\<^isub>E J X) \<in> generator"
    5.39 -      using J `I \<noteq> {}` by (intro generatorI') auto
    5.40 +      using J `I \<noteq> {}` by (intro generatorI') (auto simp: Pi_iff)
    5.41      then have "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))"
    5.42        using \<mu> by simp
    5.43      also have "\<dots> = (\<Prod> j\<in>J. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
     6.1 --- a/src/HOL/Probability/Information.thy	Fri Nov 02 14:23:40 2012 +0100
     6.2 +++ b/src/HOL/Probability/Information.thy	Fri Nov 02 14:23:54 2012 +0100
     6.3 @@ -84,10 +84,14 @@
     6.4    shows "entropy_density b M N \<in> borel_measurable M"
     6.5  proof -
     6.6    from borel_measurable_RN_deriv[OF ac] b_gt_1 show ?thesis
     6.7 -    unfolding entropy_density_def
     6.8 -    by (intro measurable_comp) auto
     6.9 +    unfolding entropy_density_def by auto
    6.10  qed
    6.11  
    6.12 +lemma borel_measurable_RN_deriv_density[measurable (raw)]:
    6.13 +  "f \<in> borel_measurable M \<Longrightarrow> RN_deriv M (density M f) \<in> borel_measurable M"
    6.14 +  using borel_measurable_RN_deriv_density[of "\<lambda>x. max 0 (f x )" M]
    6.15 +  by (simp add: density_max_0[symmetric])
    6.16 +
    6.17  lemma (in sigma_finite_measure) KL_density:
    6.18    fixes f :: "'a \<Rightarrow> real"
    6.19    assumes "1 < b"
    6.20 @@ -97,7 +101,7 @@
    6.21  proof (subst integral_density)
    6.22    show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
    6.23      using f
    6.24 -    by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density)
    6.25 +    by (auto simp: comp_def entropy_density_def)
    6.26    have "density M (RN_deriv M (density M f)) = density M f"
    6.27      using f by (intro density_RN_deriv_density) auto
    6.28    then have eq: "AE x in M. RN_deriv M (density M f) x = f x"
    6.29 @@ -366,7 +370,7 @@
    6.30    shows "AE x in P. 0 \<le> g (T x)"
    6.31    using g
    6.32    apply (subst AE_distr_iff[symmetric, OF T(1)])
    6.33 -  apply (simp add: distributed_borel_measurable)
    6.34 +  apply simp
    6.35    apply (rule absolutely_continuous_AE[OF _ T(2)])
    6.36    apply simp
    6.37    apply (simp add: distributed_AE)
    6.38 @@ -409,7 +413,7 @@
    6.39  lemma distributed_integrable:
    6.40    "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
    6.41      integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
    6.42 -  by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
    6.43 +  by (auto simp: distributed_real_AE
    6.44                      distributed_distr_eq_density[symmetric] integral_density[symmetric] integrable_distr_eq)
    6.45    
    6.46  lemma distributed_transform_integrable:
    6.47 @@ -446,7 +450,7 @@
    6.48    shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))"
    6.49    using assms unfolding finite_entropy_def
    6.50    using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"]
    6.51 -  by (auto dest!: distributed_real_measurable)
    6.52 +  by auto
    6.53  
    6.54  subsection {* Mutual Information *}
    6.55  
    6.56 @@ -464,7 +468,7 @@
    6.57        mutual_information b S T X Y = 0)"
    6.58    unfolding indep_var_distribution_eq
    6.59  proof safe
    6.60 -  assume rv: "random_variable S X" "random_variable T Y"
    6.61 +  assume rv[measurable]: "random_variable S X" "random_variable T Y"
    6.62  
    6.63    interpret X: prob_space "distr M S X"
    6.64      by (rule prob_space_distr) fact
    6.65 @@ -474,7 +478,7 @@
    6.66    interpret P: information_space P b unfolding P_def by default (rule b_gt_1)
    6.67  
    6.68    interpret Q: prob_space Q unfolding Q_def
    6.69 -    by (rule prob_space_distr) (simp add: comp_def measurable_pair_iff rv)
    6.70 +    by (rule prob_space_distr) simp
    6.71  
    6.72    { assume "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
    6.73      then have [simp]: "Q = P"  unfolding Q_def P_def by simp
    6.74 @@ -536,9 +540,9 @@
    6.75      using Fxy by (auto simp: finite_entropy_def)
    6.76  
    6.77    have X: "random_variable S X"
    6.78 -    using Px by (auto simp: distributed_def finite_entropy_def)
    6.79 +    using Px by auto
    6.80    have Y: "random_variable T Y"
    6.81 -    using Py by (auto simp: distributed_def finite_entropy_def)
    6.82 +    using Py by auto
    6.83    interpret S: sigma_finite_measure S by fact
    6.84    interpret T: sigma_finite_measure T by fact
    6.85    interpret ST: pair_sigma_finite S T ..
    6.86 @@ -568,7 +572,6 @@
    6.87      show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
    6.88        "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
    6.89        using Px Py by (auto simp: distributed_def)
    6.90 -    show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
    6.91      show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
    6.92    qed (fact | simp)+
    6.93    
    6.94 @@ -675,7 +678,6 @@
    6.95      show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
    6.96        "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
    6.97        using Px Py by (auto simp: distributed_def)
    6.98 -    show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
    6.99      show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
   6.100    qed (fact | simp)+
   6.101    
   6.102 @@ -1009,11 +1011,11 @@
   6.103  
   6.104  lemma (in information_space)
   6.105    assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
   6.106 -  assumes Px: "distributed M S X Px"
   6.107 -  assumes Pz: "distributed M P Z Pz"
   6.108 -  assumes Pyz: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
   6.109 -  assumes Pxz: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
   6.110 -  assumes Pxyz: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
   6.111 +  assumes Px[measurable]: "distributed M S X Px"
   6.112 +  assumes Pz[measurable]: "distributed M P Z Pz"
   6.113 +  assumes Pyz[measurable]: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
   6.114 +  assumes Pxz[measurable]: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
   6.115 +  assumes Pxyz[measurable]: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
   6.116    assumes I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
   6.117    assumes I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
   6.118    shows conditional_mutual_information_generic_eq: "conditional_mutual_information b S T P X Y Z
   6.119 @@ -1033,56 +1035,38 @@
   6.120    have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
   6.121    have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
   6.122      using Pyz by (simp add: distributed_measurable)
   6.123 -
   6.124 -  have Pxyz_f: "\<And>M f. f \<in> measurable M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. Pxyz (f x)) \<in> borel_measurable M"
   6.125 -    using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
   6.126 -
   6.127 -  { fix f g h M
   6.128 -    assume f: "f \<in> measurable M S" and g: "g \<in> measurable M P" and h: "h \<in> measurable M (S \<Otimes>\<^isub>M P)"
   6.129 -    from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
   6.130 -         measurable_comp[OF f Px[THEN distributed_real_measurable]]
   6.131 -         measurable_comp[OF g Pz[THEN distributed_real_measurable]]
   6.132 -    have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
   6.133 -      by (simp add: comp_def b_gt_1) }
   6.134 -  note borel_log = this
   6.135 -
   6.136 -  have measurable_cut: "(\<lambda>(x, y, z). (x, z)) \<in> measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (S \<Otimes>\<^isub>M P)"
   6.137 -    by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
   6.138    
   6.139    from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
   6.140      distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"
   6.141 -    by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
   6.142 +    by (simp add: comp_def distr_distr)
   6.143  
   6.144    have "mutual_information b S P X Z =
   6.145      (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
   6.146      by (rule mutual_information_distr[OF S P Px Pz Pxz])
   6.147    also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
   6.148      using b_gt_1 Pxz Px Pz
   6.149 -    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
   6.150 -       (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
   6.151 -             dest!: distributed_real_measurable)
   6.152 +    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"]) (auto simp: split_beta')
   6.153    finally have mi_eq:
   6.154      "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .
   6.155    
   6.156    have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
   6.157      by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
   6.158    moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
   6.159 -    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
   6.160 +    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) auto
   6.161    moreover have ae3: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
   6.162 -    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
   6.163 +    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) auto
   6.164    moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
   6.165 -    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
   6.166 +    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) auto
   6.167    moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
   6.168 -    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
   6.169 +    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
   6.170    moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
   6.171 -    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
   6.172 +    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
   6.173    moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
   6.174 -    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: measurable_snd'' TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
   6.175 +    using Pz Pz[THEN distributed_real_measurable]
   6.176 +    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
   6.177    moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
   6.178      using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
   6.179 -    using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
   6.180 -    using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
   6.181 -    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
   6.182 +    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure)
   6.183    moreover note Pxyz[THEN distributed_real_AE]
   6.184    ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
   6.185      Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
   6.186 @@ -1110,52 +1094,36 @@
   6.187    let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
   6.188    interpret P: prob_space ?P
   6.189      unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
   6.190 -    using distributed_measurable[OF Pxyz] by (rule prob_space_distr)
   6.191 +    by (rule prob_space_distr) simp
   6.192  
   6.193    let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
   6.194    interpret Q: prob_space ?Q
   6.195      unfolding distributed_distr_eq_density[OF Pyz, symmetric]
   6.196 -    using distributed_measurable[OF Pyz] by (rule prob_space_distr)
   6.197 +    by (rule prob_space_distr) simp
   6.198  
   6.199    let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
   6.200  
   6.201    from subdensity_real[of snd, OF _ Pyz Pz]
   6.202    have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
   6.203    have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
   6.204 -    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
   6.205 +    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
   6.206  
   6.207    have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
   6.208      using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
   6.209 -    apply (intro TP.AE_pair_measure)
   6.210 -    apply (auto simp: comp_def measurable_split_conv
   6.211 -                intro!: measurable_snd'' measurable_fst'' borel_measurable_ereal_eq borel_measurable_ereal
   6.212 -                        S.borel_measurable_positive_integral measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
   6.213 -                        measurable_Pair
   6.214 -                dest: distributed_real_AE distributed_real_measurable)
   6.215 -    done
   6.216 +    by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
   6.217  
   6.218 -  note M = borel_measurable_divide borel_measurable_diff borel_measurable_times borel_measurable_ereal
   6.219 -           measurable_compose[OF _ measurable_snd]
   6.220 -           measurable_Pair
   6.221 -           measurable_compose[OF _ Pxyz[THEN distributed_real_measurable]]
   6.222 -           measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
   6.223 -           measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
   6.224 -           measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
   6.225 -           measurable_compose[OF _ Px[THEN distributed_real_measurable]]
   6.226 -           TP.borel_measurable_positive_integral
   6.227    have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
   6.228      apply (subst positive_integral_density)
   6.229 -    apply (rule distributed_borel_measurable[OF Pxyz])
   6.230 +    apply simp
   6.231      apply (rule distributed_AE[OF Pxyz])
   6.232 -    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
   6.233 +    apply auto []
   6.234      apply (rule positive_integral_mono_AE)
   6.235      using ae5 ae6 ae7 ae8
   6.236      apply eventually_elim
   6.237      apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
   6.238      done
   6.239    also have "\<dots> = (\<integral>\<^isup>+(y, z). \<integral>\<^isup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^isub>M P)"
   6.240 -    by (subst STP.positive_integral_snd_measurable[symmetric])
   6.241 -       (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M)
   6.242 +    by (subst STP.positive_integral_snd_measurable[symmetric]) (auto simp add: split_beta')
   6.243    also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
   6.244      apply (rule positive_integral_cong_AE)
   6.245      using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
   6.246 @@ -1164,44 +1132,41 @@
   6.247      fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
   6.248        "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
   6.249      then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
   6.250 -      apply (subst positive_integral_multc)
   6.251 -      apply (auto intro!: borel_measurable_ereal divide_nonneg_nonneg
   6.252 -                          measurable_compose[OF _ Pxz[THEN distributed_real_measurable]] measurable_Pair
   6.253 -                  split: prod.split)
   6.254 -      done
   6.255 +      by (subst positive_integral_multc)
   6.256 +         (auto intro!: divide_nonneg_nonneg split: prod.split)
   6.257    qed
   6.258    also have "\<dots> = 1"
   6.259      using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
   6.260 -    by (subst positive_integral_density[symmetric]) (auto intro!: M)
   6.261 +    by (subst positive_integral_density[symmetric]) auto
   6.262    finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
   6.263    also have "\<dots> < \<infinity>" by simp
   6.264    finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
   6.265  
   6.266    have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
   6.267      apply (subst positive_integral_density)
   6.268 -    apply (rule distributed_borel_measurable[OF Pxyz])
   6.269 +    apply simp
   6.270      apply (rule distributed_AE[OF Pxyz])
   6.271 -    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
   6.272 +    apply auto []
   6.273      apply (simp add: split_beta')
   6.274    proof
   6.275      let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
   6.276      assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
   6.277      then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
   6.278 -      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: M borel_measurable_ereal measurable_If)
   6.279 +      by (intro positive_integral_0_iff_AE[THEN iffD1]) auto
   6.280      then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
   6.281        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   6.282        by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
   6.283      then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
   6.284        by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
   6.285      with P.emeasure_space_1 show False
   6.286 -      by (subst (asm) emeasure_density) (auto intro!: M cong: positive_integral_cong)
   6.287 +      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
   6.288    qed
   6.289  
   6.290    have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
   6.291      apply (rule positive_integral_0_iff_AE[THEN iffD2])
   6.292 -    apply (auto intro!: M simp: split_beta') []
   6.293 +    apply simp
   6.294      apply (subst AE_density)
   6.295 -    apply (auto intro!: M simp: split_beta') []
   6.296 +    apply simp
   6.297      using ae5 ae6 ae7 ae8
   6.298      apply eventually_elim
   6.299      apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
   6.300 @@ -1210,7 +1175,7 @@
   6.301    have I3: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
   6.302      apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
   6.303      using ae
   6.304 -    apply (auto intro!: M simp: split_beta')
   6.305 +    apply (auto simp: split_beta')
   6.306      done
   6.307  
   6.308    have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
   6.309 @@ -1230,15 +1195,15 @@
   6.310        by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
   6.311      show "integrable ?P ?f"
   6.312        unfolding integrable_def 
   6.313 -      using fin neg by (auto intro!: M simp: split_beta')
   6.314 +      using fin neg by (auto simp: split_beta')
   6.315      show "integrable ?P (\<lambda>x. - log b (?f x))"
   6.316        apply (subst integral_density)
   6.317 -      apply (auto intro!: M) []
   6.318 -      apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
   6.319 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   6.320 +      apply simp
   6.321 +      apply (auto intro!: distributed_real_AE[OF Pxyz]) []
   6.322 +      apply simp
   6.323        apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
   6.324 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   6.325 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   6.326 +      apply simp
   6.327 +      apply simp
   6.328        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   6.329        apply eventually_elim
   6.330        apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
   6.331 @@ -1247,9 +1212,9 @@
   6.332    also have "\<dots> = conditional_mutual_information b S T P X Y Z"
   6.333      unfolding `?eq`
   6.334      apply (subst integral_density)
   6.335 -    apply (auto intro!: M) []
   6.336 -    apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
   6.337 -    apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   6.338 +    apply simp
   6.339 +    apply (auto intro!: distributed_real_AE[OF Pxyz]) []
   6.340 +    apply simp
   6.341      apply (intro integral_cong_AE)
   6.342      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   6.343      apply eventually_elim
   6.344 @@ -1271,11 +1236,11 @@
   6.345      = (\<integral>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" (is "?eq")
   6.346      and conditional_mutual_information_generic_nonneg': "0 \<le> conditional_mutual_information b S T P X Y Z" (is "?nonneg")
   6.347  proof -
   6.348 -  note Px = Fx[THEN finite_entropy_distributed]
   6.349 -  note Pz = Fz[THEN finite_entropy_distributed]
   6.350 -  note Pyz = Fyz[THEN finite_entropy_distributed]
   6.351 -  note Pxz = Fxz[THEN finite_entropy_distributed]
   6.352 -  note Pxyz = Fxyz[THEN finite_entropy_distributed]
   6.353 +  note Px = Fx[THEN finite_entropy_distributed, measurable]
   6.354 +  note Pz = Fz[THEN finite_entropy_distributed, measurable]
   6.355 +  note Pyz = Fyz[THEN finite_entropy_distributed, measurable]
   6.356 +  note Pxz = Fxz[THEN finite_entropy_distributed, measurable]
   6.357 +  note Pxyz = Fxyz[THEN finite_entropy_distributed, measurable]
   6.358  
   6.359    interpret S: sigma_finite_measure S by fact
   6.360    interpret T: sigma_finite_measure T by fact
   6.361 @@ -1288,27 +1253,10 @@
   6.362    interpret TPS: pair_sigma_finite "T \<Otimes>\<^isub>M P" S ..
   6.363    have TP: "sigma_finite_measure (T \<Otimes>\<^isub>M P)" ..
   6.364    have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
   6.365 -  have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
   6.366 -    using Pyz by (simp add: distributed_measurable)
   6.367  
   6.368 -  have Pxyz_f: "\<And>M f. f \<in> measurable M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. Pxyz (f x)) \<in> borel_measurable M"
   6.369 -    using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
   6.370 -
   6.371 -  { fix f g h M
   6.372 -    assume f: "f \<in> measurable M S" and g: "g \<in> measurable M P" and h: "h \<in> measurable M (S \<Otimes>\<^isub>M P)"
   6.373 -    from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
   6.374 -         measurable_comp[OF f Px[THEN distributed_real_measurable]]
   6.375 -         measurable_comp[OF g Pz[THEN distributed_real_measurable]]
   6.376 -    have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
   6.377 -      by (simp add: comp_def b_gt_1) }
   6.378 -  note borel_log = this
   6.379 -
   6.380 -  have measurable_cut: "(\<lambda>(x, y, z). (x, z)) \<in> measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (S \<Otimes>\<^isub>M P)"
   6.381 -    by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
   6.382 -  
   6.383    from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
   6.384      distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"
   6.385 -    by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
   6.386 +    by (simp add: distr_distr comp_def)
   6.387  
   6.388    have "mutual_information b S P X Z =
   6.389      (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
   6.390 @@ -1316,29 +1264,26 @@
   6.391    also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
   6.392      using b_gt_1 Pxz Px Pz
   6.393      by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
   6.394 -       (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
   6.395 -             dest!: distributed_real_measurable)
   6.396 +       (auto simp: split_beta')
   6.397    finally have mi_eq:
   6.398      "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .
   6.399    
   6.400    have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
   6.401      by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
   6.402    moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
   6.403 -    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
   6.404 +    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) auto
   6.405    moreover have ae3: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
   6.406 -    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
   6.407 +    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) auto
   6.408    moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
   6.409 -    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
   6.410 +    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) auto
   6.411    moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
   6.412 -    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
   6.413 +    using Px by (intro STP.AE_pair_measure) (auto dest: distributed_real_AE)
   6.414    moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
   6.415 -    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
   6.416 +    using Pyz by (intro STP.AE_pair_measure) (auto dest: distributed_real_AE)
   6.417    moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
   6.418 -    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: measurable_snd'' TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
   6.419 +    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
   6.420    moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
   6.421      using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
   6.422 -    using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
   6.423 -    using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
   6.424      by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
   6.425    moreover note ae9 = Pxyz[THEN distributed_real_AE]
   6.426    ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
   6.427 @@ -1364,8 +1309,7 @@
   6.428      using finite_entropy_integrable_transform[OF Fyz Pxyz, of snd]
   6.429      by simp
   6.430    moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z)))) \<in> borel_measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)"
   6.431 -    using Pxyz Px Pyz
   6.432 -    by (auto intro!: borel_measurable_times measurable_fst'' measurable_snd'' dest!: distributed_real_measurable simp: split_beta')
   6.433 +    using Pxyz Px Pyz by simp
   6.434    ultimately have I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
   6.435      apply (rule integrable_cong_AE_imp)
   6.436      using ae1 ae4 ae5 ae6 ae9
   6.437 @@ -1377,12 +1321,10 @@
   6.438      using finite_entropy_integrable_transform[OF Fxz Pxyz, of "\<lambda>x. (fst x, snd (snd x))"]
   6.439      using finite_entropy_integrable_transform[OF Fx Pxyz, of fst]
   6.440      using finite_entropy_integrable_transform[OF Fz Pxyz, of "snd \<circ> snd"]
   6.441 -    by (simp add: measurable_Pair measurable_snd'' comp_def)
   6.442 +    by simp
   6.443    moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z))) \<in> borel_measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)"
   6.444      using Pxyz Px Pz
   6.445 -    by (auto intro!: measurable_compose[OF _ distributed_real_measurable[OF Pxz]]
   6.446 -                     measurable_Pair borel_measurable_times measurable_fst'' measurable_snd''
   6.447 -             dest!: distributed_real_measurable simp: split_beta')
   6.448 +    by auto
   6.449    ultimately have I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
   6.450      apply (rule integrable_cong_AE_imp)
   6.451      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 ae9
   6.452 @@ -1399,45 +1341,27 @@
   6.453  
   6.454    let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
   6.455    interpret P: prob_space ?P
   6.456 -    unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
   6.457 -    using distributed_measurable[OF Pxyz] by (rule prob_space_distr)
   6.458 +    unfolding distributed_distr_eq_density[OF Pxyz, symmetric] by (rule prob_space_distr) simp
   6.459  
   6.460    let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
   6.461    interpret Q: prob_space ?Q
   6.462 -    unfolding distributed_distr_eq_density[OF Pyz, symmetric]
   6.463 -    using distributed_measurable[OF Pyz] by (rule prob_space_distr)
   6.464 +    unfolding distributed_distr_eq_density[OF Pyz, symmetric] by (rule prob_space_distr) simp
   6.465  
   6.466    let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
   6.467  
   6.468    from subdensity_real[of snd, OF _ Pyz Pz]
   6.469    have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
   6.470    have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
   6.471 -    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
   6.472 +    using Pz by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
   6.473  
   6.474    have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
   6.475      using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
   6.476 -    apply (intro TP.AE_pair_measure)
   6.477 -    apply (auto simp: comp_def measurable_split_conv
   6.478 -                intro!: measurable_snd'' measurable_fst'' borel_measurable_ereal_eq borel_measurable_ereal
   6.479 -                        S.borel_measurable_positive_integral measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
   6.480 -                        measurable_Pair
   6.481 -                dest: distributed_real_AE distributed_real_measurable)
   6.482 -    done
   6.483 -
   6.484 -  note M = borel_measurable_divide borel_measurable_diff borel_measurable_times borel_measurable_ereal
   6.485 -           measurable_compose[OF _ measurable_snd]
   6.486 -           measurable_Pair
   6.487 -           measurable_compose[OF _ Pxyz[THEN distributed_real_measurable]]
   6.488 -           measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
   6.489 -           measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
   6.490 -           measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
   6.491 -           measurable_compose[OF _ Px[THEN distributed_real_measurable]]
   6.492 -           TP.borel_measurable_positive_integral
   6.493 +    by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
   6.494    have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
   6.495      apply (subst positive_integral_density)
   6.496      apply (rule distributed_borel_measurable[OF Pxyz])
   6.497      apply (rule distributed_AE[OF Pxyz])
   6.498 -    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
   6.499 +    apply simp
   6.500      apply (rule positive_integral_mono_AE)
   6.501      using ae5 ae6 ae7 ae8
   6.502      apply eventually_elim
   6.503 @@ -1445,7 +1369,7 @@
   6.504      done
   6.505    also have "\<dots> = (\<integral>\<^isup>+(y, z). \<integral>\<^isup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^isub>M P)"
   6.506      by (subst STP.positive_integral_snd_measurable[symmetric])
   6.507 -       (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M)
   6.508 +       (auto simp add: split_beta')
   6.509    also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
   6.510      apply (rule positive_integral_cong_AE)
   6.511      using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
   6.512 @@ -1454,44 +1378,40 @@
   6.513      fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
   6.514        "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
   6.515      then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
   6.516 -      apply (subst positive_integral_multc)
   6.517 -      apply (auto intro!: borel_measurable_ereal divide_nonneg_nonneg
   6.518 -                          measurable_compose[OF _ Pxz[THEN distributed_real_measurable]] measurable_Pair
   6.519 -                  split: prod.split)
   6.520 -      done
   6.521 +      by (subst positive_integral_multc) (auto intro!: divide_nonneg_nonneg)
   6.522    qed
   6.523    also have "\<dots> = 1"
   6.524      using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
   6.525 -    by (subst positive_integral_density[symmetric]) (auto intro!: M)
   6.526 +    by (subst positive_integral_density[symmetric]) auto
   6.527    finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
   6.528    also have "\<dots> < \<infinity>" by simp
   6.529    finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
   6.530  
   6.531    have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
   6.532      apply (subst positive_integral_density)
   6.533 -    apply (rule distributed_borel_measurable[OF Pxyz])
   6.534 +    apply simp
   6.535      apply (rule distributed_AE[OF Pxyz])
   6.536 -    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
   6.537 +    apply simp
   6.538      apply (simp add: split_beta')
   6.539    proof
   6.540      let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
   6.541      assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
   6.542      then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
   6.543 -      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: M borel_measurable_ereal measurable_If)
   6.544 +      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
   6.545      then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
   6.546        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   6.547        by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
   6.548      then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
   6.549        by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
   6.550      with P.emeasure_space_1 show False
   6.551 -      by (subst (asm) emeasure_density) (auto intro!: M cong: positive_integral_cong)
   6.552 +      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
   6.553    qed
   6.554  
   6.555    have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
   6.556      apply (rule positive_integral_0_iff_AE[THEN iffD2])
   6.557 -    apply (auto intro!: M simp: split_beta') []
   6.558 +    apply (auto simp: split_beta') []
   6.559      apply (subst AE_density)
   6.560 -    apply (auto intro!: M simp: split_beta') []
   6.561 +    apply (auto simp: split_beta') []
   6.562      using ae5 ae6 ae7 ae8
   6.563      apply eventually_elim
   6.564      apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
   6.565 @@ -1500,7 +1420,7 @@
   6.566    have I3: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
   6.567      apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
   6.568      using ae
   6.569 -    apply (auto intro!: M simp: split_beta')
   6.570 +    apply (auto simp: split_beta')
   6.571      done
   6.572  
   6.573    have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
   6.574 @@ -1520,15 +1440,15 @@
   6.575        by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
   6.576      show "integrable ?P ?f"
   6.577        unfolding integrable_def 
   6.578 -      using fin neg by (auto intro!: M simp: split_beta')
   6.579 +      using fin neg by (auto simp: split_beta')
   6.580      show "integrable ?P (\<lambda>x. - log b (?f x))"
   6.581        apply (subst integral_density)
   6.582 -      apply (auto intro!: M) []
   6.583 -      apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
   6.584 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   6.585 +      apply simp
   6.586 +      apply (auto intro!: distributed_real_AE[OF Pxyz]) []
   6.587 +      apply simp
   6.588        apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
   6.589 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   6.590 -      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   6.591 +      apply simp
   6.592 +      apply simp
   6.593        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   6.594        apply eventually_elim
   6.595        apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
   6.596 @@ -1537,9 +1457,9 @@
   6.597    also have "\<dots> = conditional_mutual_information b S T P X Y Z"
   6.598      unfolding `?eq`
   6.599      apply (subst integral_density)
   6.600 -    apply (auto intro!: M) []
   6.601 -    apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
   6.602 -    apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   6.603 +    apply simp
   6.604 +    apply (auto intro!: distributed_real_AE[OF Pxyz]) []
   6.605 +    apply simp
   6.606      apply (intro integral_cong_AE)
   6.607      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   6.608      apply eventually_elim
   6.609 @@ -1633,8 +1553,8 @@
   6.610  lemma (in information_space) conditional_entropy_generic_eq:
   6.611    fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   6.612    assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
   6.613 -  assumes Py: "distributed M T Y Py"
   6.614 -  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   6.615 +  assumes Py[measurable]: "distributed M T Y Py"
   6.616 +  assumes Pxy[measurable]: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   6.617    shows "conditional_entropy b S T X Y = - (\<integral>(x, y). Pxy (x, y) * log b (Pxy (x, y) / Py y) \<partial>(S \<Otimes>\<^isub>M T))"
   6.618  proof -
   6.619    interpret S: sigma_finite_measure S by fact
     7.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:23:40 2012 +0100
     7.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:23:54 2012 +0100
     7.3 @@ -121,7 +121,7 @@
     7.4    shows "simple_function M f \<longleftrightarrow> simple_function N f"
     7.5    unfolding simple_function_def assms ..
     7.6  
     7.7 -lemma borel_measurable_simple_function:
     7.8 +lemma borel_measurable_simple_function[measurable_dest]:
     7.9    assumes "simple_function M f"
    7.10    shows "f \<in> borel_measurable M"
    7.11  proof (rule borel_measurableI)
    7.12 @@ -918,7 +918,7 @@
    7.13    hence "a \<noteq> 0" by auto
    7.14    let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}"
    7.15    have B: "\<And>i. ?B i \<in> sets M"
    7.16 -    using f `simple_function M u` by (auto simp: borel_measurable_simple_function)
    7.17 +    using f `simple_function M u` by auto
    7.18  
    7.19    let ?uB = "\<lambda>i x. u x * indicator (?B i) x"
    7.20  
    7.21 @@ -1436,6 +1436,10 @@
    7.22    "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and>
    7.23      (\<integral>\<^isup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity> \<and> (\<integral>\<^isup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
    7.24  
    7.25 +lemma borel_measurable_integrable[measurable_dest]:
    7.26 +  "integrable M f \<Longrightarrow> f \<in> borel_measurable M"
    7.27 +  by (auto simp: integrable_def)
    7.28 +
    7.29  lemma integrableD[dest]:
    7.30    assumes "integrable M f"
    7.31    shows "f \<in> borel_measurable M" "(\<integral>\<^isup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^isup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
    7.32 @@ -1776,7 +1780,7 @@
    7.33  qed
    7.34  
    7.35  lemma integrable_abs:
    7.36 -  assumes f: "integrable M f"
    7.37 +  assumes f[measurable]: "integrable M f"
    7.38    shows "integrable M (\<lambda> x. \<bar>f x\<bar>)"
    7.39  proof -
    7.40    from assms have *: "(\<integral>\<^isup>+x. ereal (- \<bar>f x\<bar>)\<partial>M) = 0"
    7.41 @@ -1871,7 +1875,7 @@
    7.42      from mono pos show "AE x in M. ereal (f i x) \<le> ereal (f (Suc i) x) \<and> 0 \<le> ereal (f i x)"
    7.43        by eventually_elim (auto simp: mono_def)
    7.44      show "(\<lambda>x. ereal (f i x)) \<in> borel_measurable M"
    7.45 -      using i by (auto simp: integrable_def)
    7.46 +      using i by auto
    7.47    next
    7.48      show "(\<integral>\<^isup>+ x. ereal (u x) \<partial>M) = \<integral>\<^isup>+ x. (SUP i. ereal (f i x)) \<partial>M"
    7.49        apply (rule positive_integral_cong_AE)
    7.50 @@ -2045,10 +2049,10 @@
    7.51    using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
    7.52  
    7.53  lemma integral_dominated_convergence:
    7.54 -  assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>j. AE x in M. \<bar>u j x\<bar> \<le> w x"
    7.55 -  and w: "integrable M w"
    7.56 +  assumes u[measurable]: "\<And>i. integrable M (u i)" and bound: "\<And>j. AE x in M. \<bar>u j x\<bar> \<le> w x"
    7.57 +  and w[measurable]: "integrable M w"
    7.58    and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
    7.59 -  and borel: "u' \<in> borel_measurable M"
    7.60 +  and [measurable]: "u' \<in> borel_measurable M"
    7.61    shows "integrable M u'"
    7.62    and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar> \<partial>M)) ----> 0" (is "?lim_diff")
    7.63    and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim)
    7.64 @@ -2120,7 +2124,7 @@
    7.65        qed (rule trivial_limit_sequentially)
    7.66      qed
    7.67      also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^isup>+ x. max 0 (ereal (?diff n x)) \<partial>M)"
    7.68 -      using borel w u unfolding integrable_def
    7.69 +      using w u unfolding integrable_def
    7.70        by (intro positive_integral_lim_INF) (auto intro!: positive_integral_lim_INF)
    7.71      also have "\<dots> = (\<integral>\<^isup>+ x. ereal (2 * w x) \<partial>M) -
    7.72          limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
    7.73 @@ -2171,7 +2175,7 @@
    7.74  qed
    7.75  
    7.76  lemma integral_sums:
    7.77 -  assumes borel: "\<And>i. integrable M (f i)"
    7.78 +  assumes integrable[measurable]: "\<And>i. integrable M (f i)"
    7.79    and summable: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>f i x\<bar>)"
    7.80    and sums: "summable (\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
    7.81    shows "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
    7.82 @@ -2182,7 +2186,7 @@
    7.83    from bchoice[OF this]
    7.84    obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto
    7.85    then have w_borel: "w \<in> borel_measurable M" unfolding sums_def
    7.86 -    by (rule borel_measurable_LIMSEQ) (auto simp: borel[THEN integrableD(1)])
    7.87 +    by (rule borel_measurable_LIMSEQ) auto
    7.88  
    7.89    let ?w = "\<lambda>y. if y \<in> space M then w y else 0"
    7.90  
    7.91 @@ -2190,7 +2194,7 @@
    7.92      using sums unfolding summable_def ..
    7.93  
    7.94    have 1: "\<And>n. integrable M (\<lambda>x. \<Sum>i = 0..<n. f i x)"
    7.95 -    using borel by auto
    7.96 +    using integrable by auto
    7.97  
    7.98    have 2: "\<And>j. AE x in M. \<bar>\<Sum>i = 0..<j. f i x\<bar> \<le> ?w x"
    7.99      using AE_space
   7.100 @@ -2206,14 +2210,14 @@
   7.101      let ?F = "\<lambda>n y. (\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
   7.102      let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
   7.103      have "\<And>n. integrable M (?F n)"
   7.104 -      using borel by (auto intro!: integrable_abs)
   7.105 +      using integrable by (auto intro!: integrable_abs)
   7.106      thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
   7.107      show "AE x in M. mono (\<lambda>n. ?w' n x)"
   7.108        by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
   7.109      show "AE x in M. (\<lambda>n. ?w' n x) ----> ?w x"
   7.110          using w by (simp_all add: tendsto_const sums_def)
   7.111      have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
   7.112 -      using borel by (simp add: integrable_abs cong: integral_cong)
   7.113 +      using integrable by (simp add: integrable_abs cong: integral_cong)
   7.114      from abs_sum
   7.115      show "(\<lambda>i. integral\<^isup>L M (?w' i)) ----> x" unfolding * sums_def .
   7.116    qed (simp add: w_borel measurable_If_set)
   7.117 @@ -2223,11 +2227,11 @@
   7.118      by (auto intro: summable_sumr_LIMSEQ_suminf)
   7.119  
   7.120    note int = integral_dominated_convergence(1,3)[OF 1 2 3 4
   7.121 -    borel_measurable_suminf[OF integrableD(1)[OF borel]]]
   7.122 +    borel_measurable_suminf[OF integrableD(1)[OF integrable]]]
   7.123  
   7.124    from int show "integrable M ?S" by simp
   7.125  
   7.126 -  show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF borel]
   7.127 +  show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF integrable]
   7.128      using int(2) by simp
   7.129  qed
   7.130  
   7.131 @@ -2317,13 +2321,9 @@
   7.132                     positive_integral_monotone_convergence_SUP le_fun_def incseq_def)
   7.133  
   7.134  lemma positive_integral_distr:
   7.135 -  assumes T: "T \<in> measurable M M'"
   7.136 -  and f: "f \<in> borel_measurable M'"
   7.137 -  shows "integral\<^isup>P (distr M M' T) f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
   7.138 -  apply (subst (1 2) positive_integral_max_0[symmetric])
   7.139 -  apply (rule positive_integral_distr')
   7.140 -  apply (auto simp: f T)
   7.141 -  done
   7.142 +  "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^isup>P (distr M M' T) f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
   7.143 +  by (subst (1 2) positive_integral_max_0[symmetric])
   7.144 +     (simp add: positive_integral_distr')
   7.145  
   7.146  lemma integral_distr:
   7.147    "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^isup>L (distr M M' T) f = (\<integral> x. f (T x) \<partial>M)"
   7.148 @@ -2331,15 +2331,13 @@
   7.149    by (subst (1 2) positive_integral_distr) auto
   7.150  
   7.151  lemma integrable_distr_eq:
   7.152 -  assumes T: "T \<in> measurable M M'" "f \<in> borel_measurable M'"
   7.153 -  shows "integrable (distr M M' T) f \<longleftrightarrow> integrable M (\<lambda>x. f (T x))"
   7.154 -  using T measurable_comp[OF T]
   7.155 +  "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integrable (distr M M' T) f \<longleftrightarrow> integrable M (\<lambda>x. f (T x))"
   7.156    unfolding integrable_def 
   7.157    by (subst (1 2) positive_integral_distr) (auto simp: comp_def)
   7.158  
   7.159  lemma integrable_distr:
   7.160 -  assumes T: "T \<in> measurable M M'" shows "integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
   7.161 -  by (subst integrable_distr_eq[symmetric, OF T]) auto
   7.162 +  "T \<in> measurable M M' \<Longrightarrow> integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
   7.163 +  by (subst integrable_distr_eq[symmetric]) auto
   7.164  
   7.165  section {* Lebesgue integration on @{const count_space} *}
   7.166  
   7.167 @@ -2414,6 +2412,10 @@
   7.168      and space_density[simp]: "space (density M f) = space M"
   7.169    by (auto simp: density_def)
   7.170  
   7.171 +(* FIXME: add conversion to simplify space, sets and measurable *)
   7.172 +lemma space_density_imp[measurable_dest]:
   7.173 +  "\<And>x M f. x \<in> space (density M f) \<Longrightarrow> x \<in> space M" by auto
   7.174 +
   7.175  lemma 
   7.176    shows measurable_density_eq1[simp]: "g \<in> measurable (density Mg f) Mg' \<longleftrightarrow> g \<in> measurable Mg Mg'"
   7.177      and measurable_density_eq2[simp]: "h \<in> measurable Mh (density Mh' f) \<longleftrightarrow> h \<in> measurable Mh Mh'"
   7.178 @@ -2533,7 +2535,7 @@
   7.179    case (mult u c)
   7.180    moreover have "\<And>x. f x * (c * u x) = c * (f x * u x)" by (simp add: field_simps)
   7.181    ultimately show ?case
   7.182 -    by (simp add: f positive_integral_cmult)
   7.183 +    using f by (simp add: positive_integral_cmult)
   7.184  next
   7.185    case (add u v)
   7.186    moreover then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
     8.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
     8.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
     8.3 @@ -695,66 +695,6 @@
     8.4    qed
     8.5  qed
     8.6  
     8.7 -lemma borel_measurable_real_induct[consumes 2, case_names cong set mult add seq, induct set: borel_measurable]:
     8.8 -  fixes u :: "'a \<Rightarrow> real"
     8.9 -  assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"
    8.10 -  assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f"
    8.11 -  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
    8.12 -  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
    8.13 -  assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
    8.14 -  assumes seq: "\<And>U u. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. 0 \<le> U i x) \<Longrightarrow> (\<And>x. (\<lambda>i. U i x) ----> u x) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> P u"
    8.15 -  shows "P u"
    8.16 -proof -
    8.17 -  have "(\<lambda>x. ereal (u x)) \<in> borel_measurable M"
    8.18 -    using u by auto
    8.19 -  then obtain U where U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and
    8.20 -    "\<And>x. (SUP i. U i x) = max 0 (ereal (u x))" and nn: "\<And>i x. 0 \<le> U i x"
    8.21 -    using borel_measurable_implies_simple_function_sequence'[of u M] by auto
    8.22 -  then have u_eq: "\<And>x. ereal (u x) = (SUP i. U i x)"
    8.23 -    using u by (auto simp: max_def)
    8.24 -
    8.25 -  have [simp]: "\<And>i x. U i x \<noteq> \<infinity>" using U by (auto simp: image_def eq_commute)
    8.26 -
    8.27 -  { fix i x have [simp]: "U i x \<noteq> -\<infinity>" using nn[of i x] by auto }
    8.28 -  note this[simp]
    8.29 -
    8.30 -  show "P u"
    8.31 -  proof (rule seq)
    8.32 -    show "\<And>i. (\<lambda>x. real (U i x)) \<in> borel_measurable M"
    8.33 -      using U by (auto intro: borel_measurable_simple_function)
    8.34 -    show "\<And>i x. 0 \<le> real (U i x)"
    8.35 -      using nn by (auto simp: real_of_ereal_pos)
    8.36 -    show "incseq (\<lambda>i x. real (U i x))"
    8.37 -      using U(2) by (auto simp: incseq_def image_iff le_fun_def intro!: real_of_ereal_positive_mono nn)
    8.38 -    then show "\<And>x. (\<lambda>i. real (U i x)) ----> u x"
    8.39 -      by (intro SUP_eq_LIMSEQ[THEN iffD1])
    8.40 -         (auto simp: incseq_mono incseq_def le_fun_def u_eq ereal_real
    8.41 -               intro!: arg_cong2[where f=SUPR] ext)
    8.42 -    show "\<And>i. P (\<lambda>x. real (U i x))"
    8.43 -    proof (rule cong)
    8.44 -      fix x i assume x: "x \<in> space M"
    8.45 -      have [simp]: "\<And>A x. real (indicator A x :: ereal) = indicator A x"
    8.46 -        by (auto simp: indicator_def one_ereal_def)
    8.47 -      { fix y assume "y \<in> U i ` space M"
    8.48 -        then have "0 \<le> y" "y \<noteq> \<infinity>" using nn by auto
    8.49 -        then have "\<bar>y * indicator (U i -` {y} \<inter> space M) x\<bar> \<noteq> \<infinity>"
    8.50 -          by (auto simp: indicator_def) }
    8.51 -      then show "real (U i x) = (\<Sum>y \<in> U i ` space M. real y * indicator (U i -` {y} \<inter> space M) x)"
    8.52 -        unfolding simple_function_indicator_representation[OF U(1) x]
    8.53 -        by (subst setsum_real_of_ereal[symmetric]) auto
    8.54 -    next
    8.55 -      fix i
    8.56 -      have "finite (U i ` space M)" "\<And>x. x \<in> U i ` space M \<Longrightarrow> 0 \<le> x""\<And>x. x \<in> U i ` space M \<Longrightarrow> x \<noteq> \<infinity>"
    8.57 -        using U(1) nn by (auto simp: simple_function_def)
    8.58 -      then show "P (\<lambda>x. \<Sum>y \<in> U i ` space M. real y * indicator (U i -` {y} \<inter> space M) x)"
    8.59 -      proof induct
    8.60 -        case empty then show ?case
    8.61 -          using set[of "{}"] by (simp add: indicator_def[abs_def])
    8.62 -      qed (auto intro!: add mult set simple_functionD U setsum_nonneg borel_measurable_setsum mult_nonneg_nonneg real_of_ereal_pos)
    8.63 -    qed (auto intro: borel_measurable_simple_function U simple_functionD intro!: borel_measurable_setsum borel_measurable_times)
    8.64 -  qed
    8.65 -qed
    8.66 -
    8.67  lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
    8.68    by (auto simp: indicator_def one_ereal_def)
    8.69  
    8.70 @@ -1054,7 +994,7 @@
    8.71      by (intro arg_cong2[where f=sigma_sets]) (auto simp: space_PiM image_iff bchoice_iff)
    8.72  qed (auto simp: borel_eq_lessThan reals_Archimedean2)
    8.73  
    8.74 -lemma measurable_e2p:
    8.75 +lemma measurable_e2p[measurable]:
    8.76    "e2p \<in> measurable (borel::'a::ordered_euclidean_space measure) (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))"
    8.77  proof (rule measurable_sigma_sets[OF sets_product_borel])
    8.78    fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i} |x. True} "
    8.79 @@ -1065,7 +1005,11 @@
    8.80    then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
    8.81  qed (auto simp: e2p_def)
    8.82  
    8.83 -lemma measurable_p2e:
    8.84 +(* FIXME: conversion in measurable prover *)
    8.85 +lemma lborelD_Collect[measurable]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
    8.86 +lemma lborelD[measurable]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
    8.87 +
    8.88 +lemma measurable_p2e[measurable]:
    8.89    "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))
    8.90      (borel :: 'a::ordered_euclidean_space measure)"
    8.91    (is "p2e \<in> measurable ?P _")
     9.1 --- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
     9.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
     9.3 @@ -522,23 +522,50 @@
     9.4    f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N"
     9.5  
     9.6  lemma
     9.7 -  shows distributed_distr_eq_density: "distributed M N X f \<Longrightarrow> distr M N X = density N f"
     9.8 -    and distributed_measurable: "distributed M N X f \<Longrightarrow> X \<in> measurable M N"
     9.9 -    and distributed_borel_measurable: "distributed M N X f \<Longrightarrow> f \<in> borel_measurable N"
    9.10 -    and distributed_AE: "distributed M N X f \<Longrightarrow> (AE x in N. 0 \<le> f x)"
    9.11 -  by (simp_all add: distributed_def)
    9.12 +  assumes "distributed M N X f"
    9.13 +  shows distributed_distr_eq_density: "distr M N X = density N f"
    9.14 +    and distributed_measurable: "X \<in> measurable M N"
    9.15 +    and distributed_borel_measurable: "f \<in> borel_measurable N"
    9.16 +    and distributed_AE: "(AE x in N. 0 \<le> f x)"
    9.17 +  using assms by (simp_all add: distributed_def)
    9.18 +
    9.19 +lemma
    9.20 +  assumes D: "distributed M N X f"
    9.21 +  shows distributed_measurable'[measurable_dest]:
    9.22 +      "g \<in> measurable L M \<Longrightarrow> (\<lambda>x. X (g x)) \<in> measurable L N"
    9.23 +    and distributed_borel_measurable'[measurable_dest]:
    9.24 +      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
    9.25 +  using distributed_measurable[OF D] distributed_borel_measurable[OF D]
    9.26 +  by simp_all
    9.27  
    9.28  lemma
    9.29    shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N"
    9.30      and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)"
    9.31    by (simp_all add: distributed_def borel_measurable_ereal_iff)
    9.32  
    9.33 +lemma
    9.34 +  assumes D: "distributed M N X (\<lambda>x. ereal (f x))"
    9.35 +  shows distributed_real_measurable'[measurable_dest]:
    9.36 +      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
    9.37 +  using distributed_real_measurable[OF D]
    9.38 +  by simp_all
    9.39 +
    9.40 +lemma
    9.41 +  assumes D: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
    9.42 +  shows joint_distributed_measurable1[measurable_dest]:
    9.43 +      "h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S"
    9.44 +    and joint_distributed_measurable2[measurable_dest]:
    9.45 +      "h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T"
    9.46 +  using measurable_compose[OF distributed_measurable[OF D] measurable_fst]
    9.47 +  using measurable_compose[OF distributed_measurable[OF D] measurable_snd]
    9.48 +  by auto
    9.49 +
    9.50  lemma distributed_count_space:
    9.51    assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A"
    9.52    shows "P a = emeasure M (X -` {a} \<inter> space M)"
    9.53  proof -
    9.54    have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}"
    9.55 -    using X a A by (simp add: distributed_measurable emeasure_distr)
    9.56 +    using X a A by (simp add: emeasure_distr)
    9.57    also have "\<dots> = emeasure (density (count_space A) P) {a}"
    9.58      using X by (simp add: distributed_distr_eq_density)
    9.59    also have "\<dots> = (\<integral>\<^isup>+x. P a * indicator {a} x \<partial>count_space A)"
    9.60 @@ -583,17 +610,17 @@
    9.61  
    9.62  lemma distributed_emeasure:
    9.63    "distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>N)"
    9.64 -  by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable
    9.65 +  by (auto simp: distributed_AE
    9.66                   distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
    9.67  
    9.68  lemma distributed_positive_integral:
    9.69    "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^isup>+x. f x * g x \<partial>N) = (\<integral>\<^isup>+x. g (X x) \<partial>M)"
    9.70 -  by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable
    9.71 +  by (auto simp: distributed_AE
    9.72                   distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr)
    9.73  
    9.74  lemma distributed_integral:
    9.75    "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)"
    9.76 -  by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
    9.77 +  by (auto simp: distributed_real_AE
    9.78                   distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr)
    9.79    
    9.80  lemma distributed_transform_integral:
    9.81 @@ -617,7 +644,7 @@
    9.82    shows "AE x in S. Px x = Py x"
    9.83  proof -
    9.84    interpret X: prob_space "distr M S X"
    9.85 -    using distributed_measurable[OF Px] by (rule prob_space_distr)
    9.86 +    using Px by (intro prob_space_distr) simp
    9.87    have "sigma_finite_measure (distr M S X)" ..
    9.88    with sigma_finite_density_unique[of Px S Py ] Px Py
    9.89    show ?thesis
    9.90 @@ -626,8 +653,8 @@
    9.91  
    9.92  lemma (in prob_space) distributed_jointI:
    9.93    assumes "sigma_finite_measure S" "sigma_finite_measure T"
    9.94 -  assumes X[simp]: "X \<in> measurable M S" and Y[simp]: "Y \<in> measurable M T"
    9.95 -  assumes f[simp]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
    9.96 +  assumes X[measurable]: "X \<in> measurable M S" and Y[measurable]: "Y \<in> measurable M T"
    9.97 +  assumes [measurable]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" and f: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
    9.98    assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow> 
    9.99      emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)"
   9.100    shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
   9.101 @@ -655,18 +682,18 @@
   9.102        using F by (auto simp: space_pair_measure)
   9.103    next
   9.104      fix E assume "E \<in> ?E"
   9.105 -    then obtain A B where E[simp]: "E = A \<times> B" and A[simp]: "A \<in> sets S" and B[simp]: "B \<in> sets T" by auto
   9.106 +    then obtain A B where E[simp]: "E = A \<times> B"
   9.107 +      and A[measurable]: "A \<in> sets S" and B[measurable]: "B \<in> sets T" by auto
   9.108      have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
   9.109        by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
   9.110      also have "\<dots> = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
   9.111 -      by (auto simp add: eq measurable_Pair measurable_compose[OF _ f(1)] positive_integral_multc
   9.112 -               intro!: positive_integral_cong)
   9.113 +      using f by (auto simp add: eq positive_integral_multc intro!: positive_integral_cong)
   9.114      also have "\<dots> = emeasure ?R E"
   9.115        by (auto simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric]
   9.116                 intro!: positive_integral_cong split: split_indicator)
   9.117      finally show "emeasure ?L E = emeasure ?R E" .
   9.118    qed
   9.119 -qed (auto intro!: measurable_Pair)
   9.120 +qed (auto simp: f)
   9.121  
   9.122  lemma (in prob_space) distributed_swap:
   9.123    assumes "sigma_finite_measure S" "sigma_finite_measure T"
   9.124 @@ -678,14 +705,14 @@
   9.125    interpret ST: pair_sigma_finite S T by default
   9.126    interpret TS: pair_sigma_finite T S by default
   9.127  
   9.128 -  note measurable_Pxy = measurable_compose[OF _ distributed_borel_measurable[OF Pxy]]
   9.129 +  note Pxy[measurable]
   9.130    show ?thesis 
   9.131      apply (subst TS.distr_pair_swap)
   9.132      unfolding distributed_def
   9.133    proof safe
   9.134      let ?D = "distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))"
   9.135      show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D"
   9.136 -      by (auto simp: measurable_split_conv intro!: measurable_Pair measurable_Pxy)
   9.137 +      by auto
   9.138      with Pxy
   9.139      show "AE x in distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x)). 0 \<le> (case x of (x, y) \<Rightarrow> Pxy (y, x))"
   9.140        by (subst AE_distr_iff)
   9.141 @@ -693,9 +720,7 @@
   9.142                 simp: measurable_split_conv split_beta
   9.143                 intro!: measurable_Pair borel_measurable_ereal_le)
   9.144      show 2: "random_variable (distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))"
   9.145 -      using measurable_compose[OF distributed_measurable[OF Pxy] measurable_fst]
   9.146 -      using measurable_compose[OF distributed_measurable[OF Pxy] measurable_snd]
   9.147 -      by (auto intro!: measurable_Pair)
   9.148 +      using Pxy by auto
   9.149      { fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)"
   9.150        let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^isub>M T)"
   9.151        from sets_into_space[OF A]
   9.152 @@ -703,7 +728,7 @@
   9.153          emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
   9.154          by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
   9.155        also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^isub>M T))"
   9.156 -        using Pxy A by (intro distributed_emeasure measurable_sets) (auto simp: measurable_split_conv measurable_Pair)
   9.157 +        using Pxy A by (intro distributed_emeasure) auto
   9.158        finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
   9.159          (\<integral>\<^isup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^isub>M T))"
   9.160          by (auto intro!: positive_integral_cong split: split_indicator) }
   9.161 @@ -712,7 +737,7 @@
   9.162        apply (intro measure_eqI)
   9.163        apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
   9.164        apply (subst positive_integral_distr)
   9.165 -      apply (auto intro!: measurable_pair measurable_Pxy * simp: comp_def split_beta)
   9.166 +      apply (auto intro!: * simp: comp_def split_beta)
   9.167        done
   9.168    qed
   9.169  qed
   9.170 @@ -728,33 +753,29 @@
   9.171    interpret T: sigma_finite_measure T by fact
   9.172    interpret ST: pair_sigma_finite S T by default
   9.173  
   9.174 -  have XY: "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
   9.175 -    using Pxy by (rule distributed_measurable)
   9.176 -  then show X: "X \<in> measurable M S"
   9.177 -    unfolding measurable_pair_iff by (simp add: comp_def)
   9.178 -  from XY have Y: "Y \<in> measurable M T"
   9.179 -    unfolding measurable_pair_iff by (simp add: comp_def)
   9.180 +  note Pxy[measurable]
   9.181 +  show X: "X \<in> measurable M S" by simp
   9.182  
   9.183 -  from Pxy show borel: "Px \<in> borel_measurable S"
   9.184 -    by (auto intro!: T.positive_integral_fst_measurable dest!: distributed_borel_measurable simp: Px_def)
   9.185 +  show borel: "Px \<in> borel_measurable S"
   9.186 +    by (auto intro!: T.positive_integral_fst_measurable simp: Px_def)
   9.187  
   9.188    interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   9.189 -    using XY by (rule prob_space_distr)
   9.190 +    by (intro prob_space_distr) simp
   9.191    have "(\<integral>\<^isup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
   9.192      using Pxy
   9.193 -    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_borel_measurable distributed_AE)
   9.194 +    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
   9.195  
   9.196    show "distr M S X = density S Px"
   9.197    proof (rule measure_eqI)
   9.198      fix A assume A: "A \<in> sets (distr M S X)"
   9.199 -    with X Y XY have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
   9.200 -      by (auto simp add: emeasure_distr
   9.201 -               intro!: arg_cong[where f="emeasure M"] dest: measurable_space)
   9.202 +    with X measurable_space[of Y M T]
   9.203 +    have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
   9.204 +      by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"])
   9.205      also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)"
   9.206        using Pxy by (simp add: distributed_def)
   9.207      also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
   9.208        using A borel Pxy
   9.209 -      by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric] distributed_def)
   9.210 +      by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric])
   9.211      also have "\<dots> = \<integral>\<^isup>+ x. Px x * indicator A x \<partial>S"
   9.212        apply (rule positive_integral_cong_AE)
   9.213        using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
   9.214 @@ -763,7 +784,7 @@
   9.215        moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
   9.216          by (auto simp: indicator_def)
   9.217        ultimately have "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) * indicator A x"
   9.218 -        using Pxy[THEN distributed_borel_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong)
   9.219 +        by (simp add: eq positive_integral_multc cong: positive_integral_cong)
   9.220        also have "(\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) = Px x"
   9.221          by (simp add: Px_def ereal_real positive_integral_positive)
   9.222        finally show "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
   9.223 @@ -800,7 +821,7 @@
   9.224  
   9.225  lemma (in prob_space) distributed_joint_indep':
   9.226    assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
   9.227 -  assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"
   9.228 +  assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py"
   9.229    assumes indep: "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   9.230    shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
   9.231    unfolding distributed_def
   9.232 @@ -811,30 +832,23 @@
   9.233  
   9.234    interpret X: prob_space "density S Px"
   9.235      unfolding distributed_distr_eq_density[OF X, symmetric]
   9.236 -    using distributed_measurable[OF X]
   9.237 -    by (rule prob_space_distr)
   9.238 +    by (rule prob_space_distr) simp
   9.239    have sf_X: "sigma_finite_measure (density S Px)" ..
   9.240  
   9.241    interpret Y: prob_space "density T Py"
   9.242      unfolding distributed_distr_eq_density[OF Y, symmetric]
   9.243 -    using distributed_measurable[OF Y]
   9.244 -    by (rule prob_space_distr)
   9.245 +    by (rule prob_space_distr) simp
   9.246    have sf_Y: "sigma_finite_measure (density T Py)" ..
   9.247  
   9.248    show "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). Px x * Py y)"
   9.249      unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
   9.250      using distributed_borel_measurable[OF X] distributed_AE[OF X]
   9.251      using distributed_borel_measurable[OF Y] distributed_AE[OF Y]
   9.252 -    by (rule pair_measure_density[OF _ _ _ _ S T sf_X sf_Y])
   9.253 +    by (rule pair_measure_density[OF _ _ _ _ T sf_Y])
   9.254  
   9.255 -  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   9.256 -    using distributed_measurable[OF X] distributed_measurable[OF Y]
   9.257 -    by (auto intro: measurable_Pair)
   9.258 +  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" by auto
   9.259  
   9.260 -  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)"
   9.261 -    by (auto simp: split_beta' 
   9.262 -             intro!: measurable_compose[OF _ distributed_borel_measurable[OF X]]
   9.263 -                     measurable_compose[OF _ distributed_borel_measurable[OF Y]])
   9.264 +  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)" by auto
   9.265  
   9.266    show "AE x in S \<Otimes>\<^isub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)"
   9.267      apply (intro ST.AE_pair_measure borel_measurable_ereal_le Pxy borel_measurable_const)
    10.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Nov 02 14:23:40 2012 +0100
    10.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Nov 02 14:23:54 2012 +0100
    10.3 @@ -47,7 +47,7 @@
    10.4    shows "\<exists>h\<in>borel_measurable M. integral\<^isup>P M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>) \<and> (\<forall>x. 0 \<le> h x)"
    10.5  proof -
    10.6    obtain A :: "nat \<Rightarrow> 'a set" where
    10.7 -    range: "range A \<subseteq> sets M" and
    10.8 +    range[measurable]: "range A \<subseteq> sets M" and
    10.9      space: "(\<Union>i. A i) = space M" and
   10.10      measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>" and
   10.11      disjoint: "disjoint_family A"
   10.12 @@ -97,10 +97,7 @@
   10.13        assume "x \<notin> space M" then have "\<And>i. x \<notin> A i" using space by auto
   10.14        then show "0 \<le> ?h x" by auto
   10.15      qed
   10.16 -  next
   10.17 -    show "?h \<in> borel_measurable M" using range n
   10.18 -      by (auto intro!: borel_measurable_psuminf borel_measurable_ereal_times ereal_0_le_mult intro: less_imp_le)
   10.19 -  qed
   10.20 +  qed measurable
   10.21  qed
   10.22  
   10.23  subsection "Absolutely continuous"
   10.24 @@ -298,6 +295,8 @@
   10.25  proof -
   10.26    interpret N: finite_measure N by fact
   10.27    def G \<equiv> "{g \<in> borel_measurable M. (\<forall>x. 0 \<le> g x) \<and> (\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> N A)}"
   10.28 +  { fix f have "f \<in> G \<Longrightarrow> f \<in> borel_measurable M" by (auto simp: G_def) }
   10.29 +  note this[measurable_dest]
   10.30    have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
   10.31    hence "G \<noteq> {}" by auto
   10.32    { fix f g assume f: "f \<in> G" and g: "g \<in> G"
   10.33 @@ -329,10 +328,10 @@
   10.34      qed }
   10.35    note max_in_G = this
   10.36    { fix f assume  "incseq f" and f: "\<And>i. f i \<in> G"
   10.37 +    then have [measurable]: "\<And>i. f i \<in> borel_measurable M" by (auto simp: G_def)
   10.38      have "(\<lambda>x. SUP i. f i x) \<in> G" unfolding G_def
   10.39      proof safe
   10.40 -      show "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M"
   10.41 -        using f by (auto simp: G_def)
   10.42 +      show "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M" by measurable
   10.43        { fix x show "0 \<le> (SUP i. f i x)"
   10.44            using f by (auto simp: G_def intro: SUP_upper2) }
   10.45      next
   10.46 @@ -379,7 +378,7 @@
   10.47    note g_in_G = this
   10.48    have "incseq ?g" using gs_not_empty
   10.49      by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc)
   10.50 -  from SUP_in_G[OF this g_in_G] have "f \<in> G" unfolding f_def .
   10.51 +  from SUP_in_G[OF this g_in_G] have [measurable]: "f \<in> G" unfolding f_def .
   10.52    then have [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
   10.53    have "integral\<^isup>P M f = (SUP i. integral\<^isup>P M (?g i))" unfolding f_def
   10.54      using g_in_G `incseq ?g`
   10.55 @@ -467,7 +466,7 @@
   10.56        hence "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) =
   10.57            (\<integral>\<^isup>+x. f x * indicator A x \<partial>M) + b * emeasure M (A \<inter> A0)"
   10.58          using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A b `f \<in> G`
   10.59 -        by (simp add: G_def positive_integral_add positive_integral_cmult_indicator) }
   10.60 +        by (simp add: positive_integral_add positive_integral_cmult_indicator G_def) }
   10.61      note f0_eq = this
   10.62      { fix A assume A: "A \<in> sets M"
   10.63        hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   10.64 @@ -484,8 +483,8 @@
   10.65          using f_le_v N.emeasure_eq_measure[of A] positive_integral_positive[of M "?F A"]
   10.66          by (cases "\<integral>\<^isup>+x. ?F A x \<partial>M", cases "N A") auto
   10.67        finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) \<le> N A" . }
   10.68 -    hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` unfolding G_def
   10.69 -      by (auto intro!: ereal_add_nonneg_nonneg)
   10.70 +    hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G`
   10.71 +      by (auto intro!: ereal_add_nonneg_nonneg simp: G_def)
   10.72      have int_f_finite: "integral\<^isup>P M f \<noteq> \<infinity>"
   10.73        by (metis N.emeasure_finite ereal_infty_less_eq2(1) int_f_eq_y y_le)
   10.74      have  "0 < ?M (space M) - emeasure ?Mb (space M)"
   10.75 @@ -676,6 +675,7 @@
   10.76      with Q_fin show "finite_measure (?N i)"
   10.77        by (auto intro!: finite_measureI)
   10.78      show "sets (?N i) = sets (?M i)" by (simp add: sets_eq)
   10.79 +    have [measurable]: "\<And>A. A \<in> sets M \<Longrightarrow> A \<in> sets N" by (simp add: sets_eq)
   10.80      show "absolutely_continuous (?M i) (?N i)"
   10.81        using `absolutely_continuous M N` `Q i \<in> sets M`
   10.82        by (auto simp: absolutely_continuous_def null_sets_density_iff sets_eq
   10.83 @@ -731,9 +731,7 @@
   10.84        ultimately have "N A = (\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M)"
   10.85          using plus_emeasure[of "(\<Union>i. Q i) \<inter> A" N "Q0 \<inter> A"] by (simp add: sets_eq)
   10.86        with `A \<in> sets M` borel Q Q0(1) show "emeasure (density M ?f) A = N A"
   10.87 -        by (subst emeasure_density)
   10.88 -           (auto intro!: borel_measurable_ereal_add borel_measurable_psuminf measurable_If
   10.89 -                 simp: subset_eq)
   10.90 +        by (auto simp: subset_eq emeasure_density)
   10.91      qed (simp add: sets_eq)
   10.92    qed
   10.93  qed
   10.94 @@ -845,7 +843,7 @@
   10.95      unfolding indicator_def by auto
   10.96    have "\<forall>i. AE x in M. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos
   10.97      by (intro finite_density_unique[THEN iffD1] allI)
   10.98 -       (auto intro!: borel_measurable_ereal_times f measure_eqI Int simp: emeasure_density * subset_eq)
   10.99 +       (auto intro!: f measure_eqI simp: emeasure_density * subset_eq)
  10.100    moreover have "AE x in M. ?f Q0 x = ?f' Q0 x"
  10.101    proof (rule AE_I')
  10.102      { fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
  10.103 @@ -1083,7 +1081,7 @@
  10.104  
  10.105  lemma (in sigma_finite_measure) RN_deriv:
  10.106    assumes "absolutely_continuous M N" "sets N = sets M"
  10.107 -  shows borel_measurable_RN_deriv: "RN_deriv M N \<in> borel_measurable M" (is ?borel)
  10.108 +  shows borel_measurable_RN_deriv[measurable]: "RN_deriv M N \<in> borel_measurable M" (is ?borel)
  10.109      and density_RN_deriv: "density M (RN_deriv M N) = N" (is ?density)
  10.110      and RN_deriv_nonneg: "0 \<le> RN_deriv M N x" (is ?pos)
  10.111  proof -
  10.112 @@ -1164,7 +1162,7 @@
  10.113      qed
  10.114    qed
  10.115    have "(RN_deriv ?M' ?N') \<circ> T \<in> borel_measurable M"
  10.116 -    using T ac by (intro measurable_comp[where b="?M'"] M'.borel_measurable_RN_deriv) simp_all
  10.117 +    using T ac by measurable simp
  10.118    then show "(\<lambda>x. RN_deriv ?M' ?N' (T x)) \<in> borel_measurable M"
  10.119      by (simp add: comp_def)
  10.120    show "AE x in M. 0 \<le> RN_deriv ?M' ?N' (T x)" using M'.RN_deriv_nonneg[OF ac] by auto
    11.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:23:40 2012 +0100
    11.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:23:54 2012 +0100
    11.3 @@ -1263,6 +1263,11 @@
    11.4    shows "f \<in> measurable M (measure_of \<Omega> N \<mu>) \<longleftrightarrow> (\<forall>A\<in>N. f -` A \<inter> space M \<in> sets M)"
    11.5    by (metis assms in_measure_of measurable_measure_of assms measurable_sets)
    11.6  
    11.7 +lemma measurable_cong_sets:
    11.8 +  assumes sets: "sets M = sets M'" "sets N = sets N'"
    11.9 +  shows "measurable M N = measurable M' N'"
   11.10 +  using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def)
   11.11 +
   11.12  lemma measurable_cong:
   11.13    assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
   11.14    shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'"
   11.15 @@ -1275,7 +1280,22 @@
   11.16        \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
   11.17    by (simp add: measurable_def sigma_algebra_iff2)
   11.18  
   11.19 -lemma measurable_const[intro, simp]:
   11.20 +lemma measurable_compose:
   11.21 +  assumes f: "f \<in> measurable M N" and g: "g \<in> measurable N L"
   11.22 +  shows "(\<lambda>x. g (f x)) \<in> measurable M L"
   11.23 +proof -
   11.24 +  have "\<And>A. (\<lambda>x. g (f x)) -` A \<inter> space M = f -` (g -` A \<inter> space N) \<inter> space M"
   11.25 +    using measurable_space[OF f] by auto
   11.26 +  with measurable_space[OF f] measurable_space[OF g] show ?thesis
   11.27 +    by (auto intro: measurable_sets[OF f] measurable_sets[OF g]
   11.28 +             simp del: vimage_Int simp add: measurable_def)
   11.29 +qed
   11.30 +
   11.31 +lemma measurable_comp:
   11.32 +  "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> g \<circ> f \<in> measurable M L"
   11.33 +  using measurable_compose[of f M N g L] by (simp add: comp_def)
   11.34 +
   11.35 +lemma measurable_const:
   11.36    "c \<in> space M' \<Longrightarrow> (\<lambda>x. c) \<in> measurable M M'"
   11.37    by (auto simp add: measurable_def)
   11.38  
   11.39 @@ -1308,23 +1328,11 @@
   11.40    thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<inter> space M \<in> sets M` by auto
   11.41  qed
   11.42  
   11.43 -lemma measurable_ident[intro, simp]: "id \<in> measurable M M"
   11.44 -  by (auto simp add: measurable_def)
   11.45 -
   11.46 -lemma measurable_ident'[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
   11.47 +lemma measurable_ident: "id \<in> measurable M M"
   11.48    by (auto simp add: measurable_def)
   11.49  
   11.50 -lemma measurable_comp[intro]:
   11.51 -  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
   11.52 -  shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
   11.53 -  apply (auto simp add: measurable_def vimage_compose)
   11.54 -  apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
   11.55 -  apply force+
   11.56 -  done
   11.57 -
   11.58 -lemma measurable_compose:
   11.59 -  "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> (\<lambda>x. g (f x)) \<in> measurable M L"
   11.60 -  using measurable_comp[of f M N g L] by (simp add: comp_def)
   11.61 +lemma measurable_ident': "(\<lambda>x. x) \<in> measurable M M"
   11.62 +  by (auto simp add: measurable_def)
   11.63  
   11.64  lemma sets_Least:
   11.65    assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
   11.66 @@ -1469,7 +1477,7 @@
   11.67  
   11.68  lemma measurable_count_space_const:
   11.69    "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
   11.70 -  by auto
   11.71 +  by (simp add: measurable_const)
   11.72  
   11.73  lemma measurable_count_space:
   11.74    "f \<in> measurable (count_space A) (count_space UNIV)"
   11.75 @@ -1489,10 +1497,10 @@
   11.76  
   11.77  structure Data = Generic_Data
   11.78  (
   11.79 -  type T = thm list * thm list;
   11.80 -  val empty = ([], []);
   11.81 +  type T = (thm list * thm list) * thm list;
   11.82 +  val empty = (([], []), []);
   11.83    val extend = I;
   11.84 -  val merge = fn ((a, b), (c, d)) => (a @ c, b @ d);
   11.85 +  val merge = fn (((c1, g1), d1), ((c2, g2), d2)) => ((c1 @ c2, g1 @ g2), d1 @ d2);
   11.86  );
   11.87  
   11.88  val debug =
   11.89 @@ -1501,12 +1509,15 @@
   11.90  val backtrack =
   11.91    Attrib.setup_config_int @{binding measurable_backtrack} (K 40)
   11.92  
   11.93 -fun get lv = (case lv of Concrete => fst | Generic => snd) o Data.get o Context.Proof; 
   11.94 +fun get lv = (case lv of Concrete => fst | Generic => snd) o fst o Data.get o Context.Proof; 
   11.95  fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
   11.96  
   11.97 -fun update f lv = Data.map (case lv of Concrete => apfst f | Generic => apsnd f);
   11.98 +fun update f lv = Data.map (apfst (case lv of Concrete => apfst f | Generic => apsnd f));
   11.99  fun add thms' = update (fn thms => thms @ thms');
  11.100  
  11.101 +val get_dest = snd o Data.get;
  11.102 +fun add_dest thm = Data.map (apsnd (fn thms => thms @ [thm]));
  11.103 +
  11.104  fun TRYALL' tacs = fold_rev (curry op APPEND') tacs (K no_tac);
  11.105  
  11.106  fun is_too_generic thm =
  11.107 @@ -1515,11 +1526,10 @@
  11.108      val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
  11.109    in is_Var (head_of concl') end
  11.110  
  11.111 -fun import_theorem thm = if is_too_generic thm then [] else
  11.112 -  [thm] @ map_filter (try (fn th' => thm RS th'))
  11.113 -    [@{thm measurable_compose_rev}, @{thm pred_sets1}, @{thm pred_sets2}, @{thm sets_into_space}];
  11.114 +fun import_theorem ctxt thm = if is_too_generic thm then [] else
  11.115 +  [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
  11.116  
  11.117 -fun add_thm (raw, lv) thm = add (if raw then [thm] else import_theorem thm) lv;
  11.118 +fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
  11.119  
  11.120  fun debug_tac ctxt msg f = if Config.get ctxt debug then K (print_tac (msg ())) THEN' f else f
  11.121  
  11.122 @@ -1573,8 +1583,9 @@
  11.123      handle TERM _ => no_tac) 1)
  11.124  
  11.125  fun single_measurable_tac ctxt facts =
  11.126 -  debug_tac ctxt (fn () => "single + " ^ Pretty.str_of (Pretty.block (map (Syntax.pretty_term ctxt o prop_of) facts)))
  11.127 -  (resolve_tac ((maps (import_theorem o Simplifier.norm_hhf) facts) @ get_all ctxt)
  11.128 +  debug_tac ctxt (fn () => "single + " ^
  11.129 +    Pretty.str_of (Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)))))
  11.130 +  (resolve_tac ((maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt)
  11.131      APPEND' (split_fun_tac ctxt));
  11.132  
  11.133  fun is_cond_formlua n thm = if length (prems_of thm) < n then false else
  11.134 @@ -1598,6 +1609,9 @@
  11.135    Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
  11.136       Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
  11.137  
  11.138 +val dest_attr : attribute context_parser =
  11.139 +  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
  11.140 +
  11.141  val method : (Proof.context -> Method.method) context_parser =
  11.142    Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts 1)));
  11.143  
  11.144 @@ -1613,10 +1627,17 @@
  11.145  *}
  11.146  
  11.147  attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
  11.148 +attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
  11.149  method_setup measurable = {* Measurable.method *} "measurability prover"
  11.150  simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
  11.151  
  11.152  declare
  11.153 +  measurable_compose_rev[measurable_dest]
  11.154 +  pred_sets1[measurable_dest]
  11.155 +  pred_sets2[measurable_dest]
  11.156 +  sets_into_space[measurable_dest]
  11.157 +
  11.158 +declare
  11.159    top[measurable]
  11.160    empty_sets[measurable (raw)]
  11.161    Un[measurable (raw)]
  11.162 @@ -1670,7 +1691,7 @@
  11.163    "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
  11.164    "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))"
  11.165    "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
  11.166 -  by (auto intro!: sets_Collect simp: iff_conv_conj_imp pred_def)
  11.167 +  by (auto simp: iff_conv_conj_imp pred_def)
  11.168  
  11.169  lemma pred_intros_countable[measurable (raw)]:
  11.170    fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
  11.171 @@ -1743,6 +1764,34 @@
  11.172  declare
  11.173    Int[measurable (raw)]
  11.174  
  11.175 +lemma pred_in_If[measurable (raw)]:
  11.176 +  "pred M (\<lambda>x. (P x \<longrightarrow> x \<in> A x) \<and> (\<not> P x \<longrightarrow> x \<in> B x)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (if P x then A x else B x))"
  11.177 +  by auto
  11.178 +
  11.179 +lemma sets_range[measurable_dest]:
  11.180 +  "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
  11.181 +  by auto
  11.182 +
  11.183 +lemma pred_sets_range[measurable_dest]:
  11.184 +  "A ` I \<subseteq> sets N \<Longrightarrow> i \<in> I \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
  11.185 +  using pred_sets2[OF sets_range] by auto
  11.186 +
  11.187 +lemma sets_All[measurable_dest]:
  11.188 +  "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
  11.189 +  by auto
  11.190 +
  11.191 +lemma pred_sets_All[measurable_dest]:
  11.192 +  "\<forall>i. A i \<in> sets (N i) \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
  11.193 +  using pred_sets2[OF sets_All, of A N f] by auto
  11.194 +
  11.195 +lemma sets_Ball[measurable_dest]:
  11.196 +  "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
  11.197 +  by auto
  11.198 +
  11.199 +lemma pred_sets_Ball[measurable_dest]:
  11.200 +  "\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
  11.201 +  using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
  11.202 +
  11.203  hide_const (open) pred
  11.204  
  11.205  subsection {* Extend measure *}