src/HOL/GCD.thy
author nipkow
Thu Jun 25 07:34:12 2009 +0200 (2009-06-25)
changeset 31798 fe9a3043d36c
parent 31766 f767c5b1702e
child 31813 4df828bbc411
permissions -rw-r--r--
Cleaned up GCD
     1 (*  Title:      GCD.thy
     2     Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     3                 Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
     4 
     5 
     6 This file deals with the functions gcd and lcm, and properties of
     7 primes. Definitions and lemmas are proved uniformly for the natural
     8 numbers and integers.
     9 
    10 This file combines and revises a number of prior developments.
    11 
    12 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    13 and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
    14 gcd, lcm, and prime for the natural numbers.
    15 
    16 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    17 extended gcd, lcm, primes to the integers. Amine Chaieb provided
    18 another extension of the notions to the integers, and added a number
    19 of results to "Primes" and "GCD". IntPrimes also defined and developed
    20 the congruence relations on the integers. The notion was extended to
    21 the natural numbers by Chiaeb.
    22 
    23 Tobias Nipkow cleaned up a lot.
    24 *)
    25 
    26 
    27 header {* GCD *}
    28 
    29 theory GCD
    30 imports NatTransfer
    31 begin
    32 
    33 declare One_nat_def [simp del]
    34 
    35 subsection {* gcd *}
    36 
    37 class gcd = one +
    38 
    39 fixes
    40   gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
    41   lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    42 
    43 begin
    44 
    45 abbreviation
    46   coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    47 where
    48   "coprime x y == (gcd x y = 1)"
    49 
    50 end
    51 
    52 class prime = one +
    53 
    54 fixes
    55   prime :: "'a \<Rightarrow> bool"
    56 
    57 
    58 (* definitions for the natural numbers *)
    59 
    60 instantiation nat :: gcd
    61 
    62 begin
    63 
    64 fun
    65   gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    66 where
    67   "gcd_nat x y =
    68    (if y = 0 then x else gcd y (x mod y))"
    69 
    70 definition
    71   lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    72 where
    73   "lcm_nat x y = x * y div (gcd x y)"
    74 
    75 instance proof qed
    76 
    77 end
    78 
    79 
    80 instantiation nat :: prime
    81 
    82 begin
    83 
    84 definition
    85   prime_nat :: "nat \<Rightarrow> bool"
    86 where
    87   [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    88 
    89 instance proof qed
    90 
    91 end
    92 
    93 
    94 (* definitions for the integers *)
    95 
    96 instantiation int :: gcd
    97 
    98 begin
    99 
   100 definition
   101   gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
   102 where
   103   "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
   104 
   105 definition
   106   lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
   107 where
   108   "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
   109 
   110 instance proof qed
   111 
   112 end
   113 
   114 
   115 instantiation int :: prime
   116 
   117 begin
   118 
   119 definition
   120   prime_int :: "int \<Rightarrow> bool"
   121 where
   122   [code del]: "prime_int p = prime (nat p)"
   123 
   124 instance proof qed
   125 
   126 end
   127 
   128 
   129 subsection {* Set up Transfer *}
   130 
   131 
   132 lemma transfer_nat_int_gcd:
   133   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   134   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   135   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
   136   unfolding gcd_int_def lcm_int_def prime_int_def
   137   by auto
   138 
   139 lemma transfer_nat_int_gcd_closures:
   140   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
   141   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   142   by (auto simp add: gcd_int_def lcm_int_def)
   143 
   144 declare TransferMorphism_nat_int[transfer add return:
   145     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   146 
   147 lemma transfer_int_nat_gcd:
   148   "gcd (int x) (int y) = int (gcd x y)"
   149   "lcm (int x) (int y) = int (lcm x y)"
   150   "prime (int x) = prime x"
   151   by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
   152 
   153 lemma transfer_int_nat_gcd_closures:
   154   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   155   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   156   by (auto simp add: gcd_int_def lcm_int_def)
   157 
   158 declare TransferMorphism_int_nat[transfer add return:
   159     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   160 
   161 
   162 
   163 subsection {* GCD *}
   164 
   165 (* was gcd_induct *)
   166 lemma nat_gcd_induct:
   167   fixes m n :: nat
   168   assumes "\<And>m. P m 0"
   169     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   170   shows "P m n"
   171   apply (rule gcd_nat.induct)
   172   apply (case_tac "y = 0")
   173   using assms apply simp_all
   174 done
   175 
   176 (* specific to int *)
   177 
   178 lemma int_gcd_neg1 [simp]: "gcd (-x::int) y = gcd x y"
   179   by (simp add: gcd_int_def)
   180 
   181 lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y"
   182   by (simp add: gcd_int_def)
   183 
   184 lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)"
   185   by (simp add: gcd_int_def)
   186 
   187 lemma int_gcd_cases:
   188   fixes x :: int and y
   189   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   190       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   191       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   192       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   193   shows "P (gcd x y)"
   194 by (insert prems, auto simp add: int_gcd_neg1 int_gcd_neg2, arith)
   195 
   196 lemma int_gcd_ge_0 [simp]: "gcd (x::int) y >= 0"
   197   by (simp add: gcd_int_def)
   198 
   199 lemma int_lcm_neg1: "lcm (-x::int) y = lcm x y"
   200   by (simp add: lcm_int_def)
   201 
   202 lemma int_lcm_neg2: "lcm (x::int) (-y) = lcm x y"
   203   by (simp add: lcm_int_def)
   204 
   205 lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)"
   206   by (simp add: lcm_int_def)
   207 
   208 lemma int_lcm_cases:
   209   fixes x :: int and y
   210   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   211       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   212       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   213       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   214   shows "P (lcm x y)"
   215 by (insert prems, auto simp add: int_lcm_neg1 int_lcm_neg2, arith)
   216 
   217 lemma int_lcm_ge_0 [simp]: "lcm (x::int) y >= 0"
   218   by (simp add: lcm_int_def)
   219 
   220 (* was gcd_0, etc. *)
   221 lemma nat_gcd_0 [simp]: "gcd (x::nat) 0 = x"
   222   by simp
   223 
   224 (* was igcd_0, etc. *)
   225 lemma int_gcd_0 [simp]: "gcd (x::int) 0 = abs x"
   226   by (unfold gcd_int_def, auto)
   227 
   228 lemma nat_gcd_0_left [simp]: "gcd 0 (x::nat) = x"
   229   by simp
   230 
   231 lemma int_gcd_0_left [simp]: "gcd 0 (x::int) = abs x"
   232   by (unfold gcd_int_def, auto)
   233 
   234 lemma nat_gcd_red: "gcd (x::nat) y = gcd y (x mod y)"
   235   by (case_tac "y = 0", auto)
   236 
   237 (* weaker, but useful for the simplifier *)
   238 
   239 lemma nat_gcd_non_0: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   240   by simp
   241 
   242 lemma nat_gcd_1 [simp]: "gcd (m::nat) 1 = 1"
   243   by simp
   244 
   245 lemma nat_gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   246   by (simp add: One_nat_def)
   247 
   248 lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1"
   249   by (simp add: gcd_int_def)
   250 
   251 lemma nat_gcd_idem: "gcd (x::nat) x = x"
   252 by simp
   253 
   254 lemma int_gcd_idem: "gcd (x::int) x = abs x"
   255 by (subst int_gcd_abs, auto simp add: gcd_int_def)
   256 
   257 declare gcd_nat.simps [simp del]
   258 
   259 text {*
   260   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   261   conjunctions don't seem provable separately.
   262 *}
   263 
   264 lemma nat_gcd_dvd1 [iff]: "(gcd (m::nat)) n dvd m"
   265   and nat_gcd_dvd2 [iff]: "(gcd m n) dvd n"
   266   apply (induct m n rule: nat_gcd_induct)
   267   apply (simp_all add: nat_gcd_non_0)
   268   apply (blast dest: dvd_mod_imp_dvd)
   269 done
   270 
   271 lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
   272   apply (subst int_gcd_abs)
   273   apply (rule dvd_trans)
   274   apply (rule nat_gcd_dvd1 [transferred])
   275   apply auto
   276 done
   277 
   278 lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y"
   279   apply (subst int_gcd_abs)
   280   apply (rule dvd_trans)
   281   apply (rule nat_gcd_dvd2 [transferred])
   282   apply auto
   283 done
   284 
   285 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   286 by(metis nat_gcd_dvd1 dvd_trans)
   287 
   288 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   289 by(metis nat_gcd_dvd2 dvd_trans)
   290 
   291 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   292 by(metis int_gcd_dvd1 dvd_trans)
   293 
   294 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   295 by(metis int_gcd_dvd2 dvd_trans)
   296 
   297 lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   298   by (rule dvd_imp_le, auto)
   299 
   300 lemma nat_gcd_le2 [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   301   by (rule dvd_imp_le, auto)
   302 
   303 lemma int_gcd_le1 [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   304   by (rule zdvd_imp_le, auto)
   305 
   306 lemma int_gcd_le2 [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   307   by (rule zdvd_imp_le, auto)
   308 
   309 lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   310 by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
   311 
   312 lemma int_gcd_greatest:
   313   assumes "(k::int) dvd m" and "k dvd n"
   314   shows "k dvd gcd m n"
   315 
   316   apply (subst int_gcd_abs)
   317   apply (subst abs_dvd_iff [symmetric])
   318   apply (rule nat_gcd_greatest [transferred])
   319   using prems apply auto
   320 done
   321 
   322 lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) =
   323     (k dvd m & k dvd n)"
   324   by (blast intro!: nat_gcd_greatest intro: dvd_trans)
   325 
   326 lemma int_gcd_greatest_iff: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   327   by (blast intro!: int_gcd_greatest intro: dvd_trans)
   328 
   329 lemma nat_gcd_zero [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   330   by (simp only: dvd_0_left_iff [symmetric] nat_gcd_greatest_iff)
   331 
   332 lemma int_gcd_zero [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   333   by (auto simp add: gcd_int_def)
   334 
   335 lemma nat_gcd_pos [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   336   by (insert nat_gcd_zero [of m n], arith)
   337 
   338 lemma int_gcd_pos [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   339   by (insert int_gcd_zero [of m n], insert int_gcd_ge_0 [of m n], arith)
   340 
   341 lemma nat_gcd_commute: "gcd (m::nat) n = gcd n m"
   342   by (rule dvd_anti_sym, auto)
   343 
   344 lemma int_gcd_commute: "gcd (m::int) n = gcd n m"
   345   by (auto simp add: gcd_int_def nat_gcd_commute)
   346 
   347 lemma nat_gcd_assoc: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
   348   apply (rule dvd_anti_sym)
   349   apply (blast intro: dvd_trans)+
   350 done
   351 
   352 lemma int_gcd_assoc: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
   353   by (auto simp add: gcd_int_def nat_gcd_assoc)
   354 
   355 lemmas nat_gcd_left_commute =
   356   mk_left_commute[of gcd, OF nat_gcd_assoc nat_gcd_commute]
   357 
   358 lemmas int_gcd_left_commute =
   359   mk_left_commute[of gcd, OF int_gcd_assoc int_gcd_commute]
   360 
   361 lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute
   362   -- {* gcd is an AC-operator *}
   363 
   364 lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute
   365 
   366 lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and>
   367     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   368   apply auto
   369   apply (rule dvd_anti_sym)
   370   apply (erule (1) nat_gcd_greatest)
   371   apply auto
   372 done
   373 
   374 lemma int_gcd_unique: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   375     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   376   apply (case_tac "d = 0")
   377   apply force
   378   apply (rule iffI)
   379   apply (rule zdvd_anti_sym)
   380   apply arith
   381   apply (subst int_gcd_pos)
   382   apply clarsimp
   383   apply (drule_tac x = "d + 1" in spec)
   384   apply (frule zdvd_imp_le)
   385   apply (auto intro: int_gcd_greatest)
   386 done
   387 
   388 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   389 by (metis dvd.eq_iff nat_gcd_unique)
   390 
   391 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   392 by (metis dvd.eq_iff nat_gcd_unique)
   393 
   394 lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   395 by (metis abs_dvd_iff abs_eq_0 int_gcd_0_left int_gcd_abs int_gcd_unique)
   396 
   397 lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   398 by (metis gcd_proj1_if_dvd_int int_gcd_commute)
   399 
   400 
   401 text {*
   402   \medskip Multiplication laws
   403 *}
   404 
   405 lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   406     -- {* \cite[page 27]{davenport92} *}
   407   apply (induct m n rule: nat_gcd_induct)
   408   apply simp
   409   apply (case_tac "k = 0")
   410   apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2)
   411 done
   412 
   413 lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   414   apply (subst (1 2) int_gcd_abs)
   415   apply (simp add: abs_mult)
   416   apply (rule nat_gcd_mult_distrib [transferred])
   417   apply auto
   418 done
   419 
   420 lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   421   apply (insert nat_gcd_mult_distrib [of m k n])
   422   apply simp
   423   apply (erule_tac t = m in ssubst)
   424   apply simp
   425   done
   426 
   427 lemma int_coprime_dvd_mult:
   428   assumes "coprime (k::int) n" and "k dvd m * n"
   429   shows "k dvd m"
   430 
   431   using prems
   432   apply (subst abs_dvd_iff [symmetric])
   433   apply (subst dvd_abs_iff [symmetric])
   434   apply (subst (asm) int_gcd_abs)
   435   apply (rule nat_coprime_dvd_mult [transferred])
   436   apply auto
   437   apply (subst abs_mult [symmetric], auto)
   438 done
   439 
   440 lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow>
   441     (k dvd m * n) = (k dvd m)"
   442   by (auto intro: nat_coprime_dvd_mult)
   443 
   444 lemma int_coprime_dvd_mult_iff: "coprime (k::int) n \<Longrightarrow>
   445     (k dvd m * n) = (k dvd m)"
   446   by (auto intro: int_coprime_dvd_mult)
   447 
   448 lemma nat_gcd_mult_cancel: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   449   apply (rule dvd_anti_sym)
   450   apply (rule nat_gcd_greatest)
   451   apply (rule_tac n = k in nat_coprime_dvd_mult)
   452   apply (simp add: nat_gcd_assoc)
   453   apply (simp add: nat_gcd_commute)
   454   apply (simp_all add: mult_commute)
   455 done
   456 
   457 lemma int_gcd_mult_cancel:
   458   assumes "coprime (k::int) n"
   459   shows "gcd (k * m) n = gcd m n"
   460 
   461   using prems
   462   apply (subst (1 2) int_gcd_abs)
   463   apply (subst abs_mult)
   464   apply (rule nat_gcd_mult_cancel [transferred])
   465   apply (auto simp add: int_gcd_abs [symmetric])
   466 done
   467 
   468 text {* \medskip Addition laws *}
   469 
   470 lemma nat_gcd_add1 [simp]: "gcd ((m::nat) + n) n = gcd m n"
   471   apply (case_tac "n = 0")
   472   apply (simp_all add: nat_gcd_non_0)
   473 done
   474 
   475 lemma nat_gcd_add2 [simp]: "gcd (m::nat) (m + n) = gcd m n"
   476   apply (subst (1 2) nat_gcd_commute)
   477   apply (subst add_commute)
   478   apply simp
   479 done
   480 
   481 (* to do: add the other variations? *)
   482 
   483 lemma nat_gcd_diff1: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   484   by (subst nat_gcd_add1 [symmetric], auto)
   485 
   486 lemma nat_gcd_diff2: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   487   apply (subst nat_gcd_commute)
   488   apply (subst nat_gcd_diff1 [symmetric])
   489   apply auto
   490   apply (subst nat_gcd_commute)
   491   apply (subst nat_gcd_diff1)
   492   apply assumption
   493   apply (rule nat_gcd_commute)
   494 done
   495 
   496 lemma int_gcd_non_0: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   497   apply (frule_tac b = y and a = x in pos_mod_sign)
   498   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   499   apply (auto simp add: nat_gcd_non_0 nat_mod_distrib [symmetric]
   500     zmod_zminus1_eq_if)
   501   apply (frule_tac a = x in pos_mod_bound)
   502   apply (subst (1 2) nat_gcd_commute)
   503   apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2
   504     nat_le_eq_zle)
   505 done
   506 
   507 lemma int_gcd_red: "gcd (x::int) y = gcd y (x mod y)"
   508   apply (case_tac "y = 0")
   509   apply force
   510   apply (case_tac "y > 0")
   511   apply (subst int_gcd_non_0, auto)
   512   apply (insert int_gcd_non_0 [of "-y" "-x"])
   513   apply (auto simp add: int_gcd_neg1 int_gcd_neg2)
   514 done
   515 
   516 lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n"
   517 by (metis int_gcd_red mod_add_self1 zadd_commute)
   518 
   519 lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n"
   520 by (metis int_gcd_add1 int_gcd_commute zadd_commute)
   521 
   522 lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n"
   523 by (metis mod_mult_self3 nat_gcd_commute nat_gcd_red)
   524 
   525 lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n"
   526 by (metis int_gcd_commute int_gcd_red mod_mult_self1 zadd_commute)
   527 
   528 
   529 (* to do: differences, and all variations of addition rules
   530     as simplification rules for nat and int *)
   531 
   532 (* FIXME remove iff *)
   533 lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n"
   534   using mult_dvd_mono [of 1] by auto
   535 
   536 (* to do: add the three variations of these, and for ints? *)
   537 
   538 lemma finite_divisors_nat:
   539   assumes "(m::nat)~= 0" shows "finite{d. d dvd m}"
   540 proof-
   541   have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
   542   from finite_subset[OF _ this] show ?thesis using assms
   543     by(bestsimp intro!:dvd_imp_le)
   544 qed
   545 
   546 lemma finite_divisors_int:
   547   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
   548 proof-
   549   have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
   550   hence "finite{d. abs d <= abs i}" by simp
   551   from finite_subset[OF _ this] show ?thesis using assms
   552     by(bestsimp intro!:dvd_imp_le_int)
   553 qed
   554 
   555 lemma gcd_is_Max_divisors_nat:
   556   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
   557 apply(rule Max_eqI[THEN sym])
   558   apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat)
   559  apply simp
   560  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le nat_gcd_greatest_iff nat_gcd_pos)
   561 apply simp
   562 done
   563 
   564 lemma gcd_is_Max_divisors_int:
   565   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
   566 apply(rule Max_eqI[THEN sym])
   567   apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int)
   568  apply simp
   569  apply (metis int_gcd_greatest_iff int_gcd_pos zdvd_imp_le)
   570 apply simp
   571 done
   572 
   573 
   574 subsection {* Coprimality *}
   575 
   576 lemma nat_div_gcd_coprime [intro]:
   577   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   578   shows "coprime (a div gcd a b) (b div gcd a b)"
   579 proof -
   580   let ?g = "gcd a b"
   581   let ?a' = "a div ?g"
   582   let ?b' = "b div ?g"
   583   let ?g' = "gcd ?a' ?b'"
   584   have dvdg: "?g dvd a" "?g dvd b" by simp_all
   585   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   586   from dvdg dvdg' obtain ka kb ka' kb' where
   587       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   588     unfolding dvd_def by blast
   589   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   590     by simp_all
   591   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   592     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   593       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   594   have "?g \<noteq> 0" using nz by (simp add: nat_gcd_zero)
   595   then have gp: "?g > 0" by arith
   596   from nat_gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   597   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   598 qed
   599 
   600 lemma int_div_gcd_coprime [intro]:
   601   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   602   shows "coprime (a div gcd a b) (b div gcd a b)"
   603 
   604   apply (subst (1 2 3) int_gcd_abs)
   605   apply (subst (1 2) abs_div)
   606   apply auto
   607   prefer 3
   608   apply (rule nat_div_gcd_coprime [transferred])
   609   using nz apply (auto simp add: int_gcd_abs [symmetric])
   610 done
   611 
   612 lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   613   using nat_gcd_unique[of 1 a b, simplified] by auto
   614 
   615 lemma nat_coprime_Suc_0:
   616     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   617   using nat_coprime by (simp add: One_nat_def)
   618 
   619 lemma int_coprime: "coprime (a::int) b \<longleftrightarrow>
   620     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   621   using int_gcd_unique [of 1 a b]
   622   apply clarsimp
   623   apply (erule subst)
   624   apply (rule iffI)
   625   apply force
   626   apply (drule_tac x = "abs e" in exI)
   627   apply (case_tac "e >= 0")
   628   apply force
   629   apply force
   630 done
   631 
   632 lemma nat_gcd_coprime:
   633   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   634     b: "b = b' * gcd a b"
   635   shows    "coprime a' b'"
   636 
   637   apply (subgoal_tac "a' = a div gcd a b")
   638   apply (erule ssubst)
   639   apply (subgoal_tac "b' = b div gcd a b")
   640   apply (erule ssubst)
   641   apply (rule nat_div_gcd_coprime)
   642   using prems
   643   apply force
   644   apply (subst (1) b)
   645   using z apply force
   646   apply (subst (1) a)
   647   using z apply force
   648 done
   649 
   650 lemma int_gcd_coprime:
   651   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   652     b: "b = b' * gcd a b"
   653   shows    "coprime a' b'"
   654 
   655   apply (subgoal_tac "a' = a div gcd a b")
   656   apply (erule ssubst)
   657   apply (subgoal_tac "b' = b div gcd a b")
   658   apply (erule ssubst)
   659   apply (rule int_div_gcd_coprime)
   660   using prems
   661   apply force
   662   apply (subst (1) b)
   663   using z apply force
   664   apply (subst (1) a)
   665   using z apply force
   666 done
   667 
   668 lemma nat_coprime_mult: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   669     shows "coprime d (a * b)"
   670   apply (subst nat_gcd_commute)
   671   using da apply (subst nat_gcd_mult_cancel)
   672   apply (subst nat_gcd_commute, assumption)
   673   apply (subst nat_gcd_commute, rule db)
   674 done
   675 
   676 lemma int_coprime_mult: assumes da: "coprime (d::int) a" and db: "coprime d b"
   677     shows "coprime d (a * b)"
   678   apply (subst int_gcd_commute)
   679   using da apply (subst int_gcd_mult_cancel)
   680   apply (subst int_gcd_commute, assumption)
   681   apply (subst int_gcd_commute, rule db)
   682 done
   683 
   684 lemma nat_coprime_lmult:
   685   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   686 proof -
   687   have "gcd d a dvd gcd d (a * b)"
   688     by (rule nat_gcd_greatest, auto)
   689   with dab show ?thesis
   690     by auto
   691 qed
   692 
   693 lemma int_coprime_lmult:
   694   assumes "coprime (d::int) (a * b)" shows "coprime d a"
   695 proof -
   696   have "gcd d a dvd gcd d (a * b)"
   697     by (rule int_gcd_greatest, auto)
   698   with assms show ?thesis
   699     by auto
   700 qed
   701 
   702 lemma nat_coprime_rmult:
   703   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   704 proof -
   705   have "gcd d b dvd gcd d (a * b)"
   706     by (rule nat_gcd_greatest, auto intro: dvd_mult)
   707   with assms show ?thesis
   708     by auto
   709 qed
   710 
   711 lemma int_coprime_rmult:
   712   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   713 proof -
   714   have "gcd d b dvd gcd d (a * b)"
   715     by (rule int_gcd_greatest, auto intro: dvd_mult)
   716   with dab show ?thesis
   717     by auto
   718 qed
   719 
   720 lemma nat_coprime_mul_eq: "coprime (d::nat) (a * b) \<longleftrightarrow>
   721     coprime d a \<and>  coprime d b"
   722   using nat_coprime_rmult[of d a b] nat_coprime_lmult[of d a b]
   723     nat_coprime_mult[of d a b]
   724   by blast
   725 
   726 lemma int_coprime_mul_eq: "coprime (d::int) (a * b) \<longleftrightarrow>
   727     coprime d a \<and>  coprime d b"
   728   using int_coprime_rmult[of d a b] int_coprime_lmult[of d a b]
   729     int_coprime_mult[of d a b]
   730   by blast
   731 
   732 lemma nat_gcd_coprime_exists:
   733     assumes nz: "gcd (a::nat) b \<noteq> 0"
   734     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   735   apply (rule_tac x = "a div gcd a b" in exI)
   736   apply (rule_tac x = "b div gcd a b" in exI)
   737   using nz apply (auto simp add: nat_div_gcd_coprime dvd_div_mult)
   738 done
   739 
   740 lemma int_gcd_coprime_exists:
   741     assumes nz: "gcd (a::int) b \<noteq> 0"
   742     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   743   apply (rule_tac x = "a div gcd a b" in exI)
   744   apply (rule_tac x = "b div gcd a b" in exI)
   745   using nz apply (auto simp add: int_div_gcd_coprime dvd_div_mult_self)
   746 done
   747 
   748 lemma nat_coprime_exp: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   749   by (induct n, simp_all add: nat_coprime_mult)
   750 
   751 lemma int_coprime_exp: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   752   by (induct n, simp_all add: int_coprime_mult)
   753 
   754 lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   755   apply (rule nat_coprime_exp)
   756   apply (subst nat_gcd_commute)
   757   apply (rule nat_coprime_exp)
   758   apply (subst nat_gcd_commute, assumption)
   759 done
   760 
   761 lemma int_coprime_exp2 [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   762   apply (rule int_coprime_exp)
   763   apply (subst int_gcd_commute)
   764   apply (rule int_coprime_exp)
   765   apply (subst int_gcd_commute, assumption)
   766 done
   767 
   768 lemma nat_gcd_exp: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   769 proof (cases)
   770   assume "a = 0 & b = 0"
   771   thus ?thesis by simp
   772   next assume "~(a = 0 & b = 0)"
   773   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   774     by auto
   775   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   776       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   777     apply (subst (1 2) mult_commute)
   778     apply (subst nat_gcd_mult_distrib [symmetric])
   779     apply simp
   780     done
   781   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   782     apply (subst div_power)
   783     apply auto
   784     apply (rule dvd_div_mult_self)
   785     apply (rule dvd_power_same)
   786     apply auto
   787     done
   788   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
   789     apply (subst div_power)
   790     apply auto
   791     apply (rule dvd_div_mult_self)
   792     apply (rule dvd_power_same)
   793     apply auto
   794     done
   795   finally show ?thesis .
   796 qed
   797 
   798 lemma int_gcd_exp: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   799   apply (subst (1 2) int_gcd_abs)
   800   apply (subst (1 2) power_abs)
   801   apply (rule nat_gcd_exp [where n = n, transferred])
   802   apply auto
   803 done
   804 
   805 lemma nat_coprime_divprod: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   806   using nat_coprime_dvd_mult_iff[of d a b]
   807   by (auto simp add: mult_commute)
   808 
   809 lemma int_coprime_divprod: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   810   using int_coprime_dvd_mult_iff[of d a b]
   811   by (auto simp add: mult_commute)
   812 
   813 lemma nat_division_decomp: assumes dc: "(a::nat) dvd b * c"
   814   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   815 proof-
   816   let ?g = "gcd a b"
   817   {assume "?g = 0" with dc have ?thesis by auto}
   818   moreover
   819   {assume z: "?g \<noteq> 0"
   820     from nat_gcd_coprime_exists[OF z]
   821     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   822       by blast
   823     have thb: "?g dvd b" by auto
   824     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   825     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   826     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   827     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   828     with z have th_1: "a' dvd b' * c" by auto
   829     from nat_coprime_dvd_mult[OF ab'(3)] th_1
   830     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   831     from ab' have "a = ?g*a'" by algebra
   832     with thb thc have ?thesis by blast }
   833   ultimately show ?thesis by blast
   834 qed
   835 
   836 lemma int_division_decomp: assumes dc: "(a::int) dvd b * c"
   837   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   838 proof-
   839   let ?g = "gcd a b"
   840   {assume "?g = 0" with dc have ?thesis by auto}
   841   moreover
   842   {assume z: "?g \<noteq> 0"
   843     from int_gcd_coprime_exists[OF z]
   844     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   845       by blast
   846     have thb: "?g dvd b" by auto
   847     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   848     with dc have th0: "a' dvd b*c"
   849       using dvd_trans[of a' a "b*c"] by simp
   850     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   851     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   852     with z have th_1: "a' dvd b' * c" by auto
   853     from int_coprime_dvd_mult[OF ab'(3)] th_1
   854     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   855     from ab' have "a = ?g*a'" by algebra
   856     with thb thc have ?thesis by blast }
   857   ultimately show ?thesis by blast
   858 qed
   859 
   860 lemma nat_pow_divides_pow:
   861   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   862   shows "a dvd b"
   863 proof-
   864   let ?g = "gcd a b"
   865   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   866   {assume "?g = 0" with ab n have ?thesis by auto }
   867   moreover
   868   {assume z: "?g \<noteq> 0"
   869     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   870     from nat_gcd_coprime_exists[OF z]
   871     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   872       by blast
   873     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   874       by (simp add: ab'(1,2)[symmetric])
   875     hence "?g^n*a'^n dvd ?g^n *b'^n"
   876       by (simp only: power_mult_distrib mult_commute)
   877     with zn z n have th0:"a'^n dvd b'^n" by auto
   878     have "a' dvd a'^n" by (simp add: m)
   879     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   880     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   881     from nat_coprime_dvd_mult[OF nat_coprime_exp [OF ab'(3), of m]] th1
   882     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   883     hence "a'*?g dvd b'*?g" by simp
   884     with ab'(1,2)  have ?thesis by simp }
   885   ultimately show ?thesis by blast
   886 qed
   887 
   888 lemma int_pow_divides_pow:
   889   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
   890   shows "a dvd b"
   891 proof-
   892   let ?g = "gcd a b"
   893   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   894   {assume "?g = 0" with ab n have ?thesis by auto }
   895   moreover
   896   {assume z: "?g \<noteq> 0"
   897     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   898     from int_gcd_coprime_exists[OF z]
   899     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   900       by blast
   901     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   902       by (simp add: ab'(1,2)[symmetric])
   903     hence "?g^n*a'^n dvd ?g^n *b'^n"
   904       by (simp only: power_mult_distrib mult_commute)
   905     with zn z n have th0:"a'^n dvd b'^n" by auto
   906     have "a' dvd a'^n" by (simp add: m)
   907     with th0 have "a' dvd b'^n"
   908       using dvd_trans[of a' "a'^n" "b'^n"] by simp
   909     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   910     from int_coprime_dvd_mult[OF int_coprime_exp [OF ab'(3), of m]] th1
   911     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   912     hence "a'*?g dvd b'*?g" by simp
   913     with ab'(1,2)  have ?thesis by simp }
   914   ultimately show ?thesis by blast
   915 qed
   916 
   917 (* FIXME move to Divides(?) *)
   918 lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   919   by (auto intro: nat_pow_divides_pow dvd_power_same)
   920 
   921 lemma int_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   922   by (auto intro: int_pow_divides_pow dvd_power_same)
   923 
   924 lemma nat_divides_mult:
   925   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   926   shows "m * n dvd r"
   927 proof-
   928   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   929     unfolding dvd_def by blast
   930   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   931   hence "m dvd n'" using nat_coprime_dvd_mult_iff[OF mn] by simp
   932   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   933   from n' k show ?thesis unfolding dvd_def by auto
   934 qed
   935 
   936 lemma int_divides_mult:
   937   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   938   shows "m * n dvd r"
   939 proof-
   940   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   941     unfolding dvd_def by blast
   942   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   943   hence "m dvd n'" using int_coprime_dvd_mult_iff[OF mn] by simp
   944   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   945   from n' k show ?thesis unfolding dvd_def by auto
   946 qed
   947 
   948 lemma nat_coprime_plus_one [simp]: "coprime ((n::nat) + 1) n"
   949   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   950   apply force
   951   apply (rule nat_dvd_diff)
   952   apply auto
   953 done
   954 
   955 lemma nat_coprime_Suc [simp]: "coprime (Suc n) n"
   956   using nat_coprime_plus_one by (simp add: One_nat_def)
   957 
   958 lemma int_coprime_plus_one [simp]: "coprime ((n::int) + 1) n"
   959   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   960   apply force
   961   apply (rule dvd_diff)
   962   apply auto
   963 done
   964 
   965 lemma nat_coprime_minus_one: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   966   using nat_coprime_plus_one [of "n - 1"]
   967     nat_gcd_commute [of "n - 1" n] by auto
   968 
   969 lemma int_coprime_minus_one: "coprime ((n::int) - 1) n"
   970   using int_coprime_plus_one [of "n - 1"]
   971     int_gcd_commute [of "n - 1" n] by auto
   972 
   973 lemma nat_setprod_coprime [rule_format]:
   974     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
   975   apply (case_tac "finite A")
   976   apply (induct set: finite)
   977   apply (auto simp add: nat_gcd_mult_cancel)
   978 done
   979 
   980 lemma int_setprod_coprime [rule_format]:
   981     "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
   982   apply (case_tac "finite A")
   983   apply (induct set: finite)
   984   apply (auto simp add: int_gcd_mult_cancel)
   985 done
   986 
   987 lemma nat_prime_odd: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   988   unfolding prime_nat_def
   989   apply (subst even_mult_two_ex)
   990   apply clarify
   991   apply (drule_tac x = 2 in spec)
   992   apply auto
   993 done
   994 
   995 lemma int_prime_odd: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   996   unfolding prime_int_def
   997   apply (frule nat_prime_odd)
   998   apply (auto simp add: even_nat_def)
   999 done
  1000 
  1001 lemma nat_coprime_common_divisor: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1002     x dvd b \<Longrightarrow> x = 1"
  1003   apply (subgoal_tac "x dvd gcd a b")
  1004   apply simp
  1005   apply (erule (1) nat_gcd_greatest)
  1006 done
  1007 
  1008 lemma int_coprime_common_divisor: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1009     x dvd b \<Longrightarrow> abs x = 1"
  1010   apply (subgoal_tac "x dvd gcd a b")
  1011   apply simp
  1012   apply (erule (1) int_gcd_greatest)
  1013 done
  1014 
  1015 lemma nat_coprime_divisors: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
  1016     coprime d e"
  1017   apply (auto simp add: dvd_def)
  1018   apply (frule int_coprime_lmult)
  1019   apply (subst int_gcd_commute)
  1020   apply (subst (asm) (2) int_gcd_commute)
  1021   apply (erule int_coprime_lmult)
  1022 done
  1023 
  1024 lemma nat_invertible_coprime: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1025 apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red)
  1026 done
  1027 
  1028 lemma int_invertible_coprime: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1029 apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red)
  1030 done
  1031 
  1032 
  1033 subsection {* Bezout's theorem *}
  1034 
  1035 (* Function bezw returns a pair of witnesses to Bezout's theorem --
  1036    see the theorems that follow the definition. *)
  1037 fun
  1038   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1039 where
  1040   "bezw x y =
  1041   (if y = 0 then (1, 0) else
  1042       (snd (bezw y (x mod y)),
  1043        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1044 
  1045 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1046 
  1047 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1048        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1049   by simp
  1050 
  1051 declare bezw.simps [simp del]
  1052 
  1053 lemma bezw_aux [rule_format]:
  1054     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1055 proof (induct x y rule: nat_gcd_induct)
  1056   fix m :: nat
  1057   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1058     by auto
  1059   next fix m :: nat and n
  1060     assume ngt0: "n > 0" and
  1061       ih: "fst (bezw n (m mod n)) * int n +
  1062         snd (bezw n (m mod n)) * int (m mod n) =
  1063         int (gcd n (m mod n))"
  1064     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1065       apply (simp add: bezw_non_0 nat_gcd_non_0)
  1066       apply (erule subst)
  1067       apply (simp add: ring_simps)
  1068       apply (subst mod_div_equality [of m n, symmetric])
  1069       (* applying simp here undoes the last substitution!
  1070          what is procedure cancel_div_mod? *)
  1071       apply (simp only: ring_simps zadd_int [symmetric]
  1072         zmult_int [symmetric])
  1073       done
  1074 qed
  1075 
  1076 lemma int_bezout:
  1077   fixes x y
  1078   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1079 proof -
  1080   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1081       EX u v. u * x + v * y = gcd x y"
  1082     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1083     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1084     apply (unfold gcd_int_def)
  1085     apply simp
  1086     apply (subst bezw_aux [symmetric])
  1087     apply auto
  1088     done
  1089   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1090       (x \<le> 0 \<and> y \<le> 0)"
  1091     by auto
  1092   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1093     by (erule (1) bezout_aux)
  1094   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1095     apply (insert bezout_aux [of x "-y"])
  1096     apply auto
  1097     apply (rule_tac x = u in exI)
  1098     apply (rule_tac x = "-v" in exI)
  1099     apply (subst int_gcd_neg2 [symmetric])
  1100     apply auto
  1101     done
  1102   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1103     apply (insert bezout_aux [of "-x" y])
  1104     apply auto
  1105     apply (rule_tac x = "-u" in exI)
  1106     apply (rule_tac x = v in exI)
  1107     apply (subst int_gcd_neg1 [symmetric])
  1108     apply auto
  1109     done
  1110   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1111     apply (insert bezout_aux [of "-x" "-y"])
  1112     apply auto
  1113     apply (rule_tac x = "-u" in exI)
  1114     apply (rule_tac x = "-v" in exI)
  1115     apply (subst int_gcd_neg1 [symmetric])
  1116     apply (subst int_gcd_neg2 [symmetric])
  1117     apply auto
  1118     done
  1119   ultimately show ?thesis by blast
  1120 qed
  1121 
  1122 text {* versions of Bezout for nat, by Amine Chaieb *}
  1123 
  1124 lemma ind_euclid:
  1125   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1126   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1127   shows "P a b"
  1128 proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
  1129   fix n a b
  1130   assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
  1131   have "a = b \<or> a < b \<or> b < a" by arith
  1132   moreover {assume eq: "a= b"
  1133     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1134     by simp}
  1135   moreover
  1136   {assume lt: "a < b"
  1137     hence "a + b - a < n \<or> a = 0"  using H(2) by arith
  1138     moreover
  1139     {assume "a =0" with z c have "P a b" by blast }
  1140     moreover
  1141     {assume ab: "a + b - a < n"
  1142       have th0: "a + b - a = a + (b - a)" using lt by arith
  1143       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1144       have "P a b" by (simp add: th0[symmetric])}
  1145     ultimately have "P a b" by blast}
  1146   moreover
  1147   {assume lt: "a > b"
  1148     hence "b + a - b < n \<or> b = 0"  using H(2) by arith
  1149     moreover
  1150     {assume "b =0" with z c have "P a b" by blast }
  1151     moreover
  1152     {assume ab: "b + a - b < n"
  1153       have th0: "b + a - b = b + (a - b)" using lt by arith
  1154       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1155       have "P b a" by (simp add: th0[symmetric])
  1156       hence "P a b" using c by blast }
  1157     ultimately have "P a b" by blast}
  1158 ultimately  show "P a b" by blast
  1159 qed
  1160 
  1161 lemma nat_bezout_lemma:
  1162   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1163     (a * x = b * y + d \<or> b * x = a * y + d)"
  1164   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1165     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1166   using ex
  1167   apply clarsimp
  1168   apply (rule_tac x="d" in exI, simp add: dvd_add)
  1169   apply (case_tac "a * x = b * y + d" , simp_all)
  1170   apply (rule_tac x="x + y" in exI)
  1171   apply (rule_tac x="y" in exI)
  1172   apply algebra
  1173   apply (rule_tac x="x" in exI)
  1174   apply (rule_tac x="x + y" in exI)
  1175   apply algebra
  1176 done
  1177 
  1178 lemma nat_bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1179     (a * x = b * y + d \<or> b * x = a * y + d)"
  1180   apply(induct a b rule: ind_euclid)
  1181   apply blast
  1182   apply clarify
  1183   apply (rule_tac x="a" in exI, simp add: dvd_add)
  1184   apply clarsimp
  1185   apply (rule_tac x="d" in exI)
  1186   apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  1187   apply (rule_tac x="x+y" in exI)
  1188   apply (rule_tac x="y" in exI)
  1189   apply algebra
  1190   apply (rule_tac x="x" in exI)
  1191   apply (rule_tac x="x+y" in exI)
  1192   apply algebra
  1193 done
  1194 
  1195 lemma nat_bezout1: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1196     (a * x - b * y = d \<or> b * x - a * y = d)"
  1197   using nat_bezout_add[of a b]
  1198   apply clarsimp
  1199   apply (rule_tac x="d" in exI, simp)
  1200   apply (rule_tac x="x" in exI)
  1201   apply (rule_tac x="y" in exI)
  1202   apply auto
  1203 done
  1204 
  1205 lemma nat_bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
  1206   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1207 proof-
  1208  from nz have ap: "a > 0" by simp
  1209  from nat_bezout_add[of a b]
  1210  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1211    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1212  moreover
  1213     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1214      from H have ?thesis by blast }
  1215  moreover
  1216  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1217    {assume b0: "b = 0" with H  have ?thesis by simp}
  1218    moreover
  1219    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1220      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1221        by auto
  1222      moreover
  1223      {assume db: "d=b"
  1224        from prems have ?thesis apply simp
  1225 	 apply (rule exI[where x = b], simp)
  1226 	 apply (rule exI[where x = b])
  1227 	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1228     moreover
  1229     {assume db: "d < b"
  1230 	{assume "x=0" hence ?thesis  using prems by simp }
  1231 	moreover
  1232 	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1233 	  from db have "d \<le> b - 1" by simp
  1234 	  hence "d*b \<le> b*(b - 1)" by simp
  1235 	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1236 	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1237 	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1238             by simp
  1239 	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1240 	    by (simp only: mult_assoc right_distrib)
  1241 	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1242             by algebra
  1243 	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1244 	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1245 	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1246 	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1247 	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
  1248 	  hence ?thesis using H(1,2)
  1249 	    apply -
  1250 	    apply (rule exI[where x=d], simp)
  1251 	    apply (rule exI[where x="(b - 1) * y"])
  1252 	    by (rule exI[where x="x*(b - 1) - d"], simp)}
  1253 	ultimately have ?thesis by blast}
  1254     ultimately have ?thesis by blast}
  1255   ultimately have ?thesis by blast}
  1256  ultimately show ?thesis by blast
  1257 qed
  1258 
  1259 lemma nat_bezout: assumes a: "(a::nat) \<noteq> 0"
  1260   shows "\<exists>x y. a * x = b * y + gcd a b"
  1261 proof-
  1262   let ?g = "gcd a b"
  1263   from nat_bezout_add_strong[OF a, of b]
  1264   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1265   from d(1,2) have "d dvd ?g" by simp
  1266   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1267   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1268   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1269   thus ?thesis by blast
  1270 qed
  1271 
  1272 
  1273 subsection {* LCM *}
  1274 
  1275 lemma int_lcm_altdef: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1276   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1277     zmult_int [symmetric] gcd_int_def)
  1278 
  1279 lemma nat_prod_gcd_lcm: "(m::nat) * n = gcd m n * lcm m n"
  1280   unfolding lcm_nat_def
  1281   by (simp add: dvd_mult_div_cancel [OF nat_gcd_dvd_prod])
  1282 
  1283 lemma int_prod_gcd_lcm: "abs(m::int) * abs n = gcd m n * lcm m n"
  1284   unfolding lcm_int_def gcd_int_def
  1285   apply (subst int_mult [symmetric])
  1286   apply (subst nat_prod_gcd_lcm [symmetric])
  1287   apply (subst nat_abs_mult_distrib [symmetric])
  1288   apply (simp, simp add: abs_mult)
  1289 done
  1290 
  1291 lemma nat_lcm_0 [simp]: "lcm (m::nat) 0 = 0"
  1292   unfolding lcm_nat_def by simp
  1293 
  1294 lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0"
  1295   unfolding lcm_int_def by simp
  1296 
  1297 lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0"
  1298   unfolding lcm_nat_def by simp
  1299 
  1300 lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0"
  1301   unfolding lcm_int_def by simp
  1302 
  1303 lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m"
  1304   unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps)
  1305 
  1306 lemma int_lcm_commute: "lcm (m::int) n = lcm n m"
  1307   unfolding lcm_int_def by (subst nat_lcm_commute, rule refl)
  1308 
  1309 
  1310 lemma nat_lcm_pos:
  1311   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1312 by (metis gr0I mult_is_0 nat_prod_gcd_lcm)
  1313 
  1314 lemma int_lcm_pos:
  1315   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1316   apply (subst int_lcm_abs)
  1317   apply (rule nat_lcm_pos [transferred])
  1318   apply auto
  1319 done
  1320 
  1321 lemma nat_dvd_pos:
  1322   fixes n m :: nat
  1323   assumes "n > 0" and "m dvd n"
  1324   shows "m > 0"
  1325 using assms by (cases m) auto
  1326 
  1327 lemma nat_lcm_least:
  1328   assumes "(m::nat) dvd k" and "n dvd k"
  1329   shows "lcm m n dvd k"
  1330 proof (cases k)
  1331   case 0 then show ?thesis by auto
  1332 next
  1333   case (Suc _) then have pos_k: "k > 0" by auto
  1334   from assms nat_dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1335   with nat_gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
  1336   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1337   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1338   from pos_k k_m have pos_p: "p > 0" by auto
  1339   from pos_k k_n have pos_q: "q > 0" by auto
  1340   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1341     by (simp add: mult_ac nat_gcd_mult_distrib)
  1342   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1343     by (simp add: k_m [symmetric] k_n [symmetric])
  1344   also have "\<dots> = k * p * q * gcd m n"
  1345     by (simp add: mult_ac nat_gcd_mult_distrib)
  1346   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1347     by (simp only: k_m [symmetric] k_n [symmetric])
  1348   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1349     by (simp add: mult_ac)
  1350   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1351     by simp
  1352   with nat_prod_gcd_lcm [of m n]
  1353   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1354     by (simp add: mult_ac)
  1355   with pos_gcd have "lcm m n * gcd q p = k" by auto
  1356   then show ?thesis using dvd_def by auto
  1357 qed
  1358 
  1359 lemma int_lcm_least:
  1360   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1361 apply (subst int_lcm_abs)
  1362 apply (rule dvd_trans)
  1363 apply (rule nat_lcm_least [transferred, of _ "abs k" _])
  1364 apply auto
  1365 done
  1366 
  1367 lemma nat_lcm_dvd1: "(m::nat) dvd lcm m n"
  1368 proof (cases m)
  1369   case 0 then show ?thesis by simp
  1370 next
  1371   case (Suc _)
  1372   then have mpos: "m > 0" by simp
  1373   show ?thesis
  1374   proof (cases n)
  1375     case 0 then show ?thesis by simp
  1376   next
  1377     case (Suc _)
  1378     then have npos: "n > 0" by simp
  1379     have "gcd m n dvd n" by simp
  1380     then obtain k where "n = gcd m n * k" using dvd_def by auto
  1381     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1382       by (simp add: mult_ac)
  1383     also have "\<dots> = m * k" using mpos npos nat_gcd_zero by simp
  1384     finally show ?thesis by (simp add: lcm_nat_def)
  1385   qed
  1386 qed
  1387 
  1388 lemma int_lcm_dvd1: "(m::int) dvd lcm m n"
  1389   apply (subst int_lcm_abs)
  1390   apply (rule dvd_trans)
  1391   prefer 2
  1392   apply (rule nat_lcm_dvd1 [transferred])
  1393   apply auto
  1394 done
  1395 
  1396 lemma nat_lcm_dvd2: "(n::nat) dvd lcm m n"
  1397   by (subst nat_lcm_commute, rule nat_lcm_dvd1)
  1398 
  1399 lemma int_lcm_dvd2: "(n::int) dvd lcm m n"
  1400   by (subst int_lcm_commute, rule int_lcm_dvd1)
  1401 
  1402 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1403 by(metis nat_lcm_dvd1 dvd_trans)
  1404 
  1405 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1406 by(metis nat_lcm_dvd2 dvd_trans)
  1407 
  1408 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1409 by(metis int_lcm_dvd1 dvd_trans)
  1410 
  1411 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1412 by(metis int_lcm_dvd2 dvd_trans)
  1413 
  1414 lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and>
  1415     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1416   by (auto intro: dvd_anti_sym nat_lcm_least nat_lcm_dvd1 nat_lcm_dvd2)
  1417 
  1418 lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1419     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1420   by (auto intro: dvd_anti_sym [transferred] int_lcm_least)
  1421 
  1422 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1423   apply (rule sym)
  1424   apply (subst nat_lcm_unique [symmetric])
  1425   apply auto
  1426 done
  1427 
  1428 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1429   apply (rule sym)
  1430   apply (subst int_lcm_unique [symmetric])
  1431   apply auto
  1432 done
  1433 
  1434 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1435 by (subst nat_lcm_commute, erule lcm_proj2_if_dvd_nat)
  1436 
  1437 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1438 by (subst int_lcm_commute, erule lcm_proj2_if_dvd_int)
  1439 
  1440 
  1441 lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
  1442 apply(rule nat_lcm_unique[THEN iffD1])
  1443 apply (metis dvd.order_trans nat_lcm_unique)
  1444 done
  1445 
  1446 lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
  1447 apply(rule int_lcm_unique[THEN iffD1])
  1448 apply (metis dvd_trans int_lcm_unique)
  1449 done
  1450 
  1451 lemmas lcm_left_commute_nat =
  1452   mk_left_commute[of lcm, OF lcm_assoc_nat nat_lcm_commute]
  1453 
  1454 lemmas lcm_left_commute_int =
  1455   mk_left_commute[of lcm, OF lcm_assoc_int int_lcm_commute]
  1456 
  1457 lemmas lcm_ac_nat = lcm_assoc_nat nat_lcm_commute lcm_left_commute_nat
  1458 lemmas lcm_ac_int = lcm_assoc_int int_lcm_commute lcm_left_commute_int
  1459 
  1460 
  1461 subsection {* Primes *}
  1462 
  1463 (* Is there a better way to handle these, rather than making them
  1464    elim rules? *)
  1465 
  1466 lemma nat_prime_ge_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
  1467   by (unfold prime_nat_def, auto)
  1468 
  1469 lemma nat_prime_gt_0 [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
  1470   by (unfold prime_nat_def, auto)
  1471 
  1472 lemma nat_prime_ge_1 [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
  1473   by (unfold prime_nat_def, auto)
  1474 
  1475 lemma nat_prime_gt_1 [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
  1476   by (unfold prime_nat_def, auto)
  1477 
  1478 lemma nat_prime_ge_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
  1479   by (unfold prime_nat_def, auto)
  1480 
  1481 lemma nat_prime_gt_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
  1482   by (unfold prime_nat_def, auto)
  1483 
  1484 lemma nat_prime_ge_2 [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
  1485   by (unfold prime_nat_def, auto)
  1486 
  1487 lemma int_prime_ge_0 [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
  1488   by (unfold prime_int_def prime_nat_def, auto)
  1489 
  1490 lemma int_prime_gt_0 [elim]: "prime (p::int) \<Longrightarrow> p > 0"
  1491   by (unfold prime_int_def prime_nat_def, auto)
  1492 
  1493 lemma int_prime_ge_1 [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
  1494   by (unfold prime_int_def prime_nat_def, auto)
  1495 
  1496 lemma int_prime_gt_1 [elim]: "prime (p::int) \<Longrightarrow> p > 1"
  1497   by (unfold prime_int_def prime_nat_def, auto)
  1498 
  1499 lemma int_prime_ge_2 [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
  1500   by (unfold prime_int_def prime_nat_def, auto)
  1501 
  1502 thm prime_nat_def;
  1503 thm prime_nat_def [transferred];
  1504 
  1505 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
  1506     m = 1 \<or> m = p))"
  1507   using prime_nat_def [transferred]
  1508     apply (case_tac "p >= 0")
  1509     by (blast, auto simp add: int_prime_ge_0)
  1510 
  1511 (* To do: determine primality of any numeral *)
  1512 
  1513 lemma nat_zero_not_prime [simp]: "~prime (0::nat)"
  1514   by (simp add: prime_nat_def)
  1515 
  1516 lemma int_zero_not_prime [simp]: "~prime (0::int)"
  1517   by (simp add: prime_int_def)
  1518 
  1519 lemma nat_one_not_prime [simp]: "~prime (1::nat)"
  1520   by (simp add: prime_nat_def)
  1521 
  1522 lemma nat_Suc_0_not_prime [simp]: "~prime (Suc 0)"
  1523   by (simp add: prime_nat_def One_nat_def)
  1524 
  1525 lemma int_one_not_prime [simp]: "~prime (1::int)"
  1526   by (simp add: prime_int_def)
  1527 
  1528 lemma nat_two_is_prime [simp]: "prime (2::nat)"
  1529   apply (auto simp add: prime_nat_def)
  1530   apply (case_tac m)
  1531   apply (auto dest!: dvd_imp_le)
  1532   done
  1533 
  1534 lemma int_two_is_prime [simp]: "prime (2::int)"
  1535   by (rule nat_two_is_prime [transferred direction: nat "op <= (0::int)"])
  1536 
  1537 lemma nat_prime_imp_coprime: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1538   apply (unfold prime_nat_def)
  1539   apply (metis nat_gcd_dvd1 nat_gcd_dvd2)
  1540   done
  1541 
  1542 lemma int_prime_imp_coprime: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1543   apply (unfold prime_int_altdef)
  1544   apply (metis int_gcd_dvd1 int_gcd_dvd2 int_gcd_ge_0)
  1545   done
  1546 
  1547 lemma nat_prime_dvd_mult: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1548   by (blast intro: nat_coprime_dvd_mult nat_prime_imp_coprime)
  1549 
  1550 lemma int_prime_dvd_mult: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1551   by (blast intro: int_coprime_dvd_mult int_prime_imp_coprime)
  1552 
  1553 lemma nat_prime_dvd_mult_eq [simp]: "prime (p::nat) \<Longrightarrow>
  1554     p dvd m * n = (p dvd m \<or> p dvd n)"
  1555   by (rule iffI, rule nat_prime_dvd_mult, auto)
  1556 
  1557 lemma int_prime_dvd_mult_eq [simp]: "prime (p::int) \<Longrightarrow>
  1558     p dvd m * n = (p dvd m \<or> p dvd n)"
  1559   by (rule iffI, rule int_prime_dvd_mult, auto)
  1560 
  1561 lemma nat_not_prime_eq_prod: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1562     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1563   unfolding prime_nat_def dvd_def apply auto
  1564   apply (subgoal_tac "k > 1")
  1565   apply force
  1566   apply (subgoal_tac "k ~= 0")
  1567   apply force
  1568   apply (rule notI)
  1569   apply force
  1570 done
  1571 
  1572 (* there's a lot of messing around with signs of products here --
  1573    could this be made more automatic? *)
  1574 lemma int_not_prime_eq_prod: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1575     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1576   unfolding prime_int_altdef dvd_def
  1577   apply auto
  1578   apply (rule_tac x = m in exI)
  1579   apply (rule_tac x = k in exI)
  1580   apply (auto simp add: mult_compare_simps)
  1581   apply (subgoal_tac "k > 0")
  1582   apply arith
  1583   apply (case_tac "k <= 0")
  1584   apply (subgoal_tac "m * k <= 0")
  1585   apply force
  1586   apply (subst zero_compare_simps(8))
  1587   apply auto
  1588   apply (subgoal_tac "m * k <= 0")
  1589   apply force
  1590   apply (subst zero_compare_simps(8))
  1591   apply auto
  1592 done
  1593 
  1594 lemma nat_prime_dvd_power [rule_format]: "prime (p::nat) -->
  1595     n > 0 --> (p dvd x^n --> p dvd x)"
  1596   by (induct n rule: nat_induct, auto)
  1597 
  1598 lemma int_prime_dvd_power [rule_format]: "prime (p::int) -->
  1599     n > 0 --> (p dvd x^n --> p dvd x)"
  1600   apply (induct n rule: nat_induct, auto)
  1601   apply (frule int_prime_ge_0)
  1602   apply auto
  1603 done
  1604 
  1605 lemma nat_prime_imp_power_coprime: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1606     coprime a (p^m)"
  1607   apply (rule nat_coprime_exp)
  1608   apply (subst nat_gcd_commute)
  1609   apply (erule (1) nat_prime_imp_coprime)
  1610 done
  1611 
  1612 lemma int_prime_imp_power_coprime: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1613     coprime a (p^m)"
  1614   apply (rule int_coprime_exp)
  1615   apply (subst int_gcd_commute)
  1616   apply (erule (1) int_prime_imp_coprime)
  1617 done
  1618 
  1619 lemma nat_primes_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1620   apply (rule nat_prime_imp_coprime, assumption)
  1621   apply (unfold prime_nat_def, auto)
  1622 done
  1623 
  1624 lemma int_primes_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1625   apply (rule int_prime_imp_coprime, assumption)
  1626   apply (unfold prime_int_altdef, clarify)
  1627   apply (drule_tac x = q in spec)
  1628   apply (drule_tac x = p in spec)
  1629   apply auto
  1630 done
  1631 
  1632 lemma nat_primes_imp_powers_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1633     coprime (p^m) (q^n)"
  1634   by (rule nat_coprime_exp2, rule nat_primes_coprime)
  1635 
  1636 lemma int_primes_imp_powers_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1637     coprime (p^m) (q^n)"
  1638   by (rule int_coprime_exp2, rule int_primes_coprime)
  1639 
  1640 lemma nat_prime_factor: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
  1641   apply (induct n rule: nat_less_induct)
  1642   apply (case_tac "n = 0")
  1643   using nat_two_is_prime apply blast
  1644   apply (case_tac "prime n")
  1645   apply blast
  1646   apply (subgoal_tac "n > 1")
  1647   apply (frule (1) nat_not_prime_eq_prod)
  1648   apply (auto intro: dvd_mult dvd_mult2)
  1649 done
  1650 
  1651 (* An Isar version:
  1652 
  1653 lemma nat_prime_factor_b:
  1654   fixes n :: nat
  1655   assumes "n \<noteq> 1"
  1656   shows "\<exists>p. prime p \<and> p dvd n"
  1657 
  1658 using `n ~= 1`
  1659 proof (induct n rule: nat_less_induct)
  1660   fix n :: nat
  1661   assume "n ~= 1" and
  1662     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
  1663   thus "\<exists>p. prime p \<and> p dvd n"
  1664   proof -
  1665   {
  1666     assume "n = 0"
  1667     moreover note nat_two_is_prime
  1668     ultimately have ?thesis
  1669       by (auto simp del: nat_two_is_prime)
  1670   }
  1671   moreover
  1672   {
  1673     assume "prime n"
  1674     hence ?thesis by auto
  1675   }
  1676   moreover
  1677   {
  1678     assume "n ~= 0" and "~ prime n"
  1679     with `n ~= 1` have "n > 1" by auto
  1680     with `~ prime n` and nat_not_prime_eq_prod obtain m k where
  1681       "n = m * k" and "1 < m" and "m < n" by blast
  1682     with ih obtain p where "prime p" and "p dvd m" by blast
  1683     with `n = m * k` have ?thesis by auto
  1684   }
  1685   ultimately show ?thesis by blast
  1686   qed
  1687 qed
  1688 
  1689 *)
  1690 
  1691 text {* One property of coprimality is easier to prove via prime factors. *}
  1692 
  1693 lemma nat_prime_divprod_pow:
  1694   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
  1695   shows "p^n dvd a \<or> p^n dvd b"
  1696 proof-
  1697   {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
  1698       apply (cases "n=0", simp_all)
  1699       apply (cases "a=1", simp_all) done}
  1700   moreover
  1701   {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
  1702     then obtain m where m: "n = Suc m" by (cases n, auto)
  1703     from n have "p dvd p^n" by (intro dvd_power, auto)
  1704     also note pab
  1705     finally have pab': "p dvd a * b".
  1706     from nat_prime_dvd_mult[OF p pab']
  1707     have "p dvd a \<or> p dvd b" .
  1708     moreover
  1709     {assume pa: "p dvd a"
  1710       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1711       from nat_coprime_common_divisor [OF ab, OF pa] p have "\<not> p dvd b" by auto
  1712       with p have "coprime b p"
  1713         by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
  1714       hence pnb: "coprime (p^n) b"
  1715         by (subst nat_gcd_commute, rule nat_coprime_exp)
  1716       from nat_coprime_divprod[OF pnba pnb] have ?thesis by blast }
  1717     moreover
  1718     {assume pb: "p dvd b"
  1719       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1720       from nat_coprime_common_divisor [OF ab, of p] pb p have "\<not> p dvd a"
  1721         by auto
  1722       with p have "coprime a p"
  1723         by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
  1724       hence pna: "coprime (p^n) a"
  1725         by (subst nat_gcd_commute, rule nat_coprime_exp)
  1726       from nat_coprime_divprod[OF pab pna] have ?thesis by blast }
  1727     ultimately have ?thesis by blast}
  1728   ultimately show ?thesis by blast
  1729 qed
  1730 
  1731 end