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