src/HOL/Probability/Independent_Family.thy
changeset 62390 842917225d56
parent 62343 24106dc44def
child 62975 1d066f6ab25d
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -155,7 +155,7 @@
     1.4              next
     1.5                assume "J \<noteq> {j}"
     1.6                have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J-{j}. A i) \<inter> X)"
     1.7 -                using \<open>j \<in> J\<close> \<open>A j = X\<close> by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
     1.8 +                using \<open>j \<in> J\<close> \<open>A j = X\<close> by (auto intro!: arg_cong[where f=prob] split: if_split_asm)
     1.9                also have "\<dots> = prob X * (\<Prod>i\<in>J-{j}. prob (A i))"
    1.10                proof (rule indep)
    1.11                  show "J - {j} \<noteq> {}" "J - {j} \<subseteq> K" "finite (J - {j})" "j \<notin> J - {j}"
    1.12 @@ -172,7 +172,7 @@
    1.13              qed
    1.14            next
    1.15              assume "j \<notin> J"
    1.16 -            with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm)
    1.17 +            with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: if_split_asm)
    1.18              with J show ?thesis
    1.19                by (intro indep_setsD[OF G(1)]) auto
    1.20            qed
    1.21 @@ -192,10 +192,10 @@
    1.22            have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
    1.23                prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
    1.24              using A_sets sets.sets_into_space[of _ M] X \<open>J \<noteq> {}\<close>
    1.25 -            by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
    1.26 +            by (auto intro!: arg_cong[where f=prob] split: if_split_asm)
    1.27            also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)"
    1.28              using J \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> A_sets X sets.sets_into_space
    1.29 -            by (auto intro!: finite_measure_Diff sets.finite_INT split: split_if_asm)
    1.30 +            by (auto intro!: finite_measure_Diff sets.finite_INT split: if_split_asm)
    1.31            finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
    1.32                prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
    1.33            moreover {
    1.34 @@ -223,7 +223,7 @@
    1.35            then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events"
    1.36              using G by auto
    1.37            have "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
    1.38 -            using \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> \<open>j \<in> K\<close> by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
    1.39 +            using \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> \<open>j \<in> K\<close> by (auto intro!: arg_cong[where f=prob] split: if_split_asm)
    1.40            moreover have "(\<lambda>k. prob (\<Inter>i\<in>insert j J. (A(j := F k)) i)) sums prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
    1.41            proof (rule finite_measure_UNION)
    1.42              show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)"
    1.43 @@ -233,7 +233,7 @@
    1.44            qed
    1.45            moreover { fix k
    1.46              from J A \<open>j \<in> K\<close> have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
    1.47 -              by (subst indep_setsD[OF F(2)]) (auto intro!: setprod.cong split: split_if_asm)
    1.48 +              by (subst indep_setsD[OF F(2)]) (auto intro!: setprod.cong split: if_split_asm)
    1.49              also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)"
    1.50                using J A \<open>j \<in> K\<close> by (subst indep_setsD[OF G(1)]) auto
    1.51              finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . }
    1.52 @@ -271,7 +271,7 @@
    1.53              by (intro indep_setsD[OF indep]) auto
    1.54          next
    1.55            assume "j \<notin> J"
    1.56 -          with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm)
    1.57 +          with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: if_split_asm)
    1.58            with J show ?thesis
    1.59              by (intro indep_setsD[OF G(1)]) auto
    1.60          qed
    1.61 @@ -842,10 +842,10 @@
    1.62      let ?A = "\<lambda>j. if j \<in> J then A j else space M"
    1.63      have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
    1.64        using subset_trans[OF F(1) sets.space_closed] J A
    1.65 -      by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast
    1.66 +      by (auto intro!: arg_cong[where f=prob] split: if_split_asm) blast
    1.67      also
    1.68      from A F have "(\<lambda>j. if j \<in> J then A j else space M) \<in> Pi I F" (is "?A \<in> _")
    1.69 -      by (auto split: split_if_asm)
    1.70 +      by (auto split: if_split_asm)
    1.71      with indep have "prob (\<Inter>j\<in>I. ?A j) = (\<Prod>j\<in>I. prob (?A j))"
    1.72        by auto
    1.73      also have "\<dots> = (\<Prod>j\<in>J. prob (A j))"
    1.74 @@ -1089,7 +1089,7 @@
    1.75        then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)"
    1.76          by (simp add: emeasure_distr X)
    1.77        also have "?X -` E \<inter> space M = (\<Inter>i\<in>J. X i -` Y i \<inter> space M)"
    1.78 -        using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
    1.79 +        using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: if_split_asm)
    1.80        also have "emeasure M (\<Inter>i\<in>J. X i -` Y i \<inter> space M) = (\<Prod> i\<in>J. emeasure M (X i -` Y i \<inter> space M))"
    1.81          using \<open>indep_vars M' X I\<close> J \<open>I \<noteq> {}\<close> using indep_varsD[of M' X I J]
    1.82          by (auto simp: emeasure_eq_measure setprod_ereal)
    1.83 @@ -1120,7 +1120,7 @@
    1.84          Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j -` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto
    1.85        let ?E = "prod_emb I M' J (Pi\<^sub>E J Y)"
    1.86        from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M"
    1.87 -        using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
    1.88 +        using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: if_split_asm)
    1.89        then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)"
    1.90          by simp
    1.91        also have "\<dots> = emeasure ?D ?E"