src/HOL/Number_Theory/Primes.thy
author paulson <lp15@cam.ac.uk>
Fri Jan 24 15:21:00 2014 +0000 (2014-01-24)
changeset 55130 70db8d380d62
parent 54228 229282d53781
child 55215 b6c926e67350
permissions -rw-r--r--
Restored Suc rather than +1, and using Library/Binimial
     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 declare One_nat_def [simp]
    35 
    36 class prime = one +
    37   fixes prime :: "'a \<Rightarrow> bool"
    38 
    39 instantiation nat :: prime
    40 begin
    41 
    42 definition prime_nat :: "nat \<Rightarrow> bool"
    43   where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    44 
    45 instance ..
    46 
    47 end
    48 
    49 instantiation int :: prime
    50 begin
    51 
    52 definition prime_int :: "int \<Rightarrow> bool"
    53   where "prime_int p = prime (nat p)"
    54 
    55 instance ..
    56 
    57 end
    58 
    59 
    60 subsection {* Set up Transfer *}
    61 
    62 lemma transfer_nat_int_prime:
    63   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
    64   unfolding gcd_int_def lcm_int_def prime_int_def by auto
    65 
    66 declare transfer_morphism_nat_int[transfer add return:
    67     transfer_nat_int_prime]
    68 
    69 lemma transfer_int_nat_prime: "prime (int x) = prime x"
    70   unfolding gcd_int_def lcm_int_def prime_int_def by auto
    71 
    72 declare transfer_morphism_int_nat[transfer add return:
    73     transfer_int_nat_prime]
    74 
    75 
    76 subsection {* Primes *}
    77 
    78 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    79   apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
    80   apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
    81   done
    82 
    83 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    84   unfolding prime_int_def
    85   apply (frule prime_odd_nat)
    86   apply (auto simp add: even_nat_def)
    87   done
    88 
    89 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
    90 
    91 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
    92   unfolding prime_nat_def by auto
    93 
    94 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
    95   unfolding prime_nat_def by auto
    96 
    97 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
    98   unfolding prime_nat_def by auto
    99 
   100 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
   101   unfolding prime_nat_def by auto
   102 
   103 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
   104   unfolding prime_nat_def by auto
   105 
   106 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
   107   unfolding prime_nat_def by auto
   108 
   109 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
   110   unfolding prime_nat_def by auto
   111 
   112 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
   113   unfolding prime_int_def prime_nat_def by auto
   114 
   115 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
   116   unfolding prime_int_def prime_nat_def by auto
   117 
   118 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
   119   unfolding prime_int_def prime_nat_def by auto
   120 
   121 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
   122   unfolding prime_int_def prime_nat_def by auto
   123 
   124 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
   125   unfolding prime_int_def prime_nat_def by auto
   126 
   127 
   128 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
   129     m = 1 \<or> m = p))"
   130   using prime_nat_def [transferred]
   131   apply (cases "p >= 0")
   132   apply blast
   133   apply (auto simp add: prime_ge_0_int)
   134   done
   135 
   136 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   137   apply (unfold prime_nat_def)
   138   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
   139   done
   140 
   141 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   142   apply (unfold prime_int_altdef)
   143   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
   144   done
   145 
   146 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   147   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
   148 
   149 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   150   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
   151 
   152 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
   153     p dvd m * n = (p dvd m \<or> p dvd n)"
   154   by (rule iffI, rule prime_dvd_mult_nat, auto)
   155 
   156 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
   157     p dvd m * n = (p dvd m \<or> p dvd n)"
   158   by (rule iffI, rule prime_dvd_mult_int, auto)
   159 
   160 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   161     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   162   unfolding prime_nat_def dvd_def apply auto
   163   by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
   164       n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
   165 
   166 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   167     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   168   unfolding prime_int_altdef dvd_def
   169   apply auto
   170   by (metis div_mult_self1_is_id div_mult_self2_is_id
   171       int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
   172 
   173 lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   174   by (induct n) auto
   175 
   176 lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   177   by (induct n) (auto simp: prime_ge_0_int)
   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)
   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 One_nat_def 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   by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
   249 
   250 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   251   by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
   252 
   253 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   254   by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
   255 
   256 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   257   by (metis leD linear prime_gt_0_int prime_imp_coprime_int prime_int_altdef)
   258 
   259 lemma primes_imp_powers_coprime_nat:
   260     "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   261   by (rule coprime_exp2_nat, rule primes_coprime_nat)
   262 
   263 lemma primes_imp_powers_coprime_int:
   264     "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   265   by (rule coprime_exp2_int, rule primes_coprime_int)
   266 
   267 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
   268   apply (induct n rule: nat_less_induct)
   269   apply (case_tac "n = 0")
   270   using two_is_prime_nat
   271   apply blast
   272   apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
   273     nat_dvd_not_less neq0_conv prime_nat_def)
   274   done
   275 
   276 text {* One property of coprimality is easier to prove via prime factors. *}
   277 
   278 lemma prime_divprod_pow_nat:
   279   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
   280   shows "p^n dvd a \<or> p^n dvd b"
   281 proof-
   282   { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
   283       apply (cases "n=0", simp_all)
   284       apply (cases "a=1", simp_all)
   285       done }
   286   moreover
   287   { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
   288     then obtain m where m: "n = Suc m" by (cases n) auto
   289     from n have "p dvd p^n" apply (intro dvd_power) apply auto done
   290     also note pab
   291     finally have pab': "p dvd a * b".
   292     from prime_dvd_mult_nat[OF p pab']
   293     have "p dvd a \<or> p dvd b" .
   294     moreover
   295     { assume pa: "p dvd a"
   296       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
   297       with p have "coprime b p"
   298         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   299       then have pnb: "coprime (p^n) b"
   300         by (subst gcd_commute_nat, rule coprime_exp_nat)
   301       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
   302     moreover
   303     { assume pb: "p dvd b"
   304       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
   305       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
   306         by auto
   307       with p have "coprime a p"
   308         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   309       then have pna: "coprime (p^n) a"
   310         by (subst gcd_commute_nat, rule coprime_exp_nat)
   311       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
   312     ultimately have ?thesis by blast }
   313   ultimately show ?thesis by blast
   314 qed
   315 
   316 
   317 subsection {* Infinitely many primes *}
   318 
   319 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
   320 proof-
   321   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   322   from prime_factor_nat [OF f1]
   323   obtain p where "prime p" and "p dvd fact n + 1" by auto
   324   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   325   { assume "p \<le> n"
   326     from `prime p` have "p \<ge> 1" 
   327       by (cases p, simp_all)
   328     with `p <= n` have "p dvd fact n" 
   329       by (intro dvd_fact_nat)
   330     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   331       by (rule dvd_diff_nat)
   332     then have "p dvd 1" by simp
   333     then have "p <= 1" by auto
   334     moreover from `prime p` have "p > 1" by auto
   335     ultimately have False by auto}
   336   then have "n < p" by presburger
   337   with `prime p` and `p <= fact n + 1` show ?thesis by auto
   338 qed
   339 
   340 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
   341   using next_prime_bound by auto
   342 
   343 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   344 proof
   345   assume "finite {(p::nat). prime p}"
   346   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   347     by auto
   348   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   349     by auto
   350   with bigger_prime [of b] show False
   351     by auto
   352 qed
   353 
   354 end