# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1660517507 -3600
# Node ID 3842556b757c755af4fa339ad8cbb7da7e217fe9
# Parent  b0215440311d3a5aea6108e6b634ca299ea5a4c0
moved some material from Sum_of_Powers

diff -r b0215440311d -r 3842556b757c src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Sun Aug 14 18:38:40 2022 +0200
+++ b/src/HOL/Binomial.thy	Sun Aug 14 23:51:47 2022 +0100
@@ -1045,17 +1045,11 @@
     by (simp add: binomial_altdef_nat)
   also have "... = fact (m + r + k) * fact (m + k) div
                  (fact (m + k) * fact (m + r - m) * (fact k * fact m))"
-    apply (subst div_mult_div_if_dvd)
-      apply (auto simp: algebra_simps fact_fact_dvd_fact)
-    apply (metis add.assoc add.commute fact_fact_dvd_fact)
-    done
+    by (metis add_implies_diff add_le_mono1 choose_dvd diff_cancel2 div_mult_div_if_dvd le_add1 le_add2)
   also have "\<dots> = fact (m + r + k) div (fact r * (fact k * fact m))"
     by (auto simp: algebra_simps fact_fact_dvd_fact)
   also have "\<dots> = (fact (m + r + k) * fact (m + r)) div (fact r * (fact k * fact m) * fact (m + r))"
-    apply (subst div_mult_div_if_dvd [symmetric])
-    apply (auto simp add: algebra_simps)
-    apply (metis fact_fact_dvd_fact dvd_trans nat_mult_dvd_cancel_disj)
-    done
+    by simp
   also have "\<dots> =
       (fact (m + r + k) div (fact k * fact (m + r)) * (fact (m + r) div (fact r * fact m)))"
     by (auto simp: div_mult_div_if_dvd fact_fact_dvd_fact algebra_simps)
@@ -1068,6 +1062,26 @@
   "k \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> (n choose m) * (m choose k) = (n choose k) * ((n - k) choose (m - k))"
   using choose_mult_lemma [of "m-k" "n-m" k] by simp
 
+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 (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 prod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\<lambda>i. of_nat (Suc n - i)" k]
+    by (simp add: ac_simps prod.atLeast0_lessThan_Suc_shift del: prod.op_ivl_Suc)
+  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 prod_dividef)
+qed
+
 
 subsection \<open>More on Binomial Coefficients\<close>
 
diff -r b0215440311d -r 3842556b757c src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Aug 14 18:38:40 2022 +0200
+++ b/src/HOL/Nat.thy	Sun Aug 14 23:51:47 2022 +0100
@@ -1768,6 +1768,14 @@
 lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
   by (auto intro: inj_of_nat injD)
 
+lemma 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
+
 text \<open>Special cases where either operand is zero\<close>
 
 lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
diff -r b0215440311d -r 3842556b757c src/HOL/Real.thy
--- a/src/HOL/Real.thy	Sun Aug 14 18:38:40 2022 +0200
+++ b/src/HOL/Real.thy	Sun Aug 14 23:51:47 2022 +0100
@@ -1076,6 +1076,12 @@
 lemma real_of_nat_div4: "real (n div x) \<le> real n / real x" for n x :: nat
   using real_of_nat_div2 [of n x] by simp
 
+lemma real_binomial_eq_mult_binomial_Suc:
+  assumes "k \<le> n"
+  shows "real(n choose k) = (n + 1 - k) / (n + 1) * (Suc n choose k)"
+  using assms
+  by (simp add: of_nat_binomial_eq_mult_binomial_Suc [of k n] add.commute of_nat_diff)
+
 
 subsection \<open>The Archimedean Property of the Reals\<close>
 
diff -r b0215440311d -r 3842556b757c src/HOL/ex/Sum_of_Powers.thy
--- a/src/HOL/ex/Sum_of_Powers.thy	Sun Aug 14 18:38:40 2022 +0200
+++ b/src/HOL/ex/Sum_of_Powers.thy	Sun Aug 14 23:51:47 2022 +0100
@@ -5,58 +5,16 @@
 imports Complex_Main
 begin
 
-subsection \<open>Additions to \<^theory>\<open>HOL.Binomial\<close> 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 (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 prod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\<lambda>i. of_nat (Suc n - i)" k]
-    by (simp add: ac_simps prod.atLeast0_lessThan_Suc_shift del: prod.op_ivl_Suc)
-  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 prod_dividef)
-qed
-
-lemma real_binomial_eq_mult_binomial_Suc:
-  assumes "k \<le> n"
-  shows "(n choose k) = (n + 1 - k) / (n + 1) * (Suc n choose k)"
-by (metis Suc_eq_plus1 add.commute assms le_SucI of_nat_Suc of_nat_binomial_eq_mult_binomial_Suc of_nat_diff)
-
 subsection \<open>Preliminaries\<close>
 
 lemma integrals_eq:
-  assumes "f 0 = g 0"
+  assumes "f a = g a"
   assumes "\<And> x. ((\<lambda>x. f x - g x) has_real_derivative 0) (at x)"
   shows "f x = g x"
-proof -
-  show "f x = g x"
-  proof (cases "x \<noteq> 0")
-    case True
-    from assms DERIV_const_ratio_const[OF this, of "\<lambda>x. f x - g x" 0]
-    show ?thesis by auto
-  qed (simp add: assms)
-qed
+  by (metis (no_types, lifting) DERIV_isconst_all assms(1) assms(2) eq_iff_diff_eq_0)
 
 lemma sum_diff: "((\<Sum>i\<le>n::nat. f (i + 1) - f i)::'a::field) = f (n + 1) - f 0"
-by (induct n) (auto simp add: field_simps)
+  by (induct n) (auto simp add: field_simps)
 
 declare One_nat_def [simp del]