# HG changeset patch
# User hoelzl
# Date 1349863943 -7200
# Node ID 5e5b2da42a69909304c5ad16aaf5a77adeb9383a
# Parent  38b84d1802ed70e464094c7e7f7fcad3cf569e02
remove incseq assumption from measure_eqI_generator_eq

diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Oct 10 12:12:23 2012 +0200
@@ -385,7 +385,7 @@
     then show "sets ?D = sigma_sets (space ?P) ?E"
       by simp
   next
-    show "range F \<subseteq> ?E" "incseq F" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
+    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
       using F by (auto simp: space_pair_measure)
   next
     fix X assume "X \<in> ?E"
diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 10 12:12:23 2012 +0200
@@ -751,7 +751,6 @@
 
     show "range ?F \<subseteq> prod_algebra (I \<union> J) M" using F
       using fin by (auto simp: prod_algebra_eq_finite)
-    show "incseq ?F" by fact
     show "(\<Union>i. \<Pi>\<^isub>E ia\<in>I \<union> J. F ia i) = (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i))"
       using F(3) by (simp add: space_PiM)
   next
diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:23 2012 +0200
@@ -23,13 +23,6 @@
 qed auto
 
 definition (in prob_space)
-  "indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and>
-    (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
-
-definition (in prob_space)
-  "indep_event A B \<longleftrightarrow> indep_events (bool_case A B) UNIV"
-
-definition (in prob_space)
   "indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and>
     (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> (\<forall>A\<in>Pi J F. prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))"
 
@@ -37,6 +30,24 @@
   "indep_set A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV"
 
 definition (in prob_space)
+  indep_events_def_alt: "indep_events A I \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I"
+
+lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
+  by auto
+
+lemma (in prob_space) indep_events_def:
+  "indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and>
+    (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
+  unfolding indep_events_def_alt indep_sets_def
+  apply (simp add: Ball_def Pi_iff image_subset_iff_funcset)
+  apply (intro conj_cong refl arg_cong[where f=All] ext imp_cong)
+  apply auto
+  done
+
+definition (in prob_space)
+  "indep_event A B \<longleftrightarrow> indep_events (bool_case A B) UNIV"
+
+definition (in prob_space)
   "indep_vars M' X I \<longleftrightarrow>
     (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
     indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
@@ -48,11 +59,6 @@
   "I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J"
   by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+
 
-lemma (in prob_space) indep_sets_singleton_iff_indep_events:
-  "indep_sets (\<lambda>i. {F i}) I \<longleftrightarrow> indep_events F I"
-  unfolding indep_sets_def indep_events_def
-  by (simp, intro conj_cong ball_cong all_cong imp_cong) (auto simp: Pi_iff)
-
 lemma (in prob_space) indep_events_finite_index_events:
   "indep_events F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_events F J)"
   by (auto simp: indep_events_def)
@@ -660,7 +666,7 @@
   show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV"
   proof (rule indep_sets_sigma)
     show "indep_sets (\<lambda>i. {F i}) UNIV"
-      unfolding indep_sets_singleton_iff_indep_events by fact
+      unfolding indep_events_def_alt[symmetric] by fact
     fix i show "Int_stable {F i}"
       unfolding Int_stable_def by simp
   qed
@@ -892,7 +898,7 @@
       show "sets ?P' = sigma_sets (space ?P) (prod_algebra I M')"
         by (simp add: sets_PiM space_PiM cong: prod_algebra_cong)
       let ?A = "\<lambda>i. \<Pi>\<^isub>E i\<in>I. space (M' i)"
-      show "range ?A \<subseteq> prod_algebra I M'" "incseq ?A" "(\<Union>i. ?A i) = space (Pi\<^isub>M I M')"
+      show "range ?A \<subseteq> prod_algebra I M'" "(\<Union>i. ?A i) = space (Pi\<^isub>M I M')"
         by (auto simp: space_PiM intro!: space_in_prod_algebra cong: prod_algebra_cong)
       { fix i show "emeasure ?D (\<Pi>\<^isub>E i\<in>I. space (M' i)) \<noteq> \<infinity>" by auto }
     next
@@ -1042,7 +1048,7 @@
     then show "sets M = sigma_sets (space ?P) ?E"
       using sets[symmetric] by simp
   next
-    show "range F \<subseteq> ?E" "incseq F" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
+    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
       using F by (auto simp: space_pair_measure)
   next
     fix X assume "X \<in> ?E"
diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:23 2012 +0200
@@ -87,7 +87,7 @@
   let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
   show "Int_stable ?J"
     by (rule Int_stable_PiE)
-  show "range ?F \<subseteq> ?J" "incseq ?F" "(\<Union>i. ?F i) = ?\<Omega>"
+  show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
     using `finite J` by (auto intro!: prod_algebraI_finite)
   { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
   show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Oct 10 12:12:23 2012 +0200
@@ -569,7 +569,6 @@
     by (simp_all add: borel_eq_atLeastAtMost sets_eq)
 
   show "range cube \<subseteq> ?E" unfolding cube_def [abs_def] by auto
-  show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
   { fix x :: 'a have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
   then show "(\<Union>i. cube i :: 'a set) = UNIV" by auto
 
diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:23 2012 +0200
@@ -628,7 +628,7 @@
   and eq: "\<And>X. X \<in> E \<Longrightarrow> emeasure M X = emeasure N X"
   and M: "sets M = sigma_sets \<Omega> E"
   and N: "sets N = sigma_sets \<Omega> E"
-  and A: "range A \<subseteq> E" "incseq A" "(\<Union>i. A i) = \<Omega>" "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
+  and A: "range A \<subseteq> E" "(\<Union>i. A i) = \<Omega>" "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   shows "M = N"
 proof -
   let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
@@ -673,25 +673,38 @@
     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> sigma_sets \<Omega> E \<Longrightarrow> ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)"
-      by (subst (asm) *) auto }
+    have "\<And>D. D \<in> sets M \<Longrightarrow> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
+      unfolding M by (subst (asm) *) auto }
   note * = this
   show "M = N"
   proof (rule measure_eqI)
     show "sets M = sets N"
       using M N by simp
+    have [simp, intro]: "\<And>i. A i \<in> sets M"
+      using A(1) by (auto simp: subset_eq M)
     fix F assume "F \<in> sets M"
-    then have "F \<in> sigma_sets \<Omega> E"
-      using M by simp
-    let ?A = "\<lambda>i. A i \<inter> F"
-    have "range ?A \<subseteq> sigma_sets \<Omega> E" "incseq ?A"
-      using A(1,2) `F \<in> sigma_sets \<Omega> E` by (auto simp: incseq_def)
-    moreover
-    { fix i have "?\<mu> (?A i) = ?\<nu> (?A i)"
-        using *[of "A i" F] `F \<in> sigma_sets \<Omega> E` A finite by auto }
-    ultimately show "?\<mu> F = ?\<nu> F"
-      using SUP_emeasure_incseq[of ?A M] SUP_emeasure_incseq[of ?A N] A(3) `F \<in> sigma_sets \<Omega> E`
-      by (auto simp: M N SUP_emeasure_incseq)
+    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)"
+      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`
+      by (auto simp: subset_eq)
+    have "disjoint_family ?D"
+      by (auto simp: disjoint_family_disjointed)
+     moreover
+    { fix i
+      have "A i \<inter> ?D i = ?D i"
+        by (auto simp: disjointed_def)
+      then have "emeasure M (?D i) = emeasure N (?D i)"
+        using *[of "A i" "?D i", OF _ A(3)] A(1) by auto }
+     ultimately show "emeasure M F = emeasure N F"
+      using N M
+      apply (subst (1 2) F_eq)
+      apply (subst (1 2) suminf_emeasure[symmetric])
+      apply auto
+      done
   qed
 qed