(* Title: HOL/Computational_Algebra/Primes.thy Author: Christophe Tabacznyj Author: Lawrence C. Paulson Author: Amine Chaieb Author: Thomas M. Rasmussen Author: Jeremy Avigad Author: Tobias Nipkow Author: Manuel Eberl
This theory deals with properties of primes. Definitions and lemmas are proved uniformly for the natural numbers and integers.
This file combines and revises a number of prior developments.
The original theories "GCD" and "Primes" were by Christophe Tabacznyj and Lawrence C. Paulson, based on @{cite davenport92}. They introduced gcd, lcm, and prime for the natural numbers.
The original theory "IntPrimes" was by Thomas M. Rasmussen, and extended gcd, lcm, primes to the integers. Amine Chaieb provided another extension of the notions to the integers, and added a number of results to "Primes" and "GCD". IntPrimes also defined and developed the congruence relations on the integers. The notion was extended to the natural numbers by Chaieb.
Jeremy Avigad combined all of these, made everything uniform for the natural numbers and the integers, and added a number of new theorems.
Tobias Nipkow cleaned up a lot.
Florian Haftmann and Manuel Eberl put primality and prime factorisation onto an algebraic foundation and thus generalised these concepts to other rings, such as polynomials. (see also the Factorial_Ring theory).
There were also previous formalisations of unique factorisation by Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
*)
section \<open>Primes\<close>
theory Primes imports Euclidean_Algorithm begin
subsection \<open>Primes on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close>
lemma Suc_0_not_prime_nat [simp]: "\ prime (Suc 0)" using not_prime_1 [where ?'a = nat] by simp
lemma prime_ge_2_nat: "p \ 2" if "prime p" for p :: nat proof - from that have"p \ 0" and "p \ 1" by (auto dest: prime_elem_not_zeroI prime_elem_not_unit) thenshow ?thesis by simp qed
lemma prime_ge_2_int: "p \ 2" if "prime p" for p :: int proof - from that have"prime_elem p"and"\p\ = p" by (auto dest: normalize_prime) thenhave"p \ 0" and "\p\ \ 1" and "p \ 0" by (auto dest: prime_elem_not_zeroI prime_elem_not_unit) thenshow ?thesis by simp qed
lemma prime_ge_0_int: "prime p \ p \ (0::int)" using prime_ge_2_int [of p] by simp
lemma prime_gt_0_nat: "prime p \ p > (0::nat)" using prime_ge_2_nat [of p] by simp
(* As a simp or intro rule,
prime p \<Longrightarrow> p > 0
wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it leads to the backchaining
x > 0 prime x x \<in># M which is, unfortunately, count M x > 0 FIXME no, this is obsolete
*)
lemma prime_gt_0_int: "prime p \ p > (0::int)" using prime_ge_2_int [of p] by simp
lemma prime_ge_1_nat: "prime p \ p \ (1::nat)" using prime_ge_2_nat [of p] by simp
lemma prime_ge_Suc_0_nat: "prime p \ p \ Suc 0" using prime_ge_1_nat [of p] by simp
lemma prime_ge_1_int: "prime p \ p \ (1::int)" using prime_ge_2_int [of p] by simp
lemma prime_gt_1_nat: "prime p \ p > (1::nat)" using prime_ge_2_nat [of p] by simp
lemma prime_gt_Suc_0_nat: "prime p \ p > Suc 0" using prime_gt_1_nat [of p] by simp
lemma prime_gt_1_int: "prime p \ p > (1::int)" using prime_ge_2_int [of p] by simp
lemma prime_natI: "prime p"if"p \ 2" and "\m n. p dvd m * n \ p dvd m \ p dvd n" for p :: nat using that by (auto intro!: primeI prime_elemI)
lemma prime_intI: "prime p"if"p \ 2" and "\m n. p dvd m * n \ p dvd m \ p dvd n" for p :: int using that by (auto intro!: primeI prime_elemI)
lemma prime_elem_nat_iff [simp]: "prime_elem n \ prime n" for n :: nat by (simp add: prime_def)
lemma prime_elem_iff_prime_abs [simp]: "prime_elem k \ prime \k\" for k :: int by (auto intro: primeI)
lemma prime_nat_int_transfer [simp]: "prime (int n) \ prime n" (is "?P \ ?Q") proof assume ?P thenhave"n \ 2" by (auto dest: prime_ge_2_int) thenshow ?Q proof (rule prime_natI) fix r s assume"n dvd r * s" with of_nat_dvd_iff [of n "r * s"] have"int n dvd int r * int s" by simp with\<open>?P\<close> have "int n dvd int r \<or> int n dvd int s" using prime_dvd_mult_iff [of "int n""int r""int s"] by simp thenshow"n dvd r \ n dvd s" by simp qed next assume ?Q thenhave"int n \ 2" by (auto dest: prime_ge_2_nat) thenshow ?P proof (rule prime_intI) fix r s assume"int n dvd r * s" thenhave"n dvd nat \r * s\" by simp thenhave"n dvd nat \r\ * nat \s\" by (simp add: nat_abs_mult_distrib) with\<open>?Q\<close> have "n dvd nat \<bar>r\<bar> \<or> n dvd nat \<bar>s\<bar>" using prime_dvd_mult_iff [of "n""nat \r\" "nat \s\"] by simp thenshow"int n dvd r \ int n dvd s" by simp qed qed
lemma prime_nat_iff_prime [simp]: "prime (nat k) \ prime k" proof (cases "k \ 0") case True thenshow ?thesis using prime_nat_int_transfer [of "nat k"] by simp next case False thenshow ?thesis by (auto dest: prime_ge_2_int) qed
lemma prime_int_nat_transfer: "prime k \ k \ 0 \ prime (nat k)" by (auto dest: prime_ge_2_int)
lemma prime_nat_naiveI: "prime p"if"p \ 2" and dvd: "\n. n dvd p \ n = 1 \ n = p" for p :: nat proof (rule primeI, rule prime_elemI) fix m n :: nat assume"p dvd m * n" thenobtain r s where"p = r * s""r dvd m""s dvd n" by (blast dest: division_decomp) moreoverhave"r = 1 \ r = p" using\<open>r dvd m\<close> \<open>p = r * s\<close> dvd [of r] by simp ultimatelyshow"p dvd m \ p dvd n" by auto qed (use\<open>p \<ge> 2\<close> in simp_all)
lemma prime_int_naiveI: "prime p"if"p \ 2" and dvd: "\k. k dvd p \ \k\ = 1 \ \k\ = p" for p :: int proof - from\<open>p \<ge> 2\<close> have "nat p \<ge> 2" by simp thenhave"prime (nat p)" proof (rule prime_nat_naiveI) fix n assume"n dvd nat p" with\<open>p \<ge> 2\<close> have "n dvd nat \<bar>p\<bar>" by simp thenhave"int n dvd p" by simp with dvd [of "int n"] show"n = 1 \ n = nat p" by auto qed thenshow ?thesis by simp qed
lemma prime_nat_iff: "prime (n :: nat) \ (1 < n \ (\m. m dvd n \ m = 1 \ m = n))" proof (safe intro!: prime_gt_1_nat) assume"prime n" thenhave *: "prime_elem n" by simp fix m assume m: "m dvd n""m \ n" from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m" by (intro irreducibleD' prime_elem_imp_irreducible) with m show"m = 1"by (auto dest: dvd_antisym) next assume"n > 1""\m. m dvd n \ m = 1 \ m = n" thenshow"prime n" using prime_nat_naiveI [of n] by auto qed
lemma prime_nat_iff': "prime (p :: nat) \ p > 1 \ (\n \ {2.. n dvd p)" proof safe assume"p > 1"and *: "\n\{2..n dvd p" show"prime p"unfolding prime_nat_iff proof (intro conjI allI impI) fix m assume"m dvd p" with\<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto hence"m \ 1" by simp moreoverfrom\<open>m dvd p\<close> and * have "m \<notin> {2..<p}" by blast with\<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le) ultimatelyshow"m = 1 \ m = p" by simp qed fact+ qed (auto simp: prime_nat_iff)
lemma prime_int_iff: "prime (n::int) \ (1 < n \ (\m. m \ 0 \ m dvd n \ m = 1 \ m = n))" proof (intro iffI conjI allI impI; (elim conjE)?) assume *: "prime n" hence irred: "irreducible n"by (auto intro: prime_elem_imp_irreducible) from * have"n \ 0" "n \ 0" "n \ 1" by (auto simp add: prime_ge_0_int) thus"n > 1"by presburger fix m assume"m dvd n"\<open>m \<ge> 0\<close> with irred have"m dvd 1 \ n dvd m" by (auto simp: irreducible_altdef) with\<open>m dvd n\<close> \<open>m \<ge> 0\<close> \<open>n > 1\<close> show "m = 1 \<or> m = n" using associated_iff_dvd[of m n] by auto next assume n: "1 < n""\m. m \ 0 \ m dvd n \ m = 1 \ m = n" hence"nat n > 1"by simp moreoverhave"\m. m dvd nat n \ m = 1 \ m = nat n" proof (intro allI impI) fix m assume"m dvd nat n" with\<open>n > 1\<close> have "m dvd nat \<bar>n\<bar>" by simp thenhave"int m dvd n" by simp with n(2) have"int m = 1 \ int m = n" using of_nat_0_le_iff by blast thus"m = 1 \ m = nat n" by auto qed ultimatelyshow"prime n" unfolding prime_int_nat_transfer prime_nat_iff by auto qed
lemma prime_int_iff': "prime (p :: int) \ p > 1 \ (\n \ {2.. n dvd p)" (is "?P \ ?Q") proof (cases "p \ 0") case True have"?P \ prime (nat p)" by simp alsohave"\ \ p > 1 \ (\n\{2.. n dvd nat \p\)" using True by (simp add: prime_nat_iff') alsohave"{2.. using True int_eq_iff by fastforce finallyshow"?P \ ?Q" by simp next case False thenshow ?thesis by (auto simp add: prime_ge_0_int) qed
lemma prime_nat_not_dvd: assumes"prime p""p > n""n \ (1::nat)" shows"\n dvd p" proof assume"n dvd p" from assms(1) have"irreducible p"by (simp add: prime_elem_imp_irreducible) from irreducibleD'[OF this \n dvd p\] \n dvd p\ \p > n\ assms show False by (cases "n = 0") (auto dest!: dvd_imp_le) qed
lemma prime_int_not_dvd: assumes"prime p""p > n""n > (1::int)" shows"\n dvd p" proof assume"n dvd p" from assms(1) have"irreducible p"by (auto intro: prime_elem_imp_irreducible) from irreducibleD'[OF this \n dvd p\] \n dvd p\ \p > n\ assms show False by (auto dest!: zdvd_imp_le) qed
lemma prime_odd_nat: "prime p \ p > (2::nat) \ odd p" by (intro prime_nat_not_dvd) auto
lemma prime_odd_int: "prime p \ p > (2::int) \ odd p" by (intro prime_int_not_dvd) auto
lemma prime_int_altdef: "prime p = (1 < p \ (\m::int. m \ 0 \ m dvd p \
m = 1 \<or> m = p))" unfolding prime_int_iff by blast
lemma not_prime_eq_prod_nat: assumes"m > 1""\ prime (m::nat)" shows"\n k. n = m * k \ 1 < m \ m < n \ 1 < k \ k < n" using assms irreducible_altdef[of m] by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
subsection \<open>Make prime naively executable\<close>
lemma prime_int_numeral_eq [simp]: "prime (numeral m :: int) \ prime (numeral m :: nat)" by (simp add: prime_int_nat_transfer)
class check_prime_by_range = normalization_semidom + discrete_linordered_semidom + assumes prime_iff: \<open>prime a \<longleftrightarrow> 1 < a \<and> (\<forall>d\<in>{2..a div 2}. \<not> d dvd a)\<close> begin
lemma two_is_prime [simp]: \<open>prime 2\<close> by (simp add: prime_iff)
end
lemma divisor_less_eq_half_nat: \<open>m \<le> n div 2\<close> if \<open>m dvd n\<close> \<open>m < n\<close> for m n :: nat using that by (auto simp add: less_eq_div_iff_mult_less_eq)
lemma two_is_prime_nat [simp]: \<open>prime (2::nat)\<close> by (fact two_is_prime)
lemma divisor_less_eq_half_int: \<open>k \<le> l div 2\<close> if \<open>k dvd l\<close> \<open>k < l\<close> \<open>l \<ge> 0\<close> \<open>k \<ge> 0\<close> for k l :: int proof -
define m n where\<open>m = nat \<bar>k\<bar>\<close> \<open>n = nat \<bar>l\<bar>\<close> with\<open>l \<ge> 0\<close> \<open>k \<ge> 0\<close> have \<open>k = int m\<close> \<open>l = int n\<close> by simp_all with that show ?thesis using divisor_less_eq_half_nat [of m n] by simp qed
lemma prime_nat_numeral_eq [simp]: \<comment> \<open>TODO Sieve Of Erathosthenes might speed this up\<close> "prime (numeral m :: nat) \
(1::nat) < numeral m \<and>
(\<forall>n::nat \<in> set [2..<Suc (numeral m div 2)]. \<not> n dvd numeral m)" using prime_iff [of \<open>numeral m :: nat\<close>] by (simp only: set_upt atLeastLessThanSuc_atLeastAtMost)
context check_prime_by_range begin
definition check_divisors :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool\<close> where\<open>check_divisors l u a \<longleftrightarrow> (\<forall>d\<in>{l..u}. \<not> d dvd a)\<close>
lemma check_divisors_rec [code]: \<open>check_divisors l u a \<longleftrightarrow> u < l \<or> (\<not> l dvd a \<and> check_divisors (l + 1) u a)\<close> apply (auto simp add: check_divisors_def not_less) apply (metis local.add_increasing2 local.atLeastAtMost_iff local.linear local.order_eq_iff local.zero_le_one)
subgoal for d apply (cases \<open>l + 1 \<le> d\<close>) apply (auto simp add: not_le) apply (metis local.dual_order.antisym local.less_eq_iff_succ_less) done done
lemma prime_eq_check_divisors [code]: \<open>prime a \<longleftrightarrow> a > 1 \<and> check_divisors 2 (a div 2) a\<close> by (simp add: check_divisors_def prime_iff)
end
subsection \<open>Largest exponent of a prime factor\<close>
lemma prime_factor_nat: "n \ (1::nat) \ \p. prime p \ p dvd n" using prime_divisor_exists[of n] by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
lemma prime_factor_int: fixes k :: int assumes"\k\ \ 1" obtains p where"prime p""p dvd k" proof (cases "k = 0") case True thenhave"prime (2::int)"and"2 dvd k" by simp_all with that show thesis by blast next case False with assms prime_divisor_exists [of k] obtain p where"prime p""p dvd k" by auto with that show thesis by blast qed
text\<open>Possibly duplicates other material, but avoid the complexities of multisets.\<close>
lemma prime_power_cancel_less: assumes"prime p"and eq: "m * (p ^ k) = m' * (p ^ k')"and less: "k < k'"and"\ p dvd m" shows False proof - obtain l where l: "k' = k + l"and"l > 0" using less less_imp_add_positive by auto have"m = m * (p ^ k) div (p ^ k)" using\<open>prime p\<close> by simp alsohave"\ = m' * (p ^ k') div (p ^ k)" using eq by simp alsohave"\ = m' * (p ^ l) * (p ^ k) div (p ^ k)" by (simp add: l mult.commute mult.left_commute power_add) alsohave"... = m' * (p ^ l)" using\<open>prime p\<close> by simp finallyhave"p dvd m" using\<open>l > 0\<close> by simp with assms show False by simp qed
lemma prime_power_cancel: assumes"prime p"and eq: "m * (p ^ k) = m' * (p ^ k')"and"\ p dvd m" "\ p dvd m'" shows"k = k'" using prime_power_cancel_less [OF \<open>prime p\<close>] assms by (metis linorder_neqE_nat)
lemma prime_power_cancel2: assumes"prime p""m * (p ^ k) = m' * (p ^ k')""\ p dvd m" "\ p dvd m'" obtains"m = m'""k = k'" using prime_power_cancel [OF assms] assms by auto
lemma prime_power_canonical: fixes m :: nat assumes"prime p""m > 0" shows"\k n. \ p dvd n \ m = n * p ^ k" using\<open>m > 0\<close> proof (induction m rule: less_induct) case (less m) show ?case proof (cases "p dvd m") case True thenobtain m' where m': "m = p * m'" using dvdE by blast with\<open>prime p\<close> have "0 < m'" "m' < m" using less.prems prime_nat_iff by auto with m' less show ?thesis by (metis power_Suc mult.left_commute) next case False thenshow ?thesis by (metis mult.right_neutral power_0) qed qed
subsection \<open>Infinitely many primes\<close>
lemma next_prime_bound: "\p::nat. prime p \ n < p \ p \ fact n + 1"
proof- have f1: "fact n + 1 \ (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith from prime_factor_nat [OF f1] obtain p :: nat where"prime p"and"p dvd fact n + 1"by auto thenhave"p \ fact n + 1" apply (intro dvd_imp_le) apply auto done
{ assume"p \ n" from\<open>prime p\<close> have "p \<ge> 1" by (cases p, simp_all) with\<open>p <= n\<close> have "p dvd fact n" by (intro dvd_fact) with\<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n" by (rule dvd_diff_nat) thenhave"p dvd 1"by simp thenhave"p <= 1"by auto moreoverfrom\<open>prime p\<close> have "p > 1" using prime_nat_iff by blast ultimatelyhave False by auto} thenhave"n < p"by presburger with\<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto qed
lemma bigger_prime: "\p. prime p \ p > (n::nat)" using next_prime_bound by auto
lemma primes_infinite: "\ (finite {(p::nat). prime p})" proof assume"finite {(p::nat). prime p}" with Max_ge have"(\b. (\x \ {(p::nat). prime p}. x \ b))" by auto thenobtain b where"\(x::nat). prime x \ x \ b" by auto with bigger_prime [of b] show False by auto qed
subsection \<open>Powers of Primes\<close>
text\<open>Versions for type nat only\<close>
lemma prime_product: fixes p::nat assumes"prime (p * q)" shows"p = 1 \ q = 1" proof - from assms have "1 < p * q"and P: "\m. m dvd p * q \ m = 1 \ m = p * q" unfolding prime_nat_iff by auto from\<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto thenhave Q: "p = p * q \ q = 1" by auto have"p dvd p * q"by simp thenhave"p = 1 \ p = p * q" by (rule P) thenshow ?thesis by (simp add: Q) qed
(* TODO: Generalise? *) lemma prime_power_mult_nat: fixes p :: nat assumes p: "prime p"and xy: "x * y = p ^ k" shows"\i j. x = p ^ i \ y = p^ j" using xy proof(induct k arbitrary: x y) case 0 thus ?caseapply simp by (rule exI[where x="0"], simp) next case (Suc k x y) from Suc.prems have pxy: "p dvd x*y"by auto from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \ p dvd y" . from p have p0: "p \ 0" by - (rule ccontr, simp)
{assume px: "p dvd x" thenobtain d where d: "x = p*d"unfolding dvd_def by blast from Suc.prems d have"p*d*y = p^Suc k"by simp hence th: "d*y = p^k"using p0 by simp from Suc.hyps[OF th] obtain i j where ij: "d = p^i""y = p^j"by blast with d have"x = p^Suc i"by simp with ij(2) have ?caseby blast} moreover
{assume px: "p dvd y" thenobtain d where d: "y = p*d"unfolding dvd_def by blast from Suc.prems d have"p*d*x = p^Suc k"by (simp add: mult.commute) hence th: "d*x = p^k"using p0 by simp from Suc.hyps[OF th] obtain i j where ij: "d = p^i""x = p^j"by blast with d have"y = p^Suc i"by simp with ij(2) have ?caseby blast} ultimatelyshow ?caseusing pxyc by blast qed
lemma prime_power_exp_nat: fixes p::nat assumes p: "prime p"and n: "n \ 0" and xn: "x^n = p^k"shows"\i. x = p^i" using n xn proof(induct n arbitrary: k) case 0 thus ?caseby simp next case (Suc n k) hence th: "x*x^n = p^k"by simp
{assume"n = 0"with Suc have ?caseby simp (rule exI[where x="k"], simp)} moreover
{assume n: "n \ 0" from prime_power_mult_nat[OF p th] obtain i j where ij: "x = p^i""x^n = p^j"by blast from Suc.hyps[OF n ij(2)] have ?case .} ultimatelyshow ?caseby blast qed
lemma divides_primepow_nat: fixes p :: nat assumes p: "prime p" shows"d dvd p ^ k \ (\i\k. d = p ^ i)" using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd)
lemma gcd_prime_int: assumes"prime (p :: int)" shows"gcd p k = (if p dvd k then p else 1)" proof - have"p \ 0" using assms prime_ge_0_int by auto show ?thesis proof (cases "p dvd k") case True thus ?thesis using assms \<open>p \<ge> 0\<close> by auto next case False hence"coprime p k" using assms by (simp add: prime_imp_coprime) with False show ?thesis by auto qed qed
lemma bezout_gcd_nat: fixes a::nat shows"\x y. a * x - b * y = gcd a b \ b * x - a * y = gcd a b" using bezout_nat[of a b] by (metis bezout_nat diff_add_inverse gcd_add_mult gcd.commute
gcd_nat.right_neutral mult_0)
lemma gcd_bezout_sum_nat: fixes a::nat assumes"a * x + b * y = d" shows"gcd a b dvd d"
proof- let ?g = "gcd a b" have dv: "?g dvd a*x""?g dvd b * y" by simp_all from dvd_add[OF dv] assms show ?thesis by auto qed
text\<open>A binary form of the Chinese Remainder Theorem.\<close>
(* TODO: Generalise? *) lemma chinese_remainder: fixes a::nat assumes ab: "coprime a b"and a: "a \ 0" and b: "b \ 0" shows"\x q1 q2. x = u + q1 * a \ x = v + q2 * b"
proof- from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a] obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a""d1 dvd b""a * x1 = b * y1 + d1" and dxy2: "d2 dvd b""d2 dvd a""b * x2 = a * y2 + d2"by blast thenhave d12: "d1 = 1""d2 = 1" using ab coprime_common_divisor_nat [of a b] by blast+ let ?x = "v * a * x1 + u * b * x2" let ?q1 = "v * x1 + u * y2" let ?q2 = "v * y1 + u * x2" from dxy2(3)[simplified d12] dxy1(3)[simplified d12] have"?x = u + ?q1 * a""?x = v + ?q2 * b" by algebra+ thus ?thesis by blast qed
text\<open>Primality\<close>
lemma coprime_bezout_strong: fixes a::nat assumes"coprime a b""b \ 1" shows"\x y. a * x = b * y + 1" by (metis add.commute add.right_neutral assms(1) assms(2) chinese_remainder coprime_1_left coprime_1_right coprime_crossproduct_nat mult.commute mult.right_neutral mult_cancel_left)
lemma bezout_prime: assumes p: "prime p"and pa: "\ p dvd a" shows"\x y. a*x = Suc (p*y)" proof - have ap: "coprime a p" using coprime_commute p pa prime_imp_coprime by auto moreoverfrom p have"p \ 1" by auto ultimatelyhave"\x y. a * x = p * y + 1" by (rule coprime_bezout_strong) thenshow ?thesis by simp qed (* END TODO *)
subsection \<open>Multiplicity and primality for natural numbers and integers\<close>
lemma prime_factors_gt_0_nat: "p \ prime_factors x \ p > (0::nat)" by (simp add: in_prime_factors_imp_prime prime_gt_0_nat)
lemma prime_factors_gt_0_int: "p \ prime_factors x \ p > (0::int)" by (simp add: in_prime_factors_imp_prime prime_gt_0_int)
lemma prime_factors_ge_0_int [elim]: (* FIXME !? *) fixes n :: int shows"p \ prime_factors n \ p \ 0" by (drule prime_factors_gt_0_int) simp
lemma prod_mset_prime_factorization_int: fixes n :: int assumes"n > 0" shows"prod_mset (prime_factorization n) = n" using assms by (simp add: prod_mset_prime_factorization)
lemma prime_factorization_exists_nat: "n > 0 \ (\M. (\p::nat \ set_mset M. prime p) \ n = (\i \# M. i))" using prime_factorization_exists[of n] by auto
lemma prime_factorization_nat: "n > (0::nat) \ n = (\p \ prime_factors n. p ^ multiplicity p n)" by (simp add: prod_prime_factors)
lemma prime_factorization_int: "n > (0::int) \ n = (\p \ prime_factors n. p ^ multiplicity p n)" by (simp add: prod_prime_factors)
lemma prime_factorization_unique_nat: fixes f :: "nat \ _" assumes S_eq: "S = {p. 0 < f p}" and"finite S" and S: "\p\S. prime p" "n = (\p\S. p ^ f p)" shows"S = prime_factors n \ (\p. prime p \ f p = multiplicity p n)" using assms by (intro prime_factorization_unique'') auto
lemma prime_factorization_unique_int: fixes f :: "int \ _" assumes S_eq: "S = {p. 0 < f p}" and"finite S" and S: "\p\S. prime p" "abs n = (\p\S. p ^ f p)" shows"S = prime_factors n \ (\p. prime p \ f p = multiplicity p n)" using assms by (intro prime_factorization_unique'') auto
lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \
finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S" by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
lemma prime_factors_characterization'_nat: "finite {p. 0 < f (p::nat)} \
(\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}" by (rule prime_factors_characterization_nat) auto
lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \ finite S \ \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S" by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
(* TODO Move *) lemma abs_prod: "abs (prod f A :: 'a :: linordered_idom) = prod (\x. abs (f x)) A" by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
lemma primes_characterization'_int [rule_format]: "finite {p. p \ 0 \ 0 < f (p::int)} \ \p. 0 < f p \ prime p \
prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}" by (rule prime_factors_characterization_int) (auto simp: abs_prod prime_ge_0_int)
lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \ finite S \ \p\S. prime p \ prime p \
n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p" by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \
(\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow>
multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p" by (intro impI, rule multiplicity_characterization_nat) auto
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \
finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p" by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric])
(auto simp: abs_prod power_abs prime_ge_0_int intro!: prod.cong)
lemma multiplicity_characterization'_int [rule_format]: "finite {p. p \ 0 \ 0 < f (p::int)} \
(\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow>
multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p" by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0" unfolding One_nat_def [symmetric] by (rule multiplicity_one)
lemma multiplicity_eq_nat: fixes x and y::nat assumes"x > 0""y > 0""\p. prime p \ multiplicity p x = multiplicity p y" shows"x = y" using multiplicity_eq_imp_eq[of x y] assms by simp
lemma multiplicity_eq_int: fixes x y :: int assumes"x > 0""y > 0""\p. prime p \ multiplicity p x = multiplicity p y" shows"x = y" using multiplicity_eq_imp_eq[of x y] assms by simp
lemma multiplicity_prod_prime_powers: assumes"finite S""\x. x \ S \ prime x" "prime p" shows"multiplicity p (\p \ S. p ^ f p) = (if p \ S then f p else 0)" proof -
define g where"g = (\x. if x \ S then f x else 0)"
define A where"A = Abs_multiset g" have"{x. g x > 0} \ S" by (auto simp: g_def) from finite_subset[OF this assms(1)] have [simp]: "finite {x. 0 < g x}" by simp from assms have count_A: "count A x = g x"for x unfolding A_def by simp have set_mset_A: "set_mset A = {x\S. f x > 0}" unfolding set_mset_def count_A by (auto simp: g_def) with assms have prime: "prime x"if"x \# A" for x using that by auto from set_mset_A assms have"(\p \ S. p ^ f p) = (\p \ S. p ^ g p) " by (intro prod.cong) (auto simp: g_def) alsofrom set_mset_A assms have"\ = (\p \ set_mset A. p ^ g p)" by (intro prod.mono_neutral_right) (auto simp: g_def set_mset_A) alsohave"\ = prod_mset A" by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: prod.cong) alsofrom assms have"multiplicity p \ = sum_mset (image_mset (multiplicity p) A)" by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime) alsofrom assms have"image_mset (multiplicity p) A = image_mset (\x. if x = p then 1 else 0) A" by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime) alsohave"sum_mset \ = (if p \ S then f p else 0)" by (simp add: sum_mset_delta count_A g_def) finallyshow ?thesis . qed
lemma prime_factorization_prod_mset: assumes"0 \# A" shows"prime_factorization (prod_mset A) = \\<^sub>#(image_mset prime_factorization A)" using assms by (induct A) (auto simp add: prime_factorization_mult)
lemma prime_factors_prod: assumes"finite A"and"0 \ f ` A" shows"prime_factors (prod f A) = \((prime_factors \ f) ` A)" using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset)
lemma prime_factors_fact: "prime_factors (fact n) = {p \ {2..n}. prime p}" (is "?M = ?N") proof (rule set_eqI) fix p
{ fix m :: nat assume"p \ prime_factors m" thenhave"prime p"and"p dvd m"by auto moreoverassume"m > 0" ultimatelyhave"2 \ p" and "p \ m" by (auto intro: prime_ge_2_nat dest: dvd_imp_le) moreoverassume"m \ n" ultimatelyhave"2 \ p" and "p \ n" by (auto intro: order_trans)
} note * = this show"p \ ?M \ p \ ?N" by (auto simp add: fact_prod prime_factors_prod Suc_le_eq dest!: prime_prime_factors intro: *) qed
lemma prime_dvd_fact_iff: assumes"prime p" shows"p dvd fact n \ p \ n" using assms 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) moreoverhave"\ 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) moreoverhave"(fact n::nat) = fact k * fact (n-k) * (n choose k)" using binomial_fact_lemma kn by auto ultimatelyshow ?thesis using prime_n by (auto simp add: prime_dvd_mult_iff) qed
lemma (in ring_1) minus_power_prime_CHAR: assumes"p = CHAR('a)""prime p" shows"(-x :: 'a) ^ p = -(x ^ p)" proof (cases "p = 2") case False have"prime p" using assms by blast hence"odd p" using prime_imp_coprime assms False coprime_right_2_iff_odd gcd_nat.strict_iff_not by blast thus ?thesis by simp qed (use assms in\<open>auto simp: uminus_CHAR_2\<close>)
subsection \<open>Rings and fields with prime characteristic\<close>
text\<open>
We introduce some type classesfor rings and fields with prime characteristic. \<close>
class semiring_prime_char = semiring_1 + assumes prime_char_aux: "\n. prime n \ of_nat n = (0 :: 'a)" begin
lemma semiring_prime_charI [intro?]: "prime CHAR('a :: semiring_1) \ OFCLASS('a, semiring_prime_char_class)" by standard auto
lemma idom_prime_charI [intro?]: assumes"CHAR('a :: idom) > 0" shows"OFCLASS('a, semiring_prime_char_class)" proof show"prime CHAR('a)" using assms prime_CHAR_semidom by blast qed
class comm_semiring_prime_char = comm_semiring_1 + semiring_prime_char class comm_ring_prime_char = comm_ring_1 + semiring_prime_char begin subclass comm_semiring_prime_char .. end class idom_prime_char = idom + semiring_prime_char begin subclass comm_ring_prime_char .. end
class field_prime_char = field + assumes pos_char_exists: "\n>0. of_nat n = (0 :: 'a)" begin subclass idom_prime_char apply standard using pos_char_exists local.CHAR_pos_iff local.of_nat_CHAR local.prime_CHAR_semidom by blast end
lemma field_prime_charI [intro?]: "n > 0 \ of_nat n = (0 :: 'a :: field) \ OFCLASS('a, field_prime_char_class)" by standard auto
lemma field_prime_charI' [intro?]: "CHAR('a :: field) > 0 \ OFCLASS('a, field_prime_char_class)" by standard auto
subsection \<open>Finite fields\<close>
class finite_field = field_prime_char + finite
lemma finite_fieldI [intro?]: assumes"finite (UNIV :: 'a :: field set)" shows"OFCLASS('a, finite_field_class)" proof standard show"\n>0. of_nat n = (0 :: 'a)" using assms prime_CHAR_semidom[where ?'a = 'a] finite_imp_CHAR_pos[OF assms] by (intro exI[of _ "CHAR('a)"]) auto qed fact+
text\<open>
On a finite field with\<open>n\<close> elements, taking the \<open>n\<close>-th power of an element is the identity. This is an obvious consequence of the fact that the multiplicative group of
the field is a finite group of order \<open>n - 1\<close>, so \<open>x^n = 1\<close> for any non-zero \<open>x\<close>.
Note that this result is sharp in the sense that the multiplicative group of a
finite field is cyclic, i.e.\ it contains an element of order \<open>n - 1\<close>.
(We don't prove this here.) \<close> lemma finite_field_power_card_eq_same: fixes x :: "'a :: finite_field" shows"x ^ card (UNIV :: 'a set) = x" proof (cases "x = 0") case False have"x * (\y\UNIV-{0}. x * y) = x * x ^ (card (UNIV :: 'a set) - 1) * \(UNIV-{0})" by (simp add: prod.distrib mult_ac) alsohave"x * x ^ (card (UNIV :: 'a set) - 1) = x ^ Suc (card (UNIV :: 'a set) - 1)" by (subst power_Suc) auto alsohave"Suc (card (UNIV :: 'a set) - 1) = card (UNIV :: 'a set)" using finite_UNIV_card_ge_0[where ?'a = 'a] by simp alsohave"(\y\UNIV-{0}. x * y) = (\y\UNIV-{0}. y)" by (rule prod.reindex_bij_witness[of _ "\y. y / x" "\y. x * y"]) (use False in auto) finallyshow ?thesis by simp qed (use finite_UNIV_card_ge_0[where ?'a = 'a] in auto)
lemma finite_field_power_card_power_eq_same: fixes x :: "'a :: finite_field" assumes"m = card (UNIV :: 'a set) ^ n" shows"x ^ m = x" unfolding assms by (induction n) (simp_all add: finite_field_power_card_eq_same power_mult)
class enum_finite_field = finite_field + fixes enum_finite_field :: "nat \ 'a" assumes enum_finite_field: "enum_finite_field ` {.. begin
lemma inj_on_enum_finite_field: "inj_on enum_finite_field {.. using enum_finite_field by (simp add: eq_card_imp_inj_on)
end
text\<open> To get rid of the pending sort hypotheses, we prove that the field with 2 elements is indeed
a finite field. \<close> typedef gf2 = "{0, 1 :: nat}" by auto
setup_lifting type_definition_gf2
instantiation gf2 :: field begin
lift_definition zero_gf2 :: "gf2"is"0"by auto
lift_definition one_gf2 :: "gf2"is"1"by auto
lift_definition uminus_gf2 :: "gf2 \ gf2" is "\x. x" .
lift_definition plus_gf2 :: "gf2 \ gf2 \ gf2" is "\x y. if x = y then 0 else 1" by auto
lift_definition minus_gf2 :: "gf2 \ gf2 \ gf2" is "\x y. if x = y then 0 else 1" by auto
lift_definition times_gf2 :: "gf2 \ gf2 \ gf2" is "\x y. x * y" by auto
lift_definition inverse_gf2 :: "gf2 \ gf2" is "\x. x" .
lift_definition divide_gf2 :: "gf2 \ gf2 \ gf2" is "\x y. x * y" by auto
instance by standard (transfer; fastforce)+
end
instance gf2 :: finite_field proof interpret type_definition Rep_gf2 Abs_gf2 "{0, 1 :: nat}" by (rule type_definition_gf2) show"finite (UNIV :: gf2 set)" by (metis Abs_image finite.emptyI finite.insertI finite_imageI) qed
subsection \<open>The Freshman's Dream in rings of prime characteristic\<close>
lemma (in comm_semiring_1) freshmans_dream: fixes x y :: 'a and n :: nat assumes"prime CHAR('a)" assumes n_def: "n = CHAR('a)" shows"(x + y) ^ n = x ^ n + y ^ n" proof - interpret comm_semiring_prime_char by standard (auto intro!: exI[of _ "CHAR('a)"] assms) have"n > 0" unfolding n_def by simp have"(x + y) ^ n = (\k\n. of_nat (n choose k) * x ^ k * y ^ (n - k))" by (rule binomial_ring) alsohave"\ = (\k\{0,n}. of_nat (n choose k) * x ^ k * y ^ (n - k))" proof (intro sum.mono_neutral_right ballI) fix k assume"k \ {..n} - {0, n}" hence k: "k > 0""k < n" by auto have"CHAR('a) dvd (n choose k)" unfolding n_def by (rule dvd_choose_prime) (use k in\<open>auto simp: n_def\<close>) hence"of_nat (n choose k) = (0 :: 'a)" using of_nat_eq_0_iff_char_dvd by blast thus"of_nat (n choose k) * x ^ k * y ^ (n - k) = 0" by simp qed auto finallyshow ?thesis using\<open>n > 0\<close> by (simp add: add_ac) qed
lemma (in comm_semiring_1) freshmans_dream': assumes [simp]: "prime CHAR('a)"and"m = CHAR('a) ^ n" shows"(x + y :: 'a) ^ m = x ^ m + y ^ m" unfolding assms(2) proof (induction n) case (Suc n) have"(x + y) ^ (CHAR('a) ^ n * CHAR('a)) = ((x + y) ^ (CHAR('a) ^ n)) ^ CHAR('a)" by (rule power_mult) thus ?case by (simp add: Suc.IH freshmans_dream Groups.mult_ac flip: power_mult) qed auto
lemma (in comm_semiring_1) freshmans_dream_sum: fixes f :: "'b \ 'a" assumes"prime CHAR('a)"and"n = CHAR('a)" shows"sum f A ^ n = sum (\i. f i ^ n) A" using assms by (induct A rule: infinite_finite_induct)
(auto simp add: power_0_left freshmans_dream)
lemma (in comm_semiring_1) freshmans_dream_sum': fixes f :: "'b \ 'a" assumes"prime CHAR('a)""m = CHAR('a) ^ n" shows"sum f A ^ m = sum (\i. f i ^ m) A" using assms by (induction A rule: infinite_finite_induct)
(auto simp: freshmans_dream' power_0_left)
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.26Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
