diff -r de7792ea4090 -r b7c394c7a619 src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Tue Mar 10 16:12:35 2015 +0000
+++ b/src/HOL/Probability/Distributions.thy	Mon Mar 16 15:30:00 2015 +0000
@@ -83,7 +83,9 @@
       (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (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)"
-    by (intro nn_integral_cong) (simp add: field_simps)
+    apply (intro nn_integral_cong)
+    apply (simp add: field_simps)
+    by (metis (no_types) divide_inverse mult.commute mult.left_commute mult.left_neutral times_ereal.simps(1))
   also have "\<dots> = ereal (?F k a - ?F k 0)"
   proof (rule nn_integral_FTC_Icc)
     fix x assume "x \<in> {0..a}"
@@ -93,13 +95,13 @@
     next
       case (Suc k)
       have "DERIV (\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) x :>
-        ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k))"
+        ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / (fact (Suc k))"
         by (intro DERIV_diff Suc)
            (auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc
                  simp add: field_simps power_Suc[symmetric] real_of_nat_def[symmetric])
       also have "(\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) = ?F (Suc k)"
         by simp
-      also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k)) = ?f (Suc k) x"
+      also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / (fact (Suc k)) = ?f (Suc k) x"
         by (auto simp: field_simps simp del: fact_Suc)
            (simp_all add: real_of_nat_Suc field_simps)
       finally show ?case .
@@ -122,7 +124,8 @@
     apply (metis nat_ceiling_le_eq)
     done
 
-  have "((\<lambda>x. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / real (fact n))) * fact k) ---> (1 - (\<Sum>n\<le>k. 0 / real (fact n))) * fact k) at_top"
+  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"
     by (subst nn_intergal_power_times_exp_Icc)
@@ -514,7 +517,7 @@
       by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density)
   
     let ?I = "(integral\<^sup>N lborel (\<lambda>y. ereal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))"
-    let ?C = "real (fact (Suc (k\<^sub>1 + k\<^sub>2))) / (real (fact k\<^sub>1) * real (fact k\<^sub>2))"
+    let ?C = "(fact (Suc (k\<^sub>1 + k\<^sub>2))) / ((fact k\<^sub>1) * (fact k\<^sub>2))"
     let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1"
     let ?L = "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x- y) * erlang_density k\<^sub>2 l y * indicator {0..x} y) \<partial>lborel)"
 
@@ -919,10 +922,12 @@
 lemma
   fixes k :: nat
   shows gaussian_moment_even_pos:
-    "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k)))
-       ((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" (is "?even")
+    "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k)))
+       ((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" 
+       (is "?even")
     and gaussian_moment_odd_pos:
-      "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)" (is "?odd")
+      "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)" 
+      (is "?odd")
 proof -
   let ?M = "\<lambda>k x. exp (- x\<^sup>2) * x^k :: real"
 
@@ -997,9 +1002,11 @@
   proof (induct k)
     case (Suc k)
     note step[OF this]
-    also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * (real (fact (2 * k)) / real (2 ^ (2 * k) * fact k)))) =
-      sqrt pi / 2 * (real (fact (2 * Suc k)) / real (2 ^ (2 * Suc k) * fact (Suc k)))"
-      by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps)
+    also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * ((fact (2 * k)) / ((2::real)^(2*k) * fact k)))) =
+      sqrt pi / 2 * ((fact (2 * Suc k)) / ((2::real)^(2 * Suc k) * fact (Suc k)))"
+      apply (simp add: field_simps del: fact_Suc)
+      apply (simp add: real_of_nat_def of_nat_mult field_simps)
+      done
     finally show ?case
       by simp
   qed (insert gaussian_moment_0, simp)
@@ -1008,7 +1015,7 @@
   proof (induct k)
     case (Suc k)
     note step[OF this]
-    also have "(real (2 * k + 1 + 1) / 2 * (real (fact k) / 2)) = real (fact (Suc k)) / 2"
+    also have "(real (2 * k + 1 + 1) / (2::real) * ((fact k) / 2)) = (fact (Suc k)) / 2"
       by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps)
     finally show ?case
       by simp
@@ -1036,7 +1043,7 @@
     by (auto simp: fun_eq_iff field_simps real_sqrt_power[symmetric] real_sqrt_mult
                    real_sqrt_divide power_mult eq)
   also have "((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) = 
-    (inverse (sqrt 2 * \<sigma>) * (real (fact (2 * k))) / ((2/\<sigma>\<^sup>2) ^ k * real (fact k)))"
+    (inverse (sqrt 2 * \<sigma>) * ((fact (2 * k))) / ((2/\<sigma>\<^sup>2) ^ k * (fact k)))"
     by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_mult
                    power2_eq_square)
   finally show ?thesis
@@ -1047,10 +1054,10 @@
 lemma normal_moment_abs_odd:
   "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^(2 * k + 1)) (2^k * \<sigma>^(2 * k + 1) * fact k * sqrt (2 / pi))"
 proof -
-  have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1))) (fact k / 2)"
+  have "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1))) (fact k / 2)"
     by (rule has_bochner_integral_cong[THEN iffD1, OF _ _ _ gaussian_moment_odd_pos[of k]]) auto
   from has_bochner_integral_even_function[OF this]
-  have "has_bochner_integral lborel (\<lambda>x. exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) (fact k)"
+  have "has_bochner_integral lborel (\<lambda>x::real. exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) (fact k)"
     by simp
   then have "has_bochner_integral lborel (\<lambda>x. (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))
       (fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))"
@@ -1059,7 +1066,7 @@
     (\<lambda>x. exp (- (((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) * \<bar>sqrt 2 * \<sigma> * x\<bar> ^ (2 * k + 1) / sqrt (2 * pi * \<sigma>\<^sup>2))"
     by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult real_sqrt_mult)
   also have "(fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) = 
-    (inverse (sqrt 2) * inverse \<sigma> * (2 ^ k * (\<sigma> * \<sigma> ^ (2 * k)) * real (fact k) * sqrt (2 / pi)))"
+    (inverse (sqrt 2) * inverse \<sigma> * (2 ^ k * (\<sigma> * \<sigma> ^ (2 * k)) * (fact k) * sqrt (2 / pi)))"
     by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_divide
                    real_sqrt_mult)
   finally show ?thesis