# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1706632761 0
# Node ID 50ee2921da94bc8843db2fce53477e8bec406c60
# Parent  bbed18f7a522ced1bc3c73c87a5b4f2f80f6d0df
A few more new theorems taken from AFP entries

diff -r bbed18f7a522 -r 50ee2921da94 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Mon Jan 29 21:18:11 2024 +0100
+++ b/src/HOL/Binomial.thy	Tue Jan 30 16:39:21 2024 +0000
@@ -172,16 +172,14 @@
 subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close>
 
 text \<open>Avigad's version, generalized to any commutative ring\<close>
-theorem binomial_ring: "(a + b :: 'a::comm_semiring_1)^n =
-  (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n-k))"
+theorem (in comm_semiring_1) binomial_ring:
+  "(a + b :: 'a)^n = (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n-k))"
 proof (induct n)
   case 0
   then show ?case by simp
 next
   case (Suc n)
-  have decomp: "{0..n+1} = {0} \<union> {n + 1} \<union> {1..n}"
-    by auto
-  have decomp2: "{0..n} = {0} \<union> {1..n}"
+  have decomp: "{0..n+1} = {0} \<union> {n + 1} \<union> {1..n}" and decomp2: "{0..n} = {0} \<union> {1..n}"
     by auto
   have "(a + b)^(n+1) = (a + b) * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n - k))"
     using Suc.hyps by simp
@@ -208,6 +206,7 @@
     by simp
 qed
 
+
 text \<open>Original version for the naturals.\<close>
 corollary binomial: "(a + b :: nat)^n = (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n - k))"
   using binomial_ring [of "int a" "int b" n]
diff -r bbed18f7a522 -r 50ee2921da94 src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Mon Jan 29 21:18:11 2024 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy	Tue Jan 30 16:39:21 2024 +0000
@@ -784,6 +784,20 @@
   by (auto simp add: prime_factorization_subset_iff_dvd [symmetric]
     prime_factorization_prime prime_factors_fact prime_ge_2_nat)
 
+lemma dvd_choose_prime:
+  assumes kn: "k < n" and k: "k \<noteq> 0" and n: "n \<noteq> 0" and prime_n: "prime n"
+  shows "n dvd (n choose k)"
+proof -
+  have "n dvd (fact n)" by (simp add: fact_num_eq_if n)
+  moreover have "\<not> n dvd (fact k * fact (n-k))"
+    by (metis prime_dvd_fact_iff prime_dvd_mult_iff assms neq0_conv diff_less linorder_not_less)
+  moreover have "(fact n::nat) = fact k * fact (n-k) * (n choose k)"
+    using binomial_fact_lemma kn by auto
+  ultimately show ?thesis using prime_n
+    by (auto simp add: prime_dvd_mult_iff)
+qed
+
+
 (* TODO Legacy names *)
 lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
 lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
diff -r bbed18f7a522 -r 50ee2921da94 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Jan 29 21:18:11 2024 +0100
+++ b/src/HOL/GCD.thy	Tue Jan 30 16:39:21 2024 +0000
@@ -2942,4 +2942,11 @@
   in [(\<^const_syntax>\<open>semiring_char\<close>, char_type_tr')] end
 \<close>
 
+
+lemma CHAR_not_1 [simp]: "CHAR('a :: {semiring_1, zero_neq_one}) \<noteq> Suc 0"
+  by (metis One_nat_def of_nat_1 of_nat_CHAR zero_neq_one)
+
+lemma (in idom) CHAR_not_1' [simp]: "CHAR('a) \<noteq> Suc 0"
+  using local.of_nat_CHAR by fastforce
+
 end