overhauling of primes
authorhaftmann
Sat Dec 02 16:50:53 2017 +0000 (7 months ago)
changeset 6711719f627407264
parent 67116 7397a6df81d8
child 67118 ccab07d1196c
overhauling of primes
src/HOL/Computational_Algebra/Primes.thy
     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 Suc_0_not_prime_nat [simp]: "\<not> prime (Suc 0)"
    1.55 -  using not_prime_1 [where ?'a = nat] by simp
    1.56 +lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
    1.57 +  using prime_ge_2_nat [of p] by simp
    1.58 +
    1.59 +lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
    1.60 +  using prime_ge_1_nat [of p] by simp
    1.61 +
    1.62 +lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
    1.63 +  using prime_ge_2_int [of p] by simp
    1.64 +
    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