src/HOL/Number_Theory/Primes.thy
author haftmann
Wed Feb 17 21:51:57 2016 +0100 (2016-02-17)
changeset 62349 7c23469b5118
parent 62348 9a5f43dac883
child 62410 2fc7a8d9c529
permissions -rw-r--r--
cleansed junk-producing interpretations for gcd/lcm on nat altogether
     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 gcd_dvd2)
    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 of_nat_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 gcd_dvd2 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 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 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:
   171   "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
   172 proof (induct n rule: nat_less_induct)
   173   case (1 n) show ?case
   174   proof (cases "n = 0")
   175     case True then show ?thesis
   176     by (auto intro: two_is_prime_nat)
   177   next
   178     case False with "1.prems" have "n > 1" by simp
   179     with "1.hyps" show ?thesis
   180     by (metis One_nat_def dvd_mult dvd_refl not_prime_eq_prod_nat order_less_irrefl)
   181   qed
   182 qed
   183 
   184 text \<open>One property of coprimality is easier to prove via prime factors.\<close>
   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, intro prime_imp_coprime_nat)
   207       then have pnb: "coprime (p^n) b"
   208         by (subst gcd.commute, rule coprime_exp_nat)
   209       from coprime_dvd_mult[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, intro prime_imp_coprime_nat)
   217       then have pna: "coprime (p^n) a"
   218         by (subst gcd.commute, rule coprime_exp_nat)
   219       from coprime_dvd_mult[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 \<open>Infinitely many primes\<close>
   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 \<open>prime p\<close> have "p \<ge> 1"
   235       by (cases p, simp_all)
   236     with \<open>p <= n\<close> have "p dvd fact n"
   237       by (intro dvd_fact)
   238     with \<open>p dvd fact n + 1\<close> 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 \<open>prime p\<close> have "p > 1"
   243       using prime_def by blast
   244     ultimately have False by auto}
   245   then have "n < p" by presburger
   246   with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> 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\<open>Powers of Primes\<close>
   264 
   265 text\<open>Versions for type nat only\<close>
   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_def by auto
   275   from \<open>1 < p * q\<close> 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 \<open>Chinese Remainder Theorem Variants\<close>
   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.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 \<open>A binary form of the Chinese Remainder Theorem.\<close>
   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     by algebra+
   412   thus ?thesis by blast
   413 qed
   414 
   415 text \<open>Primality\<close>
   416 
   417 lemma coprime_bezout_strong:
   418   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
   419   shows "\<exists>x y. a * x = b * y + 1"
   420 by (metis assms bezout_nat gcd_nat.left_neutral)
   421 
   422 lemma bezout_prime:
   423   assumes p: "prime p" and pa: "\<not> p dvd a"
   424   shows "\<exists>x y. a*x = Suc (p*y)"
   425 proof -
   426   have ap: "coprime a p"
   427     by (metis gcd.commute p pa prime_imp_coprime_nat)
   428   moreover from p have "p \<noteq> 1" by auto
   429   ultimately have "\<exists>x y. a * x = p * y + 1"
   430     by (rule coprime_bezout_strong)
   431   then show ?thesis by simp    
   432 qed
   433 
   434 end