# HG changeset patch
# User hoelzl
# Date 1349863950 -7200
# Node ID 3c7b5988e09409caff2433746ddfe4b07a0b98e6
# Parent  dd719cdeca8f03065e71806f9fbf6bcd8e848182
indep_vars does not need sigma-sets

diff -r dd719cdeca8f -r 3c7b5988e094 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:29 2012 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:30 2012 +0200
@@ -47,14 +47,6 @@
 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"
-
-definition (in prob_space)
-  "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV"
-
 lemma (in prob_space) indep_sets_cong:
   "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+
@@ -132,16 +124,6 @@
   using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev
   by (simp add: ac_simps UNIV_bool)
 
-lemma (in prob_space) indep_var_eq:
-  "indep_var S X T Y \<longleftrightarrow>
-    (random_variable S X \<and> random_variable T Y) \<and>
-    indep_set
-      (sigma_sets (space M) { X -` A \<inter> space M | A. A \<in> sets S})
-      (sigma_sets (space M) { Y -` A \<inter> space M | A. A \<in> sets T})"
-  unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool
-  by (intro arg_cong2[where f="op \<and>"] arg_cong2[where f=indep_sets] ext)
-     (auto split: bool.split)
-
 lemma (in prob_space)
   assumes indep: "indep_set A B"
   shows indep_setD_ev1: "A \<subseteq> events"
@@ -341,18 +323,36 @@
     by (rule indep_sets_mono_sets) (intro subsetI sigma_sets.Basic)
 qed
 
-lemma (in prob_space)
-  "indep_vars M' X I \<longleftrightarrow>
+definition (in prob_space)
+  indep_vars_def2: "indep_vars M' X I \<longleftrightarrow>
     (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
     indep_sets (\<lambda>i. { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
-  unfolding indep_vars_def
+
+definition (in prob_space)
+  "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV"
+
+lemma (in prob_space) indep_vars_def:
+  "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"
+  unfolding indep_vars_def2
   apply (rule conj_cong[OF refl])
-  apply (rule indep_sets_sigma_sets_iff)
+  apply (rule indep_sets_sigma_sets_iff[symmetric])
   apply (auto simp: Int_stable_def)
   apply (rule_tac x="A \<inter> Aa" in exI)
   apply auto
   done
 
+lemma (in prob_space) indep_var_eq:
+  "indep_var S X T Y \<longleftrightarrow>
+    (random_variable S X \<and> random_variable T Y) \<and>
+    indep_set
+      (sigma_sets (space M) { X -` A \<inter> space M | A. A \<in> sets S})
+      (sigma_sets (space M) { Y -` A \<inter> space M | A. A \<in> sets T})"
+  unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool
+  by (intro arg_cong2[where f="op \<and>"] arg_cong2[where f=indep_sets] ext)
+     (auto split: bool.split)
+
 lemma (in prob_space) indep_sets2_eq:
   "indep_set A B \<longleftrightarrow> A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
   unfolding indep_set_def