src/HOL/Number_Theory/Primes.thy
author huffman
Thu Sep 12 15:08:07 2013 -0700 (2013-09-12)
changeset 53598 2bd8d459ebae
parent 47108 2a1953f0d20d
child 54228 229282d53781
permissions -rw-r--r--
remove unneeded assumption from prime_dvd_power lemmas;
add iff forms of prime_dvd_power lemmas (thanks to Jason Dagit)
     1 (*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     2                 Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
     3 
     4 
     5 This file deals with properties of primes. Definitions and lemmas are
     6 proved uniformly for the natural numbers and integers.
     7 
     8 This file combines and revises a number of prior developments.
     9 
    10 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    11 and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
    12 gcd, lcm, and prime for the natural numbers.
    13 
    14 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    15 extended gcd, lcm, primes to the integers. Amine Chaieb provided
    16 another extension of the notions to the integers, and added a number
    17 of results to "Primes" and "GCD". IntPrimes also defined and developed
    18 the congruence relations on the integers. The notion was extended to
    19 the natural numbers by Chaieb.
    20 
    21 Jeremy Avigad combined all of these, made everything uniform for the
    22 natural numbers and the integers, and added a number of new theorems.
    23 
    24 Tobias Nipkow cleaned up a lot.
    25 *)
    26 
    27 
    28 header {* Primes *}
    29 
    30 theory Primes
    31 imports "~~/src/HOL/GCD"
    32 begin
    33 
    34 class prime = one +
    35   fixes prime :: "'a \<Rightarrow> bool"
    36 
    37 instantiation nat :: prime
    38 begin
    39 
    40 definition prime_nat :: "nat \<Rightarrow> bool"
    41   where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    42 
    43 instance ..
    44 
    45 end
    46 
    47 instantiation int :: prime
    48 begin
    49 
    50 definition prime_int :: "int \<Rightarrow> bool"
    51   where "prime_int p = prime (nat p)"
    52 
    53 instance ..
    54 
    55 end
    56 
    57 
    58 subsection {* Set up Transfer *}
    59 
    60 lemma transfer_nat_int_prime:
    61   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
    62   unfolding gcd_int_def lcm_int_def prime_int_def by auto
    63 
    64 declare transfer_morphism_nat_int[transfer add return:
    65     transfer_nat_int_prime]
    66 
    67 lemma transfer_int_nat_prime: "prime (int x) = prime x"
    68   unfolding gcd_int_def lcm_int_def prime_int_def by auto
    69 
    70 declare transfer_morphism_int_nat[transfer add return:
    71     transfer_int_nat_prime]
    72 
    73 
    74 subsection {* Primes *}
    75 
    76 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    77   unfolding prime_nat_def
    78   by (metis gcd_lcm_complete_lattice_nat.bot_least nat_even_iff_2_dvd nat_neq_iff odd_1_nat)
    79 
    80 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    81   unfolding prime_int_def
    82   apply (frule prime_odd_nat)
    83   apply (auto simp add: even_nat_def)
    84   done
    85 
    86 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
    87 
    88 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
    89   unfolding prime_nat_def by auto
    90 
    91 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
    92   unfolding prime_nat_def by auto
    93 
    94 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
    95   unfolding prime_nat_def by auto
    96 
    97 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
    98   unfolding prime_nat_def by auto
    99 
   100 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
   101   unfolding prime_nat_def by auto
   102 
   103 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
   104   unfolding prime_nat_def by auto
   105 
   106 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
   107   unfolding prime_nat_def by auto
   108 
   109 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
   110   unfolding prime_int_def prime_nat_def by auto
   111 
   112 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
   113   unfolding prime_int_def prime_nat_def by auto
   114 
   115 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
   116   unfolding prime_int_def prime_nat_def by auto
   117 
   118 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
   119   unfolding prime_int_def prime_nat_def by auto
   120 
   121 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
   122   unfolding prime_int_def prime_nat_def by auto
   123 
   124 
   125 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
   126     m = 1 \<or> m = p))"
   127   using prime_nat_def [transferred]
   128   apply (cases "p >= 0")
   129   apply blast
   130   apply (auto simp add: prime_ge_0_int)
   131   done
   132 
   133 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   134   apply (unfold prime_nat_def)
   135   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
   136   done
   137 
   138 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   139   apply (unfold prime_int_altdef)
   140   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
   141   done
   142 
   143 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   144   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
   145 
   146 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   147   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
   148 
   149 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
   150     p dvd m * n = (p dvd m \<or> p dvd n)"
   151   by (rule iffI, rule prime_dvd_mult_nat, auto)
   152 
   153 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
   154     p dvd m * n = (p dvd m \<or> p dvd n)"
   155   by (rule iffI, rule prime_dvd_mult_int, auto)
   156 
   157 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   158     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   159   unfolding prime_nat_def dvd_def apply auto
   160   by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
   161       n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
   162 
   163 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   164     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   165   unfolding prime_int_altdef dvd_def
   166   apply auto
   167   by (metis div_mult_self1_is_id div_mult_self2_is_id
   168       int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
   169 
   170 lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   171   by (induct n) auto
   172 
   173 lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   174   apply (induct n)
   175   apply (frule prime_ge_0_int)
   176   apply auto
   177   done
   178 
   179 lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
   180     p dvd x^n \<longleftrightarrow> p dvd x"
   181   by (cases n) (auto elim: prime_dvd_power_nat)
   182 
   183 lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
   184     p dvd x^n \<longleftrightarrow> p dvd x"
   185   by (cases n) (auto elim: prime_dvd_power_int)
   186 
   187 
   188 subsubsection {* Make prime naively executable *}
   189 
   190 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   191   by (simp add: prime_nat_def)
   192 
   193 lemma zero_not_prime_int [simp]: "~prime (0::int)"
   194   by (simp add: prime_int_def)
   195 
   196 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
   197   by (simp add: prime_nat_def)
   198 
   199 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   200   by (simp add: prime_nat_def One_nat_def)
   201 
   202 lemma one_not_prime_int [simp]: "~prime (1::int)"
   203   by (simp add: prime_int_def)
   204 
   205 lemma prime_nat_code [code]:
   206     "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   207   apply (simp add: Ball_def)
   208   apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
   209   done
   210 
   211 lemma prime_nat_simp:
   212     "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   213   by (auto simp add: prime_nat_code)
   214 
   215 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
   216 
   217 lemma prime_int_code [code]:
   218   "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
   219 proof
   220   assume "?L"
   221   then show "?R"
   222     by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
   223 next
   224   assume "?R"
   225   then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
   226 qed
   227 
   228 lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
   229   by (auto simp add: prime_int_code)
   230 
   231 lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m
   232 
   233 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   234   by simp
   235 
   236 lemma two_is_prime_int [simp]: "prime (2::int)"
   237   by simp
   238 
   239 text{* A bit of regression testing: *}
   240 
   241 lemma "prime(97::nat)" by simp
   242 lemma "prime(97::int)" by simp
   243 lemma "prime(997::nat)" by eval
   244 lemma "prime(997::int)" by eval
   245 
   246 
   247 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   248   apply (rule coprime_exp_nat)
   249   apply (subst gcd_commute_nat)
   250   apply (erule (1) prime_imp_coprime_nat)
   251   done
   252 
   253 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   254   apply (rule coprime_exp_int)
   255   apply (subst gcd_commute_int)
   256   apply (erule (1) prime_imp_coprime_int)
   257   done
   258 
   259 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   260   apply (rule prime_imp_coprime_nat, assumption)
   261   apply (unfold prime_nat_def)
   262   apply auto
   263   done
   264 
   265 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   266   apply (rule prime_imp_coprime_int, assumption)
   267   apply (unfold prime_int_altdef)
   268   apply (metis int_one_le_iff_zero_less less_le)
   269   done
   270 
   271 lemma primes_imp_powers_coprime_nat:
   272     "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   273   by (rule coprime_exp2_nat, rule primes_coprime_nat)
   274 
   275 lemma primes_imp_powers_coprime_int:
   276     "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   277   by (rule coprime_exp2_int, rule primes_coprime_int)
   278 
   279 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
   280   apply (induct n rule: nat_less_induct)
   281   apply (case_tac "n = 0")
   282   using two_is_prime_nat
   283   apply blast
   284   apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
   285     nat_dvd_not_less neq0_conv prime_nat_def)
   286   done
   287 
   288 (* An Isar version:
   289 
   290 lemma prime_factor_b_nat:
   291   fixes n :: nat
   292   assumes "n \<noteq> 1"
   293   shows "\<exists>p. prime p \<and> p dvd n"
   294 
   295 using `n ~= 1`
   296 proof (induct n rule: less_induct_nat)
   297   fix n :: nat
   298   assume "n ~= 1" and
   299     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
   300   then show "\<exists>p. prime p \<and> p dvd n"
   301   proof -
   302   {
   303     assume "n = 0"
   304     moreover note two_is_prime_nat
   305     ultimately have ?thesis
   306       by (auto simp del: two_is_prime_nat)
   307   }
   308   moreover
   309   {
   310     assume "prime n"
   311     then have ?thesis by auto
   312   }
   313   moreover
   314   {
   315     assume "n ~= 0" and "~ prime n"
   316     with `n ~= 1` have "n > 1" by auto
   317     with `~ prime n` and not_prime_eq_prod_nat obtain m k where
   318       "n = m * k" and "1 < m" and "m < n" by blast
   319     with ih obtain p where "prime p" and "p dvd m" by blast
   320     with `n = m * k` have ?thesis by auto
   321   }
   322   ultimately show ?thesis by blast
   323   qed
   324 qed
   325 
   326 *)
   327 
   328 text {* One property of coprimality is easier to prove via prime factors. *}
   329 
   330 lemma prime_divprod_pow_nat:
   331   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
   332   shows "p^n dvd a \<or> p^n dvd b"
   333 proof-
   334   { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
   335       apply (cases "n=0", simp_all)
   336       apply (cases "a=1", simp_all)
   337       done }
   338   moreover
   339   { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
   340     then obtain m where m: "n = Suc m" by (cases n) auto
   341     from n have "p dvd p^n" apply (intro dvd_power) apply auto done
   342     also note pab
   343     finally have pab': "p dvd a * b".
   344     from prime_dvd_mult_nat[OF p pab']
   345     have "p dvd a \<or> p dvd b" .
   346     moreover
   347     { assume pa: "p dvd a"
   348       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
   349       with p have "coprime b p"
   350         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   351       then have pnb: "coprime (p^n) b"
   352         by (subst gcd_commute_nat, rule coprime_exp_nat)
   353       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
   354     moreover
   355     { assume pb: "p dvd b"
   356       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
   357       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
   358         by auto
   359       with p have "coprime a p"
   360         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   361       then have pna: "coprime (p^n) a"
   362         by (subst gcd_commute_nat, rule coprime_exp_nat)
   363       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
   364     ultimately have ?thesis by blast }
   365   ultimately show ?thesis by blast
   366 qed
   367 
   368 
   369 subsection {* Infinitely many primes *}
   370 
   371 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
   372 proof-
   373   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   374   from prime_factor_nat [OF f1]
   375   obtain p where "prime p" and "p dvd fact n + 1" by auto
   376   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   377   { assume "p \<le> n"
   378     from `prime p` have "p \<ge> 1" 
   379       by (cases p, simp_all)
   380     with `p <= n` have "p dvd fact n" 
   381       by (intro dvd_fact_nat)
   382     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   383       by (rule dvd_diff_nat)
   384     then have "p dvd 1" by simp
   385     then have "p <= 1" by auto
   386     moreover from `prime p` have "p > 1" by auto
   387     ultimately have False by auto}
   388   then have "n < p" by presburger
   389   with `prime p` and `p <= fact n + 1` show ?thesis by auto
   390 qed
   391 
   392 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
   393   using next_prime_bound by auto
   394 
   395 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   396 proof
   397   assume "finite {(p::nat). prime p}"
   398   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   399     by auto
   400   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   401     by auto
   402   with bigger_prime [of b] show False
   403     by auto
   404 qed
   405 
   406 end