--- 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>
--- 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"
--- 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>
--- 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]