changeset 50244 de72bbe42190 parent 50021 d96a3f468203 child 51329 4a3c453f99a1
```     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Thu Nov 22 10:09:54 2012 +0100
1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Nov 27 11:29:47 2012 +0100
1.3 @@ -189,13 +189,13 @@
1.4        fix B assume "B \<in> sets M" "B \<subseteq> space M - A n"
1.5        from B[OF this] show "-e < ?d B" .
1.6      next
1.7 -      show "space M - A n \<in> sets M" by (rule compl_sets) fact
1.8 +      show "space M - A n \<in> sets M" by (rule sets.compl_sets) fact
1.9      next
1.10        show "?d (space M) \<le> ?d (space M - A n)"
1.11        proof (induct n)
1.12          fix n assume "?d (space M) \<le> ?d (space M - A n)"
1.13          also have "\<dots> \<le> ?d (space M - A (Suc n))"
1.14 -          using A_in_sets sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl
1.15 +          using A_in_sets sets.sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl
1.16            by (simp del: A_simps add: sets_eq sets_eq_imp_space_eq[OF sets_eq])
1.17          finally show "?d (space M) \<le> ?d (space M - A (Suc n))" .
1.18        qed simp
1.19 @@ -241,7 +241,7 @@
1.20        by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq)
1.21      from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this
1.22      with S have "?P (S \<inter> X) S n"
1.23 -      by (simp add: measure_restricted sets_eq Int) (metis inf_absorb2)
1.24 +      by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
1.25      hence "\<exists>A. ?P A S n" .. }
1.26    note Ex_P = this
1.27    def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
1.28 @@ -309,7 +309,7 @@
1.29        hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto
1.30        hence sets': "?A \<inter> A \<in> sets N" "(space M - ?A) \<inter> A \<in> sets N" by (auto simp: sets_eq)
1.31        have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
1.32 -        using sets_into_space[OF `A \<in> sets M`] by auto
1.33 +        using sets.sets_into_space[OF `A \<in> sets M`] by auto
1.34        have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
1.35          g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
1.36          by (auto simp: indicator_def max_def)
1.37 @@ -351,7 +351,7 @@
1.38    have y_le: "?y \<le> N (space M)" unfolding G_def
1.39    proof (safe intro!: SUP_least)
1.40      fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> N A"
1.41 -    from this[THEN bspec, OF top] show "integral\<^isup>P M g \<le> N (space M)"
1.42 +    from this[THEN bspec, OF sets.top] show "integral\<^isup>P M g \<le> N (space M)"
1.43        by (simp cong: positive_integral_cong)
1.44    qed
1.45    from SUPR_countable_SUPR[OF `G \<noteq> {}`, of "integral\<^isup>P M"] guess ys .. note ys = this
1.46 @@ -507,7 +507,7 @@
1.47      with int_f_finite have "?y + 0 < integral\<^isup>P M f + b * emeasure M A0" unfolding int_f_eq_y
1.48        using `f \<in> G`
1.49        by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive)
1.50 -    also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
1.51 +    also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
1.52        by (simp cong: positive_integral_cong)
1.53      finally have "?y < integral\<^isup>P M ?f0" by simp
1.54      moreover from `?f0 \<in> G` have "integral\<^isup>P M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
1.55 @@ -536,7 +536,7 @@
1.56    let ?a = "SUP Q:?Q. emeasure M Q"
1.57    have "{} \<in> ?Q" by auto
1.58    then have Q_not_empty: "?Q \<noteq> {}" by blast
1.59 -  have "?a \<le> emeasure M (space M)" using sets_into_space
1.60 +  have "?a \<le> emeasure M (space M)" using sets.sets_into_space
1.61      by (auto intro!: SUP_least emeasure_mono)
1.62    then have "?a \<noteq> \<infinity>" using finite_emeasure_space
1.63      by auto
1.64 @@ -601,7 +601,7 @@
1.65          next
1.66            assume "emeasure M A \<noteq> 0" with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
1.67            with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \<union> A)"
1.68 -            using Q' by (auto intro!: plus_emeasure countable_UN)
1.69 +            using Q' by (auto intro!: plus_emeasure sets.countable_UN)
1.70            also have "\<dots> = (SUP i. emeasure M (?O i \<union> A))"
1.71            proof (rule SUP_emeasure_incseq[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
1.72              show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
1.73 @@ -712,7 +712,7 @@
1.74        also have "\<dots> = (\<integral>\<^isup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) \<partial>M) + \<infinity> * emeasure M (Q0 \<inter> A)"
1.75          using borel Qi Q0(1) `A \<in> sets M`
1.76          by (subst positive_integral_add) (auto simp del: ereal_infty_mult
1.77 -            simp add: positive_integral_cmult_indicator Int intro!: suminf_0_le)
1.78 +            simp add: positive_integral_cmult_indicator sets.Int intro!: suminf_0_le)
1.79        also have "\<dots> = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)"
1.80          by (subst integral_eq[OF `A \<in> sets M`], subst positive_integral_suminf) auto
1.81        finally have "(\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M) = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)" .
1.82 @@ -727,7 +727,7 @@
1.83        moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
1.84          using Q_sets `A \<in> sets M` Q0(1) by auto
1.85        moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
1.86 -        using `A \<in> sets M` sets_into_space Q0 by auto
1.87 +        using `A \<in> sets M` sets.sets_into_space Q0 by auto
1.88        ultimately have "N A = (\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M)"
1.89          using plus_emeasure[of "(\<Union>i. Q i) \<inter> A" N "Q0 \<inter> A"] by (simp add: sets_eq)
1.90        with `A \<in> sets M` borel Q Q0(1) show "emeasure (density M ?f) A = N A"
1.91 @@ -755,7 +755,7 @@
1.92      fix A assume "A \<in> null_sets ?MT"
1.93      with borel have "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> h x \<le> 0"
1.94        by (auto simp add: null_sets_density_iff)
1.95 -    with pos sets_into_space have "AE x in M. x \<notin> A"
1.96 +    with pos sets.sets_into_space have "AE x in M. x \<notin> A"
1.97        by (elim eventually_elim1) (auto simp: not_le[symmetric])
1.98      then have "A \<in> null_sets M"
1.99        using `A \<in> sets M` by (simp add: AE_iff_null_sets)
1.100 @@ -784,7 +784,7 @@
1.101    assume "density M f = density M g"
1.102    with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
1.104 -  from this[THEN bspec, OF top] fin
1.105 +  from this[THEN bspec, OF sets.top] fin
1.106    have g_fin: "integral\<^isup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
1.107    { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1.108        and pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
1.109 @@ -898,7 +898,7 @@
1.110    let ?f'M = "density M f'"
1.111    { fix A assume "A \<in> sets M"
1.112      then have "{x \<in> space M. h x * indicator A x \<noteq> 0} = A"
1.113 -      using pos(1) sets_into_space by (force simp: indicator_def)
1.114 +      using pos(1) sets.sets_into_space by (force simp: indicator_def)
1.115      then have "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M) = 0 \<longleftrightarrow> A \<in> null_sets M"
1.116        using h_borel `A \<in> sets M` h_nn by (subst positive_integral_0_iff) auto }
1.117    note h_null_sets = this
1.118 @@ -994,7 +994,7 @@
1.119    def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ereal(of_nat (Suc n))}) \<inter> space M"
1.120    { fix i j have "A i \<inter> Q j \<in> sets M"
1.121      unfolding A_def using f Q
1.122 -    apply (rule_tac Int)
1.123 +    apply (rule_tac sets.Int)
1.124      by (cases i) (auto intro: measurable_sets[OF f(1)]) }
1.125    note A_in_sets = this
1.126    let ?A = "\<lambda>n. case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
1.127 @@ -1133,12 +1133,12 @@
1.128    note sets_eq_imp_space_eq[OF N, simp]
1.129    have measurable_N[simp]: "\<And>M'. measurable N M' = measurable M M'" by (auto simp: measurable_def)
1.130    { fix A assume "A \<in> sets M"
1.131 -    with inv T T' sets_into_space[OF this]
1.132 +    with inv T T' sets.sets_into_space[OF this]
1.133      have "T -` T' -` A \<inter> T -` space M' \<inter> space M = A"
1.134        by (auto simp: measurable_def) }
1.135    note eq = this[simp]
1.136    { fix A assume "A \<in> sets M"
1.137 -    with inv T T' sets_into_space[OF this]
1.138 +    with inv T T' sets.sets_into_space[OF this]
1.139      have "(T' \<circ> T) -` A \<inter> space M = A"
1.140        by (auto simp: measurable_def) }
1.141    note eq2 = this[simp]
1.142 @@ -1168,7 +1168,7 @@
1.143
1.144    have "N = distr N M (T' \<circ> T)"
1.145      by (subst measure_of_of_measure[of N, symmetric])
1.146 -       (auto simp add: distr_def sigma_sets_eq intro!: measure_of_eq space_closed)
1.147 +       (auto simp add: distr_def sets.sigma_sets_eq intro!: measure_of_eq sets.space_closed)
1.148    also have "\<dots> = distr (distr N M' T) M T'"
1.149      using T T' by (simp add: distr_distr)
1.150    also have "\<dots> = distr (density (distr M M' T) (RN_deriv (distr M M' T) (distr N M' T))) M T'"
```