src/HOL/Number_Theory/Primes.thy
author wenzelm
Sat Sep 10 23:27:32 2011 +0200 (2011-09-10)
changeset 44872 a98ef45122f3
parent 44821 a92f65e174cf
child 45605 a89b4bc311a5
permissions -rw-r--r--
misc tuning;
     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 [rule_format]: "prime (p::nat) -->
   171     n > 0 --> (p dvd x^n --> p dvd x)"
   172   by (induct n rule: nat_induct) auto
   173 
   174 lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
   175     n > 0 --> (p dvd x^n --> p dvd x)"
   176   apply (induct n rule: nat_induct)
   177   apply auto
   178   apply (frule prime_ge_0_int)
   179   apply auto
   180   done
   181 
   182 subsubsection {* Make prime naively executable *}
   183 
   184 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   185   by (simp add: prime_nat_def)
   186 
   187 lemma zero_not_prime_int [simp]: "~prime (0::int)"
   188   by (simp add: prime_int_def)
   189 
   190 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
   191   by (simp add: prime_nat_def)
   192 
   193 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   194   by (simp add: prime_nat_def One_nat_def)
   195 
   196 lemma one_not_prime_int [simp]: "~prime (1::int)"
   197   by (simp add: prime_int_def)
   198 
   199 lemma prime_nat_code [code]:
   200     "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   201   apply (simp add: Ball_def)
   202   apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
   203   done
   204 
   205 lemma prime_nat_simp:
   206     "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   207   by (auto simp add: prime_nat_code)
   208 
   209 lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
   210 
   211 lemma prime_int_code [code]:
   212   "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
   213 proof
   214   assume "?L"
   215   then show "?R"
   216     by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
   217 next
   218   assume "?R"
   219   then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
   220 qed
   221 
   222 lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
   223   by (auto simp add: prime_int_code)
   224 
   225 lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
   226 
   227 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   228   by simp
   229 
   230 lemma two_is_prime_int [simp]: "prime (2::int)"
   231   by simp
   232 
   233 text{* A bit of regression testing: *}
   234 
   235 lemma "prime(97::nat)" by simp
   236 lemma "prime(97::int)" by simp
   237 lemma "prime(997::nat)" by eval
   238 lemma "prime(997::int)" by eval
   239 
   240 
   241 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   242   apply (rule coprime_exp_nat)
   243   apply (subst gcd_commute_nat)
   244   apply (erule (1) prime_imp_coprime_nat)
   245   done
   246 
   247 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   248   apply (rule coprime_exp_int)
   249   apply (subst gcd_commute_int)
   250   apply (erule (1) prime_imp_coprime_int)
   251   done
   252 
   253 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   254   apply (rule prime_imp_coprime_nat, assumption)
   255   apply (unfold prime_nat_def)
   256   apply auto
   257   done
   258 
   259 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   260   apply (rule prime_imp_coprime_int, assumption)
   261   apply (unfold prime_int_altdef)
   262   apply (metis int_one_le_iff_zero_less less_le)
   263   done
   264 
   265 lemma primes_imp_powers_coprime_nat:
   266     "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   267   by (rule coprime_exp2_nat, rule primes_coprime_nat)
   268 
   269 lemma primes_imp_powers_coprime_int:
   270     "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   271   by (rule coprime_exp2_int, rule primes_coprime_int)
   272 
   273 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
   274   apply (induct n rule: nat_less_induct)
   275   apply (case_tac "n = 0")
   276   using two_is_prime_nat
   277   apply blast
   278   apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
   279     nat_dvd_not_less neq0_conv prime_nat_def)
   280   done
   281 
   282 (* An Isar version:
   283 
   284 lemma prime_factor_b_nat:
   285   fixes n :: nat
   286   assumes "n \<noteq> 1"
   287   shows "\<exists>p. prime p \<and> p dvd n"
   288 
   289 using `n ~= 1`
   290 proof (induct n rule: less_induct_nat)
   291   fix n :: nat
   292   assume "n ~= 1" and
   293     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
   294   then show "\<exists>p. prime p \<and> p dvd n"
   295   proof -
   296   {
   297     assume "n = 0"
   298     moreover note two_is_prime_nat
   299     ultimately have ?thesis
   300       by (auto simp del: two_is_prime_nat)
   301   }
   302   moreover
   303   {
   304     assume "prime n"
   305     then have ?thesis by auto
   306   }
   307   moreover
   308   {
   309     assume "n ~= 0" and "~ prime n"
   310     with `n ~= 1` have "n > 1" by auto
   311     with `~ prime n` and not_prime_eq_prod_nat obtain m k where
   312       "n = m * k" and "1 < m" and "m < n" by blast
   313     with ih obtain p where "prime p" and "p dvd m" by blast
   314     with `n = m * k` have ?thesis by auto
   315   }
   316   ultimately show ?thesis by blast
   317   qed
   318 qed
   319 
   320 *)
   321 
   322 text {* One property of coprimality is easier to prove via prime factors. *}
   323 
   324 lemma prime_divprod_pow_nat:
   325   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
   326   shows "p^n dvd a \<or> p^n dvd b"
   327 proof-
   328   { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
   329       apply (cases "n=0", simp_all)
   330       apply (cases "a=1", simp_all)
   331       done }
   332   moreover
   333   { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
   334     then obtain m where m: "n = Suc m" by (cases n) auto
   335     from n have "p dvd p^n" apply (intro dvd_power) apply auto done
   336     also note pab
   337     finally have pab': "p dvd a * b".
   338     from prime_dvd_mult_nat[OF p pab']
   339     have "p dvd a \<or> p dvd b" .
   340     moreover
   341     { assume pa: "p dvd a"
   342       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
   343       with p have "coprime b p"
   344         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   345       then have pnb: "coprime (p^n) b"
   346         by (subst gcd_commute_nat, rule coprime_exp_nat)
   347       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
   348     moreover
   349     { assume pb: "p dvd b"
   350       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
   351       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
   352         by auto
   353       with p have "coprime a p"
   354         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   355       then have pna: "coprime (p^n) a"
   356         by (subst gcd_commute_nat, rule coprime_exp_nat)
   357       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
   358     ultimately have ?thesis by blast }
   359   ultimately show ?thesis by blast
   360 qed
   361 
   362 
   363 subsection {* Infinitely many primes *}
   364 
   365 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
   366 proof-
   367   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   368   from prime_factor_nat [OF f1]
   369   obtain p where "prime p" and "p dvd fact n + 1" by auto
   370   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   371   { assume "p \<le> n"
   372     from `prime p` have "p \<ge> 1" 
   373       by (cases p, simp_all)
   374     with `p <= n` have "p dvd fact n" 
   375       by (intro dvd_fact_nat)
   376     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   377       by (rule dvd_diff_nat)
   378     then have "p dvd 1" by simp
   379     then have "p <= 1" by auto
   380     moreover from `prime p` have "p > 1" by auto
   381     ultimately have False by auto}
   382   then have "n < p" by presburger
   383   with `prime p` and `p <= fact n + 1` show ?thesis by auto
   384 qed
   385 
   386 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
   387   using next_prime_bound by auto
   388 
   389 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   390 proof
   391   assume "finite {(p::nat). prime p}"
   392   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   393     by auto
   394   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   395     by auto
   396   with bigger_prime [of b] show False
   397     by auto
   398 qed
   399 
   400 end