src/HOL/Number_Theory/Primes.thy
author haftmann
Mon Jul 12 08:58:13 2010 +0200 (2010-07-12)
changeset 37765 26bdfb7b680b
parent 37607 ebb8b1a79c4c
child 40461 e876e95588ce
permissions -rw-r--r--
dropped superfluous [code del]s
     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 del]
    35 
    36 class prime = one +
    37 
    38 fixes
    39   prime :: "'a \<Rightarrow> bool"
    40 
    41 instantiation nat :: prime
    42 
    43 begin
    44 
    45 definition
    46   prime_nat :: "nat \<Rightarrow> bool"
    47 where
    48   "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    49 
    50 instance proof qed
    51 
    52 end
    53 
    54 instantiation int :: prime
    55 
    56 begin
    57 
    58 definition
    59   prime_int :: "int \<Rightarrow> bool"
    60 where
    61   "prime_int p = prime (nat p)"
    62 
    63 instance proof qed
    64 
    65 end
    66 
    67 
    68 subsection {* Set up Transfer *}
    69 
    70 
    71 lemma transfer_nat_int_prime:
    72   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
    73   unfolding gcd_int_def lcm_int_def prime_int_def
    74   by auto
    75 
    76 declare transfer_morphism_nat_int[transfer add return:
    77     transfer_nat_int_prime]
    78 
    79 lemma transfer_int_nat_prime:
    80   "prime (int x) = prime x"
    81   by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
    82 
    83 declare transfer_morphism_int_nat[transfer add return:
    84     transfer_int_nat_prime]
    85 
    86 
    87 subsection {* Primes *}
    88 
    89 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    90   unfolding prime_nat_def
    91   apply (subst even_mult_two_ex)
    92   apply clarify
    93   apply (drule_tac x = 2 in spec)
    94   apply auto
    95 done
    96 
    97 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    98   unfolding prime_int_def
    99   apply (frule prime_odd_nat)
   100   apply (auto simp add: even_nat_def)
   101 done
   102 
   103 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
   104 
   105 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
   106   by (unfold prime_nat_def, auto)
   107 
   108 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
   109   by (unfold prime_nat_def, auto)
   110 
   111 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
   112   by (unfold prime_nat_def, auto)
   113 
   114 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
   115   by (unfold prime_nat_def, auto)
   116 
   117 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
   118   by (unfold prime_nat_def, auto)
   119 
   120 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
   121   by (unfold prime_nat_def, auto)
   122 
   123 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
   124   by (unfold prime_nat_def, auto)
   125 
   126 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
   127   by (unfold prime_int_def prime_nat_def) auto
   128 
   129 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
   130   by (unfold prime_int_def prime_nat_def, auto)
   131 
   132 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
   133   by (unfold prime_int_def prime_nat_def, auto)
   134 
   135 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
   136   by (unfold prime_int_def prime_nat_def, auto)
   137 
   138 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
   139   by (unfold prime_int_def prime_nat_def, auto)
   140 
   141 
   142 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
   143     m = 1 \<or> m = p))"
   144   using prime_nat_def [transferred]
   145     apply (case_tac "p >= 0")
   146     by (blast, auto simp add: prime_ge_0_int)
   147 
   148 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   149   apply (unfold prime_nat_def)
   150   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
   151   done
   152 
   153 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   154   apply (unfold prime_int_altdef)
   155   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
   156   done
   157 
   158 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   159   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
   160 
   161 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   162   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
   163 
   164 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
   165     p dvd m * n = (p dvd m \<or> p dvd n)"
   166   by (rule iffI, rule prime_dvd_mult_nat, auto)
   167 
   168 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
   169     p dvd m * n = (p dvd m \<or> p dvd n)"
   170   by (rule iffI, rule prime_dvd_mult_int, auto)
   171 
   172 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   173     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   174   unfolding prime_nat_def dvd_def apply auto
   175   by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
   176 
   177 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   178     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   179   unfolding prime_int_altdef dvd_def
   180   apply auto
   181   by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
   182 
   183 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
   184     n > 0 --> (p dvd x^n --> p dvd x)"
   185   by (induct n rule: nat_induct, auto)
   186 
   187 lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
   188     n > 0 --> (p dvd x^n --> p dvd x)"
   189   apply (induct n rule: nat_induct, auto)
   190   apply (frule prime_ge_0_int)
   191   apply auto
   192 done
   193 
   194 subsubsection{* Make prime naively executable *}
   195 
   196 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   197   by (simp add: prime_nat_def)
   198 
   199 lemma zero_not_prime_int [simp]: "~prime (0::int)"
   200   by (simp add: prime_int_def)
   201 
   202 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
   203   by (simp add: prime_nat_def)
   204 
   205 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   206   by (simp add: prime_nat_def One_nat_def)
   207 
   208 lemma one_not_prime_int [simp]: "~prime (1::int)"
   209   by (simp add: prime_int_def)
   210 
   211 lemma prime_nat_code [code]:
   212  "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   213 apply (simp add: Ball_def)
   214 apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
   215 done
   216 
   217 lemma prime_nat_simp:
   218  "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   219 by (auto simp add: prime_nat_code)
   220 
   221 lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
   222 
   223 lemma prime_int_code [code]:
   224   "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
   225 proof
   226   assume "?L" thus "?R"
   227     by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
   228 next
   229     assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
   230 qed
   231 
   232 lemma prime_int_simp:
   233   "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
   234 by (auto simp add: prime_int_code)
   235 
   236 lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
   237 
   238 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   239 by simp
   240 
   241 lemma two_is_prime_int [simp]: "prime (2::int)"
   242 by simp
   243 
   244 text{* A bit of regression testing: *}
   245 
   246 lemma "prime(97::nat)"
   247 by simp
   248 
   249 lemma "prime(97::int)"
   250 by simp
   251 
   252 lemma "prime(997::nat)"
   253 by eval
   254 
   255 lemma "prime(997::int)"
   256 by eval
   257 
   258 
   259 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   260   apply (rule coprime_exp_nat)
   261   apply (subst gcd_commute_nat)
   262   apply (erule (1) prime_imp_coprime_nat)
   263 done
   264 
   265 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   266   apply (rule coprime_exp_int)
   267   apply (subst gcd_commute_int)
   268   apply (erule (1) prime_imp_coprime_int)
   269 done
   270 
   271 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   272   apply (rule prime_imp_coprime_nat, assumption)
   273   apply (unfold prime_nat_def, auto)
   274 done
   275 
   276 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   277   apply (rule prime_imp_coprime_int, assumption)
   278   apply (unfold prime_int_altdef, clarify)
   279   apply (drule_tac x = q in spec)
   280   apply (drule_tac x = p in spec)
   281   apply auto
   282 done
   283 
   284 lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   285   by (rule coprime_exp2_nat, rule primes_coprime_nat)
   286 
   287 lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   288   by (rule coprime_exp2_int, rule primes_coprime_int)
   289 
   290 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
   291   apply (induct n rule: nat_less_induct)
   292   apply (case_tac "n = 0")
   293   using two_is_prime_nat apply blast
   294   apply (case_tac "prime n")
   295   apply blast
   296   apply (subgoal_tac "n > 1")
   297   apply (frule (1) not_prime_eq_prod_nat)
   298   apply (auto intro: dvd_mult dvd_mult2)
   299 done
   300 
   301 (* An Isar version:
   302 
   303 lemma prime_factor_b_nat:
   304   fixes n :: nat
   305   assumes "n \<noteq> 1"
   306   shows "\<exists>p. prime p \<and> p dvd n"
   307 
   308 using `n ~= 1`
   309 proof (induct n rule: less_induct_nat)
   310   fix n :: nat
   311   assume "n ~= 1" and
   312     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
   313   thus "\<exists>p. prime p \<and> p dvd n"
   314   proof -
   315   {
   316     assume "n = 0"
   317     moreover note two_is_prime_nat
   318     ultimately have ?thesis
   319       by (auto simp del: two_is_prime_nat)
   320   }
   321   moreover
   322   {
   323     assume "prime n"
   324     hence ?thesis by auto
   325   }
   326   moreover
   327   {
   328     assume "n ~= 0" and "~ prime n"
   329     with `n ~= 1` have "n > 1" by auto
   330     with `~ prime n` and not_prime_eq_prod_nat obtain m k where
   331       "n = m * k" and "1 < m" and "m < n" by blast
   332     with ih obtain p where "prime p" and "p dvd m" by blast
   333     with `n = m * k` have ?thesis by auto
   334   }
   335   ultimately show ?thesis by blast
   336   qed
   337 qed
   338 
   339 *)
   340 
   341 text {* One property of coprimality is easier to prove via prime factors. *}
   342 
   343 lemma prime_divprod_pow_nat:
   344   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
   345   shows "p^n dvd a \<or> p^n dvd b"
   346 proof-
   347   {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
   348       apply (cases "n=0", simp_all)
   349       apply (cases "a=1", simp_all) done}
   350   moreover
   351   {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
   352     then obtain m where m: "n = Suc m" by (cases n, auto)
   353     from n have "p dvd p^n" by (intro dvd_power, auto)
   354     also note pab
   355     finally have pab': "p dvd a * b".
   356     from prime_dvd_mult_nat[OF p pab']
   357     have "p dvd a \<or> p dvd b" .
   358     moreover
   359     { assume pa: "p dvd a"
   360       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
   361       with p have "coprime b p"
   362         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   363       hence pnb: "coprime (p^n) b"
   364         by (subst gcd_commute_nat, rule coprime_exp_nat)
   365       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
   366     moreover
   367     { assume pb: "p dvd b"
   368       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
   369       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
   370         by auto
   371       with p have "coprime a p"
   372         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   373       hence pna: "coprime (p^n) a"
   374         by (subst gcd_commute_nat, rule coprime_exp_nat)
   375       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
   376     ultimately have ?thesis by blast}
   377   ultimately show ?thesis by blast
   378 qed
   379 
   380 subsection {* Infinitely many primes *}
   381 
   382 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
   383 proof-
   384   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   385   from prime_factor_nat [OF f1]
   386       obtain p where "prime p" and "p dvd fact n + 1" by auto
   387   hence "p \<le> fact n + 1" 
   388     by (intro dvd_imp_le, auto)
   389   {assume "p \<le> n"
   390     from `prime p` have "p \<ge> 1" 
   391       by (cases p, simp_all)
   392     with `p <= n` have "p dvd fact n" 
   393       by (intro dvd_fact_nat)
   394     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   395       by (rule dvd_diff_nat)
   396     hence "p dvd 1" by simp
   397     hence "p <= 1" by auto
   398     moreover from `prime p` have "p > 1" by auto
   399     ultimately have False by auto}
   400   hence "n < p" by arith
   401   with `prime p` and `p <= fact n + 1` show ?thesis by auto
   402 qed
   403 
   404 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
   405 using next_prime_bound by auto
   406 
   407 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   408 proof
   409   assume "finite {(p::nat). prime p}"
   410   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   411     by auto
   412   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   413     by auto
   414   with bigger_prime [of b] show False by auto
   415 qed
   416 
   417 
   418 end