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