# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1426614303 0
# Node ID f41a2f77ab1b84b1827d6f62d2dcc581bbe85a3b
# Parent  cd945dc13becbb37f6477d43d2296ac3dbefcaec
Inserted real_of_nat to fix factorial-related problem

diff -r cd945dc13bec -r f41a2f77ab1b src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Tue Mar 17 15:11:25 2015 +0000
+++ b/src/HOL/Probability/Distributions.thy	Tue Mar 17 17:45:03 2015 +0000
@@ -78,9 +78,8 @@
 proof -
   let ?f = "\<lambda>k x. x^k * exp (-x) / fact k"
   let ?F = "\<lambda>k x. - (\<Sum>n\<le>k. (x^n * exp (-x)) / fact n)"
-
-  have "?I * (inverse (fact k)) = 
-      (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (fact k)) \<partial>lborel)"
+  have "?I * (inverse (real_of_nat (fact k))) = 
+      (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (real_of_nat (fact k))) \<partial>lborel)"
     by (intro nn_integral_multc[symmetric]) auto
   also have "\<dots> = (\<integral>\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \<partial>lborel)"
     apply (intro nn_integral_cong)
@@ -114,7 +113,7 @@
 qed
 
 lemma nn_intergal_power_times_exp_Ici:
-  shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = fact k"
+  shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = real_of_nat (fact k)"
 proof (rule LIMSEQ_unique)
   let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \<partial>lborel"
   show "?X ----> (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
@@ -127,7 +126,7 @@
   have "((\<lambda>x::real. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / (fact n))) * fact k) --->
         (1 - (\<Sum>n\<le>k. 0 / (fact n))) * fact k) at_top"
     by (intro tendsto_intros tendsto_power_div_exp_0) simp
-  then show "?X ----> fact k"
+  then show "?X ----> real_of_nat (fact k)"
     by (subst nn_intergal_power_times_exp_Icc)
        (auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially])
 qed