author haftmann Sat Dec 02 16:50:53 2017 +0000 (16 months ago) changeset 67117 19f627407264 parent 67116 7397a6df81d8 child 67118 ccab07d1196c
overhauling of primes
```     1.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Sat Dec 02 16:50:53 2017 +0000
1.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Sat Dec 02 16:50:53 2017 +0000
1.3 @@ -42,6 +42,37 @@
1.4  imports HOL.Binomial Euclidean_Algorithm
1.5  begin
1.6
1.7 +subsection \<open>Primes on @{typ nat} and @{typ int}\<close>
1.8 +
1.9 +lemma Suc_0_not_prime_nat [simp]: "\<not> prime (Suc 0)"
1.10 +  using not_prime_1 [where ?'a = nat] by simp
1.11 +
1.12 +lemma prime_ge_2_nat:
1.13 +  "p \<ge> 2" if "prime p" for p :: nat
1.14 +proof -
1.15 +  from that have "p \<noteq> 0" and "p \<noteq> 1"
1.16 +    by (auto dest: prime_elem_not_zeroI prime_elem_not_unit)
1.17 +  then show ?thesis
1.18 +    by simp
1.19 +qed
1.20 +
1.21 +lemma prime_ge_2_int:
1.22 +  "p \<ge> 2" if "prime p" for p :: int
1.23 +proof -
1.24 +  from that have "prime_elem p" and "\<bar>p\<bar> = p"
1.25 +    by (auto dest: normalize_prime)
1.26 +  then have "p \<noteq> 0" and "\<bar>p\<bar> \<noteq> 1" and "p \<ge> 0"
1.27 +    by (auto dest: prime_elem_not_zeroI prime_elem_not_unit)
1.28 +  then show ?thesis
1.29 +    by simp
1.30 +qed
1.31 +
1.32 +lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
1.33 +  using prime_ge_2_int [of p] by simp
1.34 +
1.35 +lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
1.36 +  using prime_ge_2_nat [of p] by simp
1.37 +
1.38  (* As a simp or intro rule,
1.39
1.40       prime p \<Longrightarrow> p > 0
1.41 @@ -52,65 +83,161 @@
1.42       x > 0
1.43       prime x
1.44       x \<in># M   which is, unfortunately,
1.45 -     count M x > 0
1.46 +     count M x > 0  FIXME no, this is obsolete
1.47  *)
1.48
1.49 -declare [[coercion int]]
1.50 -declare [[coercion_enabled]]
1.51 +lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
1.52 +  using prime_ge_2_int [of p] by simp
1.53 +
1.54 +lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
1.55 +  using prime_ge_2_nat [of p] by simp
1.56 +
1.57 +lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
1.58 +  using prime_ge_1_nat [of p] by simp
1.59 +
1.60 +lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
1.61 +  using prime_ge_2_int [of p] by simp
1.62
1.63 -lemma Suc_0_not_prime_nat [simp]: "\<not> prime (Suc 0)"
1.64 -  using not_prime_1 [where ?'a = nat] by simp
1.65 +lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
1.66 +  using prime_ge_2_nat [of p] by simp
1.67 +
1.68 +lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
1.69 +  using prime_gt_1_nat [of p] by simp
1.70 +
1.71 +lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
1.72 +  using prime_ge_2_int [of p] by simp
1.73 +
1.74 +lemma prime_natI:
1.75 +  "prime p" if "p \<ge> 2" and "\<And>m n. p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" for p :: nat
1.76 +  using that by (auto intro!: primeI prime_elemI)
1.77 +
1.78 +lemma prime_intI:
1.79 +  "prime p" if "p \<ge> 2" and "\<And>m n. p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" for p :: int
1.80 +  using that by (auto intro!: primeI prime_elemI)
1.81
1.82  lemma prime_elem_nat_iff:
1.83 -  "prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.84 -proof safe
1.85 -  assume *: "prime_elem n"
1.86 -  from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
1.87 -  thus "n > 1" by (cases n) simp_all
1.88 +  "prime_elem n \<longleftrightarrow> prime n" for n :: nat
1.89 +  by (simp add: prime_def)
1.90 +
1.91 +lemma prime_nat_iff_prime_elem:
1.92 +  "prime n \<longleftrightarrow> prime_elem n" for n :: nat
1.93 +  by (simp add: prime_elem_nat_iff)
1.94 +
1.95 +lemma prime_elem_iff_prime_abs:
1.96 +  "prime_elem k \<longleftrightarrow> prime \<bar>k\<bar>" for k :: int
1.97 +  by (auto intro: primeI)
1.98 +
1.99 +lemma prime_nat_int_transfer [simp]:
1.100 +  "prime (int n) \<longleftrightarrow> prime n" (is "?P \<longleftrightarrow> ?Q")
1.101 +proof
1.102 +  assume ?P
1.103 +  then have "n \<ge> 2"
1.104 +    by (auto dest: prime_ge_2_int)
1.105 +  then show ?Q
1.106 +  proof (rule prime_natI)
1.107 +    fix r s
1.108 +    assume "n dvd r * s"
1.109 +    then have "int n dvd int (r * s)"
1.110 +      by (simp add: zdvd_int)
1.111 +    then have "int n dvd int r * int s"
1.112 +      by simp
1.113 +    with \<open>?P\<close> have "int n dvd int r \<or> int n dvd int s"
1.114 +      by (auto dest: prime_dvd_mult_iff)
1.115 +    then show "n dvd r \<or> n dvd s"
1.116 +      by (simp add: zdvd_int)
1.117 +  qed
1.118 +next
1.119 +  assume ?Q
1.120 +  then have "int n \<ge> 2"
1.121 +    by (auto dest: prime_ge_2_nat)
1.122 +  then show ?P
1.123 +  proof (rule prime_intI)
1.124 +    fix r s
1.125 +    assume "int n dvd r * s"
1.126 +    then have "n dvd nat \<bar>r * s\<bar>"
1.127 +      by (simp add: zdvd_int)
1.128 +    then have "n dvd nat \<bar>r\<bar> * nat \<bar>s\<bar>"
1.129 +      by (simp add: nat_abs_mult_distrib)
1.130 +    with \<open>?Q\<close> have "n dvd nat \<bar>r\<bar> \<or> n dvd nat \<bar>s\<bar>"
1.131 +      by (auto dest: prime_dvd_mult_iff)
1.132 +    then show "int n dvd r \<or> int n dvd s"
1.133 +      by (simp add: zdvd_int)
1.134 +  qed
1.135 +qed
1.136 +
1.137 +lemma prime_nat_iff_prime:
1.138 +  "prime (nat k) \<longleftrightarrow> prime k"
1.139 +proof (cases "k \<ge> 0")
1.140 +  case True
1.141 +  then show ?thesis
1.142 +    using prime_nat_int_transfer [of "nat k"] by simp
1.143 +next
1.144 +  case False
1.145 +  then show ?thesis
1.146 +    by (auto dest: prime_ge_2_int)
1.147 +qed
1.148 +
1.149 +lemma prime_elem_int_nat_transfer:
1.150 +  "prime_elem n \<longleftrightarrow> prime_elem (nat \<bar>n\<bar>)"
1.151 +  by (simp add: prime_elem_iff_prime_abs prime_elem_nat_iff prime_nat_iff_prime)
1.152 +
1.153 +lemma prime_elem_nat_int_transfer [simp]:
1.154 +  "prime_elem (int n) \<longleftrightarrow> prime_elem n"
1.155 +  by (simp add: prime_elem_nat_iff prime_elem_iff_prime_abs)
1.156 +
1.157 +lemma prime_int_nat_transfer:
1.158 +  "prime k \<longleftrightarrow> k \<ge> 0 \<and> prime (nat k)"
1.159 +  by (auto simp add: prime_nat_iff_prime dest: prime_ge_2_int)
1.160 +
1.161 +lemma prime_nat_naiveI:
1.162 +  "prime p" if "p \<ge> 2" and dvd: "\<And>n. n dvd p \<Longrightarrow> n = 1 \<or> n = p" for p :: nat
1.163 +proof (rule primeI, rule prime_elemI)
1.164 +  fix m n :: nat
1.165 +  assume "p dvd m * n"
1.166 +  then obtain r s where "p = r * s" "r dvd m" "s dvd n"
1.167 +    by (blast dest: division_decomp)
1.168 +  moreover have "r = 1 \<or> r = p"
1.169 +    using \<open>r dvd m\<close> \<open>p = r * s\<close> dvd [of r] by simp
1.170 +  ultimately show "p dvd m \<or> p dvd n"
1.171 +    by auto
1.172 +qed (use \<open>p \<ge> 2\<close> in simp_all)
1.173 +
1.174 +lemma prime_int_naiveI:
1.175 +  "prime p" if "p \<ge> 2" and dvd: "\<And>k. k dvd p \<Longrightarrow> \<bar>k\<bar> = 1 \<or> \<bar>k\<bar> = p" for p :: int
1.176 +proof -
1.177 +  from \<open>p \<ge> 2\<close> have "nat p \<ge> 2"
1.178 +    by simp
1.179 +  then have "prime (nat p)"
1.180 +  proof (rule prime_nat_naiveI)
1.181 +    fix n
1.182 +    assume "n dvd nat p"
1.183 +    with \<open>p \<ge> 2\<close> have "n dvd nat \<bar>p\<bar>"
1.184 +      by simp
1.185 +    then have "int n dvd p"
1.186 +      by (simp add: int_dvd_iff)
1.187 +    with dvd [of "int n"] show "n = 1 \<or> n = nat p"
1.188 +      by auto
1.189 +  qed
1.190 +  then show ?thesis
1.191 +    by (simp add: prime_nat_iff_prime)
1.192 +qed
1.193 +
1.194 +lemma prime_nat_iff:
1.195 +  "prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.196 +proof (safe intro!: prime_gt_1_nat)
1.197 +  assume "prime n"
1.198 +  then have *: "prime_elem n"
1.199 +    by simp
1.200    fix m assume m: "m dvd n" "m \<noteq> n"
1.201    from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
1.202      by (intro irreducibleD' prime_elem_imp_irreducible)
1.203    with m show "m = 1" by (auto dest: dvd_antisym)
1.204  next
1.205    assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
1.206 -  thus "prime_elem n"
1.207 -    by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
1.208 +  then show "prime n"
1.209 +    using prime_nat_naiveI [of n] by auto
1.210  qed
1.211
1.212 -lemma prime_nat_iff_prime_elem: "prime (n :: nat) \<longleftrightarrow> prime_elem n"
1.213 -  by (simp add: prime_def)
1.214 -
1.215 -lemma prime_nat_iff:
1.216 -  "prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.217 -  by (simp add: prime_nat_iff_prime_elem prime_elem_nat_iff)
1.218 -
1.219 -lemma prime_elem_int_nat_transfer: "prime_elem (n::int) \<longleftrightarrow> prime_elem (nat (abs n))"
1.220 -proof
1.221 -  assume "prime_elem n"
1.222 -  thus "prime_elem (nat (abs n))" by (auto simp: prime_elem_def nat_dvd_iff)
1.223 -next
1.224 -  assume "prime_elem (nat (abs n))"
1.225 -  thus "prime_elem n"
1.226 -    by (auto simp: dvd_int_unfold_dvd_nat prime_elem_def abs_mult nat_mult_distrib)
1.227 -qed
1.228 -
1.229 -lemma prime_elem_nat_int_transfer [simp]: "prime_elem (int n) \<longleftrightarrow> prime_elem n"
1.230 -  by (auto simp: prime_elem_int_nat_transfer)
1.231 -
1.232 -lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n"
1.233 -  by (auto simp: prime_elem_int_nat_transfer prime_def)
1.234 -
1.235 -lemma prime_int_nat_transfer: "prime (k::int) \<longleftrightarrow> k \<ge> 0 \<and> prime (nat k)"
1.236 -  by (auto simp: prime_elem_int_nat_transfer prime_def)
1.237 -
1.238 -lemma prime_elem_iff_prime_abs:
1.239 -  "prime_elem k \<longleftrightarrow> prime \<bar>k\<bar>" for k :: int
1.240 -  by (auto intro: primeI)
1.241 -
1.242 -lemma prime_nat_iff_prime:
1.243 -  "prime (nat k) \<longleftrightarrow> prime k"
1.244 -  by (cases "k \<ge> 0") (simp_all add: prime_int_nat_transfer)
1.245 -
1.246  lemma prime_int_iff:
1.247    "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
1.248  proof (intro iffI conjI allI impI; (elim conjE)?)
1.249 @@ -138,7 +265,6 @@
1.250      unfolding prime_int_nat_transfer prime_nat_iff by auto
1.251  qed
1.252
1.253 -
1.254  lemma prime_nat_not_dvd:
1.255    assumes "prime p" "p > n" "n \<noteq> (1::nat)"
1.256    shows   "\<not>n dvd p"
1.257 @@ -165,39 +291,6 @@
1.258  lemma prime_odd_int: "prime p \<Longrightarrow> p > (2::int) \<Longrightarrow> odd p"
1.259    by (intro prime_int_not_dvd) auto
1.260
1.261 -lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
1.262 -  unfolding prime_int_iff by auto
1.263 -
1.264 -lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
1.265 -  unfolding prime_nat_iff by auto
1.266 -
1.267 -lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
1.268 -  unfolding prime_int_iff by auto
1.269 -
1.270 -lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
1.271 -  unfolding prime_nat_iff by auto
1.272 -
1.273 -lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
1.274 -  unfolding prime_nat_iff by auto
1.275 -
1.276 -lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
1.277 -  unfolding prime_int_iff by auto
1.278 -
1.279 -lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
1.280 -  unfolding prime_nat_iff by auto
1.281 -
1.282 -lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
1.283 -  unfolding prime_nat_iff by auto
1.284 -
1.285 -lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
1.286 -  unfolding prime_int_iff by auto
1.287 -
1.288 -lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
1.289 -  unfolding prime_nat_iff by auto
1.290 -
1.291 -lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
1.292 -  unfolding prime_int_iff by auto
1.293 -
1.294  lemma prime_int_altdef:
1.295    "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
1.296      m = 1 \<or> m = p))"
1.297 @@ -210,7 +303,8 @@
1.298    by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
1.299
1.300
1.301 -subsection\<open>Largest exponent of a prime factor\<close>
1.302 +subsection \<open>Largest exponent of a prime factor\<close>
1.303 +
1.304  text\<open>Possibly duplicates other material, but avoid the complexities of multisets.\<close>
1.305
1.306  lemma prime_power_cancel_less:
1.307 @@ -360,7 +454,7 @@
1.308      by auto
1.309  qed
1.310
1.311 -subsection\<open>Powers of Primes\<close>
1.312 +subsection \<open>Powers of Primes\<close>
1.313
1.314  text\<open>Versions for type nat only\<close>
1.315
```