src/HOL/Number_Theory/Primes.thy
author nipkow
Fri Dec 04 08:52:09 2009 +0100 (2009-12-04)
changeset 33946 fcc20072df9a
parent 33718 06e9aff51d17
child 35644 d20cf282342e
permissions -rw-r--r--
removed redundant lemma
     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 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       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
   365       with p have "coprime b p"
   366         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   367       hence pnb: "coprime (p^n) b"
   368         by (subst gcd_commute_nat, rule coprime_exp_nat)
   369       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
   370     moreover
   371     { assume pb: "p dvd b"
   372       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
   373       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
   374         by auto
   375       with p have "coprime a p"
   376         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   377       hence pna: "coprime (p^n) a"
   378         by (subst gcd_commute_nat, rule coprime_exp_nat)
   379       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
   380     ultimately have ?thesis by blast}
   381   ultimately show ?thesis by blast
   382 qed
   383 
   384 subsection {* Infinitely many primes *}
   385 
   386 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
   387 proof-
   388   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   389   from prime_factor_nat [OF f1]
   390       obtain p where "prime p" and "p dvd fact n + 1" by auto
   391   hence "p \<le> fact n + 1" 
   392     by (intro dvd_imp_le, auto)
   393   {assume "p \<le> n"
   394     from `prime p` have "p \<ge> 1" 
   395       by (cases p, simp_all)
   396     with `p <= n` have "p dvd fact n" 
   397       by (intro dvd_fact_nat)
   398     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   399       by (rule dvd_diff_nat)
   400     hence "p dvd 1" by simp
   401     hence "p <= 1" by auto
   402     moreover from `prime p` have "p > 1" by auto
   403     ultimately have False by auto}
   404   hence "n < p" by arith
   405   with `prime p` and `p <= fact n + 1` show ?thesis by auto
   406 qed
   407 
   408 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
   409 using next_prime_bound by auto
   410 
   411 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   412 proof
   413   assume "finite {(p::nat). prime p}"
   414   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   415     by auto
   416   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   417     by auto
   418   with bigger_prime [of b] show False by auto
   419 qed
   420 
   421 
   422 end