src/HOL/Probability/Caratheodory.thy
changeset 61424 c3658c18b7bc
parent 61273 542a4d9bac96
child 61427 3c69ea85f8dd
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -417,7 +417,7 @@
     1.4        and Ble: "\<And>n. (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)"
     1.5        by auto blast
     1.6  
     1.7 -    def C \<equiv> "split B o prod_decode"
     1.8 +    def C \<equiv> "case_prod B o prod_decode"
     1.9      from B have B_in_M: "\<And>i j. B i j \<in> M"
    1.10        by (rule range_subsetD)
    1.11      then have C: "range C \<subseteq> M"
    1.12 @@ -800,24 +800,24 @@
    1.13            by blast
    1.14        qed
    1.15        from choice[OF this] guess f .. note f = this
    1.16 -      then have UN_f_eq: "(\<Union>i. split f (prod_decode i)) = (\<Union>i. A i)"
    1.17 +      then have UN_f_eq: "(\<Union>i. case_prod f (prod_decode i)) = (\<Union>i. A i)"
    1.18          unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff)
    1.19  
    1.20 -      have d: "disjoint_family (\<lambda>i. split f (prod_decode i))"
    1.21 +      have d: "disjoint_family (\<lambda>i. case_prod f (prod_decode i))"
    1.22          unfolding disjoint_family_on_def
    1.23        proof (intro ballI impI)
    1.24          fix m n :: nat assume "m \<noteq> n"
    1.25          then have neq: "prod_decode m \<noteq> prod_decode n"
    1.26            using inj_prod_decode[of UNIV] by (auto simp: inj_on_def)
    1.27 -        show "split f (prod_decode m) \<inter> split f (prod_decode n) = {}"
    1.28 +        show "case_prod f (prod_decode m) \<inter> case_prod f (prod_decode n) = {}"
    1.29          proof cases
    1.30            assume "fst (prod_decode m) = fst (prod_decode n)"
    1.31            then show ?thesis
    1.32              using neq f by (fastforce simp: disjoint_family_on_def)
    1.33          next
    1.34            assume neq: "fst (prod_decode m) \<noteq> fst (prod_decode n)"
    1.35 -          have "split f (prod_decode m) \<subseteq> A (fst (prod_decode m))"
    1.36 -            "split f (prod_decode n) \<subseteq> A (fst (prod_decode n))"
    1.37 +          have "case_prod f (prod_decode m) \<subseteq> A (fst (prod_decode m))"
    1.38 +            "case_prod f (prod_decode n) \<subseteq> A (fst (prod_decode n))"
    1.39              using f[THEN spec, of "fst (prod_decode m)"]
    1.40              using f[THEN spec, of "fst (prod_decode n)"]
    1.41              by (auto simp: set_eq_iff)
    1.42 @@ -825,12 +825,12 @@
    1.43              by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff)
    1.44          qed
    1.45        qed
    1.46 -      from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (split f (prod_decode n)))"
    1.47 +      from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (case_prod f (prod_decode n)))"
    1.48          by (intro suminf_ereal_2dimen[symmetric] positiveD2[OF pos] generated_ringI_Basic)
    1.49           (auto split: prod.split)
    1.50 -      also have "\<dots> = (\<Sum>n. \<mu> (split f (prod_decode n)))"
    1.51 +      also have "\<dots> = (\<Sum>n. \<mu> (case_prod f (prod_decode n)))"
    1.52          using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split)
    1.53 -      also have "\<dots> = \<mu> (\<Union>i. split f (prod_decode i))"
    1.54 +      also have "\<dots> = \<mu> (\<Union>i. case_prod f (prod_decode i))"
    1.55          using f `c \<in> C'` C'
    1.56          by (intro ca[unfolded countably_additive_def, rule_format])
    1.57             (auto split: prod.split simp: UN_f_eq d UN_eq)