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