src/HOL/Number_Theory/Primes.thy
author paulson <lp15@cam.ac.uk>
Sat Feb 01 20:38:29 2014 +0000 (2014-02-01)
changeset 55238 7ddb889e23bd
parent 55215 b6c926e67350
child 55242 413ec965f95d
permissions -rw-r--r--
Added material from Old_Number_Theory related to the Chinese Remainder 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 header {* Primes *}
    29 
    30 theory Primes
    31 imports "~~/src/HOL/GCD"
    32 begin
    33 
    34 declare One_nat_def [simp]
    35 
    36 class prime = one +
    37   fixes prime :: "'a \<Rightarrow> bool"
    38 
    39 instantiation nat :: prime
    40 begin
    41 
    42 definition prime_nat :: "nat \<Rightarrow> bool"
    43   where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    44 
    45 instance ..
    46 
    47 end
    48 
    49 instantiation int :: prime
    50 begin
    51 
    52 definition prime_int :: "int \<Rightarrow> bool"
    53   where "prime_int p = prime (nat p)"
    54 
    55 instance ..
    56 
    57 end
    58 
    59 
    60 subsection {* Set up Transfer *}
    61 
    62 lemma transfer_nat_int_prime:
    63   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
    64   unfolding gcd_int_def lcm_int_def prime_int_def by auto
    65 
    66 declare transfer_morphism_nat_int[transfer add return:
    67     transfer_nat_int_prime]
    68 
    69 lemma transfer_int_nat_prime: "prime (int x) = prime x"
    70   unfolding gcd_int_def lcm_int_def prime_int_def by auto
    71 
    72 declare transfer_morphism_int_nat[transfer add return:
    73     transfer_int_nat_prime]
    74 
    75 
    76 subsection {* Primes *}
    77 
    78 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    79   apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
    80   apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
    81   done
    82 
    83 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    84   unfolding prime_int_def
    85   apply (frule prime_odd_nat)
    86   apply (auto simp add: even_nat_def)
    87   done
    88 
    89 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
    90 
    91 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
    92   unfolding prime_nat_def by auto
    93 
    94 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
    95   unfolding prime_nat_def by auto
    96 
    97 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
    98   unfolding prime_nat_def by auto
    99 
   100 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
   101   unfolding prime_nat_def by auto
   102 
   103 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
   104   unfolding prime_nat_def by auto
   105 
   106 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
   107   unfolding prime_nat_def by auto
   108 
   109 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
   110   unfolding prime_nat_def by auto
   111 
   112 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
   113   unfolding prime_int_def prime_nat_def by auto
   114 
   115 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
   116   unfolding prime_int_def prime_nat_def by auto
   117 
   118 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
   119   unfolding prime_int_def prime_nat_def by auto
   120 
   121 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
   122   unfolding prime_int_def prime_nat_def by auto
   123 
   124 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
   125   unfolding prime_int_def prime_nat_def by auto
   126 
   127 
   128 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
   129     m = 1 \<or> m = p))"
   130   using prime_nat_def [transferred]
   131   apply (cases "p >= 0")
   132   apply blast
   133   apply (auto simp add: prime_ge_0_int)
   134   done
   135 
   136 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   137   apply (unfold prime_nat_def)
   138   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
   139   done
   140 
   141 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   142   apply (unfold prime_int_altdef)
   143   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
   144   done
   145 
   146 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   147   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
   148 
   149 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   150   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
   151 
   152 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
   153     p dvd m * n = (p dvd m \<or> p dvd n)"
   154   by (rule iffI, rule prime_dvd_mult_nat, auto)
   155 
   156 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
   157     p dvd m * n = (p dvd m \<or> p dvd n)"
   158   by (rule iffI, rule prime_dvd_mult_int, auto)
   159 
   160 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   161     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   162   unfolding prime_nat_def dvd_def apply auto
   163   by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
   164       n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
   165 
   166 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   167     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   168   unfolding prime_int_altdef dvd_def
   169   apply auto
   170   by (metis div_mult_self1_is_id div_mult_self2_is_id
   171       int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
   172 
   173 lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   174   by (induct n) auto
   175 
   176 lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   177   by (induct n) (auto simp: prime_ge_0_int)
   178 
   179 lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
   180     p dvd x^n \<longleftrightarrow> p dvd x"
   181   by (cases n) (auto elim: prime_dvd_power_nat)
   182 
   183 lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
   184     p dvd x^n \<longleftrightarrow> p dvd x"
   185   by (cases n) (auto elim: prime_dvd_power_int)
   186 
   187 
   188 subsubsection {* Make prime naively executable *}
   189 
   190 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   191   by (simp add: prime_nat_def)
   192 
   193 lemma zero_not_prime_int [simp]: "~prime (0::int)"
   194   by (simp add: prime_int_def)
   195 
   196 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
   197   by (simp add: prime_nat_def)
   198 
   199 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   200   by (simp add: prime_nat_def)
   201 
   202 lemma one_not_prime_int [simp]: "~prime (1::int)"
   203   by (simp add: prime_int_def)
   204 
   205 lemma prime_nat_code [code]:
   206     "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   207   apply (simp add: Ball_def)
   208   apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
   209   done
   210 
   211 lemma prime_nat_simp:
   212     "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   213   by (auto simp add: prime_nat_code)
   214 
   215 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
   216 
   217 lemma prime_int_code [code]:
   218   "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
   219 proof
   220   assume "?L"
   221   then show "?R"
   222     by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
   223 next
   224   assume "?R"
   225   then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
   226 qed
   227 
   228 lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
   229   by (auto simp add: prime_int_code)
   230 
   231 lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m
   232 
   233 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   234   by simp
   235 
   236 lemma two_is_prime_int [simp]: "prime (2::int)"
   237   by simp
   238 
   239 text{* A bit of regression testing: *}
   240 
   241 lemma "prime(97::nat)" by simp
   242 lemma "prime(97::int)" by simp
   243 lemma "prime(997::nat)" by eval
   244 lemma "prime(997::int)" by eval
   245 
   246 
   247 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   248   by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
   249 
   250 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   251   by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
   252 
   253 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   254   by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
   255 
   256 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   257   by (metis leD linear prime_gt_0_int prime_imp_coprime_int prime_int_altdef)
   258 
   259 lemma primes_imp_powers_coprime_nat:
   260     "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   261   by (rule coprime_exp2_nat, rule primes_coprime_nat)
   262 
   263 lemma primes_imp_powers_coprime_int:
   264     "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   265   by (rule coprime_exp2_int, rule primes_coprime_int)
   266 
   267 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
   268   apply (induct n rule: nat_less_induct)
   269   apply (case_tac "n = 0")
   270   using two_is_prime_nat
   271   apply blast
   272   apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
   273     nat_dvd_not_less neq0_conv prime_nat_def)
   274   done
   275 
   276 text {* One property of coprimality is easier to prove via prime factors. *}
   277 
   278 lemma prime_divprod_pow_nat:
   279   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
   280   shows "p^n dvd a \<or> p^n dvd b"
   281 proof-
   282   { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
   283       apply (cases "n=0", simp_all)
   284       apply (cases "a=1", simp_all)
   285       done }
   286   moreover
   287   { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
   288     then obtain m where m: "n = Suc m" by (cases n) auto
   289     from n have "p dvd p^n" apply (intro dvd_power) apply auto done
   290     also note pab
   291     finally have pab': "p dvd a * b".
   292     from prime_dvd_mult_nat[OF p pab']
   293     have "p dvd a \<or> p dvd b" .
   294     moreover
   295     { assume pa: "p dvd a"
   296       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
   297       with p have "coprime b p"
   298         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   299       then have pnb: "coprime (p^n) b"
   300         by (subst gcd_commute_nat, rule coprime_exp_nat)
   301       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
   302     moreover
   303     { assume pb: "p dvd b"
   304       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
   305       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
   306         by auto
   307       with p have "coprime a p"
   308         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
   309       then have pna: "coprime (p^n) a"
   310         by (subst gcd_commute_nat, rule coprime_exp_nat)
   311       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
   312     ultimately have ?thesis by blast }
   313   ultimately show ?thesis by blast
   314 qed
   315 
   316 
   317 subsection {* Infinitely many primes *}
   318 
   319 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
   320 proof-
   321   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   322   from prime_factor_nat [OF f1]
   323   obtain p where "prime p" and "p dvd fact n + 1" by auto
   324   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   325   { assume "p \<le> n"
   326     from `prime p` have "p \<ge> 1" 
   327       by (cases p, simp_all)
   328     with `p <= n` have "p dvd fact n" 
   329       by (intro dvd_fact_nat)
   330     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   331       by (rule dvd_diff_nat)
   332     then have "p dvd 1" by simp
   333     then have "p <= 1" by auto
   334     moreover from `prime p` have "p > 1" by auto
   335     ultimately have False by auto}
   336   then have "n < p" by presburger
   337   with `prime p` and `p <= fact n + 1` show ?thesis by auto
   338 qed
   339 
   340 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
   341   using next_prime_bound by auto
   342 
   343 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   344 proof
   345   assume "finite {(p::nat). prime p}"
   346   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   347     by auto
   348   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   349     by auto
   350   with bigger_prime [of b] show False
   351     by auto
   352 qed
   353 
   354 subsection{*Powers of Primes*}
   355 
   356 text{*Versions for type nat only*}
   357 
   358 lemma prime_product: 
   359   fixes p::nat
   360   assumes "prime (p * q)"
   361   shows "p = 1 \<or> q = 1"
   362 proof -
   363   from assms have 
   364     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
   365     unfolding prime_nat_def by auto
   366   from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
   367   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   368   have "p dvd p * q" by simp
   369   then have "p = 1 \<or> p = p * q" by (rule P)
   370   then show ?thesis by (simp add: Q)
   371 qed
   372 
   373 lemma prime_exp: 
   374   fixes p::nat
   375   shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
   376 proof(induct n)
   377   case 0 thus ?case by simp
   378 next
   379   case (Suc n)
   380   {assume "p = 0" hence ?case by simp}
   381   moreover
   382   {assume "p=1" hence ?case by simp}
   383   moreover
   384   {assume p: "p \<noteq> 0" "p\<noteq>1"
   385     {assume pp: "prime (p^Suc n)"
   386       hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
   387       with p have n: "n = 0"
   388         by (metis One_nat_def nat_power_eq_Suc_0_iff)
   389       with pp have "prime p \<and> Suc n = 1" by simp}
   390     moreover
   391     {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
   392     ultimately have ?case by blast}
   393   ultimately show ?case by blast
   394 qed
   395 
   396 lemma prime_power_mult: 
   397   fixes p::nat
   398   assumes p: "prime p" and xy: "x * y = p ^ k"
   399   shows "\<exists>i j. x = p ^i \<and> y = p^ j"
   400 using xy
   401 proof(induct k arbitrary: x y)
   402   case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
   403 next
   404   case (Suc k x y)
   405   from Suc.prems have pxy: "p dvd x*y" by auto
   406   from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
   407   from p have p0: "p \<noteq> 0" by - (rule ccontr, simp) 
   408   {assume px: "p dvd x"
   409     then obtain d where d: "x = p*d" unfolding dvd_def by blast
   410     from Suc.prems d  have "p*d*y = p^Suc k" by simp
   411     hence th: "d*y = p^k" using p0 by simp
   412     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
   413     with d have "x = p^Suc i" by simp 
   414     with ij(2) have ?case by blast}
   415   moreover 
   416   {assume px: "p dvd y"
   417     then obtain d where d: "y = p*d" unfolding dvd_def by blast
   418     from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult_commute)
   419     hence th: "d*x = p^k" using p0 by simp
   420     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
   421     with d have "y = p^Suc i" by simp 
   422     with ij(2) have ?case by blast}
   423   ultimately show ?case  using pxyc by blast
   424 qed
   425 
   426 lemma prime_power_exp: 
   427   fixes p::nat
   428   assumes p: "prime p" and n: "n \<noteq> 0" 
   429     and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
   430   using n xn
   431 proof(induct n arbitrary: k)
   432   case 0 thus ?case by simp
   433 next
   434   case (Suc n k) hence th: "x*x^n = p^k" by simp
   435   {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
   436   moreover
   437   {assume n: "n \<noteq> 0"
   438     from prime_power_mult[OF p th] 
   439     obtain i j where ij: "x = p^i" "x^n = p^j"by blast
   440     from Suc.hyps[OF n ij(2)] have ?case .}
   441   ultimately show ?case by blast
   442 qed
   443 
   444 lemma divides_primepow:
   445   fixes p::nat
   446   assumes p: "prime p" 
   447   shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
   448 proof
   449   assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" 
   450     unfolding dvd_def  apply (auto simp add: mult_commute) by blast
   451   from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
   452   from e ij have "p^(i + j) = p^k" by (simp add: power_add)
   453   hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp 
   454   hence "i \<le> k" by arith
   455   with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
   456 next
   457   {fix i assume H: "i \<le> k" "d = p^i"
   458     then obtain j where j: "k = i + j"
   459       by (metis le_add_diff_inverse)
   460     hence "p^k = p^j*d" using H(2) by (simp add: power_add)
   461     hence "d dvd p^k" unfolding dvd_def by auto}
   462   thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
   463 qed
   464 
   465 subsection {*Chinese Remainder Theorem Variants*}
   466 
   467 lemma bezout_gcd_nat:
   468   fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
   469   using bezout_nat[of a b]
   470 by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute 
   471   gcd_nat.right_neutral mult_0) 
   472 
   473 lemma gcd_bezout_sum_nat:
   474   fixes a::nat 
   475   assumes "a * x + b * y = d" 
   476   shows "gcd a b dvd d"
   477 proof-
   478   let ?g = "gcd a b"
   479     have dv: "?g dvd a*x" "?g dvd b * y" 
   480       by simp_all
   481     from dvd_add[OF dv] assms
   482     show ?thesis by auto
   483 qed
   484 
   485 
   486 text {* A binary form of the Chinese Remainder Theorem. *}
   487 
   488 lemma chinese_remainder: 
   489   fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
   490   shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
   491 proof-
   492   from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
   493   obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1" 
   494     and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
   495   then have d12: "d1 = 1" "d2 =1"
   496     by (metis ab coprime_nat)+
   497   let ?x = "v * a * x1 + u * b * x2"
   498   let ?q1 = "v * x1 + u * y2"
   499   let ?q2 = "v * y1 + u * x2"
   500   from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
   501   have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
   502     apply (auto simp add: algebra_simps) 
   503     apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+
   504     done
   505   thus ?thesis by blast
   506 qed
   507 
   508 text {* Primality *}
   509 
   510 lemma coprime_bezout_strong:
   511   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
   512   shows "\<exists>x y. a * x = b * y + 1"
   513 by (metis assms bezout_nat gcd_nat.left_neutral)
   514 
   515 lemma bezout_prime: 
   516   assumes p: "prime p" and pa: "\<not> p dvd a"
   517   shows "\<exists>x y. a*x = Suc (p*y)"
   518 proof-
   519   have ap: "coprime a p"
   520     by (metis gcd_nat.commute p pa prime_imp_coprime_nat) 
   521   from coprime_bezout_strong[OF ap] show ?thesis
   522     by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa) 
   523 qed
   524 
   525 end