# HG changeset patch
# User hellerar
# Date 1283434575 -7200
# Node ID f92b7e2877c2db6f8d54577c34b3975db630774d
# Parent  67da17aced5aa3a94c8c09cc0dc1b50ec27c0ba7# Parent  11314c196e119dda4c87e8478fd042ce9262e1ae
merged

diff -r 67da17aced5a -r f92b7e2877c2 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 02 15:36:15 2010 +0200
@@ -5027,7 +5027,7 @@
   (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i<DIM('a). ((a$$i \<le> x$$i \<and> x$$i \<le> b$$i) \<or> (b$$i \<le> x$$i \<and> x$$i \<le> a$$i))) \<longrightarrow> x \<in> s)"
 
 lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
-  "is_interval {a<..<b}" (is ?th2) proof - 
+  "is_interval {a<..<b}" (is ?th2) proof -
   have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
   show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
     by(meson order_trans le_less_trans less_le_trans *)+ qed
@@ -5051,6 +5051,9 @@
 lemma continuous_at_inner: "continuous (at x) (inner a)"
   unfolding continuous_at by (intro tendsto_intros)
 
+lemma continuous_at_euclidean_component[intro!, simp]: "continuous (at x) (\<lambda>x. x $$ i)"
+  unfolding euclidean_component_def by (rule continuous_at_inner)
+
 lemma continuous_on_inner:
   fixes s :: "'a::real_inner set"
   shows "continuous_on s (inner a)"
@@ -5159,6 +5162,9 @@
     by (simp add: closed_def open_halfspace_component_lt)
 qed
 
+lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
+  by (auto intro!: continuous_open_vimage)
+
 text{* This gives a simple derivation of limit component bounds.                 *}
 
 lemma Lim_component_le: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
diff -r 67da17aced5a -r f92b7e2877c2 src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Probability/Borel.thy	Thu Sep 02 15:36:15 2010 +0200
@@ -81,7 +81,7 @@
   "(\<lambda>x. c) \<in> borel_measurable M"
   by (auto intro!: measurable_const)
 
-lemma (in sigma_algebra) borel_measurable_indicator:
+lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]:
   assumes A: "A \<in> sets M"
   shows "indicator A \<in> borel_measurable M"
   unfolding indicator_def_raw using A
@@ -658,6 +658,30 @@
   "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
   using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
 
+lemma borel_measureable_euclidean_component:
+  "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel_space"
+  unfolding borel_space_def[where 'a=real]
+proof (rule borel_space.measurable_sigma)
+  fix S::"real set" assume "S \<in> open" then have "open S" unfolding mem_def .
+  from open_vimage_euclidean_component[OF this]
+  show "(\<lambda>x. x $$ i) -` S \<inter> space borel_space \<in> sets borel_space"
+    by (auto intro: borel_space_open)
+qed auto
+
+lemma (in sigma_algebra) borel_measureable_euclidean_space:
+  fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
+  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)"
+proof safe
+  fix i assume "f \<in> borel_measurable M"
+  then show "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
+    using measurable_comp[of f _ _ "\<lambda>x. x $$ i", unfolded comp_def]
+    by (auto intro: borel_measureable_euclidean_component)
+next
+  assume f: "\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M"
+  then show "f \<in> borel_measurable M"
+    unfolding borel_measurable_iff_halfspace_le by auto
+qed
+
 subsection "Borel measurable operators"
 
 lemma (in sigma_algebra) affine_borel_measurable_vector:
diff -r 67da17aced5a -r f92b7e2877c2 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Probability/Measure.thy	Thu Sep 02 15:36:15 2010 +0200
@@ -451,6 +451,32 @@
   qed
 qed
 
+lemma (in measure_space) measure_space_vimage:
+  assumes "f \<in> measurable M M'"
+  and "sigma_algebra M'"
+  shows "measure_space M' (\<lambda>A. \<mu> (f -` A \<inter> space M))" (is "measure_space M' ?T")
+proof -
+  interpret M': sigma_algebra M' by fact
+
+  show ?thesis
+  proof
+    show "?T {} = 0" by simp
+
+    show "countably_additive M' ?T"
+    proof (unfold countably_additive_def, safe)
+      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
+      hence *: "\<And>i. f -` (A i) \<inter> space M \<in> sets M"
+        using `f \<in> measurable M M'` by (auto simp: measurable_def)
+      moreover have "(\<Union>i. f -`  A i \<inter> space M) \<in> sets M"
+        using * by blast
+      moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)"
+        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
+      ultimately show "(\<Sum>\<^isub>\<infinity> i. ?T (A i)) = ?T (\<Union>i. A i)"
+        using measure_countably_additive[OF _ **] by (auto simp: comp_def vimage_UN)
+    qed
+  qed
+qed
+
 section "@{text \<sigma>}-finite Measures"
 
 locale sigma_finite_measure = measure_space +
diff -r 67da17aced5a -r f92b7e2877c2 src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Probability/Probability_Space.thy	Thu Sep 02 15:36:15 2010 +0200
@@ -1,5 +1,5 @@
 theory Probability_Space
-imports Lebesgue_Integration
+imports Lebesgue_Integration Radon_Nikodym
 begin
 
 lemma (in measure_space) measure_inter_full_set:
@@ -197,35 +197,17 @@
 qed
 
 lemma distribution_prob_space:
-  fixes S :: "('c, 'd) algebra_scheme"
-  assumes "sigma_algebra S" "random_variable S X"
+  assumes S: "sigma_algebra S" "random_variable S X"
   shows "prob_space S (distribution X)"
 proof -
-  interpret S: sigma_algebra S by fact
+  interpret S: measure_space S "distribution X"
+    using measure_space_vimage[OF S(2,1)] unfolding distribution_def .
   show ?thesis
   proof
-    show "distribution X {} = 0" unfolding distribution_def by simp
     have "X -` space S \<inter> space M = space M"
       using `random_variable S X` by (auto simp: measurable_def)
-    then show "distribution X (space S) = 1" using measure_space_1 by (simp add: distribution_def)
-
-    show "countably_additive S (distribution X)"
-    proof (unfold countably_additive_def, safe)
-      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets S" "disjoint_family A"
-      hence *: "\<And>i. X -` A i \<inter> space M \<in> sets M"
-        using `random_variable S X` by (auto simp: measurable_def)
-      moreover hence "\<And>i. \<mu> (X -` A i \<inter> space M) \<noteq> \<omega>"
-        using finite_measure by auto
-      moreover have "(\<Union>i. X -`  A i \<inter> space M) \<in> sets M"
-        using * by blast
-      moreover hence "\<mu> (\<Union>i. X -` A i \<inter> space M) \<noteq> \<omega>"
-        using finite_measure by auto
-      moreover have **: "disjoint_family (\<lambda>i. X -` A i \<inter> space M)"
-        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
-      ultimately show "(\<Sum>\<^isub>\<infinity> i. distribution X (A i)) = distribution X (\<Union>i. A i)"
-        using measure_countably_additive[OF _ **]
-        by (auto simp: distribution_def Real_real comp_def vimage_UN)
-    qed
+    then show "distribution X (space S) = 1"
+      using measure_space_1 by (simp add: distribution_def)
   qed
 qed
 
@@ -463,4 +445,182 @@
     by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1)
 qed
 
+lemma (in prob_space) prob_space_subalgebra:
+  assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+  shows "prob_space (M\<lparr> sets := N \<rparr>) \<mu>" sorry
+
+lemma (in measure_space) measure_space_subalgebra:
+  assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+  shows "measure_space (M\<lparr> sets := N \<rparr>) \<mu>" sorry
+
+lemma pinfreal_0_less_mult_iff[simp]:
+  fixes x y :: pinfreal shows "0 < x * y \<longleftrightarrow> 0 < x \<and> 0 < y"
+  by (cases x, cases y) (auto simp: zero_less_mult_iff)
+
+lemma (in sigma_algebra) simple_function_subalgebra:
+  assumes "sigma_algebra.simple_function (M\<lparr>sets:=N\<rparr>) f"
+  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets:=N\<rparr>)"
+  shows "simple_function f"
+  using assms
+  unfolding simple_function_def
+  unfolding sigma_algebra.simple_function_def[OF N_subalgebra(2)]
+  by auto
+
+lemma (in measure_space) simple_integral_subalgebra[simp]:
+  assumes "measure_space (M\<lparr>sets := N\<rparr>) \<mu>"
+  shows "measure_space.simple_integral (M\<lparr>sets := N\<rparr>) \<mu> = simple_integral"
+  unfolding simple_integral_def_raw
+  unfolding measure_space.simple_integral_def_raw[OF assms] by simp
+
+lemma (in sigma_algebra) borel_measurable_subalgebra:
+  assumes "N \<subseteq> sets M" "f \<in> borel_measurable (M\<lparr>sets:=N\<rparr>)"
+  shows "f \<in> borel_measurable M"
+  using assms unfolding measurable_def by auto
+
+lemma (in measure_space) positive_integral_subalgebra[simp]:
+  assumes borel: "f \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
+  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets := N\<rparr>)"
+  shows "measure_space.positive_integral (M\<lparr>sets := N\<rparr>) \<mu> f = positive_integral f"
+proof -
+  note msN = measure_space_subalgebra[OF N_subalgebra]
+  then interpret N: measure_space "M\<lparr>sets:=N\<rparr>" \<mu> .
+
+  from N.borel_measurable_implies_simple_function_sequence[OF borel]
+  obtain fs where Nsf: "\<And>i. N.simple_function (fs i)" and "fs \<up> f" by blast
+  then have sf: "\<And>i. simple_function (fs i)"
+    using simple_function_subalgebra[OF _ N_subalgebra] by blast
+
+  from positive_integral_isoton_simple[OF `fs \<up> f` sf] N.positive_integral_isoton_simple[OF `fs \<up> f` Nsf]
+  show ?thesis unfolding simple_integral_subalgebra[OF msN] isoton_def by simp
+qed
+
+section "Conditional Expectation and Probability"
+
+lemma (in prob_space) conditional_expectation_exists:
+  fixes X :: "'a \<Rightarrow> pinfreal"
+  assumes borel: "X \<in> borel_measurable M"
+  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+  shows "\<exists>Y\<in>borel_measurable (M\<lparr> sets := N \<rparr>). \<forall>C\<in>N.
+      positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)"
+proof -
+  interpret P: prob_space "M\<lparr> sets := N \<rparr>" \<mu>
+    using prob_space_subalgebra[OF N_subalgebra] .
+
+  let "?f A" = "\<lambda>x. X x * indicator A x"
+  let "?Q A" = "positive_integral (?f A)"
+
+  from measure_space_density[OF borel]
+  have Q: "measure_space (M\<lparr> sets := N \<rparr>) ?Q"
+    by (rule measure_space.measure_space_subalgebra[OF _ N_subalgebra])
+  then interpret Q: measure_space "M\<lparr> sets := N \<rparr>" ?Q .
+
+  have "P.absolutely_continuous ?Q"
+    unfolding P.absolutely_continuous_def
+  proof (safe, simp)
+    fix A assume "A \<in> N" "\<mu> A = 0"
+    moreover then have f_borel: "?f A \<in> borel_measurable M"
+      using borel N_subalgebra by (auto intro: borel_measurable_indicator)
+    moreover have "{x\<in>space M. ?f A x \<noteq> 0} = (?f A -` {0<..} \<inter> space M) \<inter> A"
+      by (auto simp: indicator_def)
+    moreover have "\<mu> \<dots> \<le> \<mu> A"
+      using `A \<in> N` N_subalgebra f_borel
+      by (auto intro!: measure_mono Int[of _ A] measurable_sets)
+    ultimately show "?Q A = 0"
+      by (simp add: positive_integral_0_iff)
+  qed
+  from P.Radon_Nikodym[OF Q this]
+  obtain Y where Y: "Y \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
+    "\<And>A. A \<in> sets (M\<lparr>sets:=N\<rparr>) \<Longrightarrow> ?Q A = P.positive_integral (\<lambda>x. Y x * indicator A x)"
+    by blast
+  with N_subalgebra show ?thesis
+    by (auto intro!: bexI[OF _ Y(1)])
+qed
+
+definition (in prob_space)
+  "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable (M\<lparr>sets:=N\<rparr>)
+    \<and> (\<forall>C\<in>N. positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)))"
+
+abbreviation (in prob_space)
+  "conditional_probabiltiy N A \<equiv> conditional_expectation N (indicator A)"
+
+lemma (in prob_space)
+  fixes X :: "'a \<Rightarrow> pinfreal"
+  assumes borel: "X \<in> borel_measurable M"
+  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+  shows borel_measurable_conditional_expectation:
+    "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
+  and conditional_expectation: "\<And>C. C \<in> N \<Longrightarrow>
+      positive_integral (\<lambda>x. conditional_expectation N X x * indicator C x) =
+      positive_integral (\<lambda>x. X x * indicator C x)"
+   (is "\<And>C. C \<in> N \<Longrightarrow> ?eq C")
+proof -
+  note CE = conditional_expectation_exists[OF assms, unfolded Bex_def]
+  then show "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
+    unfolding conditional_expectation_def by (rule someI2_ex) blast
+
+  from CE show "\<And>C. C\<in>N \<Longrightarrow> ?eq C"
+    unfolding conditional_expectation_def by (rule someI2_ex) blast
+qed
+
+lemma (in sigma_algebra) factorize_measurable_function:
+  fixes Z :: "'a \<Rightarrow> pinfreal" and Y :: "'a \<Rightarrow> 'c"
+  assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M"
+  shows "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)
+    \<longleftrightarrow> (\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x))"
+proof safe
+  interpret M': sigma_algebra M' by fact
+  have Y: "Y \<in> space M \<rightarrow> space M'" using assms unfolding measurable_def by auto
+  from M'.sigma_algebra_vimage[OF this]
+  interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" .
+
+  { fix g :: "'c \<Rightarrow> pinfreal" assume "g \<in> borel_measurable M'"
+    with M'.measurable_vimage_algebra[OF Y]
+    have "g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
+      by (rule measurable_comp)
+    moreover assume "\<forall>x\<in>space M. Z x = g (Y x)"
+    then have "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y) \<longleftrightarrow>
+       g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
+       by (auto intro!: measurable_cong)
+    ultimately show "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
+      by simp }
+
+  assume "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
+  from va.borel_measurable_implies_simple_function_sequence[OF this]
+  obtain f where f: "\<And>i. va.simple_function (f i)" and "f \<up> Z" by blast
+
+  have "\<forall>i. \<exists>g. M'.simple_function g \<and> (\<forall>x\<in>space M. f i x = g (Y x))"
+  proof
+    fix i
+    from f[of i] have "finite (f i`space M)" and B_ex:
+      "\<forall>z\<in>(f i)`space M. \<exists>B. B \<in> sets M' \<and> (f i) -` {z} \<inter> space M = Y -` B \<inter> space M"
+      unfolding va.simple_function_def by auto
+    from B_ex[THEN bchoice] guess B .. note B = this
+
+    let ?g = "\<lambda>x. \<Sum>z\<in>f i`space M. z * indicator (B z) x"
+
+    show "\<exists>g. M'.simple_function g \<and> (\<forall>x\<in>space M. f i x = g (Y x))"
+    proof (intro exI[of _ ?g] conjI ballI)
+      show "M'.simple_function ?g" using B by auto
+
+      fix x assume "x \<in> space M"
+      then have "\<And>z. z \<in> f i`space M \<Longrightarrow> indicator (B z) (Y x) = (indicator (f i -` {z} \<inter> space M) x::pinfreal)"
+        unfolding indicator_def using B by auto
+      then show "f i x = ?g (Y x)" using `x \<in> space M` f[of i]
+        by (subst va.simple_function_indicator_representation) auto
+    qed
+  qed
+  from choice[OF this] guess g .. note g = this
+
+  show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
+  proof (intro ballI bexI)
+    show "(SUP i. g i) \<in> borel_measurable M'"
+      using g by (auto intro: M'.borel_measurable_simple_function)
+    fix x assume "x \<in> space M"
+    have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp
+    also have "\<dots> = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand
+      using g `x \<in> space M` by simp
+    finally show "Z x = (SUP i. g i) (Y x)" .
+  qed
+qed
+
 end
diff -r 67da17aced5a -r f92b7e2877c2 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Probability/Product_Measure.thy	Thu Sep 02 15:36:15 2010 +0200
@@ -2,12 +2,11 @@
 imports Lebesgue_Integration
 begin
 
-definition dynkin
-where "dynkin M =
-      ((\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
-       space M \<in> sets M \<and> (\<forall> b \<in> sets M. \<forall> a \<in> sets M. a \<subseteq> b \<longrightarrow> b - a \<in> sets M) \<and>
-       (\<forall> a. (\<forall> i j :: nat. i \<noteq> j \<longrightarrow> a i \<inter> a j = {}) \<and>
-             (\<forall> i :: nat. a i \<in> sets M) \<longrightarrow> UNION UNIV a \<in> sets M))"
+definition "dynkin M \<longleftrightarrow>
+  space M \<in> sets M \<and>
+  (\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
+  (\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M) \<and>
+  (\<forall>A. disjoint_family A \<and> range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
 
 lemma dynkinI:
   assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
@@ -15,7 +14,7 @@
   assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
           \<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
   shows "dynkin M"
-using assms unfolding dynkin_def by auto
+using assms unfolding dynkin_def sorry
 
 lemma dynkin_subset:
   assumes "dynkin M"
@@ -42,16 +41,16 @@
   assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
   assumes "\<And> i :: nat. a i \<in> sets M"
   shows "UNION UNIV a \<in> sets M"
-using assms unfolding dynkin_def by auto
+using assms unfolding dynkin_def sorry
 
-definition Int_stable
-where "Int_stable M = (\<forall> a \<in> sets M. (\<forall> b \<in> sets M. a \<inter> b \<in> sets M))"
+definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
 
 lemma dynkin_trivial:
   shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>"
 by (rule dynkinI) auto
 
 lemma dynkin_lemma:
+  fixes D :: "'a algebra"
   assumes stab: "Int_stable E"
   and spac: "space E = space D"
   and subsED: "sets E \<subseteq> sets D"
@@ -72,23 +71,9 @@
   proof (rule dynkinI, safe)
     fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A"
     { fix d :: "('a, 'b) algebra_scheme" assume "A \<in> sets d" "dynkin d \<and> space d = space E"
-      hence "A \<subseteq> space d"
-        using dynkin_subset by auto }
-    show "x \<in> space \<delta>E" using asm
-      unfolding \<delta>E_def sets_\<delta>E_def using not_empty
-    proof auto
-      fix x A fix d :: "'a algebra"
-      assume asm: "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
-        dynkin d \<and>
-        space d = space E \<and>
-        sets E \<subseteq> sets d) \<longrightarrow>
-        A \<in> x" "x \<in> A"
-        and asm': "space d = space E" "dynkin d" "sets E \<subseteq> sets d"
-      have "A \<in> sets d"
-        apply (rule impE[OF spec[OF asm(1), of "sets d"]])
-        using exI[of _ d] asm' by auto
-      thus "x \<in> space E" using asm' dynkin_subset[OF asm'(2), of A] asm(2) by auto
-    qed
+      hence "A \<subseteq> space d" using dynkin_subset by auto }
+    show "x \<in> space \<delta>E" using asm unfolding \<delta>E_def sets_\<delta>E_def using not_empty
+      by simp (metis dynkin_subset in_mono mem_def)
   next
     show "space \<delta>E \<in> sets \<delta>E"
       unfolding \<delta>E_def sets_\<delta>E_def
@@ -103,28 +88,14 @@
       unfolding \<delta>E_def sets_\<delta>E_def apply (auto intro!:dynkin_UN[OF _ asm(1)])
       by blast
   qed
+
   def Dy == "\<lambda> d. {A | A. A \<in> sets_\<delta>E \<and> A \<inter> d \<in> sets_\<delta>E}"
   { fix d assume dasm: "d \<in> sets_\<delta>E"
     have "dynkin \<lparr> space = space E, sets = Dy d \<rparr>"
-    proof (rule dynkinI, auto)
+    proof (rule dynkinI, safe, simp_all)
       fix A x assume "A \<in> Dy d" "x \<in> A"
       thus "x \<in> space E" unfolding Dy_def sets_\<delta>E_def using not_empty
-      proof auto fix x A fix da :: "'a algebra"
-        assume asm: "x \<in> A"
-          "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
-          dynkin d \<and> space d = space E \<and>
-          sets E \<subseteq> sets d) \<longrightarrow> A \<in> x"
-          "\<forall>x. (\<exists>d. x = sets d \<and>
-          dynkin d \<and> space d = space E \<and>
-          sets E \<subseteq> sets d) \<longrightarrow> A \<inter> d \<in> x"
-          "space da = space E" "dynkin da"
-          "sets E \<subseteq> sets da"
-        have "A \<in> sets da"
-          apply (rule impE[OF spec[OF asm(2)], of "sets da"])
-          apply (rule exI[of _ da])
-          using exI[of _ da] asm(4,5,6) by auto
-        thus "x \<in> space E" using dynkin_subset[OF asm(5)] asm by auto
-      qed
+        by simp (metis dynkin_subset in_mono mem_def)
     next
       show "space E \<in> Dy d"
         unfolding Dy_def \<delta>E_def sets_\<delta>E_def
@@ -192,20 +163,7 @@
       have "\<lparr> space = space E, sets = Dy e \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
         using Dy_nkin[OF deasm[unfolded \<delta>E_def, simplified]] E_\<delta>E E_Dy by auto
       hence "sets_\<delta>E \<subseteq> Dy e"
-        unfolding sets_\<delta>E_def
-      proof auto fix x
-        assume asm: "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and>
-          dynkin d \<and>
-          space d = space E \<and>
-          sets E \<subseteq> sets d) \<longrightarrow>
-          x \<in> xa"
-          "dynkin \<lparr>space = space E, sets = Dy e\<rparr>"
-          "sets E \<subseteq> Dy e"
-        show "x \<in> Dy e"
-          apply (rule impE[OF spec[OF asm(1), of "Dy e"]])
-          apply (rule exI[of _ "\<lparr>space = space E, sets = Dy e\<rparr>"])
-          using asm by auto
-      qed
+        unfolding sets_\<delta>E_def by auto (metis E_Dy simps(1) simps(2) spac)
       hence "sets \<delta>E = Dy e" using subset unfolding \<delta>E_def by auto
       hence "d \<inter> e \<in> sets \<delta>E"
         using dasm easm deasm unfolding Dy_def \<delta>E_def by auto
@@ -214,18 +172,8 @@
         by (auto simp add:Int_commute) }
     hence "sets E \<subseteq> Dy d" by auto
     hence "sets \<delta>E \<subseteq> Dy d" using Dy_nkin[OF dasm[unfolded \<delta>E_def, simplified]]
-      unfolding \<delta>E_def sets_\<delta>E_def 
-    proof auto
-      fix x
-      assume asm: "sets E \<subseteq> Dy d"
-        "dynkin \<lparr>space = space E, sets = Dy d\<rparr>"
-        "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and> dynkin d \<and>
-            space d = space E \<and> sets E \<subseteq> sets d) \<longrightarrow> x \<in> xa"
-      show "x \<in> Dy d"
-        apply (rule impE[OF spec[OF asm(3), of "Dy d"]])
-        apply (rule exI[of _ "\<lparr>space = space E, sets = Dy d\<rparr>"])
-        using asm by auto
-    qed
+      unfolding \<delta>E_def sets_\<delta>E_def
+      by auto (metis `sets E <= Dy d` simps(1) simps(2) spac)
     hence *: "sets \<delta>E = Dy d"
       unfolding Dy_def \<delta>E_def by auto
     fix a assume aasm: "a \<in> sets \<delta>E"
@@ -394,19 +342,72 @@
     have "\<mu> (A i \<inter> B) = \<nu> (A i \<inter> B)"
       apply (rule measure_eq[of \<mu> ?M \<nu> "\<lparr> space = space E \<inter> A i, sets = op \<inter> (A i) ` sets E\<rparr>" "A i \<inter> B", simplified])
       using assms nu_i mu_i
-      apply (auto simp add:image_def) (* TODO *)
+      apply (auto simp add:image_def) (* TODO *) sorry
+    show ?thesis sorry
 qed
 
-lemma
-(*
 definition prod_sets where
   "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
 
 definition
-  "prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) -` A)))"
+  "prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))"
+
+lemma
+  fixes M1 :: "'a algebra" and M2 :: "'b algebra"
+  assumes "algebra M1" "algebra M2"
+  shows measureable_fst[intro!, simp]:
+    "fst \<in> measurable (prod_measure_space M1 M2) M1" (is ?fst)
+  and measureable_snd[intro!, simp]:
+    "snd \<in> measurable (prod_measure_space M1 M2) M2" (is ?snd)
+proof -
+  interpret M1: algebra M1 by fact
+  interpret M2: algebra M2 by fact
+
+  { fix X assume "X \<in> sets M1"
+    then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. fst -` X \<inter> space M1 \<times> space M2 = X1 \<times> X2"
+      apply - apply (rule bexI[of _ X]) apply (rule bexI[of _ "space M2"])
+      using M1.sets_into_space by force+ }
+  moreover
+  { fix X assume "X \<in> sets M2"
+    then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. snd -` X \<inter> space M1 \<times> space M2 = X1 \<times> X2"
+      apply - apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X])
+      using M2.sets_into_space by force+ }
+  ultimately show ?fst ?snd
+    by (force intro!: sigma_sets.Basic
+              simp: measurable_def prod_measure_space_def prod_sets_def sets_sigma)+
+qed
+
+lemma (in sigma_algebra) measureable_prod:
+  fixes M1 :: "'a algebra" and M2 :: "'b algebra"
+  assumes "algebra M1" "algebra M2"
+  shows "f \<in> measurable M (prod_measure_space M1 M2) \<longleftrightarrow>
+    (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
+using assms proof (safe intro!: measurable_comp[where b="prod_measure_space M1 M2"])
+  interpret M1: algebra M1 by fact
+  interpret M2: algebra M2 by fact
+  assume f: "(fst \<circ> f) \<in> measurable M M1" and s: "(snd \<circ> f) \<in> measurable M M2"
+
+  show "f \<in> measurable M (prod_measure_space M1 M2)" unfolding prod_measure_space_def
+  proof (rule measurable_sigma)
+    show "prod_sets (sets M1) (sets M2) \<subseteq> Pow (space M1 \<times> space M2)"
+      unfolding prod_sets_def using M1.sets_into_space M2.sets_into_space by auto
+    show "f \<in> space M \<rightarrow> space M1 \<times> space M2"
+      using f s by (auto simp: mem_Times_iff measurable_def comp_def)
+    fix A assume "A \<in> prod_sets (sets M1) (sets M2)"
+    then obtain B C where "B \<in> sets M1" "C \<in> sets M2" "A = B \<times> C"
+      unfolding prod_sets_def by auto
+    moreover have "(fst \<circ> f) -` B \<inter> space M \<in> sets M"
+      using f `B \<in> sets M1` unfolding measurable_def by auto
+    moreover have "(snd \<circ> f) -` C \<inter> space M \<in> sets M"
+      using s `C \<in> sets M2` unfolding measurable_def by auto
+    moreover have "f -` A \<inter> space M = ((fst \<circ> f) -` B \<inter> space M) \<inter> ((snd \<circ> f) -` C \<inter> space M)"
+      unfolding `A = B \<times> C` by (auto simp: vimage_Times)
+    ultimately show "f -` A \<inter> space M \<in> sets M" by auto
+  qed
+qed
 
 definition
-  "prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))"
+  "prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) -` A)))"
 
 lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
   by (auto simp add: prod_sets_def)
@@ -550,5 +551,4 @@
   unfolding finite_prod_measure_space[OF N, symmetric]
   using finite_measure_space_finite_prod_measure[OF N] .
 
-*)
-end
\ No newline at end of file
+end
diff -r 67da17aced5a -r f92b7e2877c2 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Sep 02 15:31:38 2010 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Sep 02 15:36:15 2010 +0200
@@ -626,6 +626,51 @@
   thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
 qed
 
+subsection {* Sigma algebra generated by function preimages *}
+
+definition (in sigma_algebra)
+  "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M \<rparr>"
+
+lemma (in sigma_algebra) in_vimage_algebra[simp]:
+  "A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
+  by (simp add: vimage_algebra_def image_iff)
+
+lemma (in sigma_algebra) space_vimage_algebra[simp]:
+  "space (vimage_algebra S f) = S"
+  by (simp add: vimage_algebra_def)
+
+lemma (in sigma_algebra) sigma_algebra_vimage:
+  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
+  shows "sigma_algebra (vimage_algebra S f)"
+proof
+  fix A assume "A \<in> sets (vimage_algebra S f)"
+  then guess B unfolding in_vimage_algebra ..
+  then show "space (vimage_algebra S f) - A \<in> sets (vimage_algebra S f)"
+    using sets_into_space assms
+    by (auto intro!: bexI[of _ "space M - B"])
+next
+  fix A assume "A \<in> sets (vimage_algebra S f)"
+  then guess A' unfolding in_vimage_algebra .. note A' = this
+  fix B assume "B \<in> sets (vimage_algebra S f)"
+  then guess B' unfolding in_vimage_algebra .. note B' = this
+  then show "A \<union> B \<in> sets (vimage_algebra S f)"
+    using sets_into_space assms A' B'
+    by (auto intro!: bexI[of _ "A' \<union> B'"])
+next
+  fix A::"nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets (vimage_algebra S f)"
+  then have "\<forall>i. \<exists>B. A i = f -` B \<inter> S \<and> B \<in> sets M"
+    by (simp add: subset_eq) blast
+  from this[THEN choice] obtain B
+    where B: "\<And>i. A i = f -` B i \<inter> S" "range B \<subseteq> sets M" by auto
+  show "(\<Union>i. A i) \<in> sets (vimage_algebra S f)"
+    using B by (auto intro!: bexI[of _ "\<Union>i. B i"])
+qed auto
+
+lemma (in sigma_algebra) measurable_vimage_algebra:
+  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
+  shows "f \<in> measurable (vimage_algebra S f) M"
+    unfolding measurable_def using assms by force
+
 subsection {* A Two-Element Series *}
 
 definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "