simplified definitions of combinatorial functions
authorhaftmann
Sat Jul 02 20:22:25 2016 +0200 (2016-07-02)
changeset 633676c731c8b7f03
parent 63366 209c4cbbc4cd
child 63368 e9e677b73011
child 63385 370cce7ad9b9
simplified definitions of combinatorial functions
src/HOL/Binomial.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Gamma.thy
src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy
src/HOL/NthRoot.thy
src/HOL/Transcendental.thy
src/HOL/ex/Sum_of_Powers.thy
     1.1 --- a/src/HOL/Binomial.thy	Sat Jul 02 15:02:24 2016 +0200
     1.2 +++ b/src/HOL/Binomial.thy	Sat Jul 02 20:22:25 2016 +0200
     1.3 @@ -14,29 +14,38 @@
     1.4  
     1.5  subsection \<open>Factorial\<close>
     1.6  
     1.7 -fun (in semiring_char_0) fact :: "nat \<Rightarrow> 'a"
     1.8 -  where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"
     1.9 +definition (in semiring_char_0) fact :: "nat \<Rightarrow> 'a"
    1.10 +where
    1.11 +  "fact n = of_nat (\<Prod>{1..n})"
    1.12 +
    1.13 +lemma fact_altdef': "fact n = of_nat (\<Prod>{1..n})"
    1.14 +  by (fact fact_def)
    1.15  
    1.16 -lemmas fact_Suc = fact.simps(2)
    1.17 +lemma fact_altdef_nat: "fact n = \<Prod>{1..n}"
    1.18 +  by (simp add: fact_def)
    1.19 +
    1.20 +lemma fact_altdef: "fact n = (\<Prod>i=1..n. of_nat i)"
    1.21 +  by (simp add: fact_def)
    1.22 +
    1.23 +lemma fact_0 [simp]: "fact 0 = 1"
    1.24 +  by (simp add: fact_def)
    1.25  
    1.26  lemma fact_1 [simp]: "fact 1 = 1"
    1.27 -  by simp
    1.28 +  by (simp add: fact_def)
    1.29  
    1.30  lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
    1.31 -  by simp
    1.32 +  by (simp add: fact_def)
    1.33 +
    1.34 +lemma fact_Suc [simp]: "fact (Suc n) = of_nat (Suc n) * fact n"
    1.35 +  by (simp add: fact_def atLeastAtMostSuc_conv algebra_simps)
    1.36  
    1.37  lemma of_nat_fact [simp]:
    1.38    "of_nat (fact n) = fact n"
    1.39 -  by (induct n) (auto simp add: algebra_simps)
    1.40 +  by (simp add: fact_def)
    1.41  
    1.42  lemma of_int_fact [simp]:
    1.43    "of_int (fact n) = fact n"
    1.44 -proof -
    1.45 -  have "of_int (of_nat (fact n)) = fact n"
    1.46 -    unfolding of_int_of_nat_eq by simp
    1.47 -  then show ?thesis
    1.48 -    by simp
    1.49 -qed
    1.50 +  by (simp only: fact_def of_int_of_nat_eq)
    1.51  
    1.52  lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
    1.53    by (cases n) auto
    1.54 @@ -61,7 +70,7 @@
    1.55      by (metis of_nat_fact of_nat_le_iff fact_mono_nat)
    1.56  
    1.57    lemma fact_ge_1 [simp]: "fact n \<ge> (1 :: 'a)"
    1.58 -    by (metis le0 fact.simps(1) fact_mono)
    1.59 +    by (metis le0 fact_0 fact_mono)
    1.60  
    1.61    lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)"
    1.62      using fact_ge_1 less_le_trans zero_less_one by blast
    1.63 @@ -107,15 +116,6 @@
    1.64  lemma fact_ge_self: "fact n \<ge> n"
    1.65    by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)
    1.66  
    1.67 -lemma fact_altdef_nat: "fact n = \<Prod>{1..n}"
    1.68 -  by (induct n) (auto simp: atLeastAtMostSuc_conv)
    1.69 -
    1.70 -lemma fact_altdef: "fact n = (\<Prod>i=1..n. of_nat i)"
    1.71 -  by (induct n) (auto simp: atLeastAtMostSuc_conv)
    1.72 -
    1.73 -lemma fact_altdef': "fact n = of_nat (\<Prod>{1..n})"
    1.74 -  by (subst fact_altdef_nat [symmetric]) simp
    1.75 -
    1.76  lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a :: {semiring_div,linordered_semidom})"
    1.77    by (induct m) (auto simp: le_Suc_eq)
    1.78  
    1.79 @@ -164,7 +164,7 @@
    1.80  
    1.81  lemma fact_numeral:  \<comment>\<open>Evaluation for specific numerals\<close>
    1.82    "fact (numeral k) = (numeral k) * (fact (pred_numeral k))"
    1.83 -  by (metis fact.simps(2) numeral_eq_Suc of_nat_numeral)
    1.84 +  by (metis fact_Suc numeral_eq_Suc of_nat_numeral)
    1.85  
    1.86  
    1.87  text \<open>This development is based on the work of Andy Gordon and
    1.88 @@ -469,49 +469,44 @@
    1.89  
    1.90  text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close>
    1.91  
    1.92 -definition (in comm_semiring_1) "pochhammer (a :: 'a) n =
    1.93 -  (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
    1.94 +definition (in comm_semiring_1) pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
    1.95 +where
    1.96 +  "pochhammer (a :: 'a) n = setprod (\<lambda>n. a + of_nat n) {..<n}"
    1.97  
    1.98 +lemma pochhammer_Suc_setprod:
    1.99 +  "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {..n}"
   1.100 +  by (simp add: pochhammer_def lessThan_Suc_atMost)
   1.101 + 
   1.102  lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
   1.103    by (simp add: pochhammer_def)
   1.104 -
   1.105 + 
   1.106  lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
   1.107 -  by (simp add: pochhammer_def)
   1.108 -
   1.109 +  by (simp add: pochhammer_def lessThan_Suc)
   1.110 + 
   1.111  lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
   1.112 -  by (simp add: pochhammer_def)
   1.113 -
   1.114 -lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
   1.115 -  by (simp add: pochhammer_def)
   1.116 -
   1.117 +  by (simp add: pochhammer_def lessThan_Suc)
   1.118 + 
   1.119 +lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
   1.120 +  by (simp add: pochhammer_def lessThan_Suc ac_simps)
   1.121 + 
   1.122  lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
   1.123    by (simp add: pochhammer_def)
   1.124  
   1.125  lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
   1.126    by (simp add: pochhammer_def)
   1.127  
   1.128 -lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
   1.129 +lemma setprod_nat_ivl_Suc: "setprod f {.. Suc n} = setprod f {..n} * f (Suc n)"
   1.130  proof -
   1.131 -  have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto
   1.132 +  have "{..Suc n} = {..n} \<union> {Suc n}" by auto
   1.133    then show ?thesis by (simp add: field_simps)
   1.134  qed
   1.135  
   1.136 -lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}"
   1.137 +lemma setprod_nat_ivl_1_Suc: "setprod f {.. Suc n} = f 0 * setprod f {1.. Suc n}"
   1.138  proof -
   1.139 -  have "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto
   1.140 +  have "{..Suc n} = {0} \<union> {1 .. Suc n}" by auto
   1.141    then show ?thesis by simp
   1.142  qed
   1.143  
   1.144 -
   1.145 -lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
   1.146 -proof (cases n)
   1.147 -  case 0
   1.148 -  then show ?thesis by simp
   1.149 -next
   1.150 -  case (Suc n)
   1.151 -  show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc ..
   1.152 -qed
   1.153 -
   1.154  lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
   1.155  proof (cases "n = 0")
   1.156    case True
   1.157 @@ -519,14 +514,14 @@
   1.158  next
   1.159    case False
   1.160    have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto
   1.161 -  have eq: "insert 0 {1 .. n} = {0..n}" by auto
   1.162 -  have **: "(\<Prod>n\<in>{1::nat..n}. a + of_nat n) = (\<Prod>n\<in>{0::nat..n - 1}. a + 1 + of_nat n)"
   1.163 +  have eq: "insert 0 {1 .. n} = {..n}" by auto
   1.164 +  have **: "(\<Prod>n\<in>{1..n}. a + of_nat n) = (\<Prod>n\<in>{..<n}. a + 1 + of_nat n)"
   1.165      apply (rule setprod.reindex_cong [where l = Suc])
   1.166      using False
   1.167 -    apply (auto simp add: fun_eq_iff field_simps)
   1.168 +    apply (auto simp add: fun_eq_iff field_simps image_Suc_lessThan)
   1.169      done
   1.170    show ?thesis
   1.171 -    apply (simp add: pochhammer_def)
   1.172 +    apply (simp add: pochhammer_def lessThan_Suc_atMost)
   1.173      unfolding setprod.insert [OF *, unfolded eq]
   1.174      using ** apply (simp add: field_simps)
   1.175      done
   1.176 @@ -545,27 +540,15 @@
   1.177  qed simp_all
   1.178  
   1.179  lemma pochhammer_fact: "fact n = pochhammer 1 n"
   1.180 -  unfolding fact_altdef
   1.181 -  apply (cases n)
   1.182 -   apply (simp_all add: pochhammer_Suc_setprod)
   1.183 +  apply (auto simp add: pochhammer_def fact_altdef)
   1.184    apply (rule setprod.reindex_cong [where l = Suc])
   1.185 -    apply (auto simp add: fun_eq_iff)
   1.186 +  apply (auto simp add: image_Suc_lessThan)
   1.187    done
   1.188  
   1.189  lemma pochhammer_of_nat_eq_0_lemma:
   1.190    assumes "k > n"
   1.191    shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
   1.192 -proof (cases "n = 0")
   1.193 -  case True
   1.194 -  then show ?thesis
   1.195 -    using assms by (cases k) (simp_all add: pochhammer_rec)
   1.196 -next
   1.197 -  case False
   1.198 -  from assms obtain h where "k = Suc h" by (cases k) auto
   1.199 -  then show ?thesis
   1.200 -    by (simp add: pochhammer_Suc_setprod)
   1.201 -       (metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1))
   1.202 -qed
   1.203 +  using assms by (auto simp add: pochhammer_def)
   1.204  
   1.205  lemma pochhammer_of_nat_eq_0_lemma':
   1.206    assumes kn: "k \<le> n"
   1.207 @@ -589,11 +572,7 @@
   1.208    by (auto simp add: not_le[symmetric])
   1.209  
   1.210  lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
   1.211 -  apply (auto simp add: pochhammer_of_nat_eq_0_iff)
   1.212 -  apply (cases n)
   1.213 -   apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
   1.214 -  apply (metis leD not_less_eq)
   1.215 -  done
   1.216 +  by (auto simp add: pochhammer_def eq_neg_iff_add_eq_0)
   1.217  
   1.218  lemma pochhammer_eq_0_mono:
   1.219    "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
   1.220 @@ -610,8 +589,8 @@
   1.221    then show ?thesis by simp
   1.222  next
   1.223    case (Suc h)
   1.224 -  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i=0..h. - 1)"
   1.225 -    using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
   1.226 +  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i\<le>h. - 1)"
   1.227 +    using setprod_constant[where A="{.. h}" and y="- 1 :: 'a"]
   1.228      by auto
   1.229    show ?thesis
   1.230      unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric]
   1.231 @@ -650,7 +629,7 @@
   1.232  
   1.233  lemma pochhammer_times_pochhammer_half:
   1.234    fixes z :: "'a :: field_char_0"
   1.235 -  shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k=0..2*n+1. z + of_nat k / 2)"
   1.236 +  shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k\<le>2*n+1. z + of_nat k / 2)"
   1.237  proof (induction n)
   1.238    case (Suc n)
   1.239    define n' where "n' = Suc n"
   1.240 @@ -661,7 +640,7 @@
   1.241    also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"
   1.242      (is "_ = ?A") by (simp add: field_simps n'_def)
   1.243    also note Suc[folded n'_def]
   1.244 -  also have "(\<Prod>k = 0..2 * n + 1. z + of_nat k / 2) * ?A = (\<Prod>k = 0..2 * Suc n + 1. z + of_nat k / 2)"
   1.245 +  also have "(\<Prod>k\<le>2 * n + 1. z + of_nat k / 2) * ?A = (\<Prod>k\<le>2 * Suc n + 1. z + of_nat k / 2)"
   1.246      by (simp add: setprod_nat_ivl_Suc)
   1.247    finally show ?case by (simp add: n'_def)
   1.248  qed (simp add: setprod_nat_ivl_Suc)
   1.249 @@ -699,8 +678,12 @@
   1.250  subsection\<open>Generalized binomial coefficients\<close>
   1.251  
   1.252  definition (in field_char_0) gbinomial :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
   1.253 -  where "a gchoose n =
   1.254 -    (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / (fact n))"
   1.255 +where
   1.256 +  "a gchoose n = setprod (\<lambda>i. a - of_nat i) {..<n} / fact n"
   1.257 +
   1.258 +lemma gbinomial_Suc:
   1.259 +  "a gchoose (Suc k) = setprod (\<lambda>i. a - of_nat i) {..k} / fact (Suc k)"
   1.260 +  by (simp add: gbinomial_def lessThan_Suc_atMost)
   1.261  
   1.262  lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
   1.263    by (simp_all add: gbinomial_def)
   1.264 @@ -711,7 +694,7 @@
   1.265    then show ?thesis by simp
   1.266  next
   1.267    case False
   1.268 -  then have eq: "(- 1) ^ n = (\<Prod>i = 0..n - 1. - 1)"
   1.269 +  then have eq: "(- 1) ^ n = (\<Prod>i<n. - 1)"
   1.270      by (auto simp add: setprod_constant)
   1.271    from False show ?thesis
   1.272      by (simp add: pochhammer_def gbinomial_def field_simps
   1.273 @@ -740,9 +723,9 @@
   1.274    { assume kn: "k \<le> n" and k0: "k\<noteq> 0"
   1.275      from k0 obtain h where h: "k = Suc h" by (cases k) auto
   1.276      from h
   1.277 -    have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {0..h}"
   1.278 +    have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {..h}"
   1.279        by (subst setprod_constant) auto
   1.280 -    have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
   1.281 +    have eq': "(\<Prod>i\<le>h. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
   1.282          using h kn
   1.283        by (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
   1.284           (auto simp: of_nat_diff)
   1.285 @@ -770,10 +753,10 @@
   1.286  qed
   1.287  
   1.288  lemma gbinomial_1[simp]: "a gchoose 1 = a"
   1.289 -  by (simp add: gbinomial_def)
   1.290 +  by (simp add: gbinomial_def lessThan_Suc)
   1.291  
   1.292  lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"
   1.293 -  by (simp add: gbinomial_def)
   1.294 +  by (simp add: gbinomial_def lessThan_Suc)
   1.295  
   1.296  lemma gbinomial_mult_1:
   1.297    fixes a :: "'a :: field_char_0"
   1.298 @@ -783,7 +766,7 @@
   1.299    have "?r = ((- 1) ^n * pochhammer (- a) n / (fact n)) * (of_nat n - (- a + of_nat n))"
   1.300      unfolding gbinomial_pochhammer
   1.301        pochhammer_Suc right_diff_distrib power_Suc
   1.302 -    apply (simp del: of_nat_Suc fact.simps)
   1.303 +    apply (simp del: of_nat_Suc fact_Suc)
   1.304      apply (auto simp add: field_simps simp del: of_nat_Suc)
   1.305      done
   1.306    also have "\<dots> = ?l" unfolding gbinomial_pochhammer
   1.307 @@ -796,20 +779,16 @@
   1.308    shows "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
   1.309    by (simp add: mult.commute gbinomial_mult_1)
   1.310  
   1.311 -lemma gbinomial_Suc:
   1.312 -    "a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / (fact (Suc k))"
   1.313 -  by (simp add: gbinomial_def)
   1.314 -
   1.315  lemma gbinomial_mult_fact:
   1.316    fixes a :: "'a::field_char_0"
   1.317    shows
   1.318     "fact (Suc k) * (a gchoose (Suc k)) =
   1.319 -    (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
   1.320 -  by (simp_all add: gbinomial_Suc field_simps del: fact.simps)
   1.321 +    (setprod (\<lambda>i. a - of_nat i) {.. k})"
   1.322 +  by (simp_all add: gbinomial_Suc field_simps del: fact_Suc)
   1.323  
   1.324  lemma gbinomial_mult_fact':
   1.325    fixes a :: "'a::field_char_0"
   1.326 -  shows "(a gchoose (Suc k)) * fact (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
   1.327 +  shows "(a gchoose (Suc k)) * fact (Suc k) = (setprod (\<lambda>i. a - of_nat i) {.. k})"
   1.328    using gbinomial_mult_fact[of k a]
   1.329    by (subst mult.commute)
   1.330  
   1.331 @@ -821,36 +800,37 @@
   1.332    then show ?thesis by simp
   1.333  next
   1.334    case (Suc h)
   1.335 -  have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
   1.336 +  have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{..h}. a - of_nat i)"
   1.337      apply (rule setprod.reindex_cong [where l = Suc])
   1.338        using Suc
   1.339 -      apply auto
   1.340 +      apply (auto simp add: image_Suc_atMost)
   1.341      done
   1.342    have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) =
   1.343          (a gchoose Suc h) * (fact (Suc (Suc h))) +
   1.344          (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
   1.345 -    by (simp add: Suc field_simps del: fact.simps)
   1.346 +    by (simp add: Suc field_simps del: fact_Suc)
   1.347    also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) +
   1.348 -                   (\<Prod>i = 0..Suc h. a - of_nat i)"
   1.349 -    by (metis fact.simps(2) gbinomial_mult_fact' of_nat_fact of_nat_id)
   1.350 +                   (\<Prod>i\<le>Suc h. a - of_nat i)"
   1.351 +    by (metis fact_Suc gbinomial_mult_fact' of_nat_fact of_nat_id)
   1.352    also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) +
   1.353 -                   (\<Prod>i = 0..Suc h. a - of_nat i)"
   1.354 -    by (simp only: fact.simps(2) mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
   1.355 -  also have "... =  of_nat (Suc (Suc h)) * (\<Prod>i = 0..h. a - of_nat i) +
   1.356 -                    (\<Prod>i = 0..Suc h. a - of_nat i)"
   1.357 +                   (\<Prod>i\<le>Suc h. a - of_nat i)"
   1.358 +    by (simp only: fact_Suc mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
   1.359 +  also have "... =  of_nat (Suc (Suc h)) * (\<Prod>i\<le>h. a - of_nat i) +
   1.360 +                    (\<Prod>i\<le>Suc h. a - of_nat i)"
   1.361      by (metis gbinomial_mult_fact mult.commute)
   1.362 -  also have "... = (\<Prod>i = 0..Suc h. a - of_nat i) +
   1.363 -                   (of_nat h * (\<Prod>i = 0..h. a - of_nat i) + 2 * (\<Prod>i = 0..h. a - of_nat i))"
   1.364 +  also have "... = (\<Prod>i\<le>Suc h. a - of_nat i) +
   1.365 +                   (of_nat h * (\<Prod>i\<le>h. a - of_nat i) + 2 * (\<Prod>i\<le>h. a - of_nat i))"
   1.366      by (simp add: field_simps)
   1.367    also have "... =
   1.368 -    ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0::nat..Suc h}. a - of_nat i)"
   1.369 +    ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{..Suc h}. a - of_nat i)"
   1.370      unfolding gbinomial_mult_fact'
   1.371      by (simp add: comm_semiring_class.distrib field_simps Suc)
   1.372 -  also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
   1.373 +  also have "\<dots> = (\<Prod>i\<in>{..h}. a - of_nat i) * (a + 1)"
   1.374      unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
   1.375 +      atMost_Suc
   1.376      by (simp add: field_simps Suc)
   1.377 -  also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
   1.378 -    using eq0
   1.379 +  also have "\<dots> = (\<Prod>i\<in>{..k}. (a + 1) - of_nat i)"
   1.380 +    using eq0 setprod_nat_ivl_1_Suc
   1.381      by (simp add: Suc setprod_nat_ivl_1_Suc)
   1.382    also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
   1.383      unfolding gbinomial_mult_fact ..
   1.384 @@ -1024,12 +1004,12 @@
   1.385  proof (cases b)
   1.386    case (Suc b)
   1.387    hence "((a + 1) gchoose (Suc (Suc b))) =
   1.388 -             (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
   1.389 -    by (simp add: field_simps gbinomial_def)
   1.390 -  also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
   1.391 -    by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
   1.392 +             (\<Prod>i\<le>Suc b. a + (1 - of_nat i)) / fact (b + 2)"
   1.393 +    by (simp add: field_simps gbinomial_def lessThan_Suc_atMost)
   1.394 +  also have "(\<Prod>i\<le>Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i\<le>b. a - of_nat i)"
   1.395 +    by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl atLeast0AtMost)
   1.396    also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
   1.397 -    by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
   1.398 +    by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl lessThan_Suc_atMost)
   1.399    finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
   1.400  qed simp
   1.401  
   1.402 @@ -1038,12 +1018,12 @@
   1.403  proof (cases b)
   1.404    case (Suc b)
   1.405    hence "((a + 1) gchoose (Suc (Suc b))) =
   1.406 -             (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
   1.407 -    by (simp add: field_simps gbinomial_def)
   1.408 -  also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
   1.409 +             (\<Prod>i\<le>Suc b. a + (1 - of_nat i)) / fact (b + 2)"
   1.410 +    by (simp add: field_simps gbinomial_def lessThan_Suc_atMost)
   1.411 +  also have "(\<Prod>i\<le>Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
   1.412      by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
   1.413    also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
   1.414 -    by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
   1.415 +    by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl lessThan_Suc_atMost atLeast0AtMost)
   1.416    finally show ?thesis by (simp add: Suc)
   1.417  qed simp
   1.418  
   1.419 @@ -1379,8 +1359,7 @@
   1.420    apply (case_tac "k = 0")
   1.421    apply auto
   1.422    apply (case_tac "k = Suc n")
   1.423 -  apply auto
   1.424 -  apply (metis Suc_le_eq fact.cases le_Suc_eq le_eq_less_or_eq)
   1.425 +  apply (auto simp add: le_Suc_eq elim: lessE)
   1.426    done
   1.427  
   1.428  lemma card_UNION:
   1.429 @@ -1579,15 +1558,20 @@
   1.430    finally show ?thesis .
   1.431  qed
   1.432  
   1.433 +lemma setprod_lessThan_fold_atLeastAtMost_nat:
   1.434 +  "setprod f {..<Suc n} = fold_atLeastAtMost_nat (times \<circ> f) 0 n 1"
   1.435 +  by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setprod_atLeastAtMost_code comp_def)
   1.436 +
   1.437 +
   1.438  lemma pochhammer_code [code]:
   1.439    "pochhammer a n = (if n = 0 then 1 else
   1.440         fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
   1.441 -  by (simp add: setprod_atLeastAtMost_code pochhammer_def)
   1.442 +  by (cases n) (simp_all add: pochhammer_def setprod_lessThan_fold_atLeastAtMost_nat comp_def)
   1.443  
   1.444  lemma gbinomial_code [code]:
   1.445    "a gchoose n = (if n = 0 then 1 else
   1.446       fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
   1.447 -  by (simp add: setprod_atLeastAtMost_code gbinomial_def)
   1.448 +  by (cases n) (simp_all add: gbinomial_def setprod_lessThan_fold_atLeastAtMost_nat comp_def)
   1.449  
   1.450  (*TODO: This code equation breaks Scala code generation in HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)
   1.451  
     2.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sat Jul 02 15:02:24 2016 +0200
     2.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Jul 02 20:22:25 2016 +0200
     2.3 @@ -3700,7 +3700,7 @@
     2.4  proof -
     2.5    have "?l$n = ?r $ n" for n
     2.6      apply (auto simp add: E_def field_simps power_Suc[symmetric]
     2.7 -      simp del: fact.simps of_nat_Suc power_Suc)
     2.8 +      simp del: fact_Suc of_nat_Suc power_Suc)
     2.9      apply (simp add: of_nat_mult field_simps)
    2.10      done
    2.11    then show ?thesis
    2.12 @@ -4154,7 +4154,7 @@
    2.13          case False
    2.14          with kn have kn': "k < n"
    2.15            by simp
    2.16 -        have m1nk: "?m1 n = setprod (\<lambda>i. - 1) {0..m}" "?m1 k = setprod (\<lambda>i. - 1) {0..h}"
    2.17 +        have m1nk: "?m1 n = setprod (\<lambda>i. - 1) {..m}" "?m1 k = setprod (\<lambda>i. - 1) {0..h}"
    2.18            by (simp_all add: setprod_constant m h)
    2.19          have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0"
    2.20            using bn0 kn
    2.21 @@ -4163,27 +4163,19 @@
    2.22            apply (erule_tac x= "n - ka - 1" in allE)
    2.23            apply (auto simp add: algebra_simps of_nat_diff)
    2.24            done
    2.25 -        have eq1: "setprod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {0 .. h} =
    2.26 +        have eq1: "setprod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {..h} =
    2.27            setprod of_nat {Suc (m - h) .. Suc m}"
    2.28            using kn' h m
    2.29            by (intro setprod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"])
    2.30               (auto simp: of_nat_diff)
    2.31 -
    2.32          have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
    2.33            unfolding m1nk
    2.34 -          unfolding m h pochhammer_Suc_setprod
    2.35 -          apply (simp add: field_simps del: fact_Suc)
    2.36 -          unfolding fact_altdef id_def
    2.37 -          unfolding of_nat_setprod
    2.38 -          unfolding setprod.distrib[symmetric]
    2.39 -          apply auto
    2.40 -          unfolding eq1
    2.41 -          apply (subst setprod.union_disjoint[symmetric])
    2.42 -          apply (auto)
    2.43 -          apply (rule setprod.cong)
    2.44 -          apply auto
    2.45 +          apply (simp add: field_simps m h pochhammer_Suc_setprod del: fact_Suc)
    2.46 +          apply (simp add: fact_altdef id_def atLeast0AtMost setprod.distrib [symmetric] eq1)
    2.47 +          apply (subst setprod.union_disjoint [symmetric])
    2.48 +          apply (auto intro!: setprod.cong)
    2.49            done
    2.50 -        have th20: "?m1 n * ?p b n = setprod (\<lambda>i. b - of_nat i) {0..m}"
    2.51 +        have th20: "?m1 n * ?p b n = setprod (\<lambda>i. b - of_nat i) {..m}"
    2.52            unfolding m1nk
    2.53            unfolding m h pochhammer_Suc_setprod
    2.54            unfolding setprod.distrib[symmetric]
    2.55 @@ -4216,7 +4208,10 @@
    2.56            by (simp add: field_simps)
    2.57          also have "\<dots> = b gchoose (n - k)"
    2.58            unfolding th1 th2
    2.59 -          using kn' by (simp add: gbinomial_def)
    2.60 +          using kn' apply (simp add: gbinomial_def atLeast0AtMost)
    2.61 +            apply (rule setprod.cong)
    2.62 +            apply auto
    2.63 +            done
    2.64          finally show ?thesis by simp
    2.65        qed
    2.66      qed
     3.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sat Jul 02 15:02:24 2016 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sat Jul 02 20:22:25 2016 +0200
     3.3 @@ -5906,7 +5906,7 @@
     3.4  
     3.5  
     3.6  lemma bb: "Suc n choose k = (n choose k) + (if k = 0 then 0 else (n choose (k - 1)))"
     3.7 -  by (simp add: Binomial.binomial.simps)
     3.8 +  by (cases k) simp_all
     3.9  
    3.10  proposition higher_deriv_mult:
    3.11    fixes z::complex
    3.12 @@ -5924,7 +5924,7 @@
    3.13    have sumeq: "(\<Sum>i = 0..n.
    3.14                 of_nat (n choose i) * (deriv ((deriv ^^ i) f) z * (deriv ^^ (n - i)) g z + deriv ((deriv ^^ (n - i)) g) z * (deriv ^^ i) f z)) =
    3.15              g z * deriv ((deriv ^^ n) f) z + (\<Sum>i = 0..n. (deriv ^^ i) f z * (of_nat (Suc n choose i) * (deriv ^^ (Suc n - i)) g z))"
    3.16 -    apply (simp add: bb distrib_right algebra_simps setsum.distrib)
    3.17 +    apply (simp add: bb algebra_simps setsum.distrib)
    3.18      apply (subst (4) setsum_Suc_reindex)
    3.19      apply (auto simp: algebra_simps Suc_diff_le intro: setsum.cong)
    3.20      done
     4.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sat Jul 02 15:02:24 2016 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sat Jul 02 20:22:25 2016 +0200
     4.3 @@ -1106,19 +1106,19 @@
     4.4              ((fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / (fact n) +
     4.5              ((fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / (fact(Suc n))) -
     4.6              ((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))"
     4.7 -          by (simp add: algebra_simps del: fact.simps)
     4.8 +          by (simp add: algebra_simps del: fact_Suc)
     4.9          also have "... = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) +
    4.10                           (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
    4.11                           (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
    4.12 -          by (simp del: fact.simps)
    4.13 +          by (simp del: fact_Suc)
    4.14          also have "... = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
    4.15                           (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
    4.16                           (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
    4.17 -          by (simp only: fact.simps of_nat_mult ac_simps) simp
    4.18 +          by (simp only: fact_Suc of_nat_mult ac_simps) simp
    4.19          also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
    4.20            by (simp add: algebra_simps)
    4.21          finally show ?thesis
    4.22 -        by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact.simps)
    4.23 +        by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact_Suc)
    4.24        qed
    4.25        finally show ?case .
    4.26      qed
     5.1 --- a/src/HOL/Multivariate_Analysis/Gamma.thy	Sat Jul 02 15:02:24 2016 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Sat Jul 02 20:22:25 2016 +0200
     5.3 @@ -512,9 +512,10 @@
     5.4      by (intro setprod.cong[OF refl], subst exp_Ln) (auto simp: field_simps plus_of_nat_eq_0_imp)
     5.5    also have "... = (\<Prod>k=1..n. z + k) / fact n" unfolding fact_altdef
     5.6      by (subst setprod_dividef [symmetric]) (simp_all add: field_simps)
     5.7 -  also from assms have "z * ... = (\<Prod>k=0..n. z + k) / fact n"
     5.8 +  also from assms have "z * ... = (\<Prod>k\<le>n. z + k) / fact n"
     5.9      by (cases n) (simp_all add: setprod_nat_ivl_1_Suc)
    5.10 -  also have "(\<Prod>k=0..n. z + k) = pochhammer z (Suc n)" unfolding pochhammer_def by simp
    5.11 +  also have "(\<Prod>k\<le>n. z + k) = pochhammer z (Suc n)" unfolding pochhammer_def
    5.12 +    by (simp add: lessThan_Suc_atMost)
    5.13    also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n"
    5.14      unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def Ln_of_nat)
    5.15    finally show ?thesis .
    5.16 @@ -999,7 +1000,7 @@
    5.17    hence "z \<noteq> - of_nat n" for n by auto
    5.18    from rGamma_series_aux[OF this] show ?thesis
    5.19      by (simp add: rGamma_series_def[abs_def] fact_altdef pochhammer_Suc_setprod
    5.20 -                  exp_def of_real_def[symmetric] suminf_def sums_def[abs_def])
    5.21 +                  exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost)
    5.22  qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)
    5.23  
    5.24  lemma Gamma_series_LIMSEQ [tendsto_intros]:
    5.25 @@ -1364,7 +1365,7 @@
    5.26              pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
    5.27          in  (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma z"
    5.28      by (simp add: fact_altdef pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
    5.29 -                  of_real_def [symmetric] suminf_def sums_def [abs_def])
    5.30 +                  of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
    5.31  qed
    5.32  
    5.33  end
    5.34 @@ -1497,7 +1498,7 @@
    5.35              pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
    5.36          in  (\<lambda>n. pochhammer' x n / (fact' n * exp (x * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma x"
    5.37      by (simp add: fact_altdef pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
    5.38 -                  of_real_def [symmetric] suminf_def sums_def [abs_def])
    5.39 +                  of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
    5.40  qed
    5.41  
    5.42  end
    5.43 @@ -2424,7 +2425,7 @@
    5.44                          setprod_inversef[symmetric] divide_inverse)
    5.45      also have "(\<Prod>k=1..n. (1 + z / of_nat k)) = pochhammer (z + 1) n / fact n"
    5.46        by (cases n) (simp_all add: pochhammer_def fact_altdef setprod_shift_bounds_cl_Suc_ivl
    5.47 -                                  setprod_dividef[symmetric] divide_simps add_ac)
    5.48 +                                  setprod_dividef[symmetric] divide_simps add_ac atLeast0AtMost lessThan_Suc_atMost)
    5.49      also have "z * \<dots> = pochhammer z (Suc n) / fact n" by (simp add: pochhammer_rec)
    5.50      finally show "?r n = Gamma_series_euler' z n / Gamma_series z n" by simp
    5.51    qed
     6.1 --- a/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy	Sat Jul 02 15:02:24 2016 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy	Sat Jul 02 20:22:25 2016 +0200
     6.3 @@ -27,11 +27,12 @@
     6.4      show "eventually (\<lambda>n. ?f n = (a gchoose n) /(a gchoose Suc n)) sequentially"
     6.5    proof eventually_elim
     6.6      fix n :: nat assume n: "n > 0"
     6.7 -    let ?P = "\<Prod>i = 0..n - 1. a - of_nat i"
     6.8 +    let ?P = "\<Prod>i<n. a - of_nat i"
     6.9      from n have "(a gchoose n) / (a gchoose Suc n) = (of_nat (Suc n) :: 'a) *
    6.10 -                   (?P / (\<Prod>i = 0..n. a - of_nat i))" by (simp add: gbinomial_def)
    6.11 -    also from n have "(\<Prod>i = 0..n. a - of_nat i) = ?P * (a - of_nat n)"
    6.12 -      by (cases n) (simp_all add: setprod_nat_ivl_Suc)
    6.13 +                   (?P / (\<Prod>i\<le>n. a - of_nat i))"
    6.14 +      by (simp add: gbinomial_def lessThan_Suc_atMost)
    6.15 +    also from n have "(\<Prod>i\<le>n. a - of_nat i) = ?P * (a - of_nat n)"
    6.16 +      by (cases n) (simp_all add: setprod_nat_ivl_Suc lessThan_Suc_atMost)
    6.17      also have "?P / \<dots> = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric])
    6.18      also from assms have "?P / ?P = 1" by auto
    6.19      also have "of_nat (Suc n) * (1 / (a - of_nat n)) = 
     7.1 --- a/src/HOL/NthRoot.thy	Sat Jul 02 15:02:24 2016 +0200
     7.2 +++ b/src/HOL/NthRoot.thy	Sat Jul 02 20:22:25 2016 +0200
     7.3 @@ -655,7 +655,7 @@
     7.4      { fix n :: nat assume "2 < n"
     7.5        have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
     7.6          using \<open>2 < n\<close> unfolding gbinomial_def binomial_gbinomial
     7.7 -        by (simp add: atLeast0AtMost atMost_Suc field_simps of_nat_diff numeral_2_eq_2)
     7.8 +        by (simp add: atLeast0AtMost lessThan_Suc field_simps of_nat_diff numeral_2_eq_2)
     7.9        also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
    7.10          by (simp add: x_def)
    7.11        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    7.12 @@ -692,7 +692,8 @@
    7.13             (simp_all add: at_infinity_eq_at_top_bot)
    7.14        { fix n :: nat assume "1 < n"
    7.15          have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
    7.16 -          using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial by simp
    7.17 +          using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial
    7.18 +            by (simp add: lessThan_Suc)
    7.19          also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
    7.20            by (simp add: x_def)
    7.21          also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
     8.1 --- a/src/HOL/Transcendental.thy	Sat Jul 02 15:02:24 2016 +0200
     8.2 +++ b/src/HOL/Transcendental.thy	Sat Jul 02 20:22:25 2016 +0200
     8.3 @@ -1758,7 +1758,7 @@
     8.4        by (rule mult_mono)
     8.5          (rule mult_mono, simp_all add: power_le_one a b)
     8.6      hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
     8.7 -      unfolding power_add by (simp add: ac_simps del: fact.simps) }
     8.8 +      unfolding power_add by (simp add: ac_simps del: fact_Suc) }
     8.9    note aux1 = this
    8.10    have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
    8.11      by (intro sums_mult geometric_sums, simp)
    8.12 @@ -3319,7 +3319,7 @@
    8.13  lemma cos_two_less_zero [simp]:
    8.14    "cos 2 < (0::real)"
    8.15  proof -
    8.16 -  note fact.simps(2) [simp del]
    8.17 +  note fact_Suc [simp del]
    8.18    from sums_minus [OF cos_paired]
    8.19    have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)"
    8.20      by simp
    8.21 @@ -3335,7 +3335,7 @@
    8.22        have "(4::real) * (fact (?six4d)) < (Suc (Suc (?six4d)) * fact (Suc (?six4d)))"
    8.23          unfolding of_nat_mult   by (rule mult_strict_mono) (simp_all add: fact_less_mono)
    8.24        then have "(4::real) * (fact (?six4d)) < (fact (Suc (Suc (?six4d))))"
    8.25 -        by (simp only: fact.simps(2) [of "Suc (?six4d)"] of_nat_mult of_nat_fact)
    8.26 +        by (simp only: fact_Suc [of "Suc (?six4d)"] of_nat_mult of_nat_fact)
    8.27        then have "(4::real) * inverse (fact (Suc (Suc (?six4d)))) < inverse (fact (?six4d))"
    8.28          by (simp add: inverse_eq_divide less_divide_eq)
    8.29      }
     9.1 --- a/src/HOL/ex/Sum_of_Powers.thy	Sat Jul 02 15:02:24 2016 +0200
     9.2 +++ b/src/HOL/ex/Sum_of_Powers.thy	Sat Jul 02 20:22:25 2016 +0200
     9.3 @@ -147,7 +147,7 @@
     9.4  
     9.5  lemma binomial_unroll:
     9.6    "n > 0 \<Longrightarrow> (n choose k) = (if k = 0 then 1 else (n - 1) choose (k - 1) + ((n - 1) choose k))"
     9.7 -by (cases n) (auto simp add: binomial.simps(2))
     9.8 +  by (auto simp add: gr0_conv_Suc)
     9.9  
    9.10  lemma setsum_unroll:
    9.11    "(\<Sum>k\<le>n::nat. f k) = (if n = 0 then f 0 else f n + (\<Sum>k\<le>n - 1. f k))"
    9.12 @@ -157,7 +157,7 @@
    9.13    "n > 0 \<Longrightarrow> bernoulli n = - 1 / (real n + 1) * (\<Sum>k\<le>n - 1. real (n + 1 choose k) * bernoulli k)"
    9.14  by (cases n) (simp add: bernoulli.simps One_nat_def)+
    9.15  
    9.16 -lemmas unroll = binomial.simps(1) binomial_unroll
    9.17 +lemmas unroll = binomial_unroll
    9.18    bernoulli.simps(1) bernoulli_unroll setsum_unroll bernpoly_def
    9.19  
    9.20  lemma sum_of_squares: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6"