add measurability prover; add support for Borel sets
authorhoelzl
Fri Nov 02 14:23:40 2012 +0100 (2012-11-02)
changeset 50002ce0d316b5b44
parent 50001 382bd3173584
child 50003 8c213922ed49
add measurability prover; add support for Borel sets
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
     1.3 @@ -100,7 +100,9 @@
     1.4  
     1.5  lemma measurable_pair_iff:
     1.6    "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.7 -  using measurable_pair[of f M M1 M2] by auto
     1.8 +  using measurable_pair[of f M M1 M2]
     1.9 +  using [[simproc del: measurable]] (* the measurable method is nonterminating when using measurable_pair *)
    1.10 +  by auto
    1.11  
    1.12  lemma measurable_split_conv:
    1.13    "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"
     2.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:00:39 2012 +0100
     2.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:23:40 2012 +0100
     2.3 @@ -30,14 +30,20 @@
     2.4  lemma space_borel[simp]: "space borel = UNIV"
     2.5    unfolding borel_def by auto
     2.6  
     2.7 -lemma borel_open[simp]:
     2.8 +lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
     2.9 +  unfolding borel_def by auto
    2.10 +
    2.11 +lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
    2.12 +  unfolding borel_def pred_def by auto
    2.13 +
    2.14 +lemma borel_open[simp, measurable (raw generic)]:
    2.15    assumes "open A" shows "A \<in> sets borel"
    2.16  proof -
    2.17    have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
    2.18    thus ?thesis unfolding borel_def by auto
    2.19  qed
    2.20  
    2.21 -lemma borel_closed[simp]:
    2.22 +lemma borel_closed[simp, measurable (raw generic)]:
    2.23    assumes "closed A" shows "A \<in> sets borel"
    2.24  proof -
    2.25    have "space borel - (- A) \<in> sets borel"
    2.26 @@ -45,23 +51,18 @@
    2.27    thus ?thesis by simp
    2.28  qed
    2.29  
    2.30 -lemma borel_comp[intro,simp]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
    2.31 -  unfolding Compl_eq_Diff_UNIV by (intro Diff) auto
    2.32 +lemma borel_insert[measurable]:
    2.33 +  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t2_space measure)"
    2.34 +  unfolding insert_def by (rule Un) auto
    2.35 +
    2.36 +lemma borel_comp[intro, simp, measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
    2.37 +  unfolding Compl_eq_Diff_UNIV by simp
    2.38  
    2.39  lemma borel_measurable_vimage:
    2.40    fixes f :: "'a \<Rightarrow> 'x::t2_space"
    2.41 -  assumes borel: "f \<in> borel_measurable M"
    2.42 +  assumes borel[measurable]: "f \<in> borel_measurable M"
    2.43    shows "f -` {x} \<inter> space M \<in> sets M"
    2.44 -proof (cases "x \<in> f ` space M")
    2.45 -  case True then obtain y where "x = f y" by auto
    2.46 -  from closed_singleton[of "f y"]
    2.47 -  have "{f y} \<in> sets borel" by (rule borel_closed)
    2.48 -  with assms show ?thesis
    2.49 -    unfolding in_borel_measurable_borel `x = f y` by auto
    2.50 -next
    2.51 -  case False hence "f -` {x} \<inter> space M = {}" by auto
    2.52 -  thus ?thesis by auto
    2.53 -qed
    2.54 +  by simp
    2.55  
    2.56  lemma borel_measurableI:
    2.57    fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space"
    2.58 @@ -81,7 +82,7 @@
    2.59        using closed_singleton[of x] by (rule borel_closed)
    2.60    qed simp
    2.61  
    2.62 -lemma borel_measurable_const[simp, intro]:
    2.63 +lemma borel_measurable_const[simp, intro, measurable (raw)]:
    2.64    "(\<lambda>x. c) \<in> borel_measurable M"
    2.65    by auto
    2.66  
    2.67 @@ -91,7 +92,7 @@
    2.68    unfolding indicator_def [abs_def] using A
    2.69    by (auto intro!: measurable_If_set)
    2.70  
    2.71 -lemma borel_measurable_indicator': 
    2.72 +lemma borel_measurable_indicator'[measurable]:
    2.73    "{x\<in>space M. x \<in> A} \<in> sets M \<Longrightarrow> indicator A \<in> borel_measurable M"
    2.74    unfolding indicator_def[abs_def]
    2.75    by (auto intro!: measurable_If)
    2.76 @@ -119,115 +120,63 @@
    2.77    shows "f \<in> borel_measurable M"
    2.78    using assms unfolding measurable_def by auto
    2.79  
    2.80 +lemma borel_measurable_continuous_on1:
    2.81 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
    2.82 +  assumes "continuous_on UNIV f"
    2.83 +  shows "f \<in> borel_measurable borel"
    2.84 +  apply(rule borel_measurableI)
    2.85 +  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
    2.86 +
    2.87  section "Borel spaces on euclidean spaces"
    2.88  
    2.89 -lemma lessThan_borel[simp, intro]:
    2.90 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
    2.91 -  shows "{..< a} \<in> sets borel"
    2.92 -  by (blast intro: borel_open)
    2.93 -
    2.94 -lemma greaterThan_borel[simp, intro]:
    2.95 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
    2.96 -  shows "{a <..} \<in> sets borel"
    2.97 -  by (blast intro: borel_open)
    2.98 -
    2.99 -lemma greaterThanLessThan_borel[simp, intro]:
   2.100 -  fixes a b :: "'a\<Colon>ordered_euclidean_space"
   2.101 -  shows "{a<..<b} \<in> sets borel"
   2.102 -  by (blast intro: borel_open)
   2.103 +lemma borel_measurable_euclidean_component'[measurable]:
   2.104 +  "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
   2.105 +  by (intro continuous_on_euclidean_component continuous_on_id borel_measurable_continuous_on1)
   2.106  
   2.107 -lemma atMost_borel[simp, intro]:
   2.108 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   2.109 -  shows "{..a} \<in> sets borel"
   2.110 -  by (blast intro: borel_closed)
   2.111 -
   2.112 -lemma atLeast_borel[simp, intro]:
   2.113 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   2.114 -  shows "{a..} \<in> sets borel"
   2.115 -  by (blast intro: borel_closed)
   2.116 -
   2.117 -lemma atLeastAtMost_borel[simp, intro]:
   2.118 -  fixes a b :: "'a\<Colon>ordered_euclidean_space"
   2.119 -  shows "{a..b} \<in> sets borel"
   2.120 -  by (blast intro: borel_closed)
   2.121 +lemma borel_measurable_euclidean_component:
   2.122 +  "(f :: 'a \<Rightarrow> 'b::euclidean_space) \<in> borel_measurable M \<Longrightarrow>(\<lambda>x. f x $$ i) \<in> borel_measurable M"
   2.123 +  by simp
   2.124  
   2.125 -lemma greaterThanAtMost_borel[simp, intro]:
   2.126 -  fixes a b :: "'a\<Colon>ordered_euclidean_space"
   2.127 -  shows "{a<..b} \<in> sets borel"
   2.128 -  unfolding greaterThanAtMost_def by blast
   2.129 -
   2.130 -lemma atLeastLessThan_borel[simp, intro]:
   2.131 +lemma [simp, intro, measurable]:
   2.132    fixes a b :: "'a\<Colon>ordered_euclidean_space"
   2.133 -  shows "{a..<b} \<in> sets borel"
   2.134 -  unfolding atLeastLessThan_def by blast
   2.135 -
   2.136 -lemma hafspace_less_borel[simp, intro]:
   2.137 -  fixes a :: real
   2.138 -  shows "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
   2.139 -  by (auto intro!: borel_open open_halfspace_component_gt)
   2.140 +  shows lessThan_borel: "{..< a} \<in> sets borel"
   2.141 +    and greaterThan_borel: "{a <..} \<in> sets borel"
   2.142 +    and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel"
   2.143 +    and atMost_borel: "{..a} \<in> sets borel"
   2.144 +    and atLeast_borel: "{a..} \<in> sets borel"
   2.145 +    and atLeastAtMost_borel: "{a..b} \<in> sets borel"
   2.146 +    and greaterThanAtMost_borel: "{a<..b} \<in> sets borel"
   2.147 +    and atLeastLessThan_borel: "{a..<b} \<in> sets borel"
   2.148 +  unfolding greaterThanAtMost_def atLeastLessThan_def
   2.149 +  by (blast intro: borel_open borel_closed)+
   2.150  
   2.151 -lemma hafspace_greater_borel[simp, intro]:
   2.152 -  fixes a :: real
   2.153 -  shows "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
   2.154 -  by (auto intro!: borel_open open_halfspace_component_lt)
   2.155 +lemma 
   2.156 +  shows hafspace_less_borel[simp, intro]: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
   2.157 +    and hafspace_greater_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
   2.158 +    and hafspace_less_eq_borel[simp, intro]: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
   2.159 +    and hafspace_greater_eq_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
   2.160 +  by simp_all
   2.161  
   2.162 -lemma hafspace_less_eq_borel[simp, intro]:
   2.163 -  fixes a :: real
   2.164 -  shows "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
   2.165 -  by (auto intro!: borel_closed closed_halfspace_component_ge)
   2.166 -
   2.167 -lemma hafspace_greater_eq_borel[simp, intro]:
   2.168 -  fixes a :: real
   2.169 -  shows "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
   2.170 -  by (auto intro!: borel_closed closed_halfspace_component_le)
   2.171 -
   2.172 -lemma borel_measurable_less[simp, intro]:
   2.173 +lemma borel_measurable_less[simp, intro, measurable]:
   2.174    fixes f :: "'a \<Rightarrow> real"
   2.175    assumes f: "f \<in> borel_measurable M"
   2.176    assumes g: "g \<in> borel_measurable M"
   2.177    shows "{w \<in> space M. f w < g w} \<in> sets M"
   2.178  proof -
   2.179 -  have "{w \<in> space M. f w < g w} =
   2.180 -        (\<Union>r. (f -` {..< of_rat r} \<inter> space M) \<inter> (g -` {of_rat r <..} \<inter> space M))"
   2.181 +  have "{w \<in> space M. f w < g w} = {x \<in> space M. \<exists>r. f x < of_rat r \<and> of_rat r < g x}"
   2.182      using Rats_dense_in_real by (auto simp add: Rats_def)
   2.183 -  then show ?thesis using f g
   2.184 -    by simp (blast intro: measurable_sets)
   2.185 -qed
   2.186 -
   2.187 -lemma borel_measurable_le[simp, intro]:
   2.188 -  fixes f :: "'a \<Rightarrow> real"
   2.189 -  assumes f: "f \<in> borel_measurable M"
   2.190 -  assumes g: "g \<in> borel_measurable M"
   2.191 -  shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
   2.192 -proof -
   2.193 -  have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}"
   2.194 -    by auto
   2.195 -  thus ?thesis using f g
   2.196 -    by simp blast
   2.197 +  with f g show ?thesis
   2.198 +    by simp
   2.199  qed
   2.200  
   2.201 -lemma borel_measurable_eq[simp, intro]:
   2.202 +lemma [simp, intro]:
   2.203    fixes f :: "'a \<Rightarrow> real"
   2.204 -  assumes f: "f \<in> borel_measurable M"
   2.205 -  assumes g: "g \<in> borel_measurable M"
   2.206 -  shows "{w \<in> space M. f w = g w} \<in> sets M"
   2.207 -proof -
   2.208 -  have "{w \<in> space M. f w = g w} =
   2.209 -        {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
   2.210 -    by auto
   2.211 -  thus ?thesis using f g by auto
   2.212 -qed
   2.213 -
   2.214 -lemma borel_measurable_neq[simp, intro]:
   2.215 -  fixes f :: "'a \<Rightarrow> real"
   2.216 -  assumes f: "f \<in> borel_measurable M"
   2.217 -  assumes g: "g \<in> borel_measurable M"
   2.218 -  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
   2.219 -proof -
   2.220 -  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
   2.221 -    by auto
   2.222 -  thus ?thesis using f g by auto
   2.223 -qed
   2.224 +  assumes f[measurable]: "f \<in> borel_measurable M"
   2.225 +  assumes g[measurable]: "g \<in> borel_measurable M"
   2.226 +  shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
   2.227 +    and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"
   2.228 +    and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
   2.229 +  unfolding eq_iff not_less[symmetric] by measurable+
   2.230  
   2.231  subsection "Borel space equals sigma algebras over intervals"
   2.232  
   2.233 @@ -377,7 +326,7 @@
   2.234      by (intro sigma_algebra_sigma_sets) simp_all
   2.235    have *: "?set = (\<Union>n. UNIV - {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})"
   2.236    proof (safe, simp_all add: not_less)
   2.237 -    fix x assume "a < x $$ i"
   2.238 +    fix x :: 'a assume "a < x $$ i"
   2.239      with reals_Archimedean[of "x $$ i - a"]
   2.240      obtain n where "a + 1 / real (Suc n) < x $$ i"
   2.241        by (auto simp: inverse_eq_divide field_simps)
   2.242 @@ -390,7 +339,7 @@
   2.243      finally show "a < x" .
   2.244    qed
   2.245    show "?set \<in> ?SIGMA" unfolding *
   2.246 -    by (auto intro!: Diff)
   2.247 +    by (auto del: Diff intro!: Diff)
   2.248  qed
   2.249  
   2.250  lemma borel_eq_halfspace_less:
   2.251 @@ -631,27 +580,13 @@
   2.252  
   2.253  lemma borel_measurable_iff_ge:
   2.254    "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
   2.255 -  using borel_measurable_iff_halfspace_ge[where 'c=real] by simp
   2.256 +  using borel_measurable_iff_halfspace_ge[where 'c=real]
   2.257 +  by simp
   2.258  
   2.259  lemma borel_measurable_iff_greater:
   2.260    "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
   2.261    using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
   2.262  
   2.263 -lemma borel_measurable_euclidean_component':
   2.264 -  "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
   2.265 -proof (rule borel_measurableI)
   2.266 -  fix S::"real set" assume "open S"
   2.267 -  from open_vimage_euclidean_component[OF this]
   2.268 -  show "(\<lambda>x. x $$ i) -` S \<inter> space borel \<in> sets borel"
   2.269 -    by (auto intro: borel_open)
   2.270 -qed
   2.271 -
   2.272 -lemma borel_measurable_euclidean_component:
   2.273 -  fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   2.274 -  assumes f: "f \<in> borel_measurable M"
   2.275 -  shows "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
   2.276 -  using measurable_comp[OF f borel_measurable_euclidean_component'] by (simp add: comp_def)
   2.277 -
   2.278  lemma borel_measurable_euclidean_space:
   2.279    fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   2.280    shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)"
   2.281 @@ -667,13 +602,6 @@
   2.282  
   2.283  subsection "Borel measurable operators"
   2.284  
   2.285 -lemma borel_measurable_continuous_on1:
   2.286 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   2.287 -  assumes "continuous_on UNIV f"
   2.288 -  shows "f \<in> borel_measurable borel"
   2.289 -  apply(rule borel_measurableI)
   2.290 -  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
   2.291 -
   2.292  lemma borel_measurable_continuous_on:
   2.293    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   2.294    assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
   2.295 @@ -693,7 +621,7 @@
   2.296      {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
   2.297      by (auto split: split_if_asm)
   2.298    also have "\<dots> \<in> sets borel"
   2.299 -    using * `open A` by (auto simp del: space_borel intro!: Un)
   2.300 +    using * `open A` by auto
   2.301    finally show "?f -` S \<inter> space borel \<in> sets borel" .
   2.302  qed
   2.303  
   2.304 @@ -705,7 +633,7 @@
   2.305    using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
   2.306    by (simp add: comp_def)
   2.307  
   2.308 -lemma borel_measurable_uminus[simp, intro]:
   2.309 +lemma borel_measurable_uminus[simp, intro, measurable (raw)]:
   2.310    fixes g :: "'a \<Rightarrow> real"
   2.311    assumes g: "g \<in> borel_measurable M"
   2.312    shows "(\<lambda>x. - g x) \<in> borel_measurable M"
   2.313 @@ -716,7 +644,7 @@
   2.314    shows "x $$ i = (if i < DIM('a) then fst x $$ i else snd x $$ (i - DIM('a)))"
   2.315    unfolding euclidean_component_def basis_prod_def inner_prod_def by auto
   2.316  
   2.317 -lemma borel_measurable_Pair[simp, intro]:
   2.318 +lemma borel_measurable_Pair[simp, intro, measurable (raw)]:
   2.319    fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   2.320    assumes f: "f \<in> borel_measurable M"
   2.321    assumes g: "g \<in> borel_measurable M"
   2.322 @@ -726,7 +654,7 @@
   2.323    have [simp]: "\<And>P A B C. {w. (P \<longrightarrow> A w \<and> B w) \<and> (\<not> P \<longrightarrow> A w \<and> C w)} = 
   2.324      {w. A w \<and> (P \<longrightarrow> B w) \<and> (\<not> P \<longrightarrow> C w)}" by auto
   2.325    from i f g show "{w \<in> space M. (f w, g w) $$ i \<le> a} \<in> sets M"
   2.326 -    by (auto simp: euclidean_component_prod intro!: sets_Collect borel_measurable_euclidean_component)
   2.327 +    by (auto simp: euclidean_component_prod)
   2.328  qed
   2.329  
   2.330  lemma continuous_on_fst: "continuous_on UNIV fst"
   2.331 @@ -757,7 +685,7 @@
   2.332      unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
   2.333  qed
   2.334  
   2.335 -lemma borel_measurable_add[simp, intro]:
   2.336 +lemma borel_measurable_add[simp, intro, measurable (raw)]:
   2.337    fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   2.338    assumes f: "f \<in> borel_measurable M"
   2.339    assumes g: "g \<in> borel_measurable M"
   2.340 @@ -766,7 +694,7 @@
   2.341    by (rule borel_measurable_continuous_Pair)
   2.342       (auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
   2.343  
   2.344 -lemma borel_measurable_setsum[simp, intro]:
   2.345 +lemma borel_measurable_setsum[simp, intro, measurable (raw)]:
   2.346    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   2.347    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   2.348    shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
   2.349 @@ -775,14 +703,14 @@
   2.350    thus ?thesis using assms by induct auto
   2.351  qed simp
   2.352  
   2.353 -lemma borel_measurable_diff[simp, intro]:
   2.354 +lemma borel_measurable_diff[simp, intro, measurable (raw)]:
   2.355    fixes f :: "'a \<Rightarrow> real"
   2.356    assumes f: "f \<in> borel_measurable M"
   2.357    assumes g: "g \<in> borel_measurable M"
   2.358    shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   2.359    unfolding diff_minus using assms by fast
   2.360  
   2.361 -lemma borel_measurable_times[simp, intro]:
   2.362 +lemma borel_measurable_times[simp, intro, measurable (raw)]:
   2.363    fixes f :: "'a \<Rightarrow> real"
   2.364    assumes f: "f \<in> borel_measurable M"
   2.365    assumes g: "g \<in> borel_measurable M"
   2.366 @@ -796,7 +724,7 @@
   2.367    shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
   2.368    unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
   2.369  
   2.370 -lemma borel_measurable_dist[simp, intro]:
   2.371 +lemma borel_measurable_dist[simp, intro, measurable (raw)]:
   2.372    fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
   2.373    assumes f: "f \<in> borel_measurable M"
   2.374    assumes g: "g \<in> borel_measurable M"
   2.375 @@ -805,6 +733,14 @@
   2.376    by (rule borel_measurable_continuous_Pair)
   2.377       (intro continuous_on_dist continuous_on_fst continuous_on_snd)
   2.378    
   2.379 +lemma borel_measurable_scaleR[measurable (raw)]:
   2.380 +  fixes g :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
   2.381 +  assumes f: "f \<in> borel_measurable M"
   2.382 +  assumes g: "g \<in> borel_measurable M"
   2.383 +  shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
   2.384 +  by (rule borel_measurable_continuous_Pair[OF f g])
   2.385 +     (auto intro!: continuous_on_scaleR continuous_on_fst continuous_on_snd)
   2.386 +
   2.387  lemma affine_borel_measurable_vector:
   2.388    fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
   2.389    assumes "f \<in> borel_measurable M"
   2.390 @@ -825,13 +761,15 @@
   2.391    qed simp
   2.392  qed
   2.393  
   2.394 -lemma affine_borel_measurable:
   2.395 -  fixes g :: "'a \<Rightarrow> real"
   2.396 -  assumes g: "g \<in> borel_measurable M"
   2.397 -  shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
   2.398 -  using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute)
   2.399 +lemma borel_measurable_const_scaleR[measurable (raw)]:
   2.400 +  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. b *\<^sub>R f x ::'a::real_normed_vector) \<in> borel_measurable M"
   2.401 +  using affine_borel_measurable_vector[of f M 0 b] by simp
   2.402  
   2.403 -lemma borel_measurable_setprod[simp, intro]:
   2.404 +lemma borel_measurable_const_add[measurable (raw)]:
   2.405 +  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M"
   2.406 +  using affine_borel_measurable_vector[of f M a 1] by simp
   2.407 +
   2.408 +lemma borel_measurable_setprod[simp, intro, measurable (raw)]:
   2.409    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   2.410    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   2.411    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
   2.412 @@ -840,7 +778,7 @@
   2.413    thus ?thesis using assms by induct auto
   2.414  qed simp
   2.415  
   2.416 -lemma borel_measurable_inverse[simp, intro]:
   2.417 +lemma borel_measurable_inverse[simp, intro, measurable (raw)]:
   2.418    fixes f :: "'a \<Rightarrow> real"
   2.419    assumes f: "f \<in> borel_measurable M"
   2.420    shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
   2.421 @@ -853,7 +791,7 @@
   2.422      done
   2.423  qed
   2.424  
   2.425 -lemma borel_measurable_divide[simp, intro]:
   2.426 +lemma borel_measurable_divide[simp, intro, measurable (raw)]:
   2.427    fixes f :: "'a \<Rightarrow> real"
   2.428    assumes "f \<in> borel_measurable M"
   2.429    and "g \<in> borel_measurable M"
   2.430 @@ -861,21 +799,21 @@
   2.431    unfolding field_divide_inverse
   2.432    by (rule borel_measurable_inverse borel_measurable_times assms)+
   2.433  
   2.434 -lemma borel_measurable_max[intro, simp]:
   2.435 +lemma borel_measurable_max[intro, simp, measurable (raw)]:
   2.436    fixes f g :: "'a \<Rightarrow> real"
   2.437    assumes "f \<in> borel_measurable M"
   2.438    assumes "g \<in> borel_measurable M"
   2.439    shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
   2.440    unfolding max_def by (auto intro!: assms measurable_If)
   2.441  
   2.442 -lemma borel_measurable_min[intro, simp]:
   2.443 +lemma borel_measurable_min[intro, simp, measurable (raw)]:
   2.444    fixes f g :: "'a \<Rightarrow> real"
   2.445    assumes "f \<in> borel_measurable M"
   2.446    assumes "g \<in> borel_measurable M"
   2.447    shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
   2.448    unfolding min_def by (auto intro!: assms measurable_If)
   2.449  
   2.450 -lemma borel_measurable_abs[simp, intro]:
   2.451 +lemma borel_measurable_abs[simp, intro, measurable (raw)]:
   2.452    assumes "f \<in> borel_measurable M"
   2.453    shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
   2.454  proof -
   2.455 @@ -883,7 +821,7 @@
   2.456    show ?thesis unfolding * using assms by auto
   2.457  qed
   2.458  
   2.459 -lemma borel_measurable_nth[simp, intro]:
   2.460 +lemma borel_measurable_nth[simp, intro, measurable (raw)]:
   2.461    "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
   2.462    using borel_measurable_euclidean_component'
   2.463    unfolding nth_conv_component by auto
   2.464 @@ -900,12 +838,12 @@
   2.465      from this q show "continuous_on {a<..<b} q"
   2.466        by (rule convex_on_continuous)
   2.467    qed
   2.468 -  moreover have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
   2.469 +  also have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
   2.470      using X by (intro measurable_cong) auto
   2.471 -  ultimately show ?thesis by simp
   2.472 +  finally show ?thesis .
   2.473  qed
   2.474  
   2.475 -lemma borel_measurable_ln[simp,intro]:
   2.476 +lemma borel_measurable_ln[simp, intro, measurable (raw)]:
   2.477    assumes f: "f \<in> borel_measurable M"
   2.478    shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
   2.479  proof -
   2.480 @@ -926,39 +864,55 @@
   2.481    finally show ?thesis .
   2.482  qed
   2.483  
   2.484 -lemma borel_measurable_log[simp,intro]:
   2.485 -  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log b (f x)) \<in> borel_measurable M"
   2.486 +lemma borel_measurable_log[simp, intro, measurable (raw)]:
   2.487 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
   2.488    unfolding log_def by auto
   2.489  
   2.490 -lemma borel_measurable_real_floor:
   2.491 -  "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
   2.492 -  unfolding borel_measurable_iff_ge
   2.493 -proof (intro allI)
   2.494 -  fix a :: real
   2.495 -  { fix x have "a \<le> real \<lfloor>x\<rfloor> \<longleftrightarrow> real \<lceil>a\<rceil> \<le> x"
   2.496 -      using le_floor_eq[of "\<lceil>a\<rceil>" x] ceiling_le_iff[of a "\<lfloor>x\<rfloor>"]
   2.497 -      unfolding real_eq_of_int by simp }
   2.498 -  then have "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} = {real \<lceil>a\<rceil>..}" by auto
   2.499 -  then show "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} \<in> sets borel" by auto
   2.500 +lemma measurable_count_space_eq2_countable:
   2.501 +  fixes f :: "'a => 'c::countable"
   2.502 +  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
   2.503 +proof -
   2.504 +  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
   2.505 +    then have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)"
   2.506 +      by auto
   2.507 +    moreover assume "\<And>a. a\<in>A \<Longrightarrow> f -` {a} \<inter> space M \<in> sets M"
   2.508 +    ultimately have "f -` X \<inter> space M \<in> sets M"
   2.509 +      using `X \<subseteq> A` by (simp add: subset_eq del: UN_simps) }
   2.510 +  then show ?thesis
   2.511 +    unfolding measurable_def by auto
   2.512  qed
   2.513  
   2.514 -lemma borel_measurable_real_natfloor[intro, simp]:
   2.515 -  assumes "f \<in> borel_measurable M"
   2.516 -  shows "(\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
   2.517 +lemma measurable_real_floor[measurable]:
   2.518 +  "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
   2.519  proof -
   2.520 -  have "\<And>x. real (natfloor (f x)) = max 0 (real \<lfloor>f x\<rfloor>)"
   2.521 -    by (auto simp: max_def natfloor_def)
   2.522 -  with borel_measurable_max[OF measurable_comp[OF assms borel_measurable_real_floor] borel_measurable_const]
   2.523 -  show ?thesis by (simp add: comp_def)
   2.524 +  have "\<And>a x. \<lfloor>x\<rfloor> = a \<longleftrightarrow> (real a \<le> x \<and> x < real (a + 1))"
   2.525 +    by (auto intro: floor_eq2)
   2.526 +  then show ?thesis
   2.527 +    by (auto simp: vimage_def measurable_count_space_eq2_countable)
   2.528  qed
   2.529  
   2.530 +lemma measurable_real_natfloor[measurable]:
   2.531 +  "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
   2.532 +  by (simp add: natfloor_def[abs_def])
   2.533 +
   2.534 +lemma measurable_real_ceiling[measurable]:
   2.535 +  "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
   2.536 +  unfolding ceiling_def[abs_def] by simp
   2.537 +
   2.538 +lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
   2.539 +  by simp
   2.540 +
   2.541 +lemma borel_measurable_real_natfloor[intro, simp]:
   2.542 +  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
   2.543 +  by simp
   2.544 +
   2.545  subsection "Borel space on the extended reals"
   2.546  
   2.547 -lemma borel_measurable_ereal[simp, intro]:
   2.548 +lemma borel_measurable_ereal[simp, intro, measurable (raw)]:
   2.549    assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
   2.550    using continuous_on_ereal f by (rule borel_measurable_continuous_on)
   2.551  
   2.552 -lemma borel_measurable_real_of_ereal[simp, intro]:
   2.553 +lemma borel_measurable_real_of_ereal[simp, intro, measurable (raw)]:
   2.554    fixes f :: "'a \<Rightarrow> ereal" 
   2.555    assumes f: "f \<in> borel_measurable M"
   2.556    shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
   2.557 @@ -977,20 +931,16 @@
   2.558    assumes H: "(\<lambda>x. H (ereal (real (f x)))) \<in> borel_measurable M"
   2.559    shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
   2.560  proof -
   2.561 -  let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then H \<infinity> else if x \<in> f -` {-\<infinity>} then H (-\<infinity>) else H (ereal (real (f x)))"
   2.562 +  let ?F = "\<lambda>x. if f x = \<infinity> then H \<infinity> else if f x = - \<infinity> then H (-\<infinity>) else H (ereal (real (f x)))"
   2.563    { fix x have "H (f x) = ?F x" by (cases "f x") auto }
   2.564 -  moreover 
   2.565 -  have "?F \<in> borel_measurable M"
   2.566 -    by (intro measurable_If_set f measurable_sets[OF f] H) auto
   2.567 -  ultimately
   2.568 -  show ?thesis by simp
   2.569 +  with f H show ?thesis by simp
   2.570  qed
   2.571  
   2.572  lemma
   2.573    fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M"
   2.574 -  shows borel_measurable_ereal_abs[intro, simp]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
   2.575 -    and borel_measurable_ereal_inverse[simp, intro]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
   2.576 -    and borel_measurable_uminus_ereal[intro]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
   2.577 +  shows borel_measurable_ereal_abs[intro, simp, measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
   2.578 +    and borel_measurable_ereal_inverse[simp, intro, measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
   2.579 +    and borel_measurable_uminus_ereal[intro, measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
   2.580    by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
   2.581  
   2.582  lemma borel_measurable_uminus_eq_ereal[simp]:
   2.583 @@ -999,44 +949,32 @@
   2.584    assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
   2.585  qed auto
   2.586  
   2.587 -lemma sets_Collect_If_set:
   2.588 -  assumes "A \<inter> space M \<in> sets M" "{x \<in> space M. P x} \<in> sets M" "{x \<in> space M. Q x} \<in> sets M"
   2.589 -  shows "{x \<in> space M. if x \<in> A then P x else Q x} \<in> sets M"
   2.590 -proof -
   2.591 -  have *: "{x \<in> space M. if x \<in> A then P x else Q x} = 
   2.592 -    {x \<in> space M. if x \<in> A \<inter> space M then P x else Q x}" by auto
   2.593 -  show ?thesis unfolding * unfolding if_bool_eq_conj using assms
   2.594 -    by (auto intro!: sets_Collect simp: Int_def conj_commute)
   2.595 -qed
   2.596 -
   2.597  lemma set_Collect_ereal2:
   2.598    fixes f g :: "'a \<Rightarrow> ereal" 
   2.599    assumes f: "f \<in> borel_measurable M"
   2.600    assumes g: "g \<in> borel_measurable M"
   2.601    assumes H: "{x \<in> space M. H (ereal (real (f x))) (ereal (real (g x)))} \<in> sets M"
   2.602 -    "{x \<in> space M. H (-\<infinity>) (ereal (real (g x)))} \<in> sets M"
   2.603 -    "{x \<in> space M. H (\<infinity>) (ereal (real (g x)))} \<in> sets M"
   2.604 -    "{x \<in> space M. H (ereal (real (f x))) (-\<infinity>)} \<in> sets M"
   2.605 -    "{x \<in> space M. H (ereal (real (f x))) (\<infinity>)} \<in> sets M"
   2.606 +    "{x \<in> space borel. H (-\<infinity>) (ereal x)} \<in> sets borel"
   2.607 +    "{x \<in> space borel. H (\<infinity>) (ereal x)} \<in> sets borel"
   2.608 +    "{x \<in> space borel. H (ereal x) (-\<infinity>)} \<in> sets borel"
   2.609 +    "{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel"
   2.610    shows "{x \<in> space M. H (f x) (g x)} \<in> sets M"
   2.611  proof -
   2.612 -  let ?G = "\<lambda>y x. if x \<in> g -` {\<infinity>} then H y \<infinity> else if x \<in> g -` {-\<infinity>} then H y (-\<infinity>) else H y (ereal (real (g x)))"
   2.613 -  let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then ?G \<infinity> x else if x \<in> f -` {-\<infinity>} then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
   2.614 +  let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = -\<infinity> then H y (-\<infinity>) else H y (ereal (real (g x)))"
   2.615 +  let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = -\<infinity> then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
   2.616    { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
   2.617 -  moreover 
   2.618 -  have "{x \<in> space M. ?F x} \<in> sets M"
   2.619 -    by (intro sets_Collect H measurable_sets[OF f] measurable_sets[OF g] sets_Collect_If_set) auto
   2.620 -  ultimately
   2.621 -  show ?thesis by simp
   2.622 +  note * = this
   2.623 +  from assms show ?thesis
   2.624 +    by (subst *) (simp del: space_borel split del: split_if)
   2.625  qed
   2.626  
   2.627  lemma
   2.628    fixes f g :: "'a \<Rightarrow> ereal"
   2.629    assumes f: "f \<in> borel_measurable M"
   2.630    assumes g: "g \<in> borel_measurable M"
   2.631 -  shows borel_measurable_ereal_le[intro,simp]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
   2.632 -    and borel_measurable_ereal_less[intro,simp]: "{x \<in> space M. f x < g x} \<in> sets M"
   2.633 -    and borel_measurable_ereal_eq[intro,simp]: "{w \<in> space M. f w = g w} \<in> sets M"
   2.634 +  shows borel_measurable_ereal_le[intro,simp,measurable(raw)]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
   2.635 +    and borel_measurable_ereal_less[intro,simp,measurable(raw)]: "{x \<in> space M. f x < g x} \<in> sets M"
   2.636 +    and borel_measurable_ereal_eq[intro,simp,measurable(raw)]: "{w \<in> space M. f w = g w} \<in> sets M"
   2.637      and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
   2.638    using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg)
   2.639  
   2.640 @@ -1060,7 +998,7 @@
   2.641    have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
   2.642    also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
   2.643    finally show "f \<in> borel_measurable M" .
   2.644 -qed (auto intro: measurable_sets borel_measurable_real_of_ereal)
   2.645 +qed simp_all
   2.646  
   2.647  lemma borel_measurable_eq_atMost_ereal:
   2.648    fixes f :: "'a \<Rightarrow> ereal"
   2.649 @@ -1080,7 +1018,8 @@
   2.650        qed }
   2.651      then have "f -` {\<infinity>} \<inter> space M = space M - (\<Union>i::nat. f -` {.. real i} \<inter> space M)"
   2.652        by (auto simp: not_le)
   2.653 -    then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos by (auto simp del: UN_simps intro!: Diff)
   2.654 +    then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos
   2.655 +      by (auto simp del: UN_simps)
   2.656      moreover
   2.657      have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto
   2.658      then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
   2.659 @@ -1150,14 +1089,11 @@
   2.660      "(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M"
   2.661    shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
   2.662  proof -
   2.663 -  let ?G = "\<lambda>y x. if x \<in> g -` {\<infinity>} then H y \<infinity> else if x \<in> g -` {-\<infinity>} then H y (-\<infinity>) else H y (ereal (real (g x)))"
   2.664 -  let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then ?G \<infinity> x else if x \<in> f -` {-\<infinity>} then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
   2.665 +  let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = - \<infinity> then H y (-\<infinity>) else H y (ereal (real (g x)))"
   2.666 +  let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = - \<infinity> then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
   2.667    { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
   2.668 -  moreover 
   2.669 -  have "?F \<in> borel_measurable M"
   2.670 -    by (intro measurable_If_set measurable_sets[OF f] measurable_sets[OF g] H) auto
   2.671 -  ultimately
   2.672 -  show ?thesis by simp
   2.673 +  note * = this
   2.674 +  from assms show ?thesis unfolding * by simp
   2.675  qed
   2.676  
   2.677  lemma
   2.678 @@ -1166,29 +1102,24 @@
   2.679      and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
   2.680    using f by auto
   2.681  
   2.682 -lemma split_sets:
   2.683 -  "{x\<in>space M. P x \<or> Q x} = {x\<in>space M. P x} \<union> {x\<in>space M. Q x}"
   2.684 -  "{x\<in>space M. P x \<and> Q x} = {x\<in>space M. P x} \<inter> {x\<in>space M. Q x}"
   2.685 -  by auto
   2.686 -
   2.687 -lemma
   2.688 +lemma [intro, simp, measurable(raw)]:
   2.689    fixes f :: "'a \<Rightarrow> ereal"
   2.690    assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   2.691 -  shows borel_measurable_ereal_add[intro, simp]: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
   2.692 -    and borel_measurable_ereal_times[intro, simp]: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
   2.693 -    and borel_measurable_ereal_min[simp, intro]: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
   2.694 -    and borel_measurable_ereal_max[simp, intro]: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
   2.695 +  shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
   2.696 +    and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
   2.697 +    and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
   2.698 +    and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
   2.699    by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def)
   2.700  
   2.701 -lemma
   2.702 +lemma [simp, intro, measurable(raw)]:
   2.703    fixes f g :: "'a \<Rightarrow> ereal"
   2.704    assumes "f \<in> borel_measurable M"
   2.705    assumes "g \<in> borel_measurable M"
   2.706 -  shows borel_measurable_ereal_diff[simp, intro]: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   2.707 -    and borel_measurable_ereal_divide[simp, intro]: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
   2.708 +  shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   2.709 +    and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
   2.710    unfolding minus_ereal_def divide_ereal_def using assms by auto
   2.711  
   2.712 -lemma borel_measurable_ereal_setsum[simp, intro]:
   2.713 +lemma borel_measurable_ereal_setsum[simp, intro,measurable (raw)]:
   2.714    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   2.715    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   2.716    shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
   2.717 @@ -1198,7 +1129,7 @@
   2.718      by induct auto
   2.719  qed simp
   2.720  
   2.721 -lemma borel_measurable_ereal_setprod[simp, intro]:
   2.722 +lemma borel_measurable_ereal_setprod[simp, intro,measurable (raw)]:
   2.723    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   2.724    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   2.725    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
   2.726 @@ -1207,7 +1138,7 @@
   2.727    thus ?thesis using assms by induct auto
   2.728  qed simp
   2.729  
   2.730 -lemma borel_measurable_SUP[simp, intro]:
   2.731 +lemma borel_measurable_SUP[simp, intro,measurable (raw)]:
   2.732    fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
   2.733    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   2.734    shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
   2.735 @@ -1220,7 +1151,7 @@
   2.736      using assms by auto
   2.737  qed
   2.738  
   2.739 -lemma borel_measurable_INF[simp, intro]:
   2.740 +lemma borel_measurable_INF[simp, intro,measurable (raw)]:
   2.741    fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
   2.742    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   2.743    shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
   2.744 @@ -1233,11 +1164,11 @@
   2.745      using assms by auto
   2.746  qed
   2.747  
   2.748 -lemma
   2.749 +lemma [simp, intro, measurable (raw)]:
   2.750    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   2.751    assumes "\<And>i. f i \<in> borel_measurable M"
   2.752 -  shows borel_measurable_liminf[simp, intro]: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   2.753 -    and borel_measurable_limsup[simp, intro]: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
   2.754 +  shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   2.755 +    and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
   2.756    unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
   2.757  
   2.758  lemma borel_measurable_ereal_LIMSEQ:
   2.759 @@ -1251,7 +1182,7 @@
   2.760    then show ?thesis by (simp add: u cong: measurable_cong)
   2.761  qed
   2.762  
   2.763 -lemma borel_measurable_psuminf[simp, intro]:
   2.764 +lemma borel_measurable_psuminf[simp, intro, measurable (raw)]:
   2.765    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   2.766    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.767    shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
   2.768 @@ -1275,38 +1206,38 @@
   2.769    ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
   2.770  qed
   2.771  
   2.772 -lemma sets_Collect_Cauchy: 
   2.773 +lemma sets_Collect_Cauchy[measurable]: 
   2.774    fixes f :: "nat \<Rightarrow> 'a => real"
   2.775 -  assumes f: "\<And>i. f i \<in> borel_measurable M"
   2.776 +  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   2.777    shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
   2.778 -  unfolding Cauchy_iff2 using f by (auto intro!: sets_Collect)
   2.779 +  unfolding Cauchy_iff2 using f by auto
   2.780  
   2.781 -lemma borel_measurable_lim:
   2.782 +lemma borel_measurable_lim[measurable (raw)]:
   2.783    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
   2.784 -  assumes f: "\<And>i. f i \<in> borel_measurable M"
   2.785 +  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   2.786    shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
   2.787  proof -
   2.788 -  have *: "\<And>x. lim (\<lambda>i. f i x) =
   2.789 -    (if Cauchy (\<lambda>i. f i x) then lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) else (THE x. False))"
   2.790 +  def u' \<equiv> "\<lambda>x. lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
   2.791 +  then have *: "\<And>x. lim (\<lambda>i. f i x) = (if Cauchy (\<lambda>i. f i x) then u' x else (THE x. False))"
   2.792      by (auto simp: lim_def convergent_eq_cauchy[symmetric])
   2.793 -  { fix x have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
   2.794 +  have "u' \<in> borel_measurable M"
   2.795 +  proof (rule borel_measurable_LIMSEQ)
   2.796 +    fix x
   2.797 +    have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
   2.798        by (cases "Cauchy (\<lambda>i. f i x)")
   2.799 -         (auto simp add: convergent_eq_cauchy[symmetric] convergent_def) }
   2.800 -  note convergent = this
   2.801 -  show ?thesis
   2.802 -    unfolding *
   2.803 -    apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
   2.804 -    apply (rule borel_measurable_LIMSEQ)
   2.805 -    apply (rule convergent_LIMSEQ_iff[THEN iffD1, OF convergent])
   2.806 -    apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
   2.807 -    done
   2.808 +         (auto simp add: convergent_eq_cauchy[symmetric] convergent_def)
   2.809 +    then show "(\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) ----> u' x"
   2.810 +      unfolding u'_def 
   2.811 +      by (rule convergent_LIMSEQ_iff[THEN iffD1])
   2.812 +  qed measurable
   2.813 +  then show ?thesis
   2.814 +    unfolding * by measurable
   2.815  qed
   2.816  
   2.817 -lemma borel_measurable_suminf:
   2.818 +lemma borel_measurable_suminf[measurable (raw)]:
   2.819    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
   2.820 -  assumes f: "\<And>i. f i \<in> borel_measurable M"
   2.821 +  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   2.822    shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   2.823 -  unfolding suminf_def sums_def[abs_def] lim_def[symmetric]
   2.824 -  by (simp add: f borel_measurable_lim)
   2.825 +  unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
   2.826  
   2.827  end 
     3.1 --- a/src/HOL/Probability/Information.thy	Fri Nov 02 14:00:39 2012 +0100
     3.2 +++ b/src/HOL/Probability/Information.thy	Fri Nov 02 14:23:40 2012 +0100
     3.3 @@ -446,7 +446,7 @@
     3.4    shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))"
     3.5    using assms unfolding finite_entropy_def
     3.6    using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"]
     3.7 -  by (auto intro: distributed_real_measurable)
     3.8 +  by (auto dest!: distributed_real_measurable)
     3.9  
    3.10  subsection {* Mutual Information *}
    3.11  
    3.12 @@ -1578,7 +1578,7 @@
    3.13    have "random_variable (count_space (X ` space M)) X"
    3.14      by (simp add: comp_def)
    3.15    then have "simple_function M X"    
    3.16 -    unfolding simple_function_def by auto
    3.17 +    unfolding simple_function_def by (auto simp: measurable_count_space_eq2)
    3.18    then have "simple_distributed M X ?Px"
    3.19      by (rule simple_distributedI) auto
    3.20    then show "distributed M (count_space (X ` space M)) X ?Px"
     4.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:00:39 2012 +0100
     4.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:23:40 2012 +0100
     4.3 @@ -70,7 +70,7 @@
     4.4    have "g -` X \<inter> space M = g -` (X \<inter> g`space M) \<inter> space M" by auto
     4.5    also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g-`{x} \<inter> space M)" by auto
     4.6    finally show "g -` X \<inter> space M \<in> sets M" using assms
     4.7 -    by (auto intro!: finite_UN simp del: UN_simps simp: simple_function_def)
     4.8 +    by (auto simp del: UN_simps simp: simple_function_def)
     4.9  qed
    4.10  
    4.11  lemma simple_function_measurable2[intro]:
    4.12 @@ -167,7 +167,7 @@
    4.13      (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
    4.14    show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
    4.15      using assms unfolding simple_function_def *
    4.16 -    by (rule_tac finite_UN) (auto intro!: finite_UN)
    4.17 +    by (rule_tac finite_UN) auto
    4.18  qed
    4.19  
    4.20  lemma simple_function_indicator[intro, simp]:
    4.21 @@ -1210,7 +1210,7 @@
    4.22      case (insert i P)
    4.23      then have "f i \<in> borel_measurable M" "AE x in M. 0 \<le> f i x"
    4.24        "(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M" "AE x in M. 0 \<le> (\<Sum>i\<in>P. f i x)"
    4.25 -      by (auto intro!: borel_measurable_ereal_setsum setsum_nonneg)
    4.26 +      by (auto intro!: setsum_nonneg)
    4.27      from positive_integral_add[OF this]
    4.28      show ?case using insert by auto
    4.29    qed simp
    4.30 @@ -1230,7 +1230,7 @@
    4.31        simp: indicator_def ereal_zero_le_0_iff)
    4.32    also have "\<dots> = c * (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)"
    4.33      using assms
    4.34 -    by (auto intro!: positive_integral_cmult borel_measurable_indicator simp: ereal_zero_le_0_iff)
    4.35 +    by (auto intro!: positive_integral_cmult simp: ereal_zero_le_0_iff)
    4.36    finally show ?thesis .
    4.37  qed
    4.38  
    4.39 @@ -1633,7 +1633,7 @@
    4.40  lemma integral_zero[simp, intro]:
    4.41    shows "integrable M (\<lambda>x. 0)" "(\<integral> x.0 \<partial>M) = 0"
    4.42    unfolding integrable_def lebesgue_integral_def
    4.43 -  by (auto simp add: borel_measurable_const)
    4.44 +  by auto
    4.45  
    4.46  lemma integral_cmult[simp, intro]:
    4.47    assumes "integrable M f"
    4.48 @@ -1644,7 +1644,7 @@
    4.49    proof (cases rule: le_cases)
    4.50      assume "0 \<le> a" show ?thesis
    4.51        using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
    4.52 -      by (simp add: integral_zero)
    4.53 +      by simp
    4.54    next
    4.55      assume "a \<le> 0" hence "0 \<le> - a" by auto
    4.56      have *: "\<And>t. - a * t + 0 = (-a) * t" by simp
    4.57 @@ -1718,7 +1718,7 @@
    4.58      by (auto split: split_indicator simp: positive_integral_0_iff_AE one_ereal_def)
    4.59    show ?int ?able
    4.60      using assms unfolding lebesgue_integral_def integrable_def
    4.61 -    by (auto simp: * positive_integral_indicator borel_measurable_indicator)
    4.62 +    by (auto simp: *)
    4.63  qed
    4.64  
    4.65  lemma integral_cmul_indicator:
    4.66 @@ -1850,7 +1850,7 @@
    4.67    assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
    4.68    shows "0 \<le> integral\<^isup>L M f"
    4.69  proof -
    4.70 -  have "0 = (\<integral>x. 0 \<partial>M)" by (auto simp: integral_zero)
    4.71 +  have "0 = (\<integral>x. 0 \<partial>M)" by auto
    4.72    also have "\<dots> \<le> integral\<^isup>L M f"
    4.73      using assms by (rule integral_mono[OF integral_zero(1)])
    4.74    finally show ?thesis .
    4.75 @@ -2206,7 +2206,7 @@
    4.76      let ?F = "\<lambda>n y. (\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
    4.77      let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
    4.78      have "\<And>n. integrable M (?F n)"
    4.79 -      using borel by (auto intro!: integral_setsum integrable_abs)
    4.80 +      using borel by (auto intro!: integrable_abs)
    4.81      thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
    4.82      show "AE x in M. mono (\<lambda>n. ?w' n x)"
    4.83        by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
    4.84 @@ -2436,7 +2436,7 @@
    4.85    by (subst density_max_0) (auto intro!: arg_cong[where f="density M"] split: split_max)
    4.86  
    4.87  lemma emeasure_density:
    4.88 -  assumes f: "f \<in> borel_measurable M" and A: "A \<in> sets M"
    4.89 +  assumes f[measurable]: "f \<in> borel_measurable M" and A[measurable]: "A \<in> sets M"
    4.90    shows "emeasure (density M f) A = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"
    4.91      (is "_ = ?\<mu> A")
    4.92    unfolding density_def
    4.93 @@ -2453,8 +2453,9 @@
    4.94      unfolding \<mu>_eq
    4.95    proof (intro countably_additiveI)
    4.96      fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M"
    4.97 +    then have "\<And>i. A i \<in> sets M" by auto
    4.98      then have *: "\<And>i. (\<lambda>x. max 0 (f x) * indicator (A i) x) \<in> borel_measurable M"
    4.99 -      using f by (auto intro!: borel_measurable_ereal_times)
   4.100 +      by (auto simp: set_eq_iff)
   4.101      assume disj: "disjoint_family A"
   4.102      have "(\<Sum>n. ?\<mu>' (A n)) = (\<integral>\<^isup>+ x. (\<Sum>n. max 0 (f x) * indicator (A n) x) \<partial>M)"
   4.103        using f * by (simp add: positive_integral_suminf)
   4.104 @@ -2483,8 +2484,7 @@
   4.105        by (intro positive_integral_0_iff) auto
   4.106      also have "\<dots> \<longleftrightarrow> (AE x in M. max 0 (f x) * indicator A x = 0)"
   4.107        using f `A \<in> sets M`
   4.108 -      by (intro AE_iff_measurable[OF _ refl, symmetric])
   4.109 -         (auto intro!: sets_Collect borel_measurable_ereal_eq)
   4.110 +      by (intro AE_iff_measurable[OF _ refl, symmetric]) auto
   4.111      also have "(AE x in M. max 0 (f x) * indicator A x = 0) \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> f x \<le> 0)"
   4.112        by (auto simp add: indicator_def max_def split: split_if_asm)
   4.113      finally have "(\<integral>\<^isup>+x. f x * indicator A x \<partial>M) = 0 \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> f x \<le> 0)" . }
   4.114 @@ -2649,7 +2649,7 @@
   4.115    "finite A \<Longrightarrow>
   4.116     g \<in> measurable M (point_measure A f) \<longleftrightarrow>
   4.117      (g \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. g -` {a} \<inter> space M \<in> sets M))"
   4.118 -  unfolding point_measure_def by simp
   4.119 +  unfolding point_measure_def by (simp add: measurable_count_space_eq2)
   4.120  
   4.121  lemma simple_function_point_measure[simp]:
   4.122    "simple_function (point_measure A f) g \<longleftrightarrow> finite (g ` A)"
     5.1 --- a/src/HOL/Probability/Measure_Space.thy	Fri Nov 02 14:00:39 2012 +0100
     5.2 +++ b/src/HOL/Probability/Measure_Space.thy	Fri Nov 02 14:23:40 2012 +0100
     5.3 @@ -447,14 +447,14 @@
     5.4  
     5.5  lemma emeasure_Diff:
     5.6    assumes finite: "emeasure M B \<noteq> \<infinity>"
     5.7 -  and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
     5.8 +  and [measurable]: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
     5.9    shows "emeasure M (A - B) = emeasure M A - emeasure M B"
    5.10  proof -
    5.11    have "0 \<le> emeasure M B" using assms by auto
    5.12    have "(A - B) \<union> B = A" using `B \<subseteq> A` by auto
    5.13    then have "emeasure M A = emeasure M ((A - B) \<union> B)" by simp
    5.14    also have "\<dots> = emeasure M (A - B) + emeasure M B"
    5.15 -    using measurable by (subst plus_emeasure[symmetric]) auto
    5.16 +    by (subst plus_emeasure[symmetric]) auto
    5.17    finally show "emeasure M (A - B) = emeasure M A - emeasure M B"
    5.18      unfolding ereal_eq_minus_iff
    5.19      using finite `0 \<le> emeasure M B` by auto
    5.20 @@ -519,12 +519,11 @@
    5.21    using INF_emeasure_decseq[OF A fin] by simp
    5.22  
    5.23  lemma emeasure_subadditive:
    5.24 -  assumes measurable: "A \<in> sets M" "B \<in> sets M"
    5.25 +  assumes [measurable]: "A \<in> sets M" "B \<in> sets M"
    5.26    shows "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
    5.27  proof -
    5.28    from plus_emeasure[of A M "B - A"]
    5.29 -  have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B - A)"
    5.30 -    using assms by (simp add: Diff)
    5.31 +  have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B - A)" by simp
    5.32    also have "\<dots> \<le> emeasure M A + emeasure M B"
    5.33      using assms by (auto intro!: add_left_mono emeasure_mono)
    5.34    finally show ?thesis .
    5.35 @@ -538,7 +537,7 @@
    5.36    then have "emeasure M (\<Union>i\<in>insert i I. A i) = emeasure M (A i \<union> (\<Union>i\<in>I. A i))"
    5.37      by simp
    5.38    also have "\<dots> \<le> emeasure M (A i) + emeasure M (\<Union>i\<in>I. A i)"
    5.39 -    using insert by (intro emeasure_subadditive finite_UN) auto
    5.40 +    using insert by (intro emeasure_subadditive) auto
    5.41    also have "\<dots> \<le> emeasure M (A i) + (\<Sum>i\<in>I. emeasure M (A i))"
    5.42      using insert by (intro add_mono) auto
    5.43    also have "\<dots> = (\<Sum>i\<in>insert i I. emeasure M (A i))"
    5.44 @@ -688,18 +687,17 @@
    5.45        by (auto simp: subset_eq)
    5.46      have "disjoint_family ?D"
    5.47        by (auto simp: disjoint_family_disjointed)
    5.48 -     moreover
    5.49 -    { fix i
    5.50 +    moreover
    5.51 +    have "(\<Sum>i. emeasure M (?D i)) = (\<Sum>i. emeasure N (?D i))"
    5.52 +    proof (intro arg_cong[where f=suminf] ext)
    5.53 +      fix i
    5.54        have "A i \<inter> ?D i = ?D i"
    5.55          by (auto simp: disjointed_def)
    5.56 -      then have "emeasure M (?D i) = emeasure N (?D i)"
    5.57 -        using *[of "A i" "?D i", OF _ A(3)] A(1) by auto }
    5.58 -     ultimately show "emeasure M F = emeasure N F"
    5.59 -      using N M
    5.60 -      apply (subst (1 2) F_eq)
    5.61 -      apply (subst (1 2) suminf_emeasure[symmetric])
    5.62 -      apply auto
    5.63 -      done
    5.64 +      then show "emeasure M (?D i) = emeasure N (?D i)"
    5.65 +        using *[of "A i" "?D i", OF _ A(3)] A(1) by auto
    5.66 +    qed
    5.67 +    ultimately show "emeasure M F = emeasure N F"
    5.68 +      by (simp add: image_subset_iff `sets M = sets N`[symmetric] F_eq[symmetric] suminf_emeasure)
    5.69    qed
    5.70  qed
    5.71  
    5.72 @@ -1112,32 +1110,23 @@
    5.73  qed
    5.74  
    5.75  lemma AE_distr_iff:
    5.76 -  assumes f: "f \<in> measurable M N" and P: "{x \<in> space N. P x} \<in> sets N"
    5.77 +  assumes f[measurable]: "f \<in> measurable M N" and P[measurable]: "{x \<in> space N. P x} \<in> sets N"
    5.78    shows "(AE x in distr M N f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
    5.79  proof (subst (1 2) AE_iff_measurable[OF _ refl])
    5.80 -  from P show "{x \<in> space (distr M N f). \<not> P x} \<in> sets (distr M N f)"
    5.81 -    by (auto intro!: sets_Collect_neg)
    5.82 -  moreover
    5.83 -  have "f -` {x \<in> space N. P x} \<inter> space M = {x \<in> space M. P (f x)}"
    5.84 -    using f by (auto dest: measurable_space)
    5.85 -  then show "{x \<in> space M. \<not> P (f x)} \<in> sets M"
    5.86 -    using measurable_sets[OF f P] by (auto intro!: sets_Collect_neg)
    5.87 -  moreover have "f -` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}"
    5.88 -    using f by (auto dest: measurable_space)
    5.89 -  ultimately show "(emeasure (distr M N f) {x \<in> space (distr M N f). \<not> P x} = 0) =
    5.90 +  have "f -` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}"
    5.91 +    using f[THEN measurable_space] by auto
    5.92 +  then show "(emeasure (distr M N f) {x \<in> space (distr M N f). \<not> P x} = 0) =
    5.93      (emeasure M {x \<in> space M. \<not> P (f x)} = 0)"
    5.94 -    using f by (simp add: emeasure_distr)
    5.95 -qed
    5.96 +    by (simp add: emeasure_distr)
    5.97 +qed auto
    5.98  
    5.99  lemma null_sets_distr_iff:
   5.100    "f \<in> measurable M N \<Longrightarrow> A \<in> null_sets (distr M N f) \<longleftrightarrow> f -` A \<inter> space M \<in> null_sets M \<and> A \<in> sets N"
   5.101 -  by (auto simp add: null_sets_def emeasure_distr measurable_sets)
   5.102 +  by (auto simp add: null_sets_def emeasure_distr)
   5.103  
   5.104  lemma distr_distr:
   5.105 -  assumes f: "g \<in> measurable N L" and g: "f \<in> measurable M N"
   5.106 -  shows "distr (distr M N f) L g = distr M L (g \<circ> f)" (is "?L = ?R")
   5.107 -  using measurable_comp[OF g f] f g
   5.108 -  by (auto simp add: emeasure_distr measurable_sets measurable_space
   5.109 +  "g \<in> measurable N L \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> distr (distr M N f) L g = distr M L (g \<circ> f)"
   5.110 +  by (auto simp add: emeasure_distr measurable_space
   5.111             intro!: arg_cong[where f="emeasure M"] measure_eqI)
   5.112  
   5.113  section {* Real measure values *}
   5.114 @@ -1381,33 +1370,6 @@
   5.115  
   5.116  section {* Counting space *}
   5.117  
   5.118 -definition count_space :: "'a set \<Rightarrow> 'a measure" where
   5.119 -  "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
   5.120 -
   5.121 -lemma 
   5.122 -  shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
   5.123 -    and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"
   5.124 -  using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>]
   5.125 -  by (auto simp: count_space_def)
   5.126 -
   5.127 -lemma measurable_count_space_eq1[simp]:
   5.128 -  "f \<in> measurable (count_space A) M \<longleftrightarrow> f \<in> A \<rightarrow> space M"
   5.129 - unfolding measurable_def by simp
   5.130 -
   5.131 -lemma measurable_count_space_eq2[simp]:
   5.132 -  assumes "finite A"
   5.133 -  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
   5.134 -proof -
   5.135 -  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
   5.136 -    with `finite A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "finite X"
   5.137 -      by (auto dest: finite_subset)
   5.138 -    moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
   5.139 -    ultimately have "f -` X \<inter> space M \<in> sets M"
   5.140 -      using `X \<subseteq> A` by (auto intro!: finite_UN simp del: UN_simps) }
   5.141 -  then show ?thesis
   5.142 -    unfolding measurable_def by auto
   5.143 -qed
   5.144 -
   5.145  lemma strict_monoI_Suc:
   5.146    assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
   5.147    unfolding strict_mono_def
     6.1 --- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
     6.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
     6.3 @@ -876,7 +876,7 @@
     6.4      then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto
     6.5      with A a X have "emeasure (distr M S X) {a} = P' a"
     6.6        by (subst emeasure_distr)
     6.7 -         (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure
     6.8 +         (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2
     6.9                 intro!: arg_cong[where f=prob])
    6.10      also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' a) * indicator {a} x \<partial>S)"
    6.11        using A X a
    6.12 @@ -934,7 +934,7 @@
    6.13  lemma simple_distributed_simple_function:
    6.14    "simple_distributed M X Px \<Longrightarrow> simple_function M X"
    6.15    unfolding simple_distributed_def distributed_def
    6.16 -  by (auto simp: simple_function_def)
    6.17 +  by (auto simp: simple_function_def measurable_count_space_eq2)
    6.18  
    6.19  lemma simple_distributed_measure:
    6.20    "simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X -` {a} \<inter> space M)"
     7.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:00:39 2012 +0100
     7.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:23:40 2012 +0100
     7.3 @@ -100,7 +100,7 @@
     7.4    with assms show ?thesis by auto
     7.5  qed
     7.6  
     7.7 -lemma (in semiring_of_sets) sets_Collect_finite_All:
     7.8 +lemma (in semiring_of_sets) sets_Collect_finite_All':
     7.9    assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}"
    7.10    shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
    7.11  proof -
    7.12 @@ -1209,6 +1209,15 @@
    7.13    "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
    7.14     unfolding measurable_def by auto
    7.15  
    7.16 +lemma measurable_sets_Collect:
    7.17 +  assumes f: "f \<in> measurable M N" and P: "{x\<in>space N. P x} \<in> sets N" shows "{x\<in>space M. P (f x)} \<in> sets M"
    7.18 +proof -
    7.19 +  have "f -` {x \<in> space N. P x} \<inter> space M = {x\<in>space M. P (f x)}"
    7.20 +    using measurable_space[OF f] by auto
    7.21 +  with measurable_sets[OF f P] show ?thesis
    7.22 +    by simp
    7.23 +qed
    7.24 +
    7.25  lemma measurable_sigma_sets:
    7.26    assumes B: "sets N = sigma_sets \<Omega> A" "A \<subseteq> Pow \<Omega>"
    7.27        and f: "f \<in> space M \<rightarrow> \<Omega>"
    7.28 @@ -1302,6 +1311,9 @@
    7.29  lemma measurable_ident[intro, simp]: "id \<in> measurable M M"
    7.30    by (auto simp add: measurable_def)
    7.31  
    7.32 +lemma measurable_ident'[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
    7.33 +  by (auto simp add: measurable_def)
    7.34 +
    7.35  lemma measurable_comp[intro]:
    7.36    fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
    7.37    shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
    7.38 @@ -1314,7 +1326,7 @@
    7.39    "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> (\<lambda>x. g (f x)) \<in> measurable M L"
    7.40    using measurable_comp[of f M N g L] by (simp add: comp_def)
    7.41  
    7.42 -lemma measurable_Least:
    7.43 +lemma sets_Least:
    7.44    assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
    7.45    shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
    7.46  proof -
    7.47 @@ -1371,6 +1383,368 @@
    7.48      measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
    7.49    using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
    7.50  
    7.51 +section {* Counting space *}
    7.52 +
    7.53 +definition count_space :: "'a set \<Rightarrow> 'a measure" where
    7.54 +  "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
    7.55 +
    7.56 +lemma 
    7.57 +  shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
    7.58 +    and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"
    7.59 +  using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>]
    7.60 +  by (auto simp: count_space_def)
    7.61 +
    7.62 +lemma measurable_count_space_eq1[simp]:
    7.63 +  "f \<in> measurable (count_space A) M \<longleftrightarrow> f \<in> A \<rightarrow> space M"
    7.64 + unfolding measurable_def by simp
    7.65 +
    7.66 +lemma measurable_count_space_eq2:
    7.67 +  assumes "finite A"
    7.68 +  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
    7.69 +proof -
    7.70 +  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
    7.71 +    with `finite A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "finite X"
    7.72 +      by (auto dest: finite_subset)
    7.73 +    moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
    7.74 +    ultimately have "f -` X \<inter> space M \<in> sets M"
    7.75 +      using `X \<subseteq> A` by (auto intro!: finite_UN simp del: UN_simps) }
    7.76 +  then show ?thesis
    7.77 +    unfolding measurable_def by auto
    7.78 +qed
    7.79 +
    7.80 +lemma measurable_compose_countable:
    7.81 +  assumes f: "\<And>i::'i::countable. (\<lambda>x. f i x) \<in> measurable M N" and g: "g \<in> measurable M (count_space UNIV)"
    7.82 +  shows "(\<lambda>x. f (g x) x) \<in> measurable M N"
    7.83 +  unfolding measurable_def
    7.84 +proof safe
    7.85 +  fix x assume "x \<in> space M" then show "f (g x) x \<in> space N"
    7.86 +    using f[THEN measurable_space] g[THEN measurable_space] by auto
    7.87 +next
    7.88 +  fix A assume A: "A \<in> sets N"
    7.89 +  have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
    7.90 +    by auto
    7.91 +  also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF A] g[THEN measurable_sets]
    7.92 +    by (auto intro!: countable_UN measurable_sets)
    7.93 +  finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
    7.94 +qed
    7.95 +
    7.96 +subsection {* Measurable method *}
    7.97 +
    7.98 +lemma (in algebra) sets_Collect_finite_All:
    7.99 +  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
   7.100 +  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
   7.101 +proof -
   7.102 +  have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (if S = {} then \<Omega> else \<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
   7.103 +    by auto
   7.104 +  with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
   7.105 +qed
   7.106 +
   7.107 +abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
   7.108 +
   7.109 +lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
   7.110 +proof
   7.111 +  assume "pred M P"
   7.112 +  then have "P -` {True} \<inter> space M \<in> sets M"
   7.113 +    by (auto simp: measurable_count_space_eq2)
   7.114 +  also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
   7.115 +  finally show "{x\<in>space M. P x} \<in> sets M" .
   7.116 +next
   7.117 +  assume P: "{x\<in>space M. P x} \<in> sets M"
   7.118 +  moreover
   7.119 +  { fix X
   7.120 +    have "X \<in> Pow (UNIV :: bool set)" by simp
   7.121 +    then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"
   7.122 +      unfolding UNIV_bool Pow_insert Pow_empty by auto
   7.123 +    then have "P -` X \<inter> space M \<in> sets M"
   7.124 +      by (auto intro!: sets_Collect_neg sets_Collect_imp sets_Collect_conj sets_Collect_const P) }
   7.125 +  then show "pred M P"
   7.126 +    by (auto simp: measurable_def)
   7.127 +qed
   7.128 +
   7.129 +lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))"
   7.130 +  by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
   7.131 +
   7.132 +lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
   7.133 +  by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
   7.134 +
   7.135 +lemma measurable_count_space_const:
   7.136 +  "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
   7.137 +  by auto
   7.138 +
   7.139 +lemma measurable_count_space:
   7.140 +  "f \<in> measurable (count_space A) (count_space UNIV)"
   7.141 +  by simp
   7.142 +
   7.143 +lemma measurable_compose_rev:
   7.144 +  assumes f: "f \<in> measurable L N" and g: "g \<in> measurable M L"
   7.145 +  shows "(\<lambda>x. f (g x)) \<in> measurable M N"
   7.146 +  using measurable_compose[OF g f] .
   7.147 +
   7.148 +ML {*
   7.149 +
   7.150 +structure Measurable =
   7.151 +struct
   7.152 +
   7.153 +datatype level = Concrete | Generic;
   7.154 +
   7.155 +structure Data = Generic_Data
   7.156 +(
   7.157 +  type T = thm list * thm list;
   7.158 +  val empty = ([], []);
   7.159 +  val extend = I;
   7.160 +  val merge = fn ((a, b), (c, d)) => (a @ c, b @ d);
   7.161 +);
   7.162 +
   7.163 +val debug =
   7.164 +  Attrib.setup_config_bool @{binding measurable_debug} (K false)
   7.165 +
   7.166 +val backtrack =
   7.167 +  Attrib.setup_config_int @{binding measurable_backtrack} (K 40)
   7.168 +
   7.169 +fun get lv = (case lv of Concrete => fst | Generic => snd) o Data.get o Context.Proof; 
   7.170 +fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
   7.171 +
   7.172 +fun update f lv = Data.map (case lv of Concrete => apfst f | Generic => apsnd f);
   7.173 +fun add thms' = update (fn thms => thms @ thms');
   7.174 +
   7.175 +fun TRYALL' tacs = fold_rev (curry op APPEND') tacs (K no_tac);
   7.176 +
   7.177 +fun is_too_generic thm =
   7.178 +  let 
   7.179 +    val concl = concl_of thm
   7.180 +    val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
   7.181 +  in is_Var (head_of concl') end
   7.182 +
   7.183 +fun import_theorem thm = if is_too_generic thm then [] else
   7.184 +  [thm] @ map_filter (try (fn th' => thm RS th'))
   7.185 +    [@{thm measurable_compose_rev}, @{thm pred_sets1}, @{thm pred_sets2}, @{thm sets_into_space}];
   7.186 +
   7.187 +fun add_thm (raw, lv) thm = add (if raw then [thm] else import_theorem thm) lv;
   7.188 +
   7.189 +fun debug_tac ctxt msg f = if Config.get ctxt debug then K (print_tac (msg ())) THEN' f else f
   7.190 +
   7.191 +fun TAKE n f thm = Seq.take n (f thm)
   7.192 +
   7.193 +fun nth_hol_goal thm i =
   7.194 +  HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
   7.195 +
   7.196 +fun dest_measurable_fun t =
   7.197 +  (case t of
   7.198 +    (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
   7.199 +  | _ => raise (TERM ("not a measurability predicate", [t])))
   7.200 +
   7.201 +fun indep (Bound i) t b = i < b orelse t <= i
   7.202 +  | indep (f $ t) top bot = indep f top bot andalso indep t top bot
   7.203 +  | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
   7.204 +  | indep _ _ _ = true;
   7.205 +
   7.206 +fun cnt_prefixes ctxt (Abs (n, T, t)) = let
   7.207 +      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
   7.208 +      fun cnt_walk (Abs (ns, T, t)) Ts =
   7.209 +          map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
   7.210 +        | cnt_walk (f $ g) Ts = let
   7.211 +            val n = length Ts - 1
   7.212 +          in
   7.213 +            map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
   7.214 +            map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
   7.215 +            (if is_countable (fastype_of1 (Ts, g)) andalso loose_bvar1 (g, n)
   7.216 +                andalso indep g n 0 andalso g <> Bound n
   7.217 +              then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
   7.218 +              else [])
   7.219 +          end
   7.220 +        | cnt_walk _ _ = []
   7.221 +    in map (fn (t1, t2) => let
   7.222 +        val T1 = fastype_of1 ([T], t2)
   7.223 +        val T2 = fastype_of1 ([T], t)
   7.224 +      in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
   7.225 +        [SOME T1, SOME T, SOME T2])
   7.226 +      end) (cnt_walk t [T])
   7.227 +    end
   7.228 +  | cnt_prefixes _ _ = []
   7.229 +
   7.230 +val split_fun_tac =
   7.231 +  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   7.232 +    let
   7.233 +      val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
   7.234 +      fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
   7.235 +      fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
   7.236 +      val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
   7.237 +    in if null cps then no_tac else debug_tac ctxt (K "split fun") (resolve_tac cps) i end
   7.238 +    handle TERM _ => no_tac) 1)
   7.239 +
   7.240 +fun single_measurable_tac ctxt facts =
   7.241 +  debug_tac ctxt (fn () => "single + " ^ Pretty.str_of (Pretty.block (map (Syntax.pretty_term ctxt o prop_of) facts)))
   7.242 +  (resolve_tac ((maps (import_theorem o Simplifier.norm_hhf) facts) @ get_all ctxt)
   7.243 +    APPEND' (split_fun_tac ctxt));
   7.244 +
   7.245 +fun is_cond_formlua n thm = if length (prems_of thm) < n then false else
   7.246 +  (case nth_hol_goal thm n of
   7.247 +    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
   7.248 +  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
   7.249 +  | _ => true)
   7.250 +  handle TERM _ => true;
   7.251 +
   7.252 +fun measurable_tac' ctxt ss facts n =
   7.253 +  TAKE (Config.get ctxt backtrack)
   7.254 +  ((single_measurable_tac ctxt facts THEN'
   7.255 +   REPEAT o (single_measurable_tac ctxt facts APPEND'
   7.256 +             SOLVED' (fn n => COND (is_cond_formlua n) (debug_tac ctxt (K "simp") (asm_full_simp_tac ss) n) no_tac))) n);
   7.257 +
   7.258 +fun measurable_tac ctxt = measurable_tac' ctxt (simpset_of ctxt);
   7.259 +
   7.260 +val attr_add = Thm.declaration_attribute o add_thm;
   7.261 +
   7.262 +val attr : attribute context_parser =
   7.263 +  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
   7.264 +     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
   7.265 +
   7.266 +val method : (Proof.context -> Method.method) context_parser =
   7.267 +  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts 1)));
   7.268 +
   7.269 +fun simproc ss redex = let
   7.270 +    val ctxt = Simplifier.the_context ss;
   7.271 +    val t = HOLogic.mk_Trueprop (term_of redex);
   7.272 +    fun tac {context = ctxt, ...} =
   7.273 +      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss) 1);
   7.274 +  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
   7.275 +
   7.276 +end
   7.277 +
   7.278 +*}
   7.279 +
   7.280 +attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
   7.281 +method_setup measurable = {* Measurable.method *} "measurability prover"
   7.282 +simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
   7.283 +
   7.284 +declare
   7.285 +  top[measurable]
   7.286 +  empty_sets[measurable (raw)]
   7.287 +  Un[measurable (raw)]
   7.288 +  Diff[measurable (raw)]
   7.289 +
   7.290 +declare
   7.291 +  measurable_count_space[measurable (raw)]
   7.292 +  measurable_ident[measurable (raw)]
   7.293 +  measurable_ident'[measurable (raw)]
   7.294 +  measurable_count_space_const[measurable (raw)]
   7.295 +  measurable_const[measurable (raw)]
   7.296 +  measurable_If[measurable (raw)]
   7.297 +  measurable_comp[measurable (raw)]
   7.298 +  measurable_sets[measurable (raw)]
   7.299 +
   7.300 +lemma predE[measurable (raw)]: 
   7.301 +  "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
   7.302 +  unfolding pred_def .
   7.303 +
   7.304 +lemma pred_intros_imp'[measurable (raw)]:
   7.305 +  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
   7.306 +  by (cases K) auto
   7.307 +
   7.308 +lemma pred_intros_conj1'[measurable (raw)]:
   7.309 +  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
   7.310 +  by (cases K) auto
   7.311 +
   7.312 +lemma pred_intros_conj2'[measurable (raw)]:
   7.313 +  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
   7.314 +  by (cases K) auto
   7.315 +
   7.316 +lemma pred_intros_disj1'[measurable (raw)]:
   7.317 +  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
   7.318 +  by (cases K) auto
   7.319 +
   7.320 +lemma pred_intros_disj2'[measurable (raw)]:
   7.321 +  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
   7.322 +  by (cases K) auto
   7.323 +
   7.324 +lemma pred_intros_logic[measurable (raw)]:
   7.325 +  "pred M (\<lambda>x. x \<in> space M)"
   7.326 +  "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
   7.327 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
   7.328 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
   7.329 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
   7.330 +  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
   7.331 +  "pred M (\<lambda>x. f x \<in> UNIV)"
   7.332 +  "pred M (\<lambda>x. f x \<in> {})"
   7.333 +  "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
   7.334 +  "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) - (B x))"
   7.335 +  "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))"
   7.336 +  "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))"
   7.337 +  "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
   7.338 +  by (auto intro!: sets_Collect simp: iff_conv_conj_imp pred_def)
   7.339 +
   7.340 +lemma pred_intros_countable[measurable (raw)]:
   7.341 +  fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
   7.342 +  shows 
   7.343 +    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
   7.344 +    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
   7.345 +  by (auto intro!: sets_Collect_countable_All sets_Collect_countable_Ex simp: pred_def)
   7.346 +
   7.347 +lemma pred_intros_countable_bounded[measurable (raw)]:
   7.348 +  fixes X :: "'i :: countable set"
   7.349 +  shows 
   7.350 +    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))"
   7.351 +    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))"
   7.352 +    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
   7.353 +    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
   7.354 +  by (auto simp: Bex_def Ball_def)
   7.355 +
   7.356 +lemma pred_intros_finite[measurable (raw)]:
   7.357 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"
   7.358 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"
   7.359 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"
   7.360 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"
   7.361 +  by (auto intro!: sets_Collect_finite_Ex sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
   7.362 +
   7.363 +lemma countable_Un_Int[measurable (raw)]:
   7.364 +  "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
   7.365 +  "I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M"
   7.366 +  by auto
   7.367 +
   7.368 +declare
   7.369 +  finite_UN[measurable (raw)]
   7.370 +  finite_INT[measurable (raw)]
   7.371 +
   7.372 +lemma sets_Int_pred[measurable (raw)]:
   7.373 +  assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
   7.374 +  shows "A \<inter> B \<in> sets M"
   7.375 +proof -
   7.376 +  have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
   7.377 +  also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
   7.378 +    using space by auto
   7.379 +  finally show ?thesis .
   7.380 +qed
   7.381 +
   7.382 +lemma [measurable (raw generic)]:
   7.383 +  assumes f: "f \<in> measurable M N" and c: "{c} \<in> sets N"
   7.384 +  shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
   7.385 +    and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
   7.386 +  using measurable_sets[OF f c] by (auto simp: Int_def conj_commute eq_commute pred_def)
   7.387 +
   7.388 +lemma pred_le_const[measurable (raw generic)]:
   7.389 +  assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
   7.390 +  using measurable_sets[OF f c]
   7.391 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   7.392 +
   7.393 +lemma pred_const_le[measurable (raw generic)]:
   7.394 +  assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
   7.395 +  using measurable_sets[OF f c]
   7.396 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   7.397 +
   7.398 +lemma pred_less_const[measurable (raw generic)]:
   7.399 +  assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
   7.400 +  using measurable_sets[OF f c]
   7.401 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   7.402 +
   7.403 +lemma pred_const_less[measurable (raw generic)]:
   7.404 +  assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
   7.405 +  using measurable_sets[OF f c]
   7.406 +  by (auto simp: Int_def conj_commute eq_commute pred_def)
   7.407 +
   7.408 +declare
   7.409 +  Int[measurable (raw)]
   7.410 +
   7.411 +hide_const (open) pred
   7.412 +
   7.413  subsection {* Extend measure *}
   7.414  
   7.415  definition "extend_measure \<Omega> I G \<mu> =