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)
```