--- a/src/HOL/Binomial.thy Sun Aug 14 23:51:47 2022 +0100
+++ b/src/HOL/Binomial.thy Mon Aug 15 12:50:24 2022 +0100
@@ -1066,7 +1066,8 @@
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
+ case 0 then show ?thesis
+ using of_nat_neq_0 by auto
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))"
@@ -1077,7 +1078,7 @@
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)
+ using of_nat_neq_0 by (auto simp: mult.commute divide_simps)
with assms show ?thesis
by (simp add: binomial_altdef_of_nat prod_dividef)
qed
--- a/src/HOL/Factorial.thy Sun Aug 14 23:51:47 2022 +0100
+++ b/src/HOL/Factorial.thy Mon Aug 15 12:50:24 2022 +0100
@@ -64,11 +64,7 @@
by (cases n) auto
lemma fact_nonzero [simp]: "fact n \<noteq> (0::'a::{semiring_char_0,semiring_no_zero_divisors})"
- apply (induct n)
- apply auto
- using of_nat_eq_0_iff
- apply fastforce
- done
+ using of_nat_0_neq by (induct n) auto
lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)"
by (induct n) (auto simp: le_Suc_eq)
--- a/src/HOL/Nat.thy Sun Aug 14 23:51:47 2022 +0100
+++ b/src/HOL/Nat.thy Mon Aug 15 12:50:24 2022 +0100
@@ -1768,14 +1768,6 @@
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"