# HG changeset patch # User paulson # 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 \The binomial theorem (courtesy of Tobias Nipkow):\ text \Avigad's version, generalized to any commutative ring\ -theorem binomial_ring: "(a + b :: 'a::comm_semiring_1)^n = - (\k\n. (of_nat (n choose k)) * a^k * b^(n-k))" +theorem (in comm_semiring_1) binomial_ring: + "(a + b :: 'a)^n = (\k\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} \ {n + 1} \ {1..n}" - by auto - have decomp2: "{0..n} = {0} \ {1..n}" + have decomp: "{0..n+1} = {0} \ {n + 1} \ {1..n}" and decomp2: "{0..n} = {0} \ {1..n}" by auto have "(a + b)^(n+1) = (a + b) * (\k\n. of_nat (n choose k) * a^k * b^(n - k))" using Suc.hyps by simp @@ -208,6 +206,7 @@ by simp qed + text \Original version for the naturals.\ corollary binomial: "(a + b :: nat)^n = (\k\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 \ 0" and n: "n \ 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 "\ 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>\semiring_char\, char_type_tr')] end \ + +lemma CHAR_not_1 [simp]: "CHAR('a :: {semiring_1, zero_neq_one}) \ 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) \ Suc 0" + using local.of_nat_CHAR by fastforce + end