src/HOL/Number_Theory/Primes.thy
author haftmann
Thu Oct 31 11:44:20 2013 +0100 (2013-10-31)
changeset 54228 229282d53781
parent 53598 2bd8d459ebae
child 55130 70db8d380d62
permissions -rw-r--r--
purely algebraic foundation for even/odd
     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   apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
    78   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)
    79   done
    80 
    81 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    82   unfolding prime_int_def
    83   apply (frule prime_odd_nat)
    84   apply (auto simp add: even_nat_def)
    85   done
    86 
    87 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
    88 
    89 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
    90   unfolding prime_nat_def by auto
    91 
    92 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
    93   unfolding prime_nat_def by auto
    94 
    95 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
    96   unfolding prime_nat_def by auto
    97 
    98 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
    99   unfolding prime_nat_def by auto
   100 
   101 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
   102   unfolding prime_nat_def by auto
   103 
   104 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
   105   unfolding prime_nat_def by auto
   106 
   107 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
   108   unfolding prime_nat_def by auto
   109 
   110 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
   111   unfolding prime_int_def prime_nat_def by auto
   112 
   113 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
   114   unfolding prime_int_def prime_nat_def by auto
   115 
   116 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
   117   unfolding prime_int_def prime_nat_def by auto
   118 
   119 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
   120   unfolding prime_int_def prime_nat_def by auto
   121 
   122 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
   123   unfolding prime_int_def prime_nat_def by auto
   124 
   125 
   126 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
   127     m = 1 \<or> m = p))"
   128   using prime_nat_def [transferred]
   129   apply (cases "p >= 0")
   130   apply blast
   131   apply (auto simp add: prime_ge_0_int)
   132   done
   133 
   134 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   135   apply (unfold prime_nat_def)
   136   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
   137   done
   138 
   139 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   140   apply (unfold prime_int_altdef)
   141   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
   142   done
   143 
   144 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   145   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
   146 
   147 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   148   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
   149 
   150 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
   151     p dvd m * n = (p dvd m \<or> p dvd n)"
   152   by (rule iffI, rule prime_dvd_mult_nat, auto)
   153 
   154 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
   155     p dvd m * n = (p dvd m \<or> p dvd n)"
   156   by (rule iffI, rule prime_dvd_mult_int, auto)
   157 
   158 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   159     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   160   unfolding prime_nat_def dvd_def apply auto
   161   by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
   162       n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
   163 
   164 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   165     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   166   unfolding prime_int_altdef dvd_def
   167   apply auto
   168   by (metis div_mult_self1_is_id div_mult_self2_is_id
   169       int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
   170 
   171 lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   172   by (induct n) auto
   173 
   174 lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   175   apply (induct n)
   176   apply (frule prime_ge_0_int)
   177   apply auto
   178   done
   179 
   180 lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
   181     p dvd x^n \<longleftrightarrow> p dvd x"
   182   by (cases n) (auto elim: prime_dvd_power_nat)
   183 
   184 lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
   185     p dvd x^n \<longleftrightarrow> p dvd x"
   186   by (cases n) (auto elim: prime_dvd_power_int)
   187 
   188 
   189 subsubsection {* Make prime naively executable *}
   190 
   191 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   192   by (simp add: prime_nat_def)
   193 
   194 lemma zero_not_prime_int [simp]: "~prime (0::int)"
   195   by (simp add: prime_int_def)
   196 
   197 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
   198   by (simp add: prime_nat_def)
   199 
   200 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   201   by (simp add: prime_nat_def One_nat_def)
   202 
   203 lemma one_not_prime_int [simp]: "~prime (1::int)"
   204   by (simp add: prime_int_def)
   205 
   206 lemma prime_nat_code [code]:
   207     "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   208   apply (simp add: Ball_def)
   209   apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
   210   done
   211 
   212 lemma prime_nat_simp:
   213     "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   214   by (auto simp add: prime_nat_code)
   215 
   216 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
   217 
   218 lemma prime_int_code [code]:
   219   "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
   220 proof
   221   assume "?L"
   222   then show "?R"
   223     by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
   224 next
   225   assume "?R"
   226   then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
   227 qed
   228 
   229 lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
   230   by (auto simp add: prime_int_code)
   231 
   232 lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m
   233 
   234 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   235   by simp
   236 
   237 lemma two_is_prime_int [simp]: "prime (2::int)"
   238   by simp
   239 
   240 text{* A bit of regression testing: *}
   241 
   242 lemma "prime(97::nat)" by simp
   243 lemma "prime(97::int)" by simp
   244 lemma "prime(997::nat)" by eval
   245 lemma "prime(997::int)" by eval
   246 
   247 
   248 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   249   apply (rule coprime_exp_nat)
   250   apply (subst gcd_commute_nat)
   251   apply (erule (1) prime_imp_coprime_nat)
   252   done
   253 
   254 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   255   apply (rule coprime_exp_int)
   256   apply (subst gcd_commute_int)
   257   apply (erule (1) prime_imp_coprime_int)
   258   done
   259 
   260 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   261   apply (rule prime_imp_coprime_nat, assumption)
   262   apply (unfold prime_nat_def)
   263   apply auto
   264   done
   265 
   266 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   267   apply (rule prime_imp_coprime_int, assumption)
   268   apply (unfold prime_int_altdef)
   269   apply (metis int_one_le_iff_zero_less less_le)
   270   done
   271 
   272 lemma primes_imp_powers_coprime_nat:
   273     "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   274   by (rule coprime_exp2_nat, rule primes_coprime_nat)
   275 
   276 lemma primes_imp_powers_coprime_int:
   277     "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   278   by (rule coprime_exp2_int, rule primes_coprime_int)
   279 
   280 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
   281   apply (induct n rule: nat_less_induct)
   282   apply (case_tac "n = 0")
   283   using two_is_prime_nat
   284   apply blast
   285   apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
   286     nat_dvd_not_less neq0_conv prime_nat_def)
   287   done
   288 
   289 (* An Isar version:
   290 
   291 lemma prime_factor_b_nat:
   292   fixes n :: nat
   293   assumes "n \<noteq> 1"
   294   shows "\<exists>p. prime p \<and> p dvd n"
   295 
   296 using `n ~= 1`
   297 proof (induct n rule: less_induct_nat)
   298   fix n :: nat
   299   assume "n ~= 1" and
   300     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
   301   then show "\<exists>p. prime p \<and> p dvd n"
   302   proof -
   303   {
   304     assume "n = 0"
   305     moreover note two_is_prime_nat
   306     ultimately have ?thesis
   307       by (auto simp del: two_is_prime_nat)
   308   }
   309   moreover
   310   {
   311     assume "prime n"
   312     then have ?thesis by auto
   313   }
   314   moreover
   315   {
   316     assume "n ~= 0" and "~ prime n"
   317     with `n ~= 1` have "n > 1" by auto
   318     with `~ prime n` and not_prime_eq_prod_nat obtain m k where
   319       "n = m * k" and "1 < m" and "m < n" by blast
   320     with ih obtain p where "prime p" and "p dvd m" by blast
   321     with `n = m * k` have ?thesis by auto
   322   }
   323   ultimately show ?thesis by blast
   324   qed
   325 qed
   326 
   327 *)
   328 
   329 text {* One property of coprimality is easier to prove via prime factors. *}
   330 
   331 lemma prime_divprod_pow_nat:
   332   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
   333   shows "p^n dvd a \<or> p^n dvd b"
   334 proof-
   335   { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
   336       apply (cases "n=0", simp_all)
   337       apply (cases "a=1", simp_all)
   338       done }
   339   moreover
   340   { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
   341     then obtain m where m: "n = Suc m" by (cases n) auto
   342     from n have "p dvd p^n" apply (intro dvd_power) apply auto done
   343     also note pab
   344     finally have pab': "p dvd a * b".
   345     from prime_dvd_mult_nat[OF p pab']
   346     have "p dvd a \<or> p dvd b" .
   347     moreover
   348     { assume pa: "p dvd a"
   349       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
   350       with p have "coprime b p"
   351         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   352       then have pnb: "coprime (p^n) b"
   353         by (subst gcd_commute_nat, rule coprime_exp_nat)
   354       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
   355     moreover
   356     { assume pb: "p dvd b"
   357       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
   358       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
   359         by auto
   360       with p have "coprime a p"
   361         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   362       then have pna: "coprime (p^n) a"
   363         by (subst gcd_commute_nat, rule coprime_exp_nat)
   364       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
   365     ultimately have ?thesis by blast }
   366   ultimately show ?thesis by blast
   367 qed
   368 
   369 
   370 subsection {* Infinitely many primes *}
   371 
   372 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
   373 proof-
   374   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   375   from prime_factor_nat [OF f1]
   376   obtain p where "prime p" and "p dvd fact n + 1" by auto
   377   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   378   { assume "p \<le> n"
   379     from `prime p` have "p \<ge> 1" 
   380       by (cases p, simp_all)
   381     with `p <= n` have "p dvd fact n" 
   382       by (intro dvd_fact_nat)
   383     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   384       by (rule dvd_diff_nat)
   385     then have "p dvd 1" by simp
   386     then have "p <= 1" by auto
   387     moreover from `prime p` have "p > 1" by auto
   388     ultimately have False by auto}
   389   then have "n < p" by presburger
   390   with `prime p` and `p <= fact n + 1` show ?thesis by auto
   391 qed
   392 
   393 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
   394   using next_prime_bound by auto
   395 
   396 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   397 proof
   398   assume "finite {(p::nat). prime p}"
   399   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   400     by auto
   401   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   402     by auto
   403   with bigger_prime [of b] show False
   404     by auto
   405 qed
   406 
   407 end