src/HOL/Number_Theory/Primes.thy
author paulson <lp15@cam.ac.uk>
Sun Feb 02 19:15:25 2014 +0000 (2014-02-02)
changeset 55242 413ec965f95d
parent 55238 7ddb889e23bd
child 55337 5d45fb978d5a
permissions -rw-r--r--
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
     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 declare [[coercion int]]
    36 declare [[coercion_enabled]]
    37 
    38 definition prime :: "nat \<Rightarrow> bool"
    39   where "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    40 
    41 lemmas prime_nat_def = prime_def
    42 
    43 
    44 subsection {* Primes *}
    45 
    46 lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    47   apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
    48   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)
    49   done
    50 
    51 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
    52 
    53 lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0"
    54   unfolding prime_nat_def by auto
    55 
    56 lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1"
    57   unfolding prime_nat_def by auto
    58 
    59 lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1"
    60   unfolding prime_nat_def by auto
    61 
    62 lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0"
    63   unfolding prime_nat_def by auto
    64 
    65 lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0"
    66   unfolding prime_nat_def by auto
    67 
    68 lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2"
    69   unfolding prime_nat_def by auto
    70 
    71 lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
    72   apply (unfold prime_nat_def)
    73   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
    74   done
    75 
    76 lemma prime_int_altdef: 
    77   "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
    78     m = 1 \<or> m = p))"
    79   apply (simp add: prime_def)
    80   apply (auto simp add: )
    81   apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
    82   apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
    83   done
    84 
    85 lemma prime_imp_coprime_int:
    86   fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
    87   apply (unfold prime_int_altdef)
    88   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
    89   done
    90 
    91 lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
    92   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
    93 
    94 lemma prime_dvd_mult_int: 
    95   fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
    96   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
    97 
    98 lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
    99     p dvd m * n = (p dvd m \<or> p dvd n)"
   100   by (rule iffI, rule prime_dvd_mult_nat, auto)
   101 
   102 lemma prime_dvd_mult_eq_int [simp]:
   103   fixes n::int 
   104   shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
   105   by (rule iffI, rule prime_dvd_mult_int, auto)
   106 
   107 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   108     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   109   unfolding prime_nat_def dvd_def apply auto
   110   by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
   111       n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
   112 
   113 lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   114   by (induct n) auto
   115 
   116 lemma prime_dvd_power_int:
   117   fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   118   by (induct n) auto
   119 
   120 lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
   121     p dvd x^n \<longleftrightarrow> p dvd x"
   122   by (cases n) (auto elim: prime_dvd_power_nat)
   123 
   124 lemma prime_dvd_power_int_iff:
   125   fixes x::int 
   126   shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
   127   by (cases n) (auto elim: prime_dvd_power_int)
   128 
   129 
   130 subsubsection {* Make prime naively executable *}
   131 
   132 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   133   by (simp add: prime_nat_def)
   134 
   135 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
   136   by (simp add: prime_nat_def)
   137 
   138 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   139   by (simp add: prime_nat_def)
   140 
   141 lemma prime_nat_code [code]:
   142     "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   143   apply (simp add: Ball_def)
   144   apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
   145   done
   146 
   147 lemma prime_nat_simp:
   148     "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   149   by (auto simp add: prime_nat_code)
   150 
   151 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
   152 
   153 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   154   by simp
   155 
   156 text{* A bit of regression testing: *}
   157 
   158 lemma "prime(97::nat)" by simp
   159 lemma "prime(997::nat)" by eval
   160 
   161 
   162 lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   163   by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
   164 
   165 lemma prime_imp_power_coprime_int:
   166   fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   167   by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
   168 
   169 lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   170   by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
   171 
   172 lemma primes_imp_powers_coprime_nat:
   173     "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   174   by (rule coprime_exp2_nat, rule primes_coprime_nat)
   175 
   176 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
   177   apply (induct n rule: nat_less_induct)
   178   apply (case_tac "n = 0")
   179   using two_is_prime_nat
   180   apply blast
   181   apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
   182     nat_dvd_not_less neq0_conv prime_nat_def)
   183   done
   184 
   185 text {* One property of coprimality is easier to prove via prime factors. *}
   186 
   187 lemma prime_divprod_pow_nat:
   188   assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   189   shows "p^n dvd a \<or> p^n dvd b"
   190 proof-
   191   { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
   192       apply (cases "n=0", simp_all)
   193       apply (cases "a=1", simp_all)
   194       done }
   195   moreover
   196   { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
   197     then obtain m where m: "n = Suc m" by (cases n) auto
   198     from n have "p dvd p^n" apply (intro dvd_power) apply auto done
   199     also note pab
   200     finally have pab': "p dvd a * b".
   201     from prime_dvd_mult_nat[OF p pab']
   202     have "p dvd a \<or> p dvd b" .
   203     moreover
   204     { assume pa: "p dvd a"
   205       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
   206       with p have "coprime b p"
   207         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   208       then have pnb: "coprime (p^n) b"
   209         by (subst gcd_commute_nat, rule coprime_exp_nat)
   210       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
   211     moreover
   212     { assume pb: "p dvd b"
   213       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
   214       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
   215         by auto
   216       with p have "coprime a p"
   217         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   218       then have pna: "coprime (p^n) a"
   219         by (subst gcd_commute_nat, rule coprime_exp_nat)
   220       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
   221     ultimately have ?thesis by blast }
   222   ultimately show ?thesis by blast
   223 qed
   224 
   225 
   226 subsection {* Infinitely many primes *}
   227 
   228 lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
   229 proof-
   230   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   231   from prime_factor_nat [OF f1]
   232   obtain p where "prime p" and "p dvd fact n + 1" by auto
   233   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   234   { assume "p \<le> n"
   235     from `prime p` have "p \<ge> 1" 
   236       by (cases p, simp_all)
   237     with `p <= n` have "p dvd fact n" 
   238       by (intro dvd_fact_nat)
   239     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   240       by (rule dvd_diff_nat)
   241     then have "p dvd 1" by simp
   242     then have "p <= 1" by auto
   243     moreover from `prime p` have "p > 1" by auto
   244     ultimately have False by auto}
   245   then have "n < p" by presburger
   246   with `prime p` and `p <= fact n + 1` show ?thesis by auto
   247 qed
   248 
   249 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
   250   using next_prime_bound by auto
   251 
   252 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   253 proof
   254   assume "finite {(p::nat). prime p}"
   255   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   256     by auto
   257   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   258     by auto
   259   with bigger_prime [of b] show False
   260     by auto
   261 qed
   262 
   263 subsection{*Powers of Primes*}
   264 
   265 text{*Versions for type nat only*}
   266 
   267 lemma prime_product: 
   268   fixes p::nat
   269   assumes "prime (p * q)"
   270   shows "p = 1 \<or> q = 1"
   271 proof -
   272   from assms have 
   273     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
   274     unfolding prime_nat_def by auto
   275   from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
   276   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   277   have "p dvd p * q" by simp
   278   then have "p = 1 \<or> p = p * q" by (rule P)
   279   then show ?thesis by (simp add: Q)
   280 qed
   281 
   282 lemma prime_exp: 
   283   fixes p::nat
   284   shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
   285 proof(induct n)
   286   case 0 thus ?case by simp
   287 next
   288   case (Suc n)
   289   {assume "p = 0" hence ?case by simp}
   290   moreover
   291   {assume "p=1" hence ?case by simp}
   292   moreover
   293   {assume p: "p \<noteq> 0" "p\<noteq>1"
   294     {assume pp: "prime (p^Suc n)"
   295       hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
   296       with p have n: "n = 0"
   297         by (metis One_nat_def nat_power_eq_Suc_0_iff)
   298       with pp have "prime p \<and> Suc n = 1" by simp}
   299     moreover
   300     {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
   301     ultimately have ?case by blast}
   302   ultimately show ?case by blast
   303 qed
   304 
   305 lemma prime_power_mult: 
   306   fixes p::nat
   307   assumes p: "prime p" and xy: "x * y = p ^ k"
   308   shows "\<exists>i j. x = p ^i \<and> y = p^ j"
   309 using xy
   310 proof(induct k arbitrary: x y)
   311   case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
   312 next
   313   case (Suc k x y)
   314   from Suc.prems have pxy: "p dvd x*y" by auto
   315   from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
   316   from p have p0: "p \<noteq> 0" by - (rule ccontr, simp) 
   317   {assume px: "p dvd x"
   318     then obtain d where d: "x = p*d" unfolding dvd_def by blast
   319     from Suc.prems d  have "p*d*y = p^Suc k" by simp
   320     hence th: "d*y = p^k" using p0 by simp
   321     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
   322     with d have "x = p^Suc i" by simp 
   323     with ij(2) have ?case by blast}
   324   moreover 
   325   {assume px: "p dvd y"
   326     then obtain d where d: "y = p*d" unfolding dvd_def by blast
   327     from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult_commute)
   328     hence th: "d*x = p^k" using p0 by simp
   329     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
   330     with d have "y = p^Suc i" by simp 
   331     with ij(2) have ?case by blast}
   332   ultimately show ?case  using pxyc by blast
   333 qed
   334 
   335 lemma prime_power_exp: 
   336   fixes p::nat
   337   assumes p: "prime p" and n: "n \<noteq> 0" 
   338     and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
   339   using n xn
   340 proof(induct n arbitrary: k)
   341   case 0 thus ?case by simp
   342 next
   343   case (Suc n k) hence th: "x*x^n = p^k" by simp
   344   {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
   345   moreover
   346   {assume n: "n \<noteq> 0"
   347     from prime_power_mult[OF p th] 
   348     obtain i j where ij: "x = p^i" "x^n = p^j"by blast
   349     from Suc.hyps[OF n ij(2)] have ?case .}
   350   ultimately show ?case by blast
   351 qed
   352 
   353 lemma divides_primepow:
   354   fixes p::nat
   355   assumes p: "prime p" 
   356   shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
   357 proof
   358   assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" 
   359     unfolding dvd_def  apply (auto simp add: mult_commute) by blast
   360   from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
   361   from e ij have "p^(i + j) = p^k" by (simp add: power_add)
   362   hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp 
   363   hence "i \<le> k" by arith
   364   with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
   365 next
   366   {fix i assume H: "i \<le> k" "d = p^i"
   367     then obtain j where j: "k = i + j"
   368       by (metis le_add_diff_inverse)
   369     hence "p^k = p^j*d" using H(2) by (simp add: power_add)
   370     hence "d dvd p^k" unfolding dvd_def by auto}
   371   thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
   372 qed
   373 
   374 subsection {*Chinese Remainder Theorem Variants*}
   375 
   376 lemma bezout_gcd_nat:
   377   fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
   378   using bezout_nat[of a b]
   379 by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute 
   380   gcd_nat.right_neutral mult_0) 
   381 
   382 lemma gcd_bezout_sum_nat:
   383   fixes a::nat 
   384   assumes "a * x + b * y = d" 
   385   shows "gcd a b dvd d"
   386 proof-
   387   let ?g = "gcd a b"
   388     have dv: "?g dvd a*x" "?g dvd b * y" 
   389       by simp_all
   390     from dvd_add[OF dv] assms
   391     show ?thesis by auto
   392 qed
   393 
   394 
   395 text {* A binary form of the Chinese Remainder Theorem. *}
   396 
   397 lemma chinese_remainder: 
   398   fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
   399   shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
   400 proof-
   401   from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
   402   obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1" 
   403     and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
   404   then have d12: "d1 = 1" "d2 =1"
   405     by (metis ab coprime_nat)+
   406   let ?x = "v * a * x1 + u * b * x2"
   407   let ?q1 = "v * x1 + u * y2"
   408   let ?q2 = "v * y1 + u * x2"
   409   from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
   410   have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
   411     apply (auto simp add: algebra_simps) 
   412     apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+
   413     done
   414   thus ?thesis by blast
   415 qed
   416 
   417 text {* Primality *}
   418 
   419 lemma coprime_bezout_strong:
   420   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
   421   shows "\<exists>x y. a * x = b * y + 1"
   422 by (metis assms bezout_nat gcd_nat.left_neutral)
   423 
   424 lemma bezout_prime: 
   425   assumes p: "prime p" and pa: "\<not> p dvd a"
   426   shows "\<exists>x y. a*x = Suc (p*y)"
   427 proof-
   428   have ap: "coprime a p"
   429     by (metis gcd_nat.commute p pa prime_imp_coprime_nat) 
   430   from coprime_bezout_strong[OF ap] show ?thesis
   431     by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa) 
   432 qed
   433 
   434 end