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