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