# HG changeset patch
# User haftmann
# Date 1468063576 -7200
# Node ID c184ec919c7073ac87186992c3865b32766de25c
# Parent  6af79184bef3dc9cfa15111ca70a0ab73eab4b2b
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
* * *
more rules for setsum, setprod on intervals

diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Binomial.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -14,38 +14,53 @@
 
 subsection \<open>Factorial\<close>
 
-definition (in semiring_char_0) fact :: "nat \<Rightarrow> 'a"
+context semiring_char_0
+begin
+
+definition fact :: "nat \<Rightarrow> 'a"
 where
-  "fact n = of_nat (\<Prod>{1..n})"
+  fact_setprod: "fact n = of_nat (\<Prod>{1..n})"
 
-lemma fact_altdef': "fact n = of_nat (\<Prod>{1..n})"
-  by (fact fact_def)
+lemma fact_setprod_Suc:
+  "fact n = of_nat (setprod Suc {0..<n})"
+  by (cases n) (simp_all add: fact_setprod setprod.atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost)
 
-lemma fact_altdef_nat: "fact n = \<Prod>{1..n}"
-  by (simp add: fact_def)
-
-lemma fact_altdef: "fact n = (\<Prod>i=1..n. of_nat i)"
-  by (simp add: fact_def)
+lemma fact_setprod_rev:
+  "fact n = of_nat (\<Prod>i = 0..<n. n - i)"
+  using setprod.atLeast_atMost_rev [of "\<lambda>i. i" 1 n]
+  by (cases n) (simp_all add: fact_setprod_Suc setprod.atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost)
 
 lemma fact_0 [simp]: "fact 0 = 1"
-  by (simp add: fact_def)
+  by (simp add: fact_setprod)
 
 lemma fact_1 [simp]: "fact 1 = 1"
-  by (simp add: fact_def)
+  by (simp add: fact_setprod)
 
-lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
-  by (simp add: fact_def)
+lemma fact_Suc_0 [simp]: "fact (Suc 0) = 1"
+  by (simp add: fact_setprod)
 
 lemma fact_Suc [simp]: "fact (Suc n) = of_nat (Suc n) * fact n"
-  by (simp add: fact_def atLeastAtMostSuc_conv algebra_simps)
+  by (simp add: fact_setprod atLeastAtMostSuc_conv algebra_simps)
+
+lemma fact_2 [simp]:
+  "fact 2 = 2"
+  by (simp add: numeral_2_eq_2)
+
+lemma fact_split:
+  assumes "k \<le> n"
+  shows "fact n = of_nat (setprod Suc {n - k..<n}) * fact (n - k)"
+  using assms by (simp add: fact_setprod_Suc setprod.union_disjoint [symmetric] ivl_disj_un
+    ac_simps of_nat_mult [symmetric])
+
+end
 
 lemma of_nat_fact [simp]:
   "of_nat (fact n) = fact n"
-  by (simp add: fact_def)
+  by (simp add: fact_setprod)
 
 lemma of_int_fact [simp]:
   "of_int (fact n) = fact n"
-  by (simp only: fact_def of_int_of_nat_eq)
+  by (simp only: fact_setprod of_int_of_nat_eq)
 
 lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
   by (cases n) auto
@@ -149,10 +164,6 @@
     "fact m = (if m=0 then 1 else of_nat m * fact (m - 1))"
 by (cases m) auto
 
-lemma fact_eq_rev_setprod_nat: "fact k = (\<Prod>i<k. k - i)"
-  unfolding fact_altdef_nat
-  by (rule setprod.reindex_bij_witness[where i="\<lambda>i. k - i" and j="\<lambda>i. k - i"]) auto
-
 lemma fact_div_fact_le_pow:
   assumes "r \<le> n" shows "fact n div fact (n - r) \<le> n ^ r"
 proof -
@@ -177,30 +188,30 @@
 
 definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65)
 where
-  "n choose k = card {K\<in>Pow {..<n}. card K = k}"
+  "n choose k = card {K\<in>Pow {0..<n}. card K = k}"
 
 theorem n_subsets:
   assumes "finite A"
   shows "card {B. B \<subseteq> A \<and> card B = k} = card A choose k"
 proof -
-  from assms obtain f where bij: "bij_betw f {..<card A} A"
-    by (blast elim: bij_betw_nat_finite)
-  then have [simp]: "card (f ` C) = card C" if "C \<subseteq> {..<card A}" for C
+  from assms obtain f where bij: "bij_betw f {0..<card A} A"
+    by (blast dest: ex_bij_betw_nat_finite)
+  then have [simp]: "card (f ` C) = card C" if "C \<subseteq> {0..<card A}" for C
     by (meson bij_betw_imp_inj_on bij_betw_subset card_image that)
-  from bij have "bij_betw (image f) (Pow {..<card A}) (Pow A)"
+  from bij have "bij_betw (image f) (Pow {0..<card A}) (Pow A)"
     by (rule bij_betw_Pow)
-  then have "inj_on (image f) (Pow {..<card A})"
+  then have "inj_on (image f) (Pow {0..<card A})"
     by (rule bij_betw_imp_inj_on)
-  moreover have "{K. K \<subseteq> {..<card A} \<and> card K = k} \<subseteq> Pow {..<card A}"
+  moreover have "{K. K \<subseteq> {0..<card A} \<and> card K = k} \<subseteq> Pow {0..<card A}"
     by auto
-  ultimately have "inj_on (image f) {K. K \<subseteq> {..<card A} \<and> card K = k}"
+  ultimately have "inj_on (image f) {K. K \<subseteq> {0..<card A} \<and> card K = k}"
     by (rule inj_on_subset)
-  then have "card {K. K \<subseteq> {..<card A} \<and> card K = k} =
-    card (image f ` {K. K \<subseteq> {..<card A} \<and> card K = k})" (is "_ = card ?C")
+  then have "card {K. K \<subseteq> {0..<card A} \<and> card K = k} =
+    card (image f ` {K. K \<subseteq> {0..<card A} \<and> card K = k})" (is "_ = card ?C")
     by (simp add: card_image)
-  also have "?C = {K. K \<subseteq> f ` {..<card A} \<and> card K = k}"
+  also have "?C = {K. K \<subseteq> f ` {0..<card A} \<and> card K = k}"
     by (auto elim!: subset_imageE)
-  also have "f ` {..<card A} = A"
+  also have "f ` {0..<card A} = A"
     by (meson bij bij_betw_def)
   finally show ?thesis
     by (simp add: binomial_def)
@@ -211,8 +222,8 @@
 lemma binomial_n_0 [simp, code]:
   "n choose 0 = 1"
 proof -
-  have "{K \<in> Pow {..<n}. card K = 0} = {{}}"
-    by (auto dest: subset_eq_range_finite) 
+  have "{K \<in> Pow {0..<n}. card K = 0} = {{}}"
+    by (auto dest: finite_subset)
   then show ?thesis
     by (simp add: binomial_def)
 qed
@@ -224,10 +235,10 @@
 lemma binomial_Suc_Suc [simp, code]:
   "Suc n choose Suc k = (n choose k) + (n choose Suc k)"
 proof -
-  let ?P = "\<lambda>n k. {K. K \<subseteq> {..<n} \<and> card K = k}"
+  let ?P = "\<lambda>n k. {K. K \<subseteq> {0..<n} \<and> card K = k}"
   let ?Q = "?P (Suc n) (Suc k)"
   have inj: "inj_on (insert n) (?P n k)"
-    by rule auto
+    by rule (auto, (metis atLeastLessThan_iff insert_iff less_irrefl subsetCE)+)
   have disjoint: "insert n ` ?P n k \<inter> ?P n (Suc k) = {}"
     by auto
   have "?Q = {K\<in>?Q. n \<in> K} \<union> {K\<in>?Q. n \<notin> K}"
@@ -235,7 +246,7 @@
   also have "{K\<in>?Q. n \<in> K} = insert n ` ?P n k" (is "?A = ?B")
   proof (rule set_eqI)
     fix K
-    have K_finite: "finite K" if "K \<subseteq> insert n {..<n}"
+    have K_finite: "finite K" if "K \<subseteq> insert n {0..<n}"
       using that by (rule finite_subset) simp_all
     have Suc_card_K: "Suc (card K - Suc 0) = card K" if "n \<in> K"
       and "finite K"
@@ -246,17 +257,17 @@
     qed
     show "K \<in> ?A \<longleftrightarrow> K \<in> ?B"
       by (subst in_image_insert_iff)
-        (auto simp add: card_insert subset_eq_range_finite Diff_subset_conv K_finite Suc_card_K)
+        (auto simp add: card_insert subset_eq_atLeast0_lessThan_finite Diff_subset_conv K_finite Suc_card_K)
   qed    
   also have "{K\<in>?Q. n \<notin> K} = ?P n (Suc k)"
-    by (auto simp add: lessThan_Suc)
+    by (auto simp add: atLeast0_lessThan_Suc)
   finally show ?thesis using inj disjoint
     by (simp add: binomial_def card_Un_disjoint card_image)
 qed
 
 lemma binomial_eq_0:
   "n < k \<Longrightarrow> n choose k = 0"
-  by (auto simp add: binomial_def dest: subset_eq_range_card)
+  by (auto simp add: binomial_def dest: subset_eq_atLeast0_lessThan_card)
 
 lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0"
   by (induct n k rule: diff_induct) simp_all
@@ -409,6 +420,29 @@
   apply (simp add: field_simps)
   by (metis mult.commute of_nat_fact of_nat_mult)
 
+lemma fact_binomial:
+  assumes "k \<le> n"
+  shows "fact k * of_nat (n choose k) = (fact n / fact (n - k) :: 'a::field_char_0)"
+  unfolding binomial_fact [OF assms] by (simp add: field_simps)
+
+lemma choose_two:
+  "n choose 2 = n * (n - 1) div 2"
+proof (cases "n \<ge> 2")
+  case False
+  then have "n = 0 \<or> n = 1"
+    by auto
+  then show ?thesis by auto
+next
+  case True
+  define m where "m = n - 2"
+  with True have "n = m + 2"
+    by simp
+  then have "fact n = n * (n - 1) * fact (n - 2)"
+    by (simp add: fact_setprod_Suc atLeast0_lessThan_Suc algebra_simps)
+  with True show ?thesis
+    by (simp add: binomial_fact')
+qed
+
 lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
   using binomial [of 1 "1" n]
   by (simp add: numeral_2_eq_2)
@@ -454,17 +488,13 @@
 lemma choose_row_sum': "(\<Sum>k\<le>n. (n choose k)) = 2 ^ n"
   using choose_row_sum[of n] by (simp add: atLeast0AtMost)
 
-lemma natsum_reverse_index:
-  fixes m::nat
-  shows "(\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)) \<Longrightarrow> (\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
-  by (rule setsum.reindex_bij_witness[where i="\<lambda>k. m+n-k" and j="\<lambda>k. m+n-k"]) auto
-
 text\<open>NW diagonal sum property\<close>
 lemma sum_choose_diagonal:
   assumes "m\<le>n" shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
 proof -
   have "(\<Sum>k=0..m. (n-k) choose (m-k)) = (\<Sum>k=0..m. (n-m+k) choose k)"
-    by (rule natsum_reverse_index) (simp add: assms)
+    using setsum.atLeast_atMost_rev [of "\<lambda>k. (n - k) choose (m - k)" 0 m] assms
+      by simp
   also have "... = Suc (n-m+m) choose m"
     by (rule sum_choose_lower)
   also have "... = Suc n choose m" using assms
@@ -477,86 +507,59 @@
 
 text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close>
 
-definition (in comm_semiring_1) pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
+context comm_semiring_1
+begin
+
+definition pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
 where
-  "pochhammer (a :: 'a) n = setprod (\<lambda>n. a + of_nat n) {..<n}"
+  pochhammer_setprod: "pochhammer a n = setprod (\<lambda>i. a + of_nat i) {0..<n}"
+
+lemma pochhammer_setprod_rev:
+  "pochhammer a n = setprod (\<lambda>i. a + of_nat (n - i)) {1..n}"
+  using setprod.atLeast_lessThan_rev_at_least_Suc_atMost [of "\<lambda>i. a + of_nat i" 0 n]
+  by (simp add: pochhammer_setprod)
 
 lemma pochhammer_Suc_setprod:
-  "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {..n}"
-  by (simp add: pochhammer_def lessThan_Suc_atMost)
- 
+  "pochhammer a (Suc n) = setprod (\<lambda>i. a + of_nat i) {0..n}"
+  by (simp add: pochhammer_setprod atLeastLessThanSuc_atLeastAtMost)
+
+lemma pochhammer_Suc_setprod_rev:
+  "pochhammer a (Suc n) = setprod (\<lambda>i. a + of_nat (n - i)) {0..n}"
+  by (simp add: pochhammer_setprod_rev setprod.atLeast_Suc_atMost_Suc_shift)
+
 lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
-  by (simp add: pochhammer_def)
+  by (simp add: pochhammer_setprod)
  
 lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
-  by (simp add: pochhammer_def lessThan_Suc)
+  by (simp add: pochhammer_setprod lessThan_Suc)
  
 lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
-  by (simp add: pochhammer_def lessThan_Suc)
+  by (simp add: pochhammer_setprod lessThan_Suc)
  
 lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
-  by (simp add: pochhammer_def lessThan_Suc ac_simps)
+  by (simp add: pochhammer_setprod atLeast0_lessThan_Suc ac_simps)
  
+end
+
 lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
-  by (simp add: pochhammer_def)
+  by (simp add: pochhammer_setprod)
 
 lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
-  by (simp add: pochhammer_def)
-
-lemma setprod_nat_ivl_Suc: "setprod f {.. Suc n} = setprod f {..n} * f (Suc n)"
-proof -
-  have "{..Suc n} = {..n} \<union> {Suc n}" by auto
-  then show ?thesis by (simp add: field_simps)
-qed
-
-lemma setprod_nat_ivl_1_Suc: "setprod f {.. Suc n} = f 0 * setprod f {1.. Suc n}"
-proof -
-  have "{..Suc n} = {0} \<union> {1 .. Suc n}" by auto
-  then show ?thesis by simp
-qed
+  by (simp add: pochhammer_setprod)
 
 lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
-proof (cases "n = 0")
-  case True
-  then show ?thesis by (simp add: pochhammer_Suc_setprod)
-next
-  case False
-  have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto
-  have eq: "insert 0 {1 .. n} = {..n}" by auto
-  have **: "(\<Prod>n\<in>{1..n}. a + of_nat n) = (\<Prod>n\<in>{..<n}. a + 1 + of_nat n)"
-    apply (rule setprod.reindex_cong [where l = Suc])
-    using False
-    apply (auto simp add: fun_eq_iff field_simps image_Suc_lessThan)
-    done
-  show ?thesis
-    apply (simp add: pochhammer_def lessThan_Suc_atMost)
-    unfolding setprod.insert [OF *, unfolded eq]
-    using ** apply (simp add: field_simps)
-    done
-qed
+  by (simp add: pochhammer_setprod setprod.atLeast0_lessThan_Suc_shift ac_simps)
 
 lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
-proof (induction n arbitrary: z)
-  case (Suc n z)
-  have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)"
-    by (simp add: pochhammer_rec)
-  also note Suc
-  also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) =
-               (z + of_nat (Suc n)) * pochhammer z (Suc n)"
-    by (simp_all add: pochhammer_rec algebra_simps)
-  finally show ?case .
-qed simp_all
+  by (simp add: pochhammer_setprod setprod.atLeast0_lessThan_Suc ac_simps)
 
 lemma pochhammer_fact: "fact n = pochhammer 1 n"
-  apply (auto simp add: pochhammer_def fact_altdef)
-  apply (rule setprod.reindex_cong [where l = Suc])
-  apply (auto simp add: image_Suc_lessThan)
-  done
+  by (simp add: pochhammer_setprod fact_setprod_Suc)
 
 lemma pochhammer_of_nat_eq_0_lemma:
   assumes "k > n"
   shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
-  using assms by (auto simp add: pochhammer_def)
+  using assms by (auto simp add: pochhammer_setprod)
 
 lemma pochhammer_of_nat_eq_0_lemma':
   assumes kn: "k \<le> n"
@@ -580,7 +583,7 @@
   by (auto simp add: not_le[symmetric])
 
 lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
-  by (auto simp add: pochhammer_def eq_neg_iff_add_eq_0)
+  by (auto simp add: pochhammer_setprod eq_neg_iff_add_eq_0)
 
 lemma pochhammer_eq_0_mono:
   "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
@@ -591,19 +594,18 @@
   unfolding pochhammer_eq_0_iff by auto
 
 lemma pochhammer_minus:
-    "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
+  "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
 proof (cases k)
   case 0
   then show ?thesis by simp
 next
   case (Suc h)
-  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i\<le>h. - 1)"
-    using setprod_constant[where A="{.. h}" and y="- 1 :: 'a"]
+  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i = 0..h. - 1)"
+    using setprod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
     by auto
-  show ?thesis
-    unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric]
-    by (rule setprod.reindex_bij_witness[where i="op - h" and j="op - h"])
-       (auto simp: of_nat_diff)
+  with Suc show ?thesis
+    using pochhammer_Suc_setprod_rev [of "b - of_nat k + 1"]
+    by (auto simp add: pochhammer_Suc_setprod setprod.distrib [symmetric] eq of_nat_diff)
 qed
 
 lemma pochhammer_minus':
@@ -637,7 +639,7 @@
 
 lemma pochhammer_times_pochhammer_half:
   fixes z :: "'a :: field_char_0"
-  shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k\<le>2*n+1. z + of_nat k / 2)"
+  shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k=0..2*n+1. z + of_nat k / 2)"
 proof (induction n)
   case (Suc n)
   define n' where "n' = Suc n"
@@ -648,10 +650,10 @@
   also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"
     (is "_ = ?A") by (simp add: field_simps n'_def)
   also note Suc[folded n'_def]
-  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)"
-    by (simp add: setprod_nat_ivl_Suc)
+  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)"
+    by (simp add: atLeast0_atMost_Suc)
   finally show ?case by (simp add: n'_def)
-qed (simp add: setprod_nat_ivl_Suc)
+qed (simp add: atLeast0_atMost_Suc)
 
 lemma pochhammer_double:
   fixes z :: "'a :: field_char_0"
@@ -687,34 +689,39 @@
 
 definition gbinomial :: "'a :: {semidom_divide, semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
 where
-  "a gchoose n = setprod (\<lambda>i. a - of_nat i) {..<n} div fact n"
+  gbinomial_setprod_rev: "a gchoose n = setprod (\<lambda>i. a - of_nat i) {0..<n} div fact n"
+
+lemma gbinomial_0 [simp]:
+  "a gchoose 0 = 1"
+  "0 gchoose (Suc n) = 0"
+  by (simp_all add: gbinomial_setprod_rev setprod.atLeast0_lessThan_Suc_shift)
 
 lemma gbinomial_Suc:
-  "a gchoose (Suc k) = setprod (\<lambda>i. a - of_nat i) {..k} / fact (Suc k)"
-  by (simp add: gbinomial_def lessThan_Suc_atMost)
+  "a gchoose (Suc k) = setprod (\<lambda>i. a - of_nat i) {0..k} div fact (Suc k)"
+  by (simp add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
 
-lemma gbinomial_0 [simp]:
+lemma gbinomial_mult_fact:
   fixes a :: "'a::field_char_0"
-  shows "a gchoose 0 = 1" "(0::'a) gchoose (Suc n) = 0"
-  by (simp_all add: gbinomial_def)
+  shows
+    "fact n * (a gchoose n) = (\<Prod>i = 0..<n. a - of_nat i)"
+  by (simp_all add: gbinomial_setprod_rev field_simps)
+
+lemma gbinomial_mult_fact':
+  fixes a :: "'a::field_char_0"
+  shows
+    "(a gchoose n) * fact n = (\<Prod>i = 0..<n. a - of_nat i)"
+  using gbinomial_mult_fact [of n a] by (simp add: ac_simps)
 
 lemma gbinomial_pochhammer:
   fixes a :: "'a::field_char_0"
-  shows "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)"
-proof (cases "n = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then have eq: "(- 1) ^ n = (\<Prod>i<n. - 1)"
-    by (auto simp add: setprod_constant)
-  from False show ?thesis
-    by (simp add: pochhammer_def gbinomial_def field_simps
-      eq setprod.distrib[symmetric])
-qed
+  shows "a gchoose n = (- 1) ^ n * pochhammer (- a) n / fact n"
+  by (cases n)
+    (simp_all add: pochhammer_minus, simp_all add: gbinomial_setprod_rev pochhammer_setprod_rev
+      power_mult_distrib [symmetric] atLeastLessThanSuc_atLeastAtMost setprod.atLeast_Suc_atMost_Suc_shift of_nat_diff)
 
 lemma gbinomial_pochhammer':
-  "(s :: 'a :: field_char_0) gchoose n = pochhammer (s - of_nat n + 1) n / fact n"
+  fixes s :: "'a::field_char_0"
+  shows "s gchoose n = pochhammer (s - of_nat n + 1) n / fact n"
 proof -
   have "s gchoose n = ((-1)^n * (-1)^n) * pochhammer (s - of_nat n + 1) n / fact n"
     by (simp add: gbinomial_pochhammer pochhammer_minus mult_ac)
@@ -727,76 +734,66 @@
 proof (cases "k \<le> n")
   case False
   then have "n < k" by (simp add: not_le)
-  then have "0 \<in> (op - n) ` {..<k}"
+  then have "0 \<in> (op - n) ` {0..<k}"
     by auto
-  then have "setprod (op - n) {..<k} = 0"
+  then have "setprod (op - n) {0..<k} = 0"
     by (auto intro: setprod_zero)
   with \<open>n < k\<close> show ?thesis
-    by (simp add: binomial_eq_0 gbinomial_def setprod_zero)
+    by (simp add: binomial_eq_0 gbinomial_setprod_rev setprod_zero)
 next
   case True
-  then have "inj_on (op - n) {..<k}"
+  then have "inj_on (op - n) {0..<k}"
     by (auto intro: inj_onI)
-  then have "\<Prod>(op - n ` {..<k}) = setprod (op - n) {..<k}"
+  then have "\<Prod>(op - n ` {0..<k}) = setprod (op - n) {0..<k}"
     by (auto dest: setprod.reindex)
-  also have "op - n ` {..<k} = {Suc (n - k)..n}"
+  also have "op - n ` {0..<k} = {Suc (n - k)..n}"
     using True by (auto simp add: image_def Bex_def) arith
-  finally have *: "setprod (\<lambda>q. n - q) {..<k} = \<Prod>{Suc (n - k)..n}" ..
+  finally have *: "setprod (\<lambda>q. n - q) {0..<k} = \<Prod>{Suc (n - k)..n}" ..
   from True have "(n choose k) = fact n div (fact k * fact (n - k))"
     by (rule binomial_fact')
   with * show ?thesis
-    by (simp add: gbinomial_def mult.commute [of "fact k"] div_mult2_eq fact_div_fact)
+    by (simp add: gbinomial_setprod_rev mult.commute [of "fact k"] div_mult2_eq fact_div_fact)
+qed
+
+lemma of_nat_gbinomial:
+  "of_nat (n gchoose k) = (of_nat n gchoose k :: 'a::field_char_0)"
+proof (cases "k \<le> n")
+  case False then show ?thesis
+    by (simp add: not_le gbinomial_binomial binomial_eq_0 gbinomial_setprod_rev)
+next
+  case True 
+  moreover define m where "m = n - k"
+  ultimately have n: "n = m + k"
+    by arith
+  from n have "fact n = ((\<Prod>i = 0..<m + k. of_nat (m + k - i) ):: 'a)"
+    by (simp add: fact_setprod_rev)
+  also have "\<dots> = ((\<Prod>i\<in>{0..<k} \<union> {k..<m + k}. of_nat (m + k - i)) :: 'a)"
+    by (simp add: ivl_disj_un)
+  finally have 
+    "fact n = (fact m * (\<Prod>i = 0..<k. of_nat m + of_nat k - of_nat i) :: 'a)"
+    using setprod_shift_bounds_nat_ivl [of "\<lambda>i. of_nat (m + k - i) :: 'a" 0 k m]
+    by (simp add: fact_setprod_rev [of m] setprod.union_disjoint of_nat_diff)
+  then have "fact n / fact (n - k) =
+    ((\<Prod>i = 0..<k. of_nat n - of_nat i) :: 'a)"
+    by (simp add: n)
+  with True have "fact k * of_nat (n gchoose k) = (fact k * (of_nat n gchoose k) :: 'a)"
+    by (simp only: gbinomial_mult_fact [of k "of_nat n"]
+      gbinomial_binomial [of n k]
+      fact_binomial)
+  then show ?thesis by simp
 qed
 
 lemma binomial_gbinomial:
-    "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
-proof -
-  { assume kn: "k > n"
-    then have ?thesis
-      by (subst binomial_eq_0[OF kn])
-         (simp add: gbinomial_pochhammer field_simps  pochhammer_of_nat_eq_0_iff) }
-  moreover
-  { assume "k=0" then have ?thesis by simp }
-  moreover
-  { assume kn: "k \<le> n" and k0: "k\<noteq> 0"
-    from k0 obtain h where h: "k = Suc h" by (cases k) auto
-    from h
-    have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {..h}"
-      by (subst setprod_constant) auto
-    have eq': "(\<Prod>i\<le>h. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
-        using h kn
-      by (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
-         (auto simp: of_nat_diff)
-    have th0: "finite {1..n - Suc h}" "finite {n - h .. n}"
-        "{1..n - Suc h} \<inter> {n - h .. n} = {}" and
-        eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}"
-      using h kn by auto
-    from eq[symmetric]
-    have ?thesis using kn
-      apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
-        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
-      apply (simp add: pochhammer_Suc_setprod fact_altdef h
-        setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)
-      unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
-      unfolding mult.assoc
-      unfolding setprod.distrib[symmetric]
-      apply simp
-      apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
-      apply (auto simp: of_nat_diff)
-      done
-  }
-  moreover
-  have "k > n \<or> k = 0 \<or> (k \<le> n \<and> k \<noteq> 0)" by arith
-  ultimately show ?thesis by blast
-qed
+  "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
+  by (simp add: gbinomial_binomial [symmetric] of_nat_gbinomial)
 
 setup \<open>Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a"})\<close>
 
 lemma gbinomial_1[simp]: "a gchoose 1 = a"
-  by (simp add: gbinomial_def lessThan_Suc)
+  by (simp add: gbinomial_setprod_rev lessThan_Suc)
 
 lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"
-  by (simp add: gbinomial_def lessThan_Suc)
+  by (simp add: gbinomial_setprod_rev lessThan_Suc)
 
 lemma gbinomial_mult_1:
   fixes a :: "'a :: field_char_0"
@@ -819,19 +816,6 @@
   shows "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
   by (simp add: mult.commute gbinomial_mult_1)
 
-lemma gbinomial_mult_fact:
-  fixes a :: "'a::field_char_0"
-  shows
-   "fact (Suc k) * (a gchoose (Suc k)) =
-    (setprod (\<lambda>i. a - of_nat i) {.. k})"
-  by (simp_all add: gbinomial_Suc field_simps del: fact_Suc)
-
-lemma gbinomial_mult_fact':
-  fixes a :: "'a::field_char_0"
-  shows "(a gchoose (Suc k)) * fact (Suc k) = (setprod (\<lambda>i. a - of_nat i) {.. k})"
-  using gbinomial_mult_fact[of k a]
-  by (subst mult.commute)
-
 lemma gbinomial_Suc_Suc:
   fixes a :: "'a :: field_char_0"
   shows "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
@@ -840,7 +824,7 @@
   then show ?thesis by simp
 next
   case (Suc h)
-  have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{..h}. a - of_nat i)"
+  have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
     apply (rule setprod.reindex_cong [where l = Suc])
       using Suc
       apply (auto simp add: image_Suc_atMost)
@@ -850,32 +834,33 @@
         (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
     by (simp add: Suc field_simps del: fact_Suc)
   also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) +
-                   (\<Prod>i\<le>Suc h. a - of_nat i)"
-    by (metis fact_Suc gbinomial_mult_fact' of_nat_fact of_nat_id)
+                   (\<Prod>i=0..Suc h. a - of_nat i)"
+    apply (simp del: fact_Suc add: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"])
+    apply (simp del: fact_Suc add: fact_Suc [of "Suc h"] field_simps gbinomial_mult_fact mult.left_commute [of _ "2"] atLeastLessThanSuc_atLeastAtMost)
+    done
   also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) +
-                   (\<Prod>i\<le>Suc h. a - of_nat i)"
+                   (\<Prod>i=0..Suc h. a - of_nat i)"
     by (simp only: fact_Suc mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
-  also have "... =  of_nat (Suc (Suc h)) * (\<Prod>i\<le>h. a - of_nat i) +
-                    (\<Prod>i\<le>Suc h. a - of_nat i)"
-    by (metis gbinomial_mult_fact mult.commute)
-  also have "... = (\<Prod>i\<le>Suc h. a - of_nat i) +
-                   (of_nat h * (\<Prod>i\<le>h. a - of_nat i) + 2 * (\<Prod>i\<le>h. a - of_nat i))"
+  also have "... =  of_nat (Suc (Suc h)) * (\<Prod>i=0..h. a - of_nat i) +
+                    (\<Prod>i=0..Suc h. a - of_nat i)"
+    unfolding gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost by auto
+  also have "... = (\<Prod>i=0..Suc h. a - of_nat i) +
+                   (of_nat h * (\<Prod>i=0..h. a - of_nat i) + 2 * (\<Prod>i=0..h. a - of_nat i))"
     by (simp add: field_simps)
   also have "... =
-    ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{..Suc h}. a - of_nat i)"
+    ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0..Suc h}. a - of_nat i)"
     unfolding gbinomial_mult_fact'
-    by (simp add: comm_semiring_class.distrib field_simps Suc)
-  also have "\<dots> = (\<Prod>i\<in>{..h}. a - of_nat i) * (a + 1)"
-    unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
-      atMost_Suc
-    by (simp add: field_simps Suc)
-  also have "\<dots> = (\<Prod>i\<in>{..k}. (a + 1) - of_nat i)"
-    using eq0 setprod_nat_ivl_1_Suc
-    by (simp add: Suc setprod_nat_ivl_1_Suc)
+    by (simp add: comm_semiring_class.distrib field_simps Suc atLeastLessThanSuc_atLeastAtMost)
+  also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
+    unfolding gbinomial_mult_fact' atLeast0_atMost_Suc
+    by (simp add: field_simps Suc atLeastLessThanSuc_atLeastAtMost)
+  also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
+    using eq0
+    by (simp add: Suc setprod.atLeast0_atMost_Suc_shift)
   also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
-    unfolding gbinomial_mult_fact ..
+    unfolding gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost ..
   finally show ?thesis
-    by (metis fact_nonzero mult_cancel_left)
+    using fact_nonzero [of "Suc k"] by auto
 qed
 
 lemma gbinomial_reduce_nat:
@@ -992,17 +977,9 @@
   Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"}\<close>
 lemma gbinomial_altdef_of_nat:
   fixes k :: nat
-    and x :: "'a :: {field_char_0,field}"
-  shows "x gchoose k = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
-proof -
-  have "(x gchoose k) = (\<Prod>i<k. x - of_nat i) / of_nat (fact k)"
-    unfolding gbinomial_def
-    by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost)
-  also have "\<dots> = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
-    unfolding fact_eq_rev_setprod_nat of_nat_setprod
-    by (auto simp add: setprod_dividef intro!: setprod.cong of_nat_diff[symmetric])
-  finally show ?thesis .
-qed
+    and x :: "'a :: field_char_0"
+  shows "x gchoose k = (\<Prod>i = 0..<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
+  by (simp add: setprod_dividef gbinomial_setprod_rev fact_setprod_rev)
 
 lemma gbinomial_ge_n_over_k_pow_k:
   fixes k :: nat
@@ -1012,11 +989,11 @@
 proof -
   have x: "0 \<le> x"
     using assms of_nat_0_le_iff order_trans by blast
-  have "(x / of_nat k :: 'a) ^ k = (\<Prod>i<k. x / of_nat k :: 'a)"
+  have "(x / of_nat k :: 'a) ^ k = (\<Prod>i = 0..<k. x / of_nat k :: 'a)"
     by (simp add: setprod_constant)
   also have "\<dots> \<le> x gchoose k"
     unfolding gbinomial_altdef_of_nat
-  proof (safe intro!: setprod_mono)
+  proof (safe intro!: setprod_mono, simp_all) -- \<open>FIXME\<close>
     fix i :: nat
     assume ik: "i < k"
     from assms have "x * of_nat i \<ge> of_nat (i * k)"
@@ -1044,12 +1021,12 @@
 proof (cases b)
   case (Suc b)
   hence "((a + 1) gchoose (Suc (Suc b))) =
-             (\<Prod>i\<le>Suc b. a + (1 - of_nat i)) / fact (b + 2)"
-    by (simp add: field_simps gbinomial_def lessThan_Suc_atMost)
-  also have "(\<Prod>i\<le>Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i\<le>b. a - of_nat i)"
-    by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl atLeast0AtMost)
+             (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
+    by (simp add: field_simps gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+  also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
+    by (simp add: setprod.atLeast0_atMost_Suc_shift)
   also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
-    by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl lessThan_Suc_atMost)
+    by (simp_all add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
   finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
 qed simp
 
@@ -1058,12 +1035,12 @@
 proof (cases b)
   case (Suc b)
   hence "((a + 1) gchoose (Suc (Suc b))) =
-             (\<Prod>i\<le>Suc b. a + (1 - of_nat i)) / fact (b + 2)"
-    by (simp add: field_simps gbinomial_def lessThan_Suc_atMost)
-  also have "(\<Prod>i\<le>Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
-    by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+             (\<Prod>i = 0 .. Suc b. a + (1 - of_nat i)) / fact (b + 2)"
+    by (simp add: field_simps gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+  also have "(\<Prod>i = 0 .. Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
+    by (simp add: setprod.atLeast0_atMost_Suc_shift)
   also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
-    by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl lessThan_Suc_atMost atLeast0AtMost)
+    by (simp_all add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
   finally show ?thesis by (simp add: Suc)
 qed simp
 
@@ -1256,10 +1233,6 @@
   apply (simp add: power_mult_distrib [symmetric])
   done
 
-lemma setsum_nat_symmetry:
-  "(\<Sum>k = 0..(m::nat). f k) = (\<Sum>k = 0..m. f (m - k))"
-  by (rule setsum.reindex_bij_witness[where i="\<lambda>i. m - i" and j="\<lambda>i. m - i"]) auto
-
 lemma binomial_r_part_sum: "(\<Sum>k\<le>m. (2 * m + 1 choose k)) = 2 ^ (2 * m)"
 proof -
   have "2 * 2^(2*m) = (\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k))"
@@ -1273,7 +1246,8 @@
   also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose (m - k)))"
     by (intro setsum.cong[OF refl], subst binomial_symmetric) simp_all
   also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose k))"
-    by (subst (2) setsum_nat_symmetry) (rule refl)
+    using setsum.atLeast_atMost_rev [of "\<lambda>k. 2 * m + 1 choose (m - k)" 0 m]
+    by simp
   also have "\<dots> + \<dots> = 2 * \<dots>" by simp
   finally show ?thesis by (subst (asm) mult_cancel1) (simp add: atLeast0AtMost)
 qed
@@ -1316,11 +1290,10 @@
 text\<open>Versions of the theorems above for the natural-number version of "choose"\<close>
 lemma binomial_altdef_of_nat:
   fixes n k :: nat
-    and x :: "'a :: {field_char_0,field}"  \<comment>\<open>the point is to constrain @{typ 'a}\<close>
+    and x :: "'a :: field_char_0"
   assumes "k \<le> n"
-  shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
-using assms
-by (simp add: gbinomial_altdef_of_nat binomial_gbinomial of_nat_diff)
+  shows "of_nat (n choose k) = (\<Prod>i = 0..<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
+  using assms by (simp add: gbinomial_altdef_of_nat binomial_gbinomial of_nat_diff)
 
 lemma binomial_ge_n_over_k_pow_k:
   fixes k n :: nat
@@ -1593,7 +1566,8 @@
 lemma fact_code [code]:
   "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a :: semiring_char_0)"
 proof -
-  have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)" by (simp add: fact_altdef')
+  have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
+    by (simp add: fact_setprod)
   also have "\<Prod>{1..n} = \<Prod>{2..n}"
     by (intro setprod.mono_neutral_right) auto
   also have "\<dots> = fold_atLeastAtMost_nat (op *) 2 n 1"
@@ -1601,19 +1575,15 @@
   finally show ?thesis .
 qed
 
-lemma setprod_lessThan_fold_atLeastAtMost_nat:
-  "setprod f {..<Suc n} = fold_atLeastAtMost_nat (times \<circ> f) 0 n 1"
-  by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setprod_atLeastAtMost_code comp_def)
-
 lemma pochhammer_code [code]:
   "pochhammer a n = (if n = 0 then 1 else
-       fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
-  by (cases n) (simp_all add: pochhammer_def setprod_lessThan_fold_atLeastAtMost_nat comp_def)
+     fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
+  by (cases n) (simp_all add: pochhammer_setprod setprod_atLeastAtMost_code [symmetric] atLeastLessThanSuc_atLeastAtMost)
 
 lemma gbinomial_code [code]:
   "a gchoose n = (if n = 0 then 1 else
      fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
-  by (cases n) (simp_all add: gbinomial_def setprod_lessThan_fold_atLeastAtMost_nat comp_def)
+  by (cases n) (simp_all add: gbinomial_setprod_rev setprod_atLeastAtMost_code [symmetric] atLeastLessThanSuc_atLeastAtMost)
 
 (*TODO: This code equation breaks Scala code generation in HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)
 
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -4027,7 +4027,7 @@
 qed
 
 lemma setprod_fact: "real (\<Prod> {1..<1 + k}) = fact (k :: nat)"
-by (metis Suc_eq_plus1_left atLeastLessThanSuc_atLeastAtMost fact_altdef_nat of_nat_fact)
+  by (simp add: fact_setprod atLeastLessThanSuc_atLeastAtMost)
 
 lemma approx_tse:
   assumes "bounded_by xs vs"
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Divides.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -1432,6 +1432,15 @@
   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
   done
 
+lemma (in field_char_0) of_nat_div:
+  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
+proof -
+  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
+    unfolding of_nat_add by (cases "n = 0") simp_all
+  then show ?thesis
+    by simp
+qed
+
 
 subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
 
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -1711,7 +1711,7 @@
 
 lemma fps_deriv_maclauren_0:
   "(fps_nth_deriv k (f :: 'a::comm_semiring_1 fps)) $ 0 = of_nat (fact k) * f $ k"
-  by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult)
+  by (induct k arbitrary: f) (auto simp add: field_simps)
 
 
 subsection \<open>Powers\<close>
@@ -3701,7 +3701,7 @@
   have "?l$n = ?r $ n" for n
     apply (auto simp add: E_def field_simps power_Suc[symmetric]
       simp del: fact_Suc of_nat_Suc power_Suc)
-    apply (simp add: of_nat_mult field_simps)
+    apply (simp add: field_simps)
     done
   then show ?thesis
     by (simp add: fps_eq_iff)
@@ -4110,6 +4110,7 @@
       (is ?pochhammer)
     if kn: "k \<in> {0..n}" for k
   proof -
+    from kn have "k \<le> n" by simp
     have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0"
     proof
       assume "pochhammer (1 + b - of_nat n) n = 0"
@@ -4169,32 +4170,25 @@
           by (intro setprod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"])
              (auto simp: of_nat_diff)
         have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
-          unfolding m1nk
-          apply (simp add: field_simps m h pochhammer_Suc_setprod del: fact_Suc)
-          apply (simp add: fact_altdef id_def atLeast0AtMost setprod.distrib [symmetric] eq1)
-          apply (subst setprod.union_disjoint [symmetric])
-          apply (auto intro!: setprod.cong)
+          apply (simp add: pochhammer_minus field_simps)
+          using \<open>k \<le> n\<close> apply (simp add: fact_split [of k n])
+          apply (simp add: pochhammer_setprod)
+          using setprod.atLeast_lessThan_shift_bounds [where ?'a = 'a, of "\<lambda>i. 1 + of_nat i" 0 "n - k" k]
+          apply (auto simp add: of_nat_diff field_simps)
           done
-        have th20: "?m1 n * ?p b n = setprod (\<lambda>i. b - of_nat i) {..m}"
-          unfolding m1nk
-          unfolding m h pochhammer_Suc_setprod
-          unfolding setprod.distrib[symmetric]
-          apply (rule setprod.cong)
-          apply auto
+        have th20: "?m1 n * ?p b n = setprod (\<lambda>i. b - of_nat i) {0..m}"
+          apply (simp add: pochhammer_minus field_simps m)
+          apply (auto simp add: pochhammer_setprod_rev of_nat_diff setprod.atLeast_Suc_atMost_Suc_shift)
           done
         have th21:"pochhammer (b - of_nat n + 1) k = setprod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
-          unfolding h m
-          unfolding pochhammer_Suc_setprod
-          using kn m h
-          by (intro setprod.reindex_bij_witness[where i="\<lambda>k. n - 1 - k" and j="\<lambda>i. m-i"])
-             (auto simp: of_nat_diff)
-
+          using kn apply (simp add: pochhammer_setprod_rev m h setprod.atLeast_Suc_atMost_Suc_shift)
+          using setprod.atLeast_atMost_shift_0 [of "m - h" m, where ?'a = 'a]
+          apply (auto simp add: of_nat_diff field_simps)
+          done
         have "?m1 n * ?p b n =
-          pochhammer (b - of_nat n + 1) k * setprod (\<lambda>i. b - of_nat i) {0.. n - k - 1}"
-          unfolding th20 th21
-          unfolding h m
-          apply (subst setprod.union_disjoint[symmetric])
-          using kn' h m
+          setprod (\<lambda>i. b - of_nat i) {0.. n - k - 1} * pochhammer (b - of_nat n + 1) k"
+          using kn' m h unfolding th20 th21 apply simp
+          apply (subst setprod.union_disjoint [symmetric])
           apply auto
           apply (rule setprod.cong)
           apply auto
@@ -4208,10 +4202,11 @@
           by (simp add: field_simps)
         also have "\<dots> = b gchoose (n - k)"
           unfolding th1 th2
-          using kn' apply (simp add: gbinomial_def atLeast0AtMost)
-            apply (rule setprod.cong)
-            apply auto
-            done
+          using kn' m h
+          apply (simp add: field_simps gbinomial_mult_fact)
+          apply (rule setprod.cong)
+          apply auto
+          done
         finally show ?thesis by simp
       qed
     qed
@@ -4230,10 +4225,6 @@
     unfolding gbinomial_pochhammer
     using bn0
     apply (simp add: setsum_left_distrib setsum_right_distrib field_simps)
-    apply (rule setsum.cong)
-    apply (rule refl)
-    apply (drule th00(2))
-    apply (simp add: field_simps power_add[symmetric])
     done
   finally show ?thesis by simp
 qed
@@ -4355,7 +4346,7 @@
   apply (cases n)
   apply simp
   apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc)
-  apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
+  apply simp
   done
 
 lemma fps_cos_nth_0 [simp]: "fps_cos c $ 0 = 1"
@@ -4368,7 +4359,7 @@
   "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat (n + 1) * of_nat (n + 2)))"
   unfolding fps_cos_def
   apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc)
-  apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
+  apply simp
   done
 
 lemma nat_induct2: "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P (n::nat)"
@@ -4593,7 +4584,7 @@
   apply (simp del: of_nat_Suc of_nat_add fact_Suc)
   apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc)
   unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc
-  apply (simp add: algebra_simps of_nat_mult)
+  apply (simp add: algebra_simps)
   done
 
 lemma XD_nth[simp]: "XD a $ n = (if n = 0 then 0 else of_nat n * a$n)"
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Multivariate_Analysis/Gamma.thy
--- a/src/HOL/Multivariate_Analysis/Gamma.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -504,18 +504,21 @@
   assumes "n > 0" "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "exp (ln_Gamma_series z n :: complex) = Gamma_series z n"
 proof -
+  from assms obtain m where m: "n = Suc m" by (cases n) blast
   from assms have "z \<noteq> 0" by (intro notI) auto
   with assms have "exp (ln_Gamma_series z n) =
           (of_nat n) powr z / (z * (\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))))"
     unfolding ln_Gamma_series_def powr_def by (simp add: exp_diff exp_setsum)
   also from assms have "(\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))) = (\<Prod>k=1..n. z / of_nat k + 1)"
     by (intro setprod.cong[OF refl], subst exp_Ln) (auto simp: field_simps plus_of_nat_eq_0_imp)
-  also have "... = (\<Prod>k=1..n. z + k) / fact n" unfolding fact_altdef
-    by (subst setprod_dividef [symmetric]) (simp_all add: field_simps)
-  also from assms have "z * ... = (\<Prod>k\<le>n. z + k) / fact n"
-    by (cases n) (simp_all add: setprod_nat_ivl_1_Suc)
-  also have "(\<Prod>k\<le>n. z + k) = pochhammer z (Suc n)" unfolding pochhammer_def
-    by (simp add: lessThan_Suc_atMost)
+  also have "... = (\<Prod>k=1..n. z + k) / fact n"
+    by (simp add: fact_setprod)
+    (subst setprod_dividef [symmetric], simp_all add: field_simps)
+  also from m have "z * ... = (\<Prod>k=0..n. z + k) / fact n"
+    by (simp add: setprod.atLeast0_atMost_Suc_shift setprod.atLeast_Suc_atMost_Suc_shift)
+  also have "(\<Prod>k=0..n. z + k) = pochhammer z (Suc n)"
+    unfolding pochhammer_setprod
+    by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
   also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n"
     unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def Ln_of_nat)
   finally show ?thesis .
@@ -999,7 +1002,7 @@
   case False
   hence "z \<noteq> - of_nat n" for n by auto
   from rGamma_series_aux[OF this] show ?thesis
-    by (simp add: rGamma_series_def[abs_def] fact_altdef pochhammer_Suc_setprod
+    by (simp add: rGamma_series_def[abs_def] fact_setprod pochhammer_Suc_setprod
                   exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost)
 qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)
 
@@ -1149,7 +1152,7 @@
   apply (rule has_field_derivative_at_within)
   using differentiable_rGamma_aux2[of n]
   unfolding Let_def has_field_derivative_def has_derivative_def netlimit_at
-  by (simp only: bounded_linear_mult_right mult_ac of_real_def [symmetric] fact_altdef)
+  by (simp only: bounded_linear_mult_right mult_ac of_real_def [symmetric] fact_setprod) simp
 
 lemma has_field_derivative_rGamma [derivative_intros]:
   "(rGamma has_field_derivative (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>norm z\<rfloor>) * fact (nat \<lfloor>norm z\<rfloor>)
@@ -1355,7 +1358,7 @@
   from has_field_derivative_rGamma_complex_nonpos_Int[of n]
   show "let z = - of_nat n in (\<lambda>y. (rGamma y - rGamma z - (- 1) ^ n * setprod of_nat {1..n} *
                   (y - z)) /\<^sub>R cmod (y - z)) \<midarrow>z\<rightarrow> 0"
-    by (simp add: has_field_derivative_def has_derivative_def fact_altdef netlimit_at Let_def)
+    by (simp add: has_field_derivative_def has_derivative_def fact_setprod netlimit_at Let_def)
 next
   fix z :: complex
   from rGamma_series_complex_converges[of z] have "rGamma_series z \<longlonglongrightarrow> rGamma z"
@@ -1364,7 +1367,7 @@
             exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e;
             pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
         in  (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma z"
-    by (simp add: fact_altdef pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
+    by (simp add: fact_setprod pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
                   of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
 qed
 
@@ -1485,7 +1488,7 @@
                   simp: Polygamma_of_real rGamma_real_def [abs_def])
   thus "let x = - of_nat n in (\<lambda>y. (rGamma y - rGamma x - (- 1) ^ n * setprod of_nat {1..n} *
                   (y - x)) /\<^sub>R norm (y - x)) \<midarrow>x::real\<rightarrow> 0"
-    by (simp add: has_field_derivative_def has_derivative_def fact_altdef netlimit_at Let_def)
+    by (simp add: has_field_derivative_def has_derivative_def fact_setprod netlimit_at Let_def)
 next
   fix x :: real
   have "rGamma_series x \<longlonglongrightarrow> rGamma x"
@@ -1497,7 +1500,7 @@
             exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e;
             pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
         in  (\<lambda>n. pochhammer' x n / (fact' n * exp (x * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma x"
-    by (simp add: fact_altdef pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
+    by (simp add: fact_setprod pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
                   of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
 qed
 
@@ -2424,8 +2427,8 @@
          (simp_all add: Gamma_series_euler'_def setprod.distrib
                         setprod_inversef[symmetric] divide_inverse)
     also have "(\<Prod>k=1..n. (1 + z / of_nat k)) = pochhammer (z + 1) n / fact n"
-      by (cases n) (simp_all add: pochhammer_def fact_altdef setprod_shift_bounds_cl_Suc_ivl
-                                  setprod_dividef[symmetric] divide_simps add_ac atLeast0AtMost lessThan_Suc_atMost)
+      by (cases n) (simp_all add: pochhammer_setprod fact_setprod atLeastLessThanSuc_atLeastAtMost
+        setprod_dividef [symmetric] field_simps setprod.atLeast_Suc_atMost_Suc_shift)
     also have "z * \<dots> = pochhammer z (Suc n) / fact n" by (simp add: pochhammer_rec)
     finally show "?r n = Gamma_series_euler' z n / Gamma_series z n" by simp
   qed
@@ -2679,7 +2682,7 @@
         using Suc.IH[of "z+1"] Suc.prems by (intro has_integral_mult_left) (simp_all add: add_ac pochhammer_rec)
       also have "?A = (\<lambda>t. ?f t * ?g' t)" by (intro ext) (simp_all add: field_simps)
       also have "?B = - (of_nat (Suc n) * fact n / pochhammer z (n+2))"
-        by (simp add: divide_simps setprod_nat_ivl_1_Suc pochhammer_rec
+        by (simp add: divide_simps pochhammer_rec
               setprod_shift_bounds_cl_Suc_ivl del: of_nat_Suc)
       finally show "((\<lambda>t. ?f t * ?g' t) has_integral (?f 1 * ?g 1 - ?f 0 * ?g 0 - ?I)) {0..1}"
         by simp
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy
--- a/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -27,12 +27,13 @@
     show "eventually (\<lambda>n. ?f n = (a gchoose n) /(a gchoose Suc n)) sequentially"
   proof eventually_elim
     fix n :: nat assume n: "n > 0"
-    let ?P = "\<Prod>i<n. a - of_nat i"
+    then obtain q where q: "n = Suc q" by (cases n) blast
+    let ?P = "\<Prod>i=0..<n. a - of_nat i"
     from n have "(a gchoose n) / (a gchoose Suc n) = (of_nat (Suc n) :: 'a) *
-                   (?P / (\<Prod>i\<le>n. a - of_nat i))"
-      by (simp add: gbinomial_def lessThan_Suc_atMost)
-    also from n have "(\<Prod>i\<le>n. a - of_nat i) = ?P * (a - of_nat n)"
-      by (cases n) (simp_all add: setprod_nat_ivl_Suc lessThan_Suc_atMost)
+                   (?P / (\<Prod>i=0..n. a - of_nat i))"
+      by (simp add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+    also from q have "(\<Prod>i=0..n. a - of_nat i) = ?P * (a - of_nat n)"
+      by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
     also have "?P / \<dots> = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric])
     also from assms have "?P / ?P = 1" by auto
     also have "of_nat (Suc n) * (1 / (a - of_nat n)) = 
@@ -119,7 +120,7 @@
   have "\<exists>c. \<forall>z\<in>ball 0 K. f z * (1 + z) powr (-a) = c"
   proof (rule has_field_derivative_zero_constant)
     fix z :: complex assume z': "z \<in> ball 0 K"
-    hence z: "norm z < K" by (simp add: dist_0_norm)
+    hence z: "norm z < K" by simp
     with K have nz: "1 + z \<noteq> 0" by (auto dest!: minus_unique)
     from z K have "norm z < 1" by simp
     hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: complex_nonpos_Reals_iff)
@@ -209,7 +210,7 @@
   also have "(of_real (1 + z) :: complex) powr (of_real a) = of_real ((1 + z) powr a)"
     using assms by (subst powr_of_real) simp_all
   also have "(of_real a gchoose n :: complex) = of_real (a gchoose n)" for n 
-    by (simp add: gbinomial_def)
+    by (simp add: gbinomial_setprod_rev)
   hence "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) =
            (\<lambda>n. of_real ((a gchoose n) * z ^ n))" by (intro ext) simp
   finally show ?thesis by (simp only: sums_of_real_iff)
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Multivariate_Analysis/ex/Approximations.thy
--- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -185,11 +185,11 @@
   also have "\<dots> = (\<Sum>k\<le>n. 1 / fact k)"
   proof (intro setsum.cong refl)
     fix k assume k: "k \<in> {..n}"
-    have "fact n = (\<Prod>i=1..n. real i)" by (rule fact_altdef)
+    have "fact n = (\<Prod>i=1..n. real i)" by (simp add: fact_setprod)
     also from k have "{1..n} = {1..k} \<union> {k+1..n}" by auto
     also have "setprod real \<dots> / (\<Prod>i=k+1..n. real i) = (\<Prod>i=1..k. real i)"
       by (subst nonzero_divide_eq_eq, simp, subst setprod.union_disjoint [symmetric]) auto
-    also have "\<dots> = fact k" by (simp only: fact_altdef)
+    also have "\<dots> = fact k" by (simp add: fact_setprod)
     finally show "1 / (fact n / setprod real {k + 1..n}) = 1 / fact k" by simp
   qed
   also have "\<dots> = euler_approx n" by (simp add: euler_approx_def field_simps)
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/NthRoot.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -246,7 +246,7 @@
   have "continuous_on ({0..} \<union> {.. 0}) (\<lambda>x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)"
     using n by (intro continuous_on_If continuous_intros) auto
   then have "continuous_on UNIV ?f"
-    by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less sgn_neg le_less n)
+    by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less le_less n)
   then have [simp]: "\<And>x. isCont ?f x"
     by (simp add: continuous_on_eq_continuous_at)
 
@@ -654,8 +654,7 @@
          (simp_all add: at_infinity_eq_at_top_bot)
     { fix n :: nat assume "2 < n"
       have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
-        using \<open>2 < n\<close> unfolding gbinomial_def binomial_gbinomial
-        by (simp add: atLeast0AtMost lessThan_Suc field_simps of_nat_diff numeral_2_eq_2)
+        by (auto simp add: choose_two of_nat_div mod_eq_0_iff_dvd)
       also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
         by (simp add: x_def)
       also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
@@ -692,8 +691,7 @@
            (simp_all add: at_infinity_eq_at_top_bot)
       { fix n :: nat assume "1 < n"
         have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
-          using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial
-            by (simp add: lessThan_Suc)
+          by (simp add: choose_one)
         also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
           by (simp add: x_def)
         also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -426,7 +426,7 @@
     apply auto
     done
   also have "\<dots> = fact (p - 1) mod p"
-    apply (subst fact_altdef_nat)
+    apply (simp add: fact_setprod)
     apply (insert assms)
     apply (subst res_prime_units_eq)
     apply (simp add: int_setprod zmod_int setprod_int_eq)
@@ -443,7 +443,7 @@
 proof (cases "p = 2")
   case True
   then show ?thesis
-    by (simp add: cong_int_def fact_altdef_nat)
+    by (simp add: cong_int_def fact_setprod)
 next
   case False
   then show ?thesis
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Power.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -164,7 +164,7 @@
 
 lemma of_nat_power [simp]:
   "of_nat (m ^ n) = of_nat m ^ n"
-  by (induct n) (simp_all add: of_nat_mult)
+  by (induct n) simp_all
 
 lemma zero_power:
   "0 < n \<Longrightarrow> 0 ^ n = 0"
@@ -645,10 +645,10 @@
   by (simp add: le_less)
 
 lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2"
-  by (simp add: power2_eq_square abs_mult abs_mult_self)
+  by (simp add: power2_eq_square)
 
 lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
-  by (simp add: power2_eq_square abs_mult_self)
+  by (simp add: power2_eq_square)
 
 lemma odd_power_less_zero:
   "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
@@ -749,6 +749,18 @@
   "(x - y)\<^sup>2 = (y - x)\<^sup>2"
   by (simp add: algebra_simps power2_eq_square)
 
+lemma (in comm_ring_1) minus_power_mult_self:
+  "(- a) ^ n * (- a) ^ n = a ^ (2 * n)"
+  by (simp add: power_mult_distrib [symmetric]) (simp add: power2_eq_square [symmetric] power_mult [symmetric])
+  
+lemma (in comm_ring_1) minus_one_mult_self [simp]:
+  "(- 1) ^ n * (- 1) ^ n = 1"
+  using minus_power_mult_self [of 1 n] by simp
+
+lemma (in comm_ring_1) left_minus_one_mult_self [simp]:
+  "(- 1) ^ n * ((- 1) ^ n * a) = a"
+  by (simp add: mult.assoc [symmetric])
+
 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
 
 lemmas zero_compare_simps =
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Set_Interval.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -743,18 +743,43 @@
 used, the opposite orientation seems preferable because it reduces a
 specific concept to a more general one.\<close>
 
-lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
+lemma atLeast0LessThan [code_abbrev]: "{0::nat..<n} = {..<n}"
 by(simp add:lessThan_def atLeastLessThan_def)
 
-lemma atLeast0AtMost: "{0..n::nat} = {..n}"
+lemma atLeast0AtMost [code_abbrev]: "{0..n::nat} = {..n}"
 by(simp add:atMost_def atLeastAtMost_def)
 
-declare atLeast0LessThan[symmetric, code_unfold]
-        atLeast0AtMost[symmetric, code_unfold]
+lemma lessThan_atLeast0:
+  "{..<n} = {0::nat..<n}"
+  by (simp add: atLeast0LessThan)
+
+lemma atMost_atLeast0:
+  "{..n} = {0::nat..n}"
+  by (simp add: atLeast0AtMost)
 
 lemma atLeastLessThan0: "{m..<0::nat} = {}"
 by (simp add: atLeastLessThan_def)
 
+lemma atLeast0_lessThan_Suc:
+  "{0..<Suc n} = insert n {0..<n}"
+  by (simp add: atLeast0LessThan lessThan_Suc)
+
+lemma atLeast0_lessThan_Suc_eq_insert_0:
+  "{0..<Suc n} = insert 0 (Suc ` {0..<n})"
+  by (simp add: atLeast0LessThan lessThan_Suc_eq_insert_0)
+
+
+subsubsection \<open>The Constant @{term atLeastAtMost}\<close>
+
+lemma atLeast0_atMost_Suc:
+  "{0..Suc n} = insert (Suc n) {0..n}"
+  by (simp add: atLeast0AtMost atMost_Suc)
+
+lemma atLeast0_atMost_Suc_eq_insert_0:
+  "{0..Suc n} = insert 0 (Suc ` {0..n})"
+  by (simp add: atLeast0AtMost Iic_Suc_eq_insert_0)
+
+
 subsubsection \<open>Intervals of nats with @{term Suc}\<close>
 
 text\<open>Not a simprule because the RHS is too messy.\<close>
@@ -1164,11 +1189,17 @@
 lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
   by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
 
-lemma subset_eq_range_finite:
+lemma subset_eq_atLeast0_lessThan_finite:
   fixes n :: nat
-  assumes "N \<subseteq> {..<n}"
+  assumes "N \<subseteq> {0..<n}"
   shows "finite N" 
-  using assms finite_lessThan by (rule finite_subset)
+  using assms finite_atLeastLessThan by (rule finite_subset)
+
+lemma subset_eq_atLeast0_atMost_finite:
+  fixes n :: nat
+  assumes "N \<subseteq> {0..n}"
+  shows "finite N" 
+  using assms finite_atLeastAtMost by (rule finite_subset)
 
 lemma ex_bij_betw_nat_finite:
   "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
@@ -1180,18 +1211,6 @@
   "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
 by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
 
-lemma bij_betw_nat_finite:
-  assumes "finite A"
-  obtains f where "bij_betw f {..<card A} A"
-proof -
-  from assms obtain f where "bij_betw f {0..<card A} A"
-    by (blast dest: ex_bij_betw_nat_finite)
-  also have "{0..<card A} = {..<card A}"
-    by auto
-  finally show thesis using that
-    by blast
-qed
-
 lemma finite_same_card_bij:
   "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
 apply(drule ex_bij_betw_finite_nat)
@@ -1236,12 +1255,12 @@
   ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast
 qed (insert assms, auto)
 
-lemma subset_eq_range_card:
+lemma subset_eq_atLeast0_lessThan_card:
   fixes n :: nat
-  assumes "N \<subseteq> {..<n}"
+  assumes "N \<subseteq> {0..<n}"
   shows "card N \<le> n"
 proof -
-  from assms finite_lessThan have "card N \<le> card {..<n}"
+  from assms finite_lessThan have "card N \<le> card {0..<n}"
     using card_mono by blast
   then show ?thesis by simp
 qed
@@ -1480,6 +1499,100 @@
 done
 
 
+subsection \<open>Generic big monoid operation over intervals\<close>
+
+lemma inj_on_add_nat' [simp]:
+  "inj_on (plus k) N" for k :: nat
+  by rule simp
+
+context comm_monoid_set
+begin
+
+lemma atLeast_lessThan_shift_bounds:
+  fixes m n k :: nat
+  shows "F g {m + k..<n + k} = F (g \<circ> plus k) {m..<n}"
+proof -
+  have "{m + k..<n + k} = plus k ` {m..<n}"
+    by (auto simp add: image_add_atLeastLessThan [symmetric])
+  also have "F g (plus k ` {m..<n}) = F (g \<circ> plus k) {m..<n}"
+    by (rule reindex) simp
+  finally show ?thesis .
+qed
+
+lemma atLeast_atMost_shift_bounds:
+  fixes m n k :: nat
+  shows "F g {m + k..n + k} = F (g \<circ> plus k) {m..n}"
+proof -
+  have "{m + k..n + k} = plus k ` {m..n}"
+    by (auto simp del: image_add_atLeastAtMost simp add: image_add_atLeastAtMost [symmetric])
+  also have "F g (plus k ` {m..n}) = F (g \<circ> plus k) {m..n}"
+    by (rule reindex) simp
+  finally show ?thesis .
+qed
+
+lemma atLeast_Suc_lessThan_Suc_shift:
+  "F g {Suc m..<Suc n} = F (g \<circ> Suc) {m..<n}"
+  using atLeast_lessThan_shift_bounds [of _ _ 1] by simp
+
+lemma atLeast_Suc_atMost_Suc_shift:
+  "F g {Suc m..Suc n} = F (g \<circ> Suc) {m..n}"
+  using atLeast_atMost_shift_bounds [of _ _ 1] by simp
+
+lemma atLeast0_lessThan_Suc:
+  "F g {0..<Suc n} = F g {0..<n} \<^bold>* g n"
+  by (simp add: atLeast0_lessThan_Suc ac_simps)
+
+lemma atLeast0_atMost_Suc:
+  "F g {0..Suc n} = F g {0..n} \<^bold>* g (Suc n)"
+  by (simp add: atLeast0_atMost_Suc ac_simps)
+
+lemma atLeast0_lessThan_Suc_shift:
+  "F g {0..<Suc n} = g 0 \<^bold>* F (g \<circ> Suc) {0..<n}"
+  by (simp add: atLeast0_lessThan_Suc_eq_insert_0 atLeast_Suc_lessThan_Suc_shift)
+
+lemma atLeast0_atMost_Suc_shift:
+  "F g {0..Suc n} = g 0 \<^bold>* F (g \<circ> Suc) {0..n}"
+  by (simp add: atLeast0_atMost_Suc_eq_insert_0 atLeast_Suc_atMost_Suc_shift)
+
+lemma ivl_cong:
+  "a = c \<Longrightarrow> b = d \<Longrightarrow> (\<And>x. c \<le> x \<Longrightarrow> x < d \<Longrightarrow> g x = h x)
+    \<Longrightarrow> F g {a..<b} = F h {c..<d}"
+  by (rule cong) simp_all
+
+lemma atLeast_lessThan_shift_0:
+  fixes m n p :: nat
+  shows "F g {m..<n} = F (g \<circ> plus m) {0..<n - m}"
+  using atLeast_lessThan_shift_bounds [of g 0 m "n - m"]
+  by (cases "m \<le> n") simp_all
+
+lemma atLeast_atMost_shift_0:
+  fixes m n p :: nat
+  assumes "m \<le> n"
+  shows "F g {m..n} = F (g \<circ> plus m) {0..n - m}"
+  using assms atLeast_atMost_shift_bounds [of g 0 m "n - m"] by simp
+
+lemma atLeast_lessThan_concat:
+  fixes m n p :: nat
+  shows "m \<le> n \<Longrightarrow> n \<le> p \<Longrightarrow> F g {m..<n} \<^bold>* F g {n..<p} = F g {m..<p}"
+  by (simp add: union_disjoint [symmetric] ivl_disj_un)
+
+lemma atLeast_lessThan_rev:
+  "F g {n..<m} = F (\<lambda>i. g (m + n - Suc i)) {n..<m}"
+  by (rule reindex_bij_witness [where i="\<lambda>i. m + n - Suc i" and j="\<lambda>i. m + n - Suc i"], auto)
+
+lemma atLeast_atMost_rev:
+  fixes n m :: nat
+  shows "F g {n..m} = F (\<lambda>i. g (m + n - i)) {n..m}"
+  by (rule reindex_bij_witness [where i="\<lambda>i. m + n - i" and j="\<lambda>i. m + n - i"]) auto
+
+lemma atLeast_lessThan_rev_at_least_Suc_atMost:
+  "F g {n..<m} = F (\<lambda>i. g (m + n - i)) {Suc n..m}"
+  unfolding atLeast_lessThan_rev [of g n m]
+  by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost)
+
+end
+
+
 subsection \<open>Summation indexed over intervals\<close>
 
 syntax (ASCII)
@@ -1539,27 +1652,26 @@
 with the simplifier who adds the unsimplified premise @{term"x:B"} to
 the context.\<close>
 
-lemma setsum_ivl_cong:
- "\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow>
- setsum f {a..<b} = setsum g {c..<d}"
-by(rule setsum.cong, simp_all)
+lemmas setsum_ivl_cong = setsum.ivl_cong
 
 (* FIXME why are the following simp rules but the corresponding eqns
 on intervals are not? *)
 
-lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)"
-by (simp add:atMost_Suc ac_simps)
+lemma setsum_atMost_Suc [simp]:
+  "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f (Suc n)"
+  by (simp add: atMost_Suc ac_simps)
 
-lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
-by (simp add:lessThan_Suc ac_simps)
+lemma setsum_lessThan_Suc [simp]:
+  "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
+  by (simp add: lessThan_Suc ac_simps)
 
-lemma setsum_cl_ivl_Suc[simp]:
+lemma setsum_cl_ivl_Suc [simp]:
   "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
-by (auto simp:ac_simps atLeastAtMostSuc_conv)
+  by (auto simp: ac_simps atLeastAtMostSuc_conv)
 
-lemma setsum_op_ivl_Suc[simp]:
+lemma setsum_op_ivl_Suc [simp]:
   "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
-by (auto simp:ac_simps atLeastLessThanSuc)
+  by (auto simp: ac_simps atLeastLessThanSuc)
 (*
 lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
     (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
@@ -1598,9 +1710,7 @@
     atLeastSucAtMost_greaterThanAtMost)
 qed
 
-lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
-  setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
-by (simp add:setsum.union_disjoint[symmetric] ivl_disj_int ivl_disj_un)
+lemmas setsum_add_nat_ivl = setsum.atLeast_lessThan_concat
 
 lemma setsum_diff_nat_ivl:
 fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
@@ -1639,7 +1749,8 @@
 lemma nat_diff_setsum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
   by (rule setsum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
 
-subsection\<open>Shifting bounds\<close>
+
+subsubsection \<open>Shifting bounds\<close>
 
 lemma setsum_shift_bounds_nat_ivl:
   "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
@@ -1723,7 +1834,7 @@
 qed
 
 
-subsection \<open>Telescoping\<close>
+subsubsection \<open>Telescoping\<close>
 
 lemma setsum_telescope:
   fixes f::"nat \<Rightarrow> 'a::ab_group_add"
@@ -1735,7 +1846,8 @@
   shows   "(\<Sum>k\<in>{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"
   by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)
 
-subsection \<open>The formula for geometric sums\<close>
+
+subsubsection \<open>The formula for geometric sums\<close>
 
 lemma geometric_sum:
   assumes "x \<noteq> 1"
@@ -1743,7 +1855,7 @@
 proof -
   from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
   moreover have "(\<Sum>i<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
-    by (induct n) (simp_all add: power_Suc field_simps \<open>y \<noteq> 0\<close>)
+    by (induct n) (simp_all add: field_simps \<open>y \<noteq> 0\<close>)
   ultimately show ?thesis by simp
 qed
 
@@ -1755,15 +1867,15 @@
 proof (induct n)
   case (Suc n)
   have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)"
-    by (simp add: power_Suc)
+    by simp
   also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)"
-    by (simp add: power_Suc algebra_simps)
+    by (simp add: algebra_simps)
   also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
     by (simp only: Suc)
   also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
     by (simp only: mult.left_commute)
   also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
-    by (simp add: power_Suc field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
+    by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
   finally show ?case .
 qed simp
 
@@ -1791,7 +1903,7 @@
 by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
 
 
-subsection \<open>The formula for arithmetic sums\<close>
+subsubsection \<open>The formula for arithmetic sums\<close>
 
 lemma gauss_sum:
   "(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) = of_nat n*((of_nat n)+1)"
@@ -1854,6 +1966,29 @@
   by (subst setsum_subtractf_nat) auto
 
 
+subsubsection \<open>Division remainder\<close>
+
+lemma range_mod:
+  fixes n :: nat
+  assumes "n > 0"
+  shows "range (\<lambda>m. m mod n) = {0..<n}" (is "?A = ?B")
+proof (rule set_eqI)
+  fix m
+  show "m \<in> ?A \<longleftrightarrow> m \<in> ?B"
+  proof
+    assume "m \<in> ?A"
+    with assms show "m \<in> ?B"
+      by auto 
+  next
+    assume "m \<in> ?B"
+    moreover have "m mod n \<in> ?A"
+      by (rule rangeI)
+    ultimately show "m \<in> ?A"
+      by simp
+  qed
+qed
+
+
 subsection \<open>Products indexed over intervals\<close>
 
 syntax (ASCII)
@@ -1884,44 +2019,6 @@
   "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST setprod (\<lambda>i. t) {..n}"
   "\<Prod>i<n. t" \<rightleftharpoons> "CONST setprod (\<lambda>i. t) {..<n}"
 
-
-subsection \<open>Transfer setup\<close>
-
-lemma transfer_nat_int_set_functions:
-    "{..n} = nat ` {0..int n}"
-    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
-  apply (auto simp add: image_def)
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
-  done
-
-lemma transfer_nat_int_set_function_closures:
-    "x >= 0 \<Longrightarrow> nat_set {x..y}"
-  by (simp add: nat_set_def)
-
-declare transfer_morphism_nat_int[transfer add
-  return: transfer_nat_int_set_functions
-    transfer_nat_int_set_function_closures
-]
-
-lemma transfer_int_nat_set_functions:
-    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
-  by (simp only: is_nat_def transfer_nat_int_set_functions
-    transfer_nat_int_set_function_closures
-    transfer_nat_int_set_return_embed nat_0_le
-    cong: transfer_nat_int_set_cong)
-
-lemma transfer_int_nat_set_function_closures:
-    "is_nat x \<Longrightarrow> nat_set {x..y}"
-  by (simp only: transfer_nat_int_set_function_closures is_nat_def)
-
-declare transfer_morphism_int_nat[transfer add
-  return: transfer_int_nat_set_functions
-    transfer_int_nat_set_function_closures
-]
-
 lemma setprod_int_plus_eq: "setprod int {i..i+j} =  \<Prod>{int i..int (i+j)}"
   by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)
 
@@ -1937,7 +2034,7 @@
 qed
 
 
-subsection \<open>Shifting bounds\<close>
+subsubsection \<open>Shifting bounds\<close>
 
 lemma setprod_shift_bounds_nat_ivl:
   "setprod f {m+k..<n+k} = setprod (%i. f(i + k)){m..<n::nat}"
@@ -1974,29 +2071,6 @@
 qed
 
 
-subsection \<open>Division remainder\<close>
-
-lemma range_mod:
-  fixes n :: nat
-  assumes "n > 0"
-  shows "range (\<lambda>m. m mod n) = {0..<n}" (is "?A = ?B")
-proof (rule set_eqI)
-  fix m
-  show "m \<in> ?A \<longleftrightarrow> m \<in> ?B"
-  proof
-    assume "m \<in> ?A"
-    with assms show "m \<in> ?B"
-      by auto 
-  next
-    assume "m \<in> ?B"
-    moreover have "m mod n \<in> ?A"
-      by (rule rangeI)
-    ultimately show "m \<in> ?A"
-      by simp
-  qed
-qed
-
-
 subsection \<open>Efficient folding over intervals\<close>
 
 function fold_atLeastAtMost_nat where
@@ -2044,4 +2118,42 @@
 
 (* TODO: Add support for more kinds of intervals here *)
 
+
+subsection \<open>Transfer setup\<close>
+
+lemma transfer_nat_int_set_functions:
+    "{..n} = nat ` {0..int n}"
+    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
+  apply (auto simp add: image_def)
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+  done
+
+lemma transfer_nat_int_set_function_closures:
+    "x >= 0 \<Longrightarrow> nat_set {x..y}"
+  by (simp add: nat_set_def)
+
+declare transfer_morphism_nat_int[transfer add
+  return: transfer_nat_int_set_functions
+    transfer_nat_int_set_function_closures
+]
+
+lemma transfer_int_nat_set_functions:
+    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
+  by (simp only: is_nat_def transfer_nat_int_set_functions
+    transfer_nat_int_set_function_closures
+    transfer_nat_int_set_return_embed nat_0_le
+    cong: transfer_nat_int_set_cong)
+
+lemma transfer_int_nat_set_function_closures:
+    "is_nat x \<Longrightarrow> nat_set {x..y}"
+  by (simp only: transfer_nat_int_set_function_closures is_nat_def)
+
+declare transfer_morphism_int_nat[transfer add
+  return: transfer_int_nat_set_functions
+    transfer_int_nat_set_function_closures
+]
+
 end
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Transcendental.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -36,7 +36,7 @@
   by (metis of_nat_fact of_real_of_nat_eq)
 
 lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
-  by (simp add: pochhammer_def)
+  by (simp add: pochhammer_setprod)
 
 lemma norm_fact [simp]:
   "norm (fact n :: 'a :: {real_normed_algebra_1}) = fact n"
diff -r 6af79184bef3 -r c184ec919c70 src/HOL/ex/Sum_of_Powers.thy
--- a/src/HOL/ex/Sum_of_Powers.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/ex/Sum_of_Powers.thy	Sat Jul 09 13:26:16 2016 +0200
@@ -7,32 +7,32 @@
 
 subsection \<open>Additions to @{theory Binomial} Theory\<close>
 
+lemma (in field_char_0) one_plus_of_nat_neq_zero [simp]:
+  "1 + of_nat n \<noteq> 0"
+proof -
+  have "of_nat (Suc n) \<noteq> of_nat 0"
+    unfolding of_nat_eq_iff by simp
+  then show ?thesis by simp
+qed
+
 lemma of_nat_binomial_eq_mult_binomial_Suc:
   assumes "k \<le> n"
   shows "(of_nat :: (nat \<Rightarrow> ('a :: field_char_0))) (n choose k) = of_nat (n + 1 - k) / of_nat (n + 1) * of_nat (Suc n choose k)"
-proof -
-  have "of_nat (n + 1) * (\<Prod>i<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i<k. of_nat (Suc n - i))"
-  proof -
-    have "of_nat (n + 1) * (\<Prod>i<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1) * (\<Prod>i\<in>Suc ` {..<k}. of_nat (Suc n - i))"
-      by (auto simp add: setprod.reindex)
-    also have "... = (\<Prod>i\<le>k. of_nat (Suc n - i))"
-    proof (cases k)
-      case (Suc k')
-      have "of_nat (n + 1) * (\<Prod>i\<in>Suc ` {..<Suc k'}. of_nat (Suc n - i)) = (\<Prod>i\<in>insert 0 (Suc ` {..k'}). of_nat (Suc n - i))"
-        by (subst setprod.insert) (auto simp add: lessThan_Suc_atMost)
-      also have "... = (\<Prod>i\<le>Suc k'. of_nat (Suc n - i))" by (simp only: Iic_Suc_eq_insert_0)
-      finally show ?thesis using Suc by simp
-    qed (simp)
-    also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i<k. of_nat (Suc n - i))"
-      by (cases k) (auto simp add: atMost_Suc lessThan_Suc_atMost)
-    also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i<k. of_nat (Suc n - i))"
-      by (simp only: Suc_eq_plus1)
-    finally show ?thesis .
-  qed
-  then have "(\<Prod>i<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) / of_nat (n + 1) * (\<Prod>i<k. of_nat (Suc n - i))"
-    by (metis (no_types, lifting) le_add2 nonzero_mult_divide_cancel_left not_one_le_zero of_nat_eq_0_iff times_divide_eq_left)
-  from assms this show ?thesis
-    by (auto simp add: binomial_altdef_of_nat setprod_dividef)
+proof (cases k)
+  case 0 then show ?thesis by simp
+next
+  case (Suc l)
+  have "of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
+    using setprod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\<lambda>i. of_nat (Suc n - i)" k]
+    by (simp add: ac_simps setprod.atLeast0_lessThan_Suc_shift)
+  also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
+    by (simp add: Suc atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
+  also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
+    by (simp only: Suc_eq_plus1)
+  finally have "(\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) / of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
+    by (simp add: field_simps)
+  with assms show ?thesis
+    by (simp add: binomial_altdef_of_nat setprod_dividef)
 qed
 
 lemma real_binomial_eq_mult_binomial_Suc: