src/HOL/Probability/Independent_Family.thy
 changeset 55414 eab03e9cee8a parent 53015 a1119cf551e8 child 56154 f0a927235162
```     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Feb 12 08:35:56 2014 +0100
1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Feb 12 08:35:57 2014 +0100
1.3 @@ -13,7 +13,7 @@
1.4      (\<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))))"
1.5
1.6  definition (in prob_space)
1.7 -  "indep_set A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV"
1.8 +  "indep_set A B \<longleftrightarrow> indep_sets (case_bool A B) UNIV"
1.9
1.10  definition (in prob_space)
1.11    indep_events_def_alt: "indep_events A I \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I"
1.12 @@ -28,7 +28,7 @@
1.13    done
1.14
1.15  definition (in prob_space)
1.16 -  "indep_event A B \<longleftrightarrow> indep_events (bool_case A B) UNIV"
1.17 +  "indep_event A B \<longleftrightarrow> indep_events (case_bool A B) UNIV"
1.18
1.19  lemma (in prob_space) indep_sets_cong:
1.20    "I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J"
1.21 @@ -104,7 +104,7 @@
1.22  lemma (in prob_space) indep_setD:
1.23    assumes indep: "indep_set A B" and ev: "a \<in> A" "b \<in> B"
1.24    shows "prob (a \<inter> b) = prob a * prob b"
1.25 -  using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev
1.26 +  using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "case_bool a b"] ev
1.27    by (simp add: ac_simps UNIV_bool)
1.28
1.29  lemma (in prob_space)
1.30 @@ -312,7 +312,7 @@
1.31      indep_sets (\<lambda>i. { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
1.32
1.33  definition (in prob_space)
1.34 -  "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV"
1.35 +  "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (case_bool Ma Mb) (case_bool A B) UNIV"
1.36
1.37  lemma (in prob_space) indep_vars_def:
1.38    "indep_vars M' X I \<longleftrightarrow>
1.39 @@ -340,16 +340,16 @@
1.40    "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.41    unfolding indep_set_def
1.42  proof (intro iffI ballI conjI)
1.43 -  assume indep: "indep_sets (bool_case A B) UNIV"
1.44 +  assume indep: "indep_sets (case_bool A B) UNIV"
1.45    { fix a b assume "a \<in> A" "b \<in> B"
1.46 -    with indep_setsD[OF indep, of UNIV "bool_case a b"]
1.47 +    with indep_setsD[OF indep, of UNIV "case_bool a b"]
1.48      show "prob (a \<inter> b) = prob a * prob b"
1.49        unfolding UNIV_bool by (simp add: ac_simps) }
1.50    from indep show "A \<subseteq> events" "B \<subseteq> events"
1.51      unfolding indep_sets_def UNIV_bool by auto
1.52  next
1.53    assume *: "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.54 -  show "indep_sets (bool_case A B) UNIV"
1.55 +  show "indep_sets (case_bool A B) UNIV"
1.56    proof (rule indep_setsI)
1.57      fix i show "(case i of True \<Rightarrow> A | False \<Rightarrow> B) \<subseteq> events"
1.58        using * by (auto split: bool.split)
1.59 @@ -369,7 +369,7 @@
1.60  proof -
1.61    have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A | False \<Rightarrow> B)) UNIV"
1.62    proof (rule indep_sets_sigma)
1.63 -    show "indep_sets (bool_case A B) UNIV"
1.64 +    show "indep_sets (case_bool A B) UNIV"
1.65        by (rule `indep_set A B`[unfolded indep_set_def])
1.66      fix i show "Int_stable (case i of True \<Rightarrow> A | False \<Rightarrow> B)"
1.67        using A B by (cases i) auto
1.68 @@ -572,19 +572,19 @@
1.69    qed
1.70
1.71    { fix n
1.72 -    have "indep_sets (\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) UNIV"
1.73 +    have "indep_sets (\<lambda>b. sigma_sets (space M) (\<Union>m\<in>case_bool {..n} {Suc n..} b. A m)) UNIV"
1.74      proof (rule indep_sets_collect_sigma)
1.75        have *: "(\<Union>b. case b of True \<Rightarrow> {..n} | False \<Rightarrow> {Suc n..}) = UNIV" (is "?U = _")
1.76          by (simp split: bool.split add: set_eq_iff) (metis not_less_eq_eq)
1.77        with indep show "indep_sets A ?U" by simp
1.78 -      show "disjoint_family (bool_case {..n} {Suc n..})"
1.79 +      show "disjoint_family (case_bool {..n} {Suc n..})"
1.80          unfolding disjoint_family_on_def by (auto split: bool.split)
1.81        fix m
1.82        show "Int_stable (A m)"
1.83          unfolding Int_stable_def using A.Int by auto
1.84      qed
1.85 -    also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) =
1.86 -      bool_case (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
1.87 +    also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>case_bool {..n} {Suc n..} b. A m)) =
1.88 +      case_bool (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
1.89        by (auto intro!: ext split: bool.split)
1.90      finally have indep: "indep_set (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
1.91        unfolding indep_set_def by simp
1.92 @@ -923,9 +923,9 @@
1.93      prob (A -` Xa \<inter> space M) * prob (B -` Xb \<inter> space M)"
1.94  proof -
1.95    have "prob ((\<lambda>x. (A x, B x)) -` (Xa \<times> Xb) \<inter> space M) =
1.96 -    prob (\<Inter>i\<in>UNIV. (bool_case A B i -` bool_case Xa Xb i \<inter> space M))"
1.97 +    prob (\<Inter>i\<in>UNIV. (case_bool A B i -` case_bool Xa Xb i \<inter> space M))"
1.98      by (auto intro!: arg_cong[where f=prob] simp: UNIV_bool)
1.99 -  also have "\<dots> = (\<Prod>i\<in>UNIV. prob (bool_case A B i -` bool_case Xa Xb i \<inter> space M))"
1.100 +  also have "\<dots> = (\<Prod>i\<in>UNIV. prob (case_bool A B i -` case_bool Xa Xb i \<inter> space M))"
1.101      using indep unfolding indep_var_def
1.102      by (rule indep_varsD) (auto split: bool.split intro: sets)
1.103    also have "\<dots> = prob (A -` Xa \<inter> space M) * prob (B -` Xb \<inter> space M)"
1.104 @@ -938,7 +938,7 @@
1.105    shows indep_var_rv1: "random_variable S X"
1.106      and indep_var_rv2: "random_variable T Y"
1.107  proof -
1.108 -  have "\<forall>i\<in>UNIV. random_variable (bool_case S T i) (bool_case X Y i)"
1.109 +  have "\<forall>i\<in>UNIV. random_variable (case_bool S T i) (case_bool X Y i)"
1.110      using assms unfolding indep_var_def indep_vars_def by auto
1.111    then show "random_variable S X" "random_variable T Y"
1.112      unfolding UNIV_bool by auto
```