src/HOL/Probability/Independent_Family.thy
changeset 49794 3c7b5988e094
parent 49784 5e5b2da42a69
child 49795 9f2fb9b25a77
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:29 2012 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:30 2012 +0200
     1.3 @@ -47,14 +47,6 @@
     1.4  definition (in prob_space)
     1.5    "indep_event A B \<longleftrightarrow> indep_events (bool_case A B) UNIV"
     1.6  
     1.7 -definition (in prob_space)
     1.8 -  "indep_vars M' X I \<longleftrightarrow>
     1.9 -    (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
    1.10 -    indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
    1.11 -
    1.12 -definition (in prob_space)
    1.13 -  "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV"
    1.14 -
    1.15  lemma (in prob_space) indep_sets_cong:
    1.16    "I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J"
    1.17    by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+
    1.18 @@ -132,16 +124,6 @@
    1.19    using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev
    1.20    by (simp add: ac_simps UNIV_bool)
    1.21  
    1.22 -lemma (in prob_space) indep_var_eq:
    1.23 -  "indep_var S X T Y \<longleftrightarrow>
    1.24 -    (random_variable S X \<and> random_variable T Y) \<and>
    1.25 -    indep_set
    1.26 -      (sigma_sets (space M) { X -` A \<inter> space M | A. A \<in> sets S})
    1.27 -      (sigma_sets (space M) { Y -` A \<inter> space M | A. A \<in> sets T})"
    1.28 -  unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool
    1.29 -  by (intro arg_cong2[where f="op \<and>"] arg_cong2[where f=indep_sets] ext)
    1.30 -     (auto split: bool.split)
    1.31 -
    1.32  lemma (in prob_space)
    1.33    assumes indep: "indep_set A B"
    1.34    shows indep_setD_ev1: "A \<subseteq> events"
    1.35 @@ -341,18 +323,36 @@
    1.36      by (rule indep_sets_mono_sets) (intro subsetI sigma_sets.Basic)
    1.37  qed
    1.38  
    1.39 -lemma (in prob_space)
    1.40 -  "indep_vars M' X I \<longleftrightarrow>
    1.41 +definition (in prob_space)
    1.42 +  indep_vars_def2: "indep_vars M' X I \<longleftrightarrow>
    1.43      (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
    1.44      indep_sets (\<lambda>i. { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
    1.45 -  unfolding indep_vars_def
    1.46 +
    1.47 +definition (in prob_space)
    1.48 +  "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV"
    1.49 +
    1.50 +lemma (in prob_space) indep_vars_def:
    1.51 +  "indep_vars M' X I \<longleftrightarrow>
    1.52 +    (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
    1.53 +    indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
    1.54 +  unfolding indep_vars_def2
    1.55    apply (rule conj_cong[OF refl])
    1.56 -  apply (rule indep_sets_sigma_sets_iff)
    1.57 +  apply (rule indep_sets_sigma_sets_iff[symmetric])
    1.58    apply (auto simp: Int_stable_def)
    1.59    apply (rule_tac x="A \<inter> Aa" in exI)
    1.60    apply auto
    1.61    done
    1.62  
    1.63 +lemma (in prob_space) indep_var_eq:
    1.64 +  "indep_var S X T Y \<longleftrightarrow>
    1.65 +    (random_variable S X \<and> random_variable T Y) \<and>
    1.66 +    indep_set
    1.67 +      (sigma_sets (space M) { X -` A \<inter> space M | A. A \<in> sets S})
    1.68 +      (sigma_sets (space M) { Y -` A \<inter> space M | A. A \<in> sets T})"
    1.69 +  unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool
    1.70 +  by (intro arg_cong2[where f="op \<and>"] arg_cong2[where f=indep_sets] ext)
    1.71 +     (auto split: bool.split)
    1.72 +
    1.73  lemma (in prob_space) indep_sets2_eq:
    1.74    "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)"
    1.75    unfolding indep_set_def