src/HOL/Probability/Probability_Mass_Function.thy
changeset 59557 ebd8ecacfba6
parent 59527 edaabc1ab1ed
child 59664 224741ede5ae
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 18 22:46:48 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Feb 19 11:53:36 2015 +0100
     1.3 @@ -582,14 +582,14 @@
     1.4    (* Proof by Manuel Eberl *)
     1.5  
     1.6    have summable: "summable (\<lambda>x::nat. rate ^ x / fact x)" using summable_exp
     1.7 -    by (simp add: field_simps field_divide_inverse[symmetric])
     1.8 +    by (simp add: field_simps divide_inverse [symmetric])
     1.9    have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x * exp (-rate) \<partial>count_space UNIV) =
    1.10            exp (-rate) * (\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV)"
    1.11      by (simp add: field_simps nn_integral_cmult[symmetric])
    1.12    also from rate_pos have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV) = (\<Sum>x. rate ^ x / fact x)"
    1.13      by (simp_all add: nn_integral_count_space_nat suminf_ereal summable suminf_ereal_finite)
    1.14    also have "... = exp rate" unfolding exp_def
    1.15 -    by (simp add: field_simps field_divide_inverse[symmetric] transfer_int_nat_factorial)
    1.16 +    by (simp add: field_simps divide_inverse [symmetric] transfer_int_nat_factorial)
    1.17    also have "ereal (exp (-rate)) * ereal (exp rate) = 1"
    1.18      by (simp add: mult_exp_exp)
    1.19    finally show "(\<integral>\<^sup>+ x. ereal (rate ^ x / real (fact x) * exp (- rate)) \<partial>count_space UNIV) = 1" .