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