src/HOL/Library/Stirling.thy
changeset 63918 6bf55e6e0b75
parent 63487 6e29fb72e659
child 64240 eabf80376aab
     1.1 --- a/src/HOL/Library/Stirling.thy	Mon Sep 19 12:53:30 2016 +0200
     1.2 +++ b/src/HOL/Library/Stirling.thy	Mon Sep 19 20:06:21 2016 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4      also have "\<dots> = Suc n * (\<Sum>k=1..n. fact n div k) + Suc n * fact n div Suc n"
     1.5        by (metis nat.distinct(1) nonzero_mult_divide_cancel_left)
     1.6      also have "\<dots> = (\<Sum>k=1..n. fact (Suc n) div k) + fact (Suc n) div Suc n"
     1.7 -      by (simp add: setsum_right_distrib div_mult_swap dvd_fact)
     1.8 +      by (simp add: setsum_distrib_left div_mult_swap dvd_fact)
     1.9      also have "\<dots> = (\<Sum>k=1..Suc n. fact (Suc n) div k)"
    1.10        by simp
    1.11      finally show ?thesis .
    1.12 @@ -162,7 +162,7 @@
    1.13    also have "\<dots> = (\<Sum>k\<le>n. n * stirling n (Suc k) + stirling n k)"
    1.14      by simp
    1.15    also have "\<dots> = n * (\<Sum>k\<le>n. stirling n (Suc k)) + (\<Sum>k\<le>n. stirling n k)"
    1.16 -    by (simp add: setsum.distrib setsum_right_distrib)
    1.17 +    by (simp add: setsum.distrib setsum_distrib_left)
    1.18    also have "\<dots> = n * fact n + fact n"
    1.19    proof -
    1.20      have "n * (\<Sum>k\<le>n. stirling n (Suc k)) = n * ((\<Sum>k\<le>Suc n. stirling n k) - stirling n 0)"
    1.21 @@ -195,7 +195,7 @@
    1.22      by (subst setsum_atMost_Suc_shift) (simp add: setsum.distrib ring_distribs)
    1.23    also have "\<dots> = pochhammer x (Suc n)"
    1.24      by (subst setsum_atMost_Suc_shift [symmetric])
    1.25 -      (simp add: algebra_simps setsum.distrib setsum_right_distrib pochhammer_Suc Suc [symmetric])
    1.26 +      (simp add: algebra_simps setsum.distrib setsum_distrib_left pochhammer_Suc Suc [symmetric])
    1.27    finally show ?case .
    1.28  qed
    1.29