src/HOL/Probability/Caratheodory.thy
changeset 35704 5007843dae33
parent 35582 b16d99a72dc9
child 36649 bfd8c550faa6
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Wed Mar 10 15:38:33 2010 -0800
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Wed Mar 10 15:57:01 2010 -0800
     1.3 @@ -816,9 +816,9 @@
     1.4            by (simp add: eqe) 
     1.5          finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
     1.6        qed
     1.7 -    def C \<equiv> "(split BB) o nat_to_nat2"
     1.8 +    def C \<equiv> "(split BB) o prod_decode"
     1.9      have C: "!!n. C n \<in> sets M"
    1.10 -      apply (rule_tac p="nat_to_nat2 n" in PairE)
    1.11 +      apply (rule_tac p="prod_decode n" in PairE)
    1.12        apply (simp add: C_def)
    1.13        apply (metis BB subsetD rangeI)  
    1.14        done
    1.15 @@ -828,11 +828,10 @@
    1.16          assume x: "x \<in> A i"
    1.17          with sbBB [of i] obtain j where "x \<in> BB i j"
    1.18            by blast        
    1.19 -        thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
    1.20 -          by (metis nat_to_nat2_surj internal_split_def prod.cases 
    1.21 -                prod_case_split surj_f_inv_f)
    1.22 +        thus "\<exists>i. x \<in> split BB (prod_decode i)"
    1.23 +          by (metis prod_encode_inverse prod.cases prod_case_split)
    1.24        qed 
    1.25 -    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
    1.26 +    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
    1.27        by (rule ext)  (auto simp add: C_def) 
    1.28      also have "... sums suminf ll" 
    1.29        proof (rule suminf_2dimen)