# HG changeset patch # User haftmann # Date 1512233453 0 # Node ID 19f6274072643f85d646f78b48e4ffdb6f494a7b # Parent 7397a6df81d81242fd9d8aa5b7e3e3682a5cf34c overhauling of primes diff -r 7397a6df81d8 -r 19f627407264 src/HOL/Computational_Algebra/Primes.thy --- a/src/HOL/Computational_Algebra/Primes.thy Sat Dec 02 16:50:53 2017 +0000 +++ b/src/HOL/Computational_Algebra/Primes.thy Sat Dec 02 16:50:53 2017 +0000 @@ -42,6 +42,37 @@ imports HOL.Binomial Euclidean_Algorithm begin +subsection \Primes on @{typ nat} and @{typ int}\ + +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) + then show ?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) + then have "p \ 0" and "\p\ \ 1" and "p \ 0" + by (auto dest: prime_elem_not_zeroI prime_elem_not_unit) + then show ?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 \ p > 0 @@ -52,65 +83,161 @@ x > 0 prime x x \# M which is, unfortunately, - count M x > 0 + count M x > 0 FIXME no, this is obsolete *) -declare [[coercion int]] -declare [[coercion_enabled]] +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 Suc_0_not_prime_nat [simp]: "\ prime (Suc 0)" - using not_prime_1 [where ?'a = nat] 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: - "prime_elem (n :: nat) \ (1 < n \ (\m. m dvd n \ m = 1 \ m = n))" -proof safe - assume *: "prime_elem n" - from * have "n \ 0" "n \ 1" by (intro notI, simp del: One_nat_def)+ - thus "n > 1" by (cases n) simp_all + "prime_elem n \ prime n" for n :: nat + by (simp add: prime_def) + +lemma prime_nat_iff_prime_elem: + "prime n \ prime_elem n" for n :: nat + by (simp add: prime_elem_nat_iff) + +lemma prime_elem_iff_prime_abs: + "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 + then have "n \ 2" + by (auto dest: prime_ge_2_int) + then show ?Q + proof (rule prime_natI) + fix r s + assume "n dvd r * s" + then have "int n dvd int (r * s)" + by (simp add: zdvd_int) + then have "int n dvd int r * int s" + by simp + with \?P\ have "int n dvd int r \ int n dvd int s" + by (auto dest: prime_dvd_mult_iff) + then show "n dvd r \ n dvd s" + by (simp add: zdvd_int) + qed +next + assume ?Q + then have "int n \ 2" + by (auto dest: prime_ge_2_nat) + then show ?P + proof (rule prime_intI) + fix r s + assume "int n dvd r * s" + then have "n dvd nat \r * s\" + by (simp add: zdvd_int) + then have "n dvd nat \r\ * nat \s\" + by (simp add: nat_abs_mult_distrib) + with \?Q\ have "n dvd nat \r\ \ n dvd nat \s\" + by (auto dest: prime_dvd_mult_iff) + then show "int n dvd r \ int n dvd s" + by (simp add: zdvd_int) + qed +qed + +lemma prime_nat_iff_prime: + "prime (nat k) \ prime k" +proof (cases "k \ 0") + case True + then show ?thesis + using prime_nat_int_transfer [of "nat k"] by simp +next + case False + then show ?thesis + by (auto dest: prime_ge_2_int) +qed + +lemma prime_elem_int_nat_transfer: + "prime_elem n \ prime_elem (nat \n\)" + by (simp add: prime_elem_iff_prime_abs prime_elem_nat_iff prime_nat_iff_prime) + +lemma prime_elem_nat_int_transfer [simp]: + "prime_elem (int n) \ prime_elem n" + by (simp add: prime_elem_nat_iff prime_elem_iff_prime_abs) + +lemma prime_int_nat_transfer: + "prime k \ k \ 0 \ prime (nat k)" + by (auto simp add: prime_nat_iff_prime 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" + then obtain r s where "p = r * s" "r dvd m" "s dvd n" + by (blast dest: division_decomp) + moreover have "r = 1 \ r = p" + using \r dvd m\ \p = r * s\ dvd [of r] by simp + ultimately show "p dvd m \ p dvd n" + by auto +qed (use \p \ 2\ 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 \p \ 2\ have "nat p \ 2" + by simp + then have "prime (nat p)" + proof (rule prime_nat_naiveI) + fix n + assume "n dvd nat p" + with \p \ 2\ have "n dvd nat \p\" + by simp + then have "int n dvd p" + by (simp add: int_dvd_iff) + with dvd [of "int n"] show "n = 1 \ n = nat p" + by auto + qed + then show ?thesis + by (simp add: prime_nat_iff_prime) +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" + then have *: "prime_elem n" + by simp fix m assume m: "m dvd n" "m \ n" from * \m dvd n\ have "n dvd m \ 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" - thus "prime_elem n" - by (auto simp: prime_elem_iff_irreducible irreducible_altdef) + then show "prime n" + using prime_nat_naiveI [of n] by auto qed -lemma prime_nat_iff_prime_elem: "prime (n :: nat) \ prime_elem n" - by (simp add: prime_def) - -lemma prime_nat_iff: - "prime (n :: nat) \ (1 < n \ (\m. m dvd n \ m = 1 \ m = n))" - by (simp add: prime_nat_iff_prime_elem prime_elem_nat_iff) - -lemma prime_elem_int_nat_transfer: "prime_elem (n::int) \ prime_elem (nat (abs n))" -proof - assume "prime_elem n" - thus "prime_elem (nat (abs n))" by (auto simp: prime_elem_def nat_dvd_iff) -next - assume "prime_elem (nat (abs n))" - thus "prime_elem n" - by (auto simp: dvd_int_unfold_dvd_nat prime_elem_def abs_mult nat_mult_distrib) -qed - -lemma prime_elem_nat_int_transfer [simp]: "prime_elem (int n) \ prime_elem n" - by (auto simp: prime_elem_int_nat_transfer) - -lemma prime_nat_int_transfer [simp]: "prime (int n) \ prime n" - by (auto simp: prime_elem_int_nat_transfer prime_def) - -lemma prime_int_nat_transfer: "prime (k::int) \ k \ 0 \ prime (nat k)" - by (auto simp: prime_elem_int_nat_transfer prime_def) - -lemma prime_elem_iff_prime_abs: - "prime_elem k \ prime \k\" for k :: int - by (auto intro: primeI) - -lemma prime_nat_iff_prime: - "prime (nat k) \ prime k" - by (cases "k \ 0") (simp_all add: prime_int_nat_transfer) - 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)?) @@ -138,7 +265,6 @@ unfolding prime_int_nat_transfer prime_nat_iff by auto qed - lemma prime_nat_not_dvd: assumes "prime p" "p > n" "n \ (1::nat)" shows "\n dvd p" @@ -165,39 +291,6 @@ lemma prime_odd_int: "prime p \ p > (2::int) \ odd p" by (intro prime_int_not_dvd) auto -lemma prime_ge_0_int: "prime p \ p \ (0::int)" - unfolding prime_int_iff by auto - -lemma prime_gt_0_nat: "prime p \ p > (0::nat)" - unfolding prime_nat_iff by auto - -lemma prime_gt_0_int: "prime p \ p > (0::int)" - unfolding prime_int_iff by auto - -lemma prime_ge_1_nat: "prime p \ p \ (1::nat)" - unfolding prime_nat_iff by auto - -lemma prime_ge_Suc_0_nat: "prime p \ p \ Suc 0" - unfolding prime_nat_iff by auto - -lemma prime_ge_1_int: "prime p \ p \ (1::int)" - unfolding prime_int_iff by auto - -lemma prime_gt_1_nat: "prime p \ p > (1::nat)" - unfolding prime_nat_iff by auto - -lemma prime_gt_Suc_0_nat: "prime p \ p > Suc 0" - unfolding prime_nat_iff by auto - -lemma prime_gt_1_int: "prime p \ p > (1::int)" - unfolding prime_int_iff by auto - -lemma prime_ge_2_nat: "prime p \ p \ (2::nat)" - unfolding prime_nat_iff by auto - -lemma prime_ge_2_int: "prime p \ p \ (2::int)" - unfolding prime_int_iff by auto - lemma prime_int_altdef: "prime p = (1 < p \ (\m::int. m \ 0 \ m dvd p \ m = 1 \ m = p))" @@ -210,7 +303,8 @@ by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef) -subsection\Largest exponent of a prime factor\ +subsection \Largest exponent of a prime factor\ + text\Possibly duplicates other material, but avoid the complexities of multisets.\ lemma prime_power_cancel_less: @@ -360,7 +454,7 @@ by auto qed -subsection\Powers of Primes\ +subsection \Powers of Primes\ text\Versions for type nat only\