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