# HG changeset patch
# User hoelzl
# Date 1349863947 -7200
# Node ID e0a4cb91a8a9333a8aab00ac94f263dca3302e4f
# Parent  3c10763f5cb42ed41ff7f0ebea71702314671f8a
add induction rule for intersection-stable sigma-sets

diff -r 3c10763f5cb4 -r e0a4cb91a8a9 src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Oct 10 12:12:26 2012 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Oct 10 12:12:27 2012 +0200
@@ -33,15 +33,18 @@
       {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}
       (\<lambda>X. \<integral>\<^isup>+x. (\<integral>\<^isup>+y. indicator X (x,y) \<partial>B) \<partial>A)"
 
+lemma pair_measure_closed: "{a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} \<subseteq> Pow (space A \<times> space B)"
+  using space_closed[of A] space_closed[of B] by auto
+
 lemma space_pair_measure:
   "space (A \<Otimes>\<^isub>M B) = space A \<times> space B"
-  unfolding pair_measure_def using space_closed[of A] space_closed[of B]
-  by (intro space_measure_of) auto
+  unfolding pair_measure_def using pair_measure_closed[of A B]
+  by (rule space_measure_of)
 
 lemma sets_pair_measure:
   "sets (A \<Otimes>\<^isub>M B) = sigma_sets (space A \<times> space B) {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}"
-  unfolding pair_measure_def using space_closed[of A] space_closed[of B]
-  by (intro sets_measure_of) auto
+  unfolding pair_measure_def using pair_measure_closed[of A B]
+  by (rule sets_measure_of)
 
 lemma sets_pair_measure_cong[cong]:
   "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
@@ -162,40 +165,24 @@
   assumes "Q \<in> sets (N \<Otimes>\<^isub>M M)"
   shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N"
     (is "?s Q \<in> _")
-proof -
-  let ?\<Omega> = "space N \<times> space M" and ?D = "{A\<in>sets (N \<Otimes>\<^isub>M M). ?s A \<in> borel_measurable N}"
-  note space_pair_measure[simp]
-  interpret dynkin_system ?\<Omega> ?D
-  proof (intro dynkin_systemI)
-    fix A assume "A \<in> ?D" then show "A \<subseteq> ?\<Omega>"
-      using sets_into_space[of A "N \<Otimes>\<^isub>M M"] by simp
-  next
-    from top show "?\<Omega> \<in> ?D"
-      by (auto simp add: if_distrib intro!: measurable_If)
-  next
-    fix A assume "A \<in> ?D"
-    with sets_into_space have "\<And>x. emeasure M (Pair x -` (?\<Omega> - A)) =
-        (if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
-      by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
-    with `A \<in> ?D` top show "?\<Omega> - A \<in> ?D"
-      by (auto intro!: measurable_If)
-  next
-    fix F :: "nat \<Rightarrow> ('b\<times>'a) set" assume "disjoint_family F" "range F \<subseteq> ?D"
-    moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
-      by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
-    ultimately show "(\<Union>i. F i) \<in> ?D"
-      by (auto simp: vimage_UN intro!: borel_measurable_psuminf)
-  qed
-  let ?G = "{a \<times> b | a b. a \<in> sets N \<and> b \<in> sets M}"
-  have "sigma_sets ?\<Omega> ?G = ?D"
-  proof (rule dynkin_lemma)
-    show "?G \<subseteq> ?D"
-      by (auto simp: if_distrib Int_def[symmetric] intro!: measurable_If)
-  qed (auto simp: sets_pair_measure  Int_stable_pair_measure_generator)
-  with `Q \<in> sets (N \<Otimes>\<^isub>M M)` have "Q \<in> ?D"
-    by (simp add: sets_pair_measure[symmetric])
-  then show "?s Q \<in> borel_measurable N" by simp
-qed
+  using Int_stable_pair_measure_generator pair_measure_closed assms
+  unfolding sets_pair_measure
+proof (induct rule: sigma_sets_induct_disjoint)
+  case (compl A)
+  with sets_into_space have "\<And>x. emeasure M (Pair x -` ((space N \<times> space M) - A)) =
+      (if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
+    unfolding sets_pair_measure[symmetric]
+    by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
+  with compl top show ?case
+    by (auto intro!: measurable_If simp: space_pair_measure)
+next
+  case (union F)
+  moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
+    unfolding sets_pair_measure[symmetric]
+    by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
+  ultimately show ?case
+    by (auto simp: vimage_UN)
+qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
 
 lemma (in sigma_finite_measure) measurable_emeasure_Pair:
   assumes Q: "Q \<in> sets (N \<Otimes>\<^isub>M M)" shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N" (is "?s Q \<in> _")
diff -r 3c10763f5cb4 -r e0a4cb91a8a9 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:26 2012 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:27 2012 +0200
@@ -633,48 +633,45 @@
 proof -
   let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
   interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
-  { fix F assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
+  have "space M = \<Omega>"
+    using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
+
+  { fix F D assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
     then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
-    let ?D = "{D \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)}"
     have "?\<nu> F \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` `F \<in> E` eq by simp
-    interpret D: dynkin_system \<Omega> ?D
-    proof (rule dynkin_systemI, simp_all)
-      fix A assume "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
-      then show "A \<subseteq> \<Omega>" using S.sets_into_space by auto
+    assume "D \<in> sets M"
+    with `Int_stable E` `E \<subseteq> Pow \<Omega>` have "emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
+      unfolding M
+    proof (induct rule: sigma_sets_induct_disjoint)
+      case (basic A)
+      then have "F \<inter> A \<in> E" using `Int_stable E` `F \<in> E` by (auto simp: Int_stable_def)
+      then show ?case using eq by auto
     next
-      have "F \<inter> \<Omega> = F" using `F \<in> E` `E \<subseteq> Pow \<Omega>` by auto
-      then show "?\<mu> (F \<inter> \<Omega>) = ?\<nu> (F \<inter> \<Omega>)"
-        using `F \<in> E` eq by (auto intro: sigma_sets_top)
+      case empty then show ?case by simp
     next
-      fix A assume *: "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
+      case (compl A)
       then have **: "F \<inter> (\<Omega> - A) = F - (F \<inter> A)"
         and [intro]: "F \<inter> A \<in> sigma_sets \<Omega> E"
-        using `F \<in> E` S.sets_into_space by auto
+        using `F \<in> E` S.sets_into_space by (auto simp: M)
       have "?\<nu> (F \<inter> A) \<le> ?\<nu> F" by (auto intro!: emeasure_mono simp: M N)
       then have "?\<nu> (F \<inter> A) \<noteq> \<infinity>" using `?\<nu> F \<noteq> \<infinity>` by auto
       have "?\<mu> (F \<inter> A) \<le> ?\<mu> F" by (auto intro!: emeasure_mono simp: M N)
       then have "?\<mu> (F \<inter> A) \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` by auto
       then have "?\<mu> (F \<inter> (\<Omega> - A)) = ?\<mu> F - ?\<mu> (F \<inter> A)" unfolding **
         using `F \<inter> A \<in> sigma_sets \<Omega> E` by (auto intro!: emeasure_Diff simp: M N)
-      also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` * by simp
+      also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` compl by simp
       also have "\<dots> = ?\<nu> (F \<inter> (\<Omega> - A))" unfolding **
         using `F \<inter> A \<in> sigma_sets \<Omega> E` `?\<nu> (F \<inter> A) \<noteq> \<infinity>`
         by (auto intro!: emeasure_Diff[symmetric] simp: M N)
-      finally show "\<Omega> - A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Omega> - A)) = ?\<nu> (F \<inter> (\<Omega> - A))"
-        using * by auto
+      finally show ?case
+        using `space M = \<Omega>` by auto
     next
-      fix A :: "nat \<Rightarrow> 'a set"
-      assume "disjoint_family A" and A: "range A \<subseteq> {X \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> X) = ?\<nu> (F \<inter> X)}"
+      case (union A)
       then have "?\<mu> (\<Union>x. F \<inter> A x) = ?\<nu> (\<Union>x. F \<inter> A x)"
         by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N)
-      with A show "(\<Union>x. A x) \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Union>x. A x)) = ?\<nu> (F \<inter> (\<Union>x. A x))"
+      with A show ?case
         by auto
-    qed
-    have *: "sigma_sets \<Omega> E = ?D"
-      using `F \<in> E` `Int_stable E`
-      by (intro D.dynkin_lemma) (auto simp add: Int_stable_def eq)
-    have "\<And>D. D \<in> sets M \<Longrightarrow> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
-      unfolding M by (subst (asm) *) auto }
+    qed }
   note * = this
   show "M = N"
   proof (rule measure_eqI)
@@ -684,9 +681,7 @@
       using A(1) by (auto simp: subset_eq M)
     fix F assume "F \<in> sets M"
     let ?D = "disjointed (\<lambda>i. F \<inter> A i)"
-    have "space M = \<Omega>"
-      using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
-    then have F_eq: "F = (\<Union>i. ?D i)"
+    from `space M = \<Omega>` have F_eq: "F = (\<Union>i. ?D i)"
       using `F \<in> sets M`[THEN sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
     have [simp, intro]: "\<And>i. ?D i \<in> sets M"
       using range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
diff -r 3c10763f5cb4 -r e0a4cb91a8a9 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 10 12:12:26 2012 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 10 12:12:27 2012 +0200
@@ -2041,4 +2041,25 @@
     using assms by (auto simp: dynkin_def)
 qed
 
+lemma sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
+  assumes "Int_stable G"
+    and closed: "G \<subseteq> Pow \<Omega>"
+    and A: "A \<in> sigma_sets \<Omega> G"
+  assumes basic: "\<And>A. A \<in> G \<Longrightarrow> P A"
+    and empty: "P {}"
+    and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
+    and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
+  shows "P A"
+proof -
+  let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
+  interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
+    using closed by (rule sigma_algebra_sigma_sets)
+  from compl[OF _ empty] closed have space: "P \<Omega>" by simp
+  interpret dynkin_system \<Omega> ?D
+    by default (auto dest: sets_into_space intro!: space compl union)
+  have "sigma_sets \<Omega> G = ?D"
+    by (rule dynkin_lemma) (auto simp: basic `Int_stable G`)
+  with A show ?thesis by auto
+qed
+
 end