# HG changeset patch
# User wenzelm
# Date 1353088186 -3600
# Node ID 3d89c38408cd72170e74d3c794d2817e4e6acd00
# Parent  a3bede207a0488a088a080c3485ce795aa94ef5a# Parent  5e01e32dadbea9273ff6959db3383db56f8ce537
merged

diff -r 5e01e32dadbe -r 3d89c38408cd src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 16 18:49:46 2012 +0100
@@ -84,8 +84,13 @@
   unfolding indicator_def [abs_def] using A
   by (auto intro!: measurable_If_set)
 
-lemma borel_measurable_indicator'[measurable]:
-  "{x\<in>space M. x \<in> A} \<in> sets M \<Longrightarrow> indicator A \<in> borel_measurable M"
+lemma borel_measurable_count_space[measurable (raw)]:
+  "f \<in> borel_measurable (count_space S)"
+  unfolding measurable_def by auto
+
+lemma borel_measurable_indicator'[measurable (raw)]:
+  assumes [measurable]: "{x\<in>space M. f x \<in> A x} \<in> sets M"
+  shows "(\<lambda>x. indicator (A x) (f x)) \<in> borel_measurable M"
   unfolding indicator_def[abs_def]
   by (auto intro!: measurable_If)
 
diff -r 5e01e32dadbe -r 3d89c38408cd src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Fri Nov 16 18:49:46 2012 +0100
@@ -1278,7 +1278,7 @@
 subsection {* Isomorphism between Functions and Finite Maps *}
 
 lemma
-  measurable_compose:
+  measurable_finmap_compose:
   fixes f::"'a \<Rightarrow> 'b"
   assumes inj: "\<And>j. j \<in> J \<Longrightarrow> f' (f j) = j"
   assumes "finite J"
@@ -1326,7 +1326,7 @@
   shows "(\<lambda>m. compose (f ` J) m f') \<in> measurable (PiM J (\<lambda>_. M)) (PiM (f ` J) (\<lambda>_. M))"
 proof -
   have "(\<lambda>m. compose (f ` J) m f') \<in> measurable (Pi\<^isub>M (f' ` f ` J) (\<lambda>_. M)) (Pi\<^isub>M (f ` J) (\<lambda>_. M))"
-    using assms by (auto intro: measurable_compose)
+    using assms by (auto intro: measurable_finmap_compose)
   moreover
   from inj have "f' ` f ` J = J" by (metis (hide_lams, mono_tags) image_iff set_eqI)
   ultimately show ?thesis by simp
@@ -1426,7 +1426,7 @@
 proof (rule measurable_comp, rule measurable_proj_PiM)
   show "(\<lambda>g. compose J g f) \<in>
     measurable (Pi\<^isub>M (f ` J) (\<lambda>x. M)) (Pi\<^isub>M J (\<lambda>_. M))"
-    by (rule measurable_compose, rule inv) auto
+    by (rule measurable_finmap_compose, rule inv) auto
 qed (auto simp add: space_PiM extensional_def assms)
 
 lemma fm_image_measurable:
diff -r 5e01e32dadbe -r 3d89c38408cd src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
@@ -540,6 +540,18 @@
   finally show "f -` A \<inter> space N \<in> sets N" .
 qed (auto simp: space)
 
+lemma measurable_PiM_single':
+  assumes f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> measurable N (M i)"
+    and "(\<lambda>\<omega> i. f i \<omega>) \<in> space N \<rightarrow> (\<Pi>\<^isub>E i\<in>I. space (M i))"
+  shows "(\<lambda>\<omega> i. f i \<omega>) \<in> measurable N (Pi\<^isub>M I M)"
+proof (rule measurable_PiM_single)
+  fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
+  then have "{\<omega> \<in> space N. f i \<omega> \<in> A} = f i -` A \<inter> space N"
+    by auto
+  then show "{\<omega> \<in> space N. f i \<omega> \<in> A} \<in> sets N"
+    using A f by (auto intro!: measurable_sets)
+qed fact
+
 lemma sets_PiM_I_finite[measurable]:
   assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
   shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
@@ -562,12 +574,22 @@
   shows "(\<lambda>x. (f x) i) \<in> measurable N (M i)"
   using measurable_compose[OF f measurable_component_singleton, OF i] .
 
+lemma measurable_PiM_component_rev[measurable (raw)]:
+  "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N"
+  by simp
+
 lemma measurable_nat_case[measurable (raw)]:
   assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N"
     "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
   shows "(\<lambda>x. nat_case (f x) (g x) i) \<in> measurable M N"
   by (cases i) simp_all
 
+lemma measurable_nat_case'[measurable (raw)]:
+  assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
+  shows "(\<lambda>x. nat_case (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
+  using fg[THEN measurable_space]
+  by (auto intro!: measurable_PiM_single' simp add: space_PiM Pi_iff split: nat.split)
+
 lemma measurable_add_dim[measurable]:
   "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
     (is "?f \<in> measurable ?P ?I")
diff -r 5e01e32dadbe -r 3d89c38408cd src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
@@ -449,23 +449,6 @@
 
 subsection {* Sequence space *}
 
-lemma measurable_nat_case: "(\<lambda>(x, \<omega>). nat_case x \<omega>) \<in> measurable (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
-proof (rule measurable_PiM_single)
-  show "(\<lambda>(x, \<omega>). nat_case x \<omega>) \<in> space (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) \<rightarrow> (UNIV \<rightarrow>\<^isub>E space M)"
-    by (auto simp: space_pair_measure space_PiM Pi_iff split: nat.split)
-  fix i :: nat and A assume A: "A \<in> sets M"
-  then have *: "{\<omega> \<in> space (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case nat_case \<omega> i \<in> A} =
-    (case i of 0 \<Rightarrow> A \<times> space (\<Pi>\<^isub>M i\<in>UNIV. M) | Suc n \<Rightarrow> space M \<times> {\<omega>\<in>space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> n \<in> A})"
-    by (auto simp: space_PiM space_pair_measure split: nat.split dest: sets_into_space)
-  show "{\<omega> \<in> space (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case nat_case \<omega> i \<in> A} \<in> sets (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M))"
-    unfolding * by (auto simp: A split: nat.split intro!: sets_Collect_single)
-qed
-
-lemma measurable_nat_case':
-  assumes f: "f \<in> measurable N M" and g: "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
-  shows "(\<lambda>x. nat_case (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
-  using measurable_compose[OF measurable_Pair[OF f g] measurable_nat_case] by simp
-
 definition comb_seq :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)" where
   "comb_seq i \<omega> \<omega>' j = (if j < i then \<omega> j else \<omega>' (j - i))"
 
@@ -475,7 +458,8 @@
 lemma split_comb_seq_asm: "P (comb_seq i \<omega> \<omega>' j) \<longleftrightarrow> \<not> ((j < i \<and> \<not> P (\<omega> j)) \<or> (\<exists>k. j = i + k \<and> \<not> P (\<omega>' k)))"
   by (auto simp: comb_seq_def)
 
-lemma measurable_comb_seq: "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> measurable ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
+lemma measurable_comb_seq:
+  "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> measurable ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
 proof (rule measurable_PiM_single)
   show "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) \<rightarrow> (UNIV \<rightarrow>\<^isub>E space M)"
     by (auto simp: space_pair_measure space_PiM Pi_iff split: split_comb_seq)
@@ -488,11 +472,33 @@
     unfolding * by (auto simp: A intro!: sets_Collect_single)
 qed
 
-lemma measurable_comb_seq':
+lemma measurable_comb_seq'[measurable (raw)]:
   assumes f: "f \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)" and g: "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
   shows "(\<lambda>x. comb_seq i (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
   using measurable_compose[OF measurable_Pair[OF f g] measurable_comb_seq] by simp
 
+lemma comb_seq_0: "comb_seq 0 \<omega> \<omega>' = \<omega>'"
+  by (auto simp add: comb_seq_def)
+
+lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (nat_case (\<omega> n) \<omega>')"
+  by (auto simp add: comb_seq_def not_less less_Suc_eq le_imp_diff_is_add intro!: ext split: nat.split)
+
+lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = nat_case (\<omega> 0)"
+  by (intro ext) (simp add: comb_seq_Suc comb_seq_0)
+
+lemma comb_seq_less: "i < n \<Longrightarrow> comb_seq n \<omega> \<omega>' i = \<omega> i"
+  by (auto split: split_comb_seq)
+
+lemma comb_seq_add: "comb_seq n \<omega> \<omega>' (i + n) = \<omega>' i"
+  by (auto split: nat.split split_comb_seq)
+
+lemma nat_case_comb_seq: "nat_case s' (comb_seq n \<omega> \<omega>') (i + n) = nat_case (nat_case s' \<omega> n) \<omega>' i"
+  by (auto split: nat.split split_comb_seq)
+
+lemma nat_case_comb_seq':
+  "nat_case s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (nat_case s \<omega>) \<omega>'"
+  by (auto split: split_comb_seq nat.split)
+
 locale sequence_space = product_prob_space "\<lambda>i. M" "UNIV :: nat set" for M
 begin
 
@@ -578,7 +584,7 @@
    by (auto simp: space_pair_measure space_PiM Pi_iff prod_emb_def all_conj_distrib
       split: nat.split nat.split_asm)
   then have "emeasure ?D ?X = emeasure (M \<Otimes>\<^isub>M S) (?E \<times> ?F)"
-    by (subst emeasure_distr[OF measurable_nat_case])
+    by (subst emeasure_distr)
        (auto intro!: sets_PiM_I simp: split_beta' J)
   also have "\<dots> = emeasure M ?E * emeasure S ?F"
     using J by (intro P.emeasure_pair_measure_Times) (auto intro!: sets_PiM_I finite_vimageI)
diff -r 5e01e32dadbe -r 3d89c38408cd src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 16 18:49:46 2012 +0100
@@ -1181,6 +1181,17 @@
   by (subst positive_integral_eq_simple_integral)
      (auto simp: simple_function_indicator simple_integral_indicator)
 
+lemma positive_integral_indicator':
+  assumes [measurable]: "A \<inter> space M \<in> sets M"
+  shows "(\<integral>\<^isup>+ x. indicator A x \<partial>M) = emeasure M (A \<inter> space M)"
+proof -
+  have "(\<integral>\<^isup>+ x. indicator A x \<partial>M) = (\<integral>\<^isup>+ x. indicator (A \<inter> space M) x \<partial>M)"
+    by (intro positive_integral_cong) (simp split: split_indicator)
+  also have "\<dots> = emeasure M (A \<inter> space M)"
+    by simp
+  finally show ?thesis .
+qed
+
 lemma positive_integral_add:
   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   and g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
@@ -1430,6 +1441,32 @@
     done
 qed
 
+lemma positive_integral_nat_function:
+  fixes f :: "'a \<Rightarrow> nat"
+  assumes "f \<in> measurable M (count_space UNIV)"
+  shows "(\<integral>\<^isup>+x. ereal (of_nat (f x)) \<partial>M) = (\<Sum>t. emeasure M {x\<in>space M. t < f x})"
+proof -
+  def F \<equiv> "\<lambda>i. {x\<in>space M. i < f x}"
+  with assms have [measurable]: "\<And>i. F i \<in> sets M"
+    by auto
+
+  { fix x assume "x \<in> space M"
+    have "(\<lambda>i. if i < f x then 1 else 0) sums (of_nat (f x)::real)"
+      using sums_If_finite[of "\<lambda>i. i < f x" "\<lambda>_. 1::real"] by simp
+    then have "(\<lambda>i. ereal(if i < f x then 1 else 0)) sums (ereal(of_nat(f x)))"
+      unfolding sums_ereal .
+    moreover have "\<And>i. ereal (if i < f x then 1 else 0) = indicator (F i) x"
+      using `x \<in> space M` by (simp add: one_ereal_def F_def)
+    ultimately have "ereal(of_nat(f x)) = (\<Sum>i. indicator (F i) x)"
+      by (simp add: sums_iff) }
+  then have "(\<integral>\<^isup>+x. ereal (of_nat (f x)) \<partial>M) = (\<integral>\<^isup>+x. (\<Sum>i. indicator (F i) x) \<partial>M)"
+    by (simp cong: positive_integral_cong)
+  also have "\<dots> = (\<Sum>i. emeasure M (F i))"
+    by (simp add: positive_integral_suminf)
+  finally show ?thesis
+    by (simp add: F_def)
+qed
+
 section "Lebesgue Integral"
 
 definition integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" where
@@ -1639,25 +1676,9 @@
   unfolding integrable_def lebesgue_integral_def
   by auto
 
-lemma integral_cmult[simp, intro]:
-  assumes "integrable M f"
-  shows "integrable M (\<lambda>t. a * f t)" (is ?P)
-  and "(\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f" (is ?I)
-proof -
-  have "integrable M (\<lambda>t. a * f t) \<and> (\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f"
-  proof (cases rule: le_cases)
-    assume "0 \<le> a" show ?thesis
-      using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
-      by simp
-  next
-    assume "a \<le> 0" hence "0 \<le> - a" by auto
-    have *: "\<And>t. - a * t + 0 = (-a) * t" by simp
-    show ?thesis using integral_linear[OF assms integral_zero(1) `0 \<le> - a`]
-        integral_minus(1)[of M "\<lambda>t. - a * f t"]
-      unfolding * integral_zero by simp
-  qed
-  thus ?P ?I by auto
-qed
+lemma lebesgue_integral_uminus:
+    "(\<integral>x. - f x \<partial>M) = - integral\<^isup>L M f"
+  unfolding lebesgue_integral_def by simp
 
 lemma lebesgue_integral_cmult_nonneg:
   assumes f: "f \<in> borel_measurable M" and "0 \<le> c"
@@ -1682,10 +1703,6 @@
     by (simp add: lebesgue_integral_def field_simps)
 qed
 
-lemma lebesgue_integral_uminus:
-  "(\<integral>x. - f x \<partial>M) = - integral\<^isup>L M f"
-    unfolding lebesgue_integral_def by simp
-
 lemma lebesgue_integral_cmult:
   assumes f: "f \<in> borel_measurable M"
   shows "(\<integral>x. c * f x \<partial>M) = c * integral\<^isup>L M f"
@@ -1698,10 +1715,33 @@
     by (simp add: lebesgue_integral_def)
 qed
 
+lemma lebesgue_integral_multc:
+  "f \<in> borel_measurable M \<Longrightarrow> (\<integral>x. f x * c \<partial>M) = integral\<^isup>L M f * c"
+  using lebesgue_integral_cmult[of f M c] by (simp add: ac_simps)
+
 lemma integral_multc:
+  "integrable M f \<Longrightarrow> (\<integral> x. f x * c \<partial>M) = integral\<^isup>L M f * c"
+  by (simp add: lebesgue_integral_multc)
+
+lemma integral_cmult[simp, intro]:
   assumes "integrable M f"
-  shows "(\<integral> x. f x * c \<partial>M) = integral\<^isup>L M f * c"
-  unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
+  shows "integrable M (\<lambda>t. a * f t)" (is ?P)
+  and "(\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f" (is ?I)
+proof -
+  have "integrable M (\<lambda>t. a * f t) \<and> (\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f"
+  proof (cases rule: le_cases)
+    assume "0 \<le> a" show ?thesis
+      using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
+      by simp
+  next
+    assume "a \<le> 0" hence "0 \<le> - a" by auto
+    have *: "\<And>t. - a * t + 0 = (-a) * t" by simp
+    show ?thesis using integral_linear[OF assms integral_zero(1) `0 \<le> - a`]
+        integral_minus(1)[of M "\<lambda>t. - a * f t"]
+      unfolding * integral_zero by simp
+  qed
+  thus ?P ?I by auto
+qed
 
 lemma integral_diff[simp, intro]:
   assumes f: "integrable M f" and g: "integrable M g"
@@ -1713,7 +1753,7 @@
 
 lemma integral_indicator[simp, intro]:
   assumes "A \<in> sets M" and "(emeasure M) A \<noteq> \<infinity>"
-  shows "integral\<^isup>L M (indicator A) = real ((emeasure M) A)" (is ?int)
+  shows "integral\<^isup>L M (indicator A) = real (emeasure M A)" (is ?int)
   and "integrable M (indicator A)" (is ?able)
 proof -
   from `A \<in> sets M` have *:
@@ -1850,6 +1890,16 @@
   finally show ?thesis .
 qed
 
+lemma integrable_nonneg:
+  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "(\<integral>\<^isup>+ x. f x \<partial>M) \<noteq> \<infinity>"
+  shows "integrable M f"
+  unfolding integrable_def
+proof (intro conjI f)
+  have "(\<integral>\<^isup>+ x. ereal (- f x) \<partial>M) = 0"
+    using f by (subst positive_integral_0_iff_AE) auto
+  then show "(\<integral>\<^isup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>" by simp
+qed
+
 lemma integral_positive:
   assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
   shows "0 \<le> integral\<^isup>L M f"
@@ -1986,7 +2036,7 @@
 
 lemma (in finite_measure) lebesgue_integral_const[simp]:
   shows "integrable M (\<lambda>x. a)"
-  and  "(\<integral>x. a \<partial>M) = a * (measure M) (space M)"
+  and  "(\<integral>x. a \<partial>M) = a * measure M (space M)"
 proof -
   { fix a :: real assume "0 \<le> a"
     then have "(\<integral>\<^isup>+ x. ereal a \<partial>M) = ereal a * (emeasure M) (space M)"
@@ -2008,6 +2058,10 @@
     by (simp add: lebesgue_integral_def positive_integral_const_If emeasure_eq_measure)
 qed
 
+lemma (in finite_measure) integrable_const_bound:
+  assumes "AE x in M. \<bar>f x\<bar> \<le> B" and "f \<in> borel_measurable M" shows "integrable M f"
+  by (auto intro: integrable_bound[where f="\<lambda>x. B"] lebesgue_integral_const assms)
+
 lemma indicator_less[simp]:
   "indicator A x \<le> (indicator B x::ereal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
   by (simp add: indicator_def not_le)
diff -r 5e01e32dadbe -r 3d89c38408cd src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
@@ -219,6 +219,17 @@
   with AE_in_set_eq_1 assms show ?thesis by simp
 qed
 
+lemma (in prob_space) AE_const[simp]: "(AE x in M. P) \<longleftrightarrow> P"
+  by (cases P) (auto simp: AE_False)
+
+lemma (in prob_space) AE_contr:
+  assumes ae: "AE \<omega> in M. P \<omega>" "AE \<omega> in M. \<not> P \<omega>"
+  shows False
+proof -
+  from ae have "AE \<omega> in M. False" by eventually_elim auto
+  then show False by auto
+qed
+
 lemma (in finite_measure) prob_space_increasing: "increasing M (measure M)"
   by (auto intro!: finite_measure_mono simp: increasing_def)
 
@@ -438,6 +449,23 @@
   then show ?thesis by simp
 qed (simp add: measure_notin_sets)
 
+lemma (in prob_space) prob_Collect_eq_0:
+  "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 0 \<longleftrightarrow> (AE x in M. \<not> P x)"
+  using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"] by (simp add: emeasure_eq_measure)
+
+lemma (in prob_space) prob_Collect_eq_1:
+  "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 1 \<longleftrightarrow> (AE x in M. P x)"
+  using AE_in_set_eq_1[of "{x\<in>space M. P x}"] by simp
+
+lemma (in prob_space) prob_eq_0:
+  "A \<in> sets M \<Longrightarrow> prob A = 0 \<longleftrightarrow> (AE x in M. x \<notin> A)"
+  using AE_iff_measurable[OF _ refl, of M "\<lambda>x. x \<notin> A"]
+  by (auto simp add: emeasure_eq_measure Int_def[symmetric])
+
+lemma (in prob_space) prob_eq_1:
+  "A \<in> sets M \<Longrightarrow> prob A = 1 \<longleftrightarrow> (AE x in M. x \<in> A)"
+  using AE_in_set_eq_1[of A] by simp
+
 lemma (in prob_space) prob_sums:
   assumes P: "\<And>n. {x\<in>space M. P n x} \<in> events"
   assumes Q: "{x\<in>space M. Q x} \<in> events"
diff -r 5e01e32dadbe -r 3d89c38408cd src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Fri Nov 16 18:49:46 2012 +0100
@@ -81,7 +81,7 @@
   fixes I::"'i set" and P::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M::"('i \<Rightarrow> 'a measure)"
   assumes projective: "\<And>J H X. J \<noteq> {} \<Longrightarrow> J \<subseteq> H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> finite H \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow>
      (P H) (prod_emb H M J X) = (P J) X"
-  assumes prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
+  assumes proj_prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
   assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)"
   assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
 begin
@@ -133,7 +133,7 @@
   let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
   show "Int_stable ?J"
     by (rule Int_stable_PiE)
-  interpret prob_space "P J" using prob_space `finite J` by simp
+  interpret prob_space "P J" using proj_prob_space `finite J` by simp
   show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
   show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
   show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
@@ -165,7 +165,7 @@
   have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
   proof
     fix i assume "i \<in> L"
-    interpret prob_space "P {i}" using prob_space by simp
+    interpret prob_space "P {i}" using proj_prob_space by simp
     from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
   qed
   from bchoice[OF this]
diff -r 5e01e32dadbe -r 3d89c38408cd src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Fri Nov 16 18:49:46 2012 +0100
@@ -207,7 +207,7 @@
       OF `I \<noteq> {}`, OF `I \<noteq> {}`])
     fix A assume "A \<in> ?G"
     with generatorE guess J X . note JX = this
-    interpret prob_space "P J" using prob_space[OF `finite J`] .
+    interpret prob_space "P J" using proj_prob_space[OF `finite J`] .
     show "\<mu>G A \<noteq> \<infinity>" using JX by (simp add: limP_finite)
   next
     fix Z assume Z: "range Z \<subseteq> ?G" "decseq Z" "(\<Inter>i. Z i) = {}"
@@ -241,7 +241,7 @@
       note [simp] = `\<And>n. finite (J n)`
       from J  Z_emb have Z_eq: "\<And>n. Z n = emb I (J n) (B n)" "\<And>n. Z n \<in> ?G"
         unfolding J_def B_def by (subst prod_emb_trans) (insert Z, auto)
-      interpret prob_space "P (J i)" for i using prob_space by simp
+      interpret prob_space "P (J i)" for i using proj_prob_space by simp
       have "?a \<le> \<mu>G (Z 0)" by (auto intro: INF_lower)
       also have "\<dots> < \<infinity>" using J by (auto simp: Z_eq \<mu>G_eq limP_finite proj_sets)
       finally have "?a \<noteq> \<infinity>" by simp
@@ -636,13 +636,13 @@
   show "emeasure (lim\<^isub>B I P) (space (lim\<^isub>B I P)) = 1"
   proof cases
     assume "I = {}"
-    interpret prob_space "P {}" using prob_space by simp
+    interpret prob_space "P {}" using proj_prob_space by simp
     show ?thesis
       by (simp add: space_PiM_empty limP_finite emeasure_space_1 `I = {}`)
   next
     assume "I \<noteq> {}"
     then obtain i where "i \<in> I" by auto
-    interpret prob_space "P {i}" using prob_space by simp
+    interpret prob_space "P {i}" using proj_prob_space by simp
     have R: "(space (lim\<^isub>B I P)) = (emb I {i} (Pi\<^isub>E {i} (\<lambda>_. space borel)))"
       by (auto simp: prod_emb_def space_PiM)
     moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM)
@@ -660,7 +660,7 @@
   assumes X: "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"
   shows "emeasure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = emeasure (P J) (Pi\<^isub>E J B)"
 proof cases
-  interpret prob_space "P {}" using prob_space by simp
+  interpret prob_space "P {}" using proj_prob_space by simp
   assume "J = {}"
   moreover have "emb I {} {\<lambda>x. undefined} = space (lim\<^isub>B I P)"
     by (auto simp: space_PiM prod_emb_def)
@@ -677,7 +677,7 @@
   assumes "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"
   shows "measure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = measure (P J) (Pi\<^isub>E J B)"
 proof -
-  interpret prob_space "P J" using prob_space assms by simp
+  interpret prob_space "P J" using proj_prob_space assms by simp
   show ?thesis
     using emeasure_limB_emb[OF assms]
     unfolding emeasure_eq_measure limP_finite[OF `finite J` `J \<subseteq> I`] P.emeasure_eq_measure
diff -r 5e01e32dadbe -r 3d89c38408cd src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 16 18:49:46 2012 +0100
@@ -1616,7 +1616,7 @@
       fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
       fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
       val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
-    in if null cps then no_tac else debug_tac ctxt (K ("split countable fun")) (resolve_tac cps i) end
+    in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
     handle TERM _ => no_tac) 1)
 
 fun measurable_tac' ctxt ss facts = let
@@ -1764,7 +1764,7 @@
   "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
   "pred M (\<lambda>x. f x \<in> UNIV)"
   "pred M (\<lambda>x. f x \<in> {})"
-  "pred M (\<lambda>x. P' (f x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {x. P' x})"
+  "pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
   "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
   "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))"
   "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))"
@@ -1815,10 +1815,23 @@
 qed
 
 lemma [measurable (raw generic)]:
-  assumes f: "f \<in> measurable M N" and c: "{c} \<in> sets N"
+  assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
   shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
     and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
-  using measurable_sets[OF f c] by (auto simp: Int_def conj_commute eq_commute pred_def)
+proof -
+  show "pred M (\<lambda>x. f x = c)"
+  proof cases
+    assume "c \<in> space N"
+    with measurable_sets[OF f c] show ?thesis
+      by (auto simp: Int_def conj_commute pred_def)
+  next
+    assume "c \<notin> space N"
+    with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
+    then show ?thesis by (auto simp: pred_def cong: conj_cong)
+  qed
+  then show "pred M (\<lambda>x. c = f x)"
+    by (simp add: eq_commute)
+qed
 
 lemma pred_le_const[measurable (raw generic)]:
   assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
@@ -1872,6 +1885,21 @@
   "\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
   using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
 
+lemma measurable_finite[measurable (raw)]:
+  fixes S :: "'a \<Rightarrow> nat set"
+  assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
+  shows "pred M (\<lambda>x. finite (S x))"
+  unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
+
+lemma measurable_Least[measurable]:
+  assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
+  shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
+  unfolding measurable_def by (safe intro!: sets_Least) simp_all
+
+lemma measurable_count_space_insert[measurable (raw)]:
+  "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
+  by simp
+
 hide_const (open) pred
 
 subsection {* Extend measure *}