src/HOL/GCD.thy
author nipkow
Mon Oct 17 17:33:07 2016 +0200 (2016-10-17)
changeset 64272 f76b6dda2e56
parent 64242 93c6f0da5c70
child 64591 240a39af9ec4
permissions -rw-r--r--
setprod -> prod
     1 (*  Title:      HOL/GCD.thy
     2     Author:     Christophe Tabacznyj
     3     Author:     Lawrence C. Paulson
     4     Author:     Amine Chaieb
     5     Author:     Thomas M. Rasmussen
     6     Author:     Jeremy Avigad
     7     Author:     Tobias Nipkow
     8 
     9 This file deals with the functions gcd and lcm.  Definitions and
    10 lemmas are proved uniformly for the natural numbers and integers.
    11 
    12 This file combines and revises a number of prior developments.
    13 
    14 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    15 and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
    16 gcd, lcm, and prime for the natural numbers.
    17 
    18 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    19 extended gcd, lcm, primes to the integers. Amine Chaieb provided
    20 another extension of the notions to the integers, and added a number
    21 of results to "Primes" and "GCD". IntPrimes also defined and developed
    22 the congruence relations on the integers. The notion was extended to
    23 the natural numbers by Chaieb.
    24 
    25 Jeremy Avigad combined all of these, made everything uniform for the
    26 natural numbers and the integers, and added a number of new theorems.
    27 
    28 Tobias Nipkow cleaned up a lot.
    29 *)
    30 
    31 section \<open>Greatest common divisor and least common multiple\<close>
    32 
    33 theory GCD
    34   imports Main
    35 begin
    36 
    37 
    38 subsection \<open>Abstract GCD and LCM\<close>
    39 
    40 class gcd = zero + one + dvd +
    41   fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    42     and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    43 begin
    44 
    45 abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    46   where "coprime x y \<equiv> gcd x y = 1"
    47 
    48 end
    49 
    50 class Gcd = gcd +
    51   fixes Gcd :: "'a set \<Rightarrow> 'a"
    52     and Lcm :: "'a set \<Rightarrow> 'a"
    53 begin
    54 
    55 abbreviation GREATEST_COMMON_DIVISOR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    56   where "GREATEST_COMMON_DIVISOR A f \<equiv> Gcd (f ` A)"
    57 
    58 abbreviation LEAST_COMMON_MULTIPLE :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    59   where "LEAST_COMMON_MULTIPLE A f \<equiv> Lcm (f ` A)"
    60 
    61 end
    62 
    63 syntax
    64   "_GCD1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3GCD _./ _)" [0, 10] 10)
    65   "_GCD"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3GCD _\<in>_./ _)" [0, 0, 10] 10)
    66   "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3LCM _./ _)" [0, 10] 10)
    67   "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
    68 translations
    69   "GCD x y. B"   \<rightleftharpoons> "GCD x. GCD y. B"
    70   "GCD x. B"     \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR CONST UNIV (\<lambda>x. B)"
    71   "GCD x. B"     \<rightleftharpoons> "GCD x \<in> CONST UNIV. B"
    72   "GCD x\<in>A. B"   \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR A (\<lambda>x. B)"
    73   "LCM x y. B"   \<rightleftharpoons> "LCM x. LCM y. B"
    74   "LCM x. B"     \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE CONST UNIV (\<lambda>x. B)"
    75   "LCM x. B"     \<rightleftharpoons> "LCM x \<in> CONST UNIV. B"
    76   "LCM x\<in>A. B"   \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE A (\<lambda>x. B)"
    77 
    78 print_translation \<open>
    79   [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax GREATEST_COMMON_DIVISOR} @{syntax_const "_GCD"},
    80     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax LEAST_COMMON_MULTIPLE} @{syntax_const "_LCM"}]
    81 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    82 
    83 class semiring_gcd = normalization_semidom + gcd +
    84   assumes gcd_dvd1 [iff]: "gcd a b dvd a"
    85     and gcd_dvd2 [iff]: "gcd a b dvd b"
    86     and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
    87     and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
    88     and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
    89 begin
    90 
    91 lemma gcd_greatest_iff [simp]: "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
    92   by (blast intro!: gcd_greatest intro: dvd_trans)
    93 
    94 lemma gcd_dvdI1: "a dvd c \<Longrightarrow> gcd a b dvd c"
    95   by (rule dvd_trans) (rule gcd_dvd1)
    96 
    97 lemma gcd_dvdI2: "b dvd c \<Longrightarrow> gcd a b dvd c"
    98   by (rule dvd_trans) (rule gcd_dvd2)
    99 
   100 lemma dvd_gcdD1: "a dvd gcd b c \<Longrightarrow> a dvd b"
   101   using gcd_dvd1 [of b c] by (blast intro: dvd_trans)
   102 
   103 lemma dvd_gcdD2: "a dvd gcd b c \<Longrightarrow> a dvd c"
   104   using gcd_dvd2 [of b c] by (blast intro: dvd_trans)
   105 
   106 lemma gcd_0_left [simp]: "gcd 0 a = normalize a"
   107   by (rule associated_eqI) simp_all
   108 
   109 lemma gcd_0_right [simp]: "gcd a 0 = normalize a"
   110   by (rule associated_eqI) simp_all
   111 
   112 lemma gcd_eq_0_iff [simp]: "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
   113   (is "?P \<longleftrightarrow> ?Q")
   114 proof
   115   assume ?P
   116   then have "0 dvd gcd a b"
   117     by simp
   118   then have "0 dvd a" and "0 dvd b"
   119     by (blast intro: dvd_trans)+
   120   then show ?Q
   121     by simp
   122 next
   123   assume ?Q
   124   then show ?P
   125     by simp
   126 qed
   127 
   128 lemma unit_factor_gcd: "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)"
   129 proof (cases "gcd a b = 0")
   130   case True
   131   then show ?thesis by simp
   132 next
   133   case False
   134   have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b"
   135     by (rule unit_factor_mult_normalize)
   136   then have "unit_factor (gcd a b) * gcd a b = gcd a b"
   137     by simp
   138   then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b"
   139     by simp
   140   with False show ?thesis
   141     by simp
   142 qed
   143 
   144 lemma is_unit_gcd [simp]: "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
   145   by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
   146 
   147 sublocale gcd: abel_semigroup gcd
   148 proof
   149   fix a b c
   150   show "gcd a b = gcd b a"
   151     by (rule associated_eqI) simp_all
   152   from gcd_dvd1 have "gcd (gcd a b) c dvd a"
   153     by (rule dvd_trans) simp
   154   moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
   155     by (rule dvd_trans) simp
   156   ultimately have P1: "gcd (gcd a b) c dvd gcd a (gcd b c)"
   157     by (auto intro!: gcd_greatest)
   158   from gcd_dvd2 have "gcd a (gcd b c) dvd b"
   159     by (rule dvd_trans) simp
   160   moreover from gcd_dvd2 have "gcd a (gcd b c) dvd c"
   161     by (rule dvd_trans) simp
   162   ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
   163     by (auto intro!: gcd_greatest)
   164   from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)"
   165     by (rule associated_eqI) simp_all
   166 qed
   167 
   168 lemma gcd_self [simp]: "gcd a a = normalize a"
   169 proof -
   170   have "a dvd gcd a a"
   171     by (rule gcd_greatest) simp_all
   172   then show ?thesis
   173     by (auto intro: associated_eqI)
   174 qed
   175 
   176 lemma gcd_left_idem [simp]: "gcd a (gcd a b) = gcd a b"
   177   by (auto intro: associated_eqI)
   178 
   179 lemma gcd_right_idem [simp]: "gcd (gcd a b) b = gcd a b"
   180   unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
   181 
   182 lemma coprime_1_left [simp]: "coprime 1 a"
   183   by (rule associated_eqI) simp_all
   184 
   185 lemma coprime_1_right [simp]: "coprime a 1"
   186   using coprime_1_left [of a] by (simp add: ac_simps)
   187 
   188 lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
   189 proof (cases "c = 0")
   190   case True
   191   then show ?thesis by simp
   192 next
   193   case False
   194   then have *: "c * gcd a b dvd gcd (c * a) (c * b)"
   195     by (auto intro: gcd_greatest)
   196   moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b"
   197     by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
   198   ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
   199     by (auto intro: associated_eqI)
   200   then show ?thesis
   201     by (simp add: normalize_mult)
   202 qed
   203 
   204 lemma gcd_mult_right: "gcd (a * c) (b * c) = gcd b a * normalize c"
   205   using gcd_mult_left [of c a b] by (simp add: ac_simps)
   206 
   207 lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
   208   by (simp add: gcd_mult_left mult.assoc [symmetric])
   209 
   210 lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
   211   using mult_gcd_left [of c a b] by (simp add: ac_simps)
   212 
   213 lemma dvd_lcm1 [iff]: "a dvd lcm a b"
   214 proof -
   215   have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
   216     by (simp add: lcm_gcd normalize_mult div_mult_swap)
   217   then show ?thesis
   218     by (simp add: lcm_gcd)
   219 qed
   220 
   221 lemma dvd_lcm2 [iff]: "b dvd lcm a b"
   222 proof -
   223   have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
   224     by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
   225   then show ?thesis
   226     by (simp add: lcm_gcd)
   227 qed
   228 
   229 lemma dvd_lcmI1: "a dvd b \<Longrightarrow> a dvd lcm b c"
   230   by (rule dvd_trans) (assumption, blast)
   231 
   232 lemma dvd_lcmI2: "a dvd c \<Longrightarrow> a dvd lcm b c"
   233   by (rule dvd_trans) (assumption, blast)
   234 
   235 lemma lcm_dvdD1: "lcm a b dvd c \<Longrightarrow> a dvd c"
   236   using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
   237 
   238 lemma lcm_dvdD2: "lcm a b dvd c \<Longrightarrow> b dvd c"
   239   using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
   240 
   241 lemma lcm_least:
   242   assumes "a dvd c" and "b dvd c"
   243   shows "lcm a b dvd c"
   244 proof (cases "c = 0")
   245   case True
   246   then show ?thesis by simp
   247 next
   248   case False
   249   then have *: "is_unit (unit_factor c)"
   250     by simp
   251   show ?thesis
   252   proof (cases "gcd a b = 0")
   253     case True
   254     with assms show ?thesis by simp
   255   next
   256     case False
   257     then have "a \<noteq> 0 \<or> b \<noteq> 0"
   258       by simp
   259     with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b"
   260       by (simp_all add: mult_dvd_mono)
   261     then have "normalize (a * b) dvd gcd (a * c) (b * c)"
   262       by (auto intro: gcd_greatest simp add: ac_simps)
   263     then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
   264       using * by (simp add: dvd_mult_unit_iff)
   265     then have "normalize (a * b) dvd gcd a b * c"
   266       by (simp add: mult_gcd_right [of a b c])
   267     then have "normalize (a * b) div gcd a b dvd c"
   268       using False by (simp add: div_dvd_iff_mult ac_simps)
   269     then show ?thesis
   270       by (simp add: lcm_gcd)
   271   qed
   272 qed
   273 
   274 lemma lcm_least_iff [simp]: "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
   275   by (blast intro!: lcm_least intro: dvd_trans)
   276 
   277 lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b"
   278   by (simp add: lcm_gcd dvd_normalize_div)
   279 
   280 lemma lcm_0_left [simp]: "lcm 0 a = 0"
   281   by (simp add: lcm_gcd)
   282 
   283 lemma lcm_0_right [simp]: "lcm a 0 = 0"
   284   by (simp add: lcm_gcd)
   285 
   286 lemma lcm_eq_0_iff: "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   287   (is "?P \<longleftrightarrow> ?Q")
   288 proof
   289   assume ?P
   290   then have "0 dvd lcm a b"
   291     by simp
   292   then have "0 dvd normalize (a * b) div gcd a b"
   293     by (simp add: lcm_gcd)
   294   then have "0 * gcd a b dvd normalize (a * b)"
   295     using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
   296   then have "normalize (a * b) = 0"
   297     by simp
   298   then show ?Q
   299     by simp
   300 next
   301   assume ?Q
   302   then show ?P
   303     by auto
   304 qed
   305 
   306 lemma lcm_eq_1_iff [simp]: "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
   307   by (auto intro: associated_eqI)
   308 
   309 lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
   310   by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
   311 
   312 sublocale lcm: abel_semigroup lcm
   313 proof
   314   fix a b c
   315   show "lcm a b = lcm b a"
   316     by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
   317   have "lcm (lcm a b) c dvd lcm a (lcm b c)"
   318     and "lcm a (lcm b c) dvd lcm (lcm a b) c"
   319     by (auto intro: lcm_least
   320       dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
   321       dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
   322       dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
   323       dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
   324   then show "lcm (lcm a b) c = lcm a (lcm b c)"
   325     by (rule associated_eqI) simp_all
   326 qed
   327 
   328 lemma lcm_self [simp]: "lcm a a = normalize a"
   329 proof -
   330   have "lcm a a dvd a"
   331     by (rule lcm_least) simp_all
   332   then show ?thesis
   333     by (auto intro: associated_eqI)
   334 qed
   335 
   336 lemma lcm_left_idem [simp]: "lcm a (lcm a b) = lcm a b"
   337   by (auto intro: associated_eqI)
   338 
   339 lemma lcm_right_idem [simp]: "lcm (lcm a b) b = lcm a b"
   340   unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
   341 
   342 lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
   343   by (simp add: lcm_gcd normalize_mult)
   344 
   345 lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b"
   346   using gcd_mult_lcm [of a b] by (simp add: ac_simps)
   347 
   348 lemma gcd_lcm:
   349   assumes "a \<noteq> 0" and "b \<noteq> 0"
   350   shows "gcd a b = normalize (a * b) div lcm a b"
   351 proof -
   352   from assms have "lcm a b \<noteq> 0"
   353     by (simp add: lcm_eq_0_iff)
   354   have "gcd a b * lcm a b = normalize a * normalize b"
   355     by simp
   356   then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
   357     by (simp_all add: normalize_mult)
   358   with \<open>lcm a b \<noteq> 0\<close> show ?thesis
   359     using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
   360 qed
   361 
   362 lemma lcm_1_left [simp]: "lcm 1 a = normalize a"
   363   by (simp add: lcm_gcd)
   364 
   365 lemma lcm_1_right [simp]: "lcm a 1 = normalize a"
   366   by (simp add: lcm_gcd)
   367 
   368 lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b"
   369   by (cases "c = 0")
   370     (simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
   371       simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
   372 
   373 lemma lcm_mult_right: "lcm (a * c) (b * c) = lcm b a * normalize c"
   374   using lcm_mult_left [of c a b] by (simp add: ac_simps)
   375 
   376 lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
   377   by (simp add: lcm_mult_left mult.assoc [symmetric])
   378 
   379 lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
   380   using mult_lcm_left [of c a b] by (simp add: ac_simps)
   381 
   382 lemma gcdI:
   383   assumes "c dvd a" and "c dvd b"
   384     and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
   385     and "normalize c = c"
   386   shows "c = gcd a b"
   387   by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
   388 
   389 lemma gcd_unique:
   390   "d dvd a \<and> d dvd b \<and> normalize d = d \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   391   by rule (auto intro: gcdI simp: gcd_greatest)
   392 
   393 lemma gcd_dvd_prod: "gcd a b dvd k * b"
   394   using mult_dvd_mono [of 1] by auto
   395 
   396 lemma gcd_proj2_if_dvd: "b dvd a \<Longrightarrow> gcd a b = normalize b"
   397   by (rule gcdI [symmetric]) simp_all
   398 
   399 lemma gcd_proj1_if_dvd: "a dvd b \<Longrightarrow> gcd a b = normalize a"
   400   by (rule gcdI [symmetric]) simp_all
   401 
   402 lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n"
   403 proof
   404   assume *: "gcd m n = normalize m"
   405   show "m dvd n"
   406   proof (cases "m = 0")
   407     case True
   408     with * show ?thesis by simp
   409   next
   410     case [simp]: False
   411     from * have **: "m = gcd m n * unit_factor m"
   412       by (simp add: unit_eq_div2)
   413     show ?thesis
   414       by (subst **) (simp add: mult_unit_dvd_iff)
   415   qed
   416 next
   417   assume "m dvd n"
   418   then show "gcd m n = normalize m"
   419     by (rule gcd_proj1_if_dvd)
   420 qed
   421 
   422 lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m"
   423   using gcd_proj1_iff [of n m] by (simp add: ac_simps)
   424 
   425 lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)"
   426   by (rule gcdI) (auto simp: normalize_mult gcd_greatest mult_dvd_mono gcd_mult_left[symmetric])
   427 
   428 lemma gcd_mult_distrib: "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
   429 proof-
   430   have "normalize k * gcd a b = gcd (k * a) (k * b)"
   431     by (simp add: gcd_mult_distrib')
   432   then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
   433     by simp
   434   then have "normalize k * unit_factor k * gcd a b  = gcd (k * a) (k * b) * unit_factor k"
   435     by (simp only: ac_simps)
   436   then show ?thesis
   437     by simp
   438 qed
   439 
   440 lemma lcm_mult_unit1: "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
   441   by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
   442 
   443 lemma lcm_mult_unit2: "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
   444   using lcm_mult_unit1 [of a c b] by (simp add: ac_simps)
   445 
   446 lemma lcm_div_unit1:
   447   "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c"
   448   by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1)
   449 
   450 lemma lcm_div_unit2: "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
   451   by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
   452 
   453 lemma normalize_lcm_left [simp]: "lcm (normalize a) b = lcm a b"
   454 proof (cases "a = 0")
   455   case True
   456   then show ?thesis
   457     by simp
   458 next
   459   case False
   460   then have "is_unit (unit_factor a)"
   461     by simp
   462   moreover have "normalize a = a div unit_factor a"
   463     by simp
   464   ultimately show ?thesis
   465     by (simp only: lcm_div_unit1)
   466 qed
   467 
   468 lemma normalize_lcm_right [simp]: "lcm a (normalize b) = lcm a b"
   469   using normalize_lcm_left [of b a] by (simp add: ac_simps)
   470 
   471 lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
   472   apply (rule gcdI)
   473      apply simp_all
   474   apply (rule dvd_trans)
   475    apply (rule gcd_dvd1)
   476   apply (simp add: unit_simps)
   477   done
   478 
   479 lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
   480   apply (subst gcd.commute)
   481   apply (subst gcd_mult_unit1)
   482    apply assumption
   483   apply (rule gcd.commute)
   484   done
   485 
   486 lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
   487   by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
   488 
   489 lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
   490   by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
   491 
   492 lemma normalize_gcd_left [simp]: "gcd (normalize a) b = gcd a b"
   493 proof (cases "a = 0")
   494   case True
   495   then show ?thesis
   496     by simp
   497 next
   498   case False
   499   then have "is_unit (unit_factor a)"
   500     by simp
   501   moreover have "normalize a = a div unit_factor a"
   502     by simp
   503   ultimately show ?thesis
   504     by (simp only: gcd_div_unit1)
   505 qed
   506 
   507 lemma normalize_gcd_right [simp]: "gcd a (normalize b) = gcd a b"
   508   using normalize_gcd_left [of b a] by (simp add: ac_simps)
   509 
   510 lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
   511   by standard (simp_all add: fun_eq_iff ac_simps)
   512 
   513 lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
   514   by standard (simp_all add: fun_eq_iff ac_simps)
   515 
   516 lemma gcd_dvd_antisym: "gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d"
   517 proof (rule gcdI)
   518   assume *: "gcd a b dvd gcd c d"
   519     and **: "gcd c d dvd gcd a b"
   520   have "gcd c d dvd c"
   521     by simp
   522   with * show "gcd a b dvd c"
   523     by (rule dvd_trans)
   524   have "gcd c d dvd d"
   525     by simp
   526   with * show "gcd a b dvd d"
   527     by (rule dvd_trans)
   528   show "normalize (gcd a b) = gcd a b"
   529     by simp
   530   fix l assume "l dvd c" and "l dvd d"
   531   then have "l dvd gcd c d"
   532     by (rule gcd_greatest)
   533   from this and ** show "l dvd gcd a b"
   534     by (rule dvd_trans)
   535 qed
   536 
   537 lemma coprime_dvd_mult:
   538   assumes "coprime a b" and "a dvd c * b"
   539   shows "a dvd c"
   540 proof (cases "c = 0")
   541   case True
   542   then show ?thesis by simp
   543 next
   544   case False
   545   then have unit: "is_unit (unit_factor c)"
   546     by simp
   547   from \<open>coprime a b\<close> mult_gcd_left [of c a b]
   548   have "gcd (c * a) (c * b) * unit_factor c = c"
   549     by (simp add: ac_simps)
   550   moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
   551     by (simp add: dvd_mult_unit_iff unit)
   552   ultimately show ?thesis
   553     by simp
   554 qed
   555 
   556 lemma coprime_dvd_mult_iff: "coprime a c \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd b"
   557   by (auto intro: coprime_dvd_mult)
   558 
   559 lemma gcd_mult_cancel: "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   560   apply (rule associated_eqI)
   561      apply (rule gcd_greatest)
   562       apply (rule_tac b = c in coprime_dvd_mult)
   563        apply (simp add: gcd.assoc)
   564        apply (simp_all add: ac_simps)
   565   done
   566 
   567 lemma coprime_crossproduct:
   568   fixes a b c d :: 'a
   569   assumes "coprime a d" and "coprime b c"
   570   shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
   571     normalize a = normalize b \<and> normalize c = normalize d"
   572     (is "?lhs \<longleftrightarrow> ?rhs")
   573 proof
   574   assume ?rhs
   575   then show ?lhs by simp
   576 next
   577   assume ?lhs
   578   from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
   579     by (auto intro: dvdI dest: sym)
   580   with \<open>coprime a d\<close> have "a dvd b"
   581     by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   582   from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
   583     by (auto intro: dvdI dest: sym)
   584   with \<open>coprime b c\<close> have "b dvd a"
   585     by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   586   from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
   587     by (auto intro: dvdI dest: sym simp add: mult.commute)
   588   with \<open>coprime b c\<close> have "c dvd d"
   589     by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   590   from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
   591     by (auto intro: dvdI dest: sym simp add: mult.commute)
   592   with \<open>coprime a d\<close> have "d dvd c"
   593     by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   594   from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
   595     by (rule associatedI)
   596   moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
   597     by (rule associatedI)
   598   ultimately show ?rhs ..
   599 qed
   600 
   601 lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
   602   by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
   603 
   604 lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
   605   using gcd_add1 [of n m] by (simp add: ac_simps)
   606 
   607 lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
   608   by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
   609 
   610 lemma coprimeI: "(\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
   611   by (rule sym, rule gcdI) simp_all
   612 
   613 lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
   614   by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
   615 
   616 lemma div_gcd_coprime:
   617   assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   618   shows "coprime (a div gcd a b) (b div gcd a b)"
   619 proof -
   620   let ?g = "gcd a b"
   621   let ?a' = "a div ?g"
   622   let ?b' = "b div ?g"
   623   let ?g' = "gcd ?a' ?b'"
   624   have dvdg: "?g dvd a" "?g dvd b"
   625     by simp_all
   626   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
   627     by simp_all
   628   from dvdg dvdg' obtain ka kb ka' kb' where
   629     kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   630     unfolding dvd_def by blast
   631   from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   632     by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
   633   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   634     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   635   have "?g \<noteq> 0"
   636     using nz by simp
   637   moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   638   ultimately show ?thesis
   639     using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
   640 qed
   641 
   642 
   643 lemma divides_mult:
   644   assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
   645   shows "a * b dvd c"
   646 proof -
   647   from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
   648   with \<open>a dvd c\<close> have "a dvd b' * b"
   649     by (simp add: ac_simps)
   650   with \<open>coprime a b\<close> have "a dvd b'"
   651     by (simp add: coprime_dvd_mult_iff)
   652   then obtain a' where "b' = a * a'" ..
   653   with \<open>c = b * b'\<close> have "c = (a * b) * a'"
   654     by (simp add: ac_simps)
   655   then show ?thesis ..
   656 qed
   657 
   658 lemma coprime_lmult:
   659   assumes dab: "gcd d (a * b) = 1"
   660   shows "gcd d a = 1"
   661 proof (rule coprimeI)
   662   fix l
   663   assume "l dvd d" and "l dvd a"
   664   then have "l dvd a * b"
   665     by simp
   666   with \<open>l dvd d\<close> and dab show "l dvd 1"
   667     by (auto intro: gcd_greatest)
   668 qed
   669 
   670 lemma coprime_rmult:
   671   assumes dab: "gcd d (a * b) = 1"
   672   shows "gcd d b = 1"
   673 proof (rule coprimeI)
   674   fix l
   675   assume "l dvd d" and "l dvd b"
   676   then have "l dvd a * b"
   677     by simp
   678   with \<open>l dvd d\<close> and dab show "l dvd 1"
   679     by (auto intro: gcd_greatest)
   680 qed
   681 
   682 lemma coprime_mult:
   683   assumes "coprime d a"
   684     and "coprime d b"
   685   shows "coprime d (a * b)"
   686   apply (subst gcd.commute)
   687   using assms(1) apply (subst gcd_mult_cancel)
   688    apply (subst gcd.commute)
   689    apply assumption
   690   apply (subst gcd.commute)
   691   apply (rule assms(2))
   692   done
   693 
   694 lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
   695   using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
   696   by blast
   697 
   698 lemma gcd_coprime:
   699   assumes c: "gcd a b \<noteq> 0"
   700     and a: "a = a' * gcd a b"
   701     and b: "b = b' * gcd a b"
   702   shows "gcd a' b' = 1"
   703 proof -
   704   from c have "a \<noteq> 0 \<or> b \<noteq> 0"
   705     by simp
   706   with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
   707   also from assms have "a div gcd a b = a'"
   708     using dvd_div_eq_mult local.gcd_dvd1 by blast
   709   also from assms have "b div gcd a b = b'"
   710     using dvd_div_eq_mult local.gcd_dvd1 by blast
   711   finally show ?thesis .
   712 qed
   713 
   714 lemma coprime_power:
   715   assumes "0 < n"
   716   shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1"
   717   using assms
   718 proof (induct n)
   719   case 0
   720   then show ?case by simp
   721 next
   722   case (Suc n)
   723   then show ?case
   724     by (cases n) (simp_all add: coprime_mul_eq)
   725 qed
   726 
   727 lemma gcd_coprime_exists:
   728   assumes "gcd a b \<noteq> 0"
   729   shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
   730   apply (rule_tac x = "a div gcd a b" in exI)
   731   apply (rule_tac x = "b div gcd a b" in exI)
   732   using assms
   733   apply (auto intro: div_gcd_coprime)
   734   done
   735 
   736 lemma coprime_exp: "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
   737   by (induct n) (simp_all add: coprime_mult)
   738 
   739 lemma coprime_exp_left: "coprime a b \<Longrightarrow> coprime (a ^ n) b"
   740   by (induct n) (simp_all add: gcd_mult_cancel)
   741 
   742 lemma coprime_exp2:
   743   assumes "coprime a b"
   744   shows "coprime (a ^ n) (b ^ m)"
   745 proof (rule coprime_exp_left)
   746   from assms show "coprime a (b ^ m)"
   747     by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
   748 qed
   749 
   750 lemma gcd_exp: "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
   751 proof (cases "a = 0 \<and> b = 0")
   752   case True
   753   then show ?thesis
   754     by (cases n) simp_all
   755 next
   756   case False
   757   then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
   758     using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
   759   then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
   760     by simp
   761   also note gcd_mult_distrib
   762   also have "unit_factor (gcd a b ^ n) = 1"
   763     using False by (auto simp add: unit_factor_power unit_factor_gcd)
   764   also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
   765     apply (subst ac_simps)
   766     apply (subst div_power)
   767      apply simp
   768     apply (rule dvd_div_mult_self)
   769     apply (rule dvd_power_same)
   770     apply simp
   771     done
   772   also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
   773     apply (subst ac_simps)
   774     apply (subst div_power)
   775      apply simp
   776     apply (rule dvd_div_mult_self)
   777     apply (rule dvd_power_same)
   778     apply simp
   779     done
   780   finally show ?thesis by simp
   781 qed
   782 
   783 lemma coprime_common_divisor: "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
   784   apply (subgoal_tac "a dvd gcd a b")
   785    apply simp
   786   apply (erule (1) gcd_greatest)
   787   done
   788 
   789 lemma division_decomp:
   790   assumes "a dvd b * c"
   791   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   792 proof (cases "gcd a b = 0")
   793   case True
   794   then have "a = 0 \<and> b = 0"
   795     by simp
   796   then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
   797     by simp
   798   then show ?thesis by blast
   799 next
   800   case False
   801   let ?d = "gcd a b"
   802   from gcd_coprime_exists [OF False]
   803     obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
   804     by blast
   805   from ab'(1) have "a' dvd a"
   806     unfolding dvd_def by blast
   807   with assms have "a' dvd b * c"
   808     using dvd_trans[of a' a "b*c"] by simp
   809   from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
   810     by simp
   811   then have "?d * a' dvd ?d * (b' * c)"
   812     by (simp add: mult_ac)
   813   with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
   814     by simp
   815   with coprime_dvd_mult[OF ab'(3)] have "a' dvd c"
   816     by (subst (asm) ac_simps) blast
   817   with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
   818     by (simp add: mult_ac)
   819   then show ?thesis by blast
   820 qed
   821 
   822 lemma pow_divs_pow:
   823   assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
   824   shows "a dvd b"
   825 proof (cases "gcd a b = 0")
   826   case True
   827   then show ?thesis by simp
   828 next
   829   case False
   830   let ?d = "gcd a b"
   831   from n obtain m where m: "n = Suc m"
   832     by (cases n) simp_all
   833   from False have zn: "?d ^ n \<noteq> 0"
   834     by (rule power_not_zero)
   835   from gcd_coprime_exists [OF False]
   836   obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
   837     by blast
   838   from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
   839     by (simp add: ab'(1,2)[symmetric])
   840   then have "?d^n * a'^n dvd ?d^n * b'^n"
   841     by (simp only: power_mult_distrib ac_simps)
   842   with zn have "a'^n dvd b'^n"
   843     by simp
   844   then have "a' dvd b'^n"
   845     using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
   846   then have "a' dvd b'^m * b'"
   847     by (simp add: m ac_simps)
   848   with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
   849   have "a' dvd b'" by (subst (asm) ac_simps) blast
   850   then have "a' * ?d dvd b' * ?d"
   851     by (rule mult_dvd_mono) simp
   852   with ab'(1,2) show ?thesis
   853     by simp
   854 qed
   855 
   856 lemma pow_divs_eq [simp]: "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   857   by (auto intro: pow_divs_pow dvd_power_same)
   858 
   859 lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
   860   by (subst add_commute) simp
   861 
   862 lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
   863   by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
   864 
   865 lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
   866   by (induct xs) (simp_all add: gcd_mult_cancel)
   867 
   868 lemma coprime_divisors:
   869   assumes "d dvd a" "e dvd b" "gcd a b = 1"
   870   shows "gcd d e = 1"
   871 proof -
   872   from assms obtain k l where "a = d * k" "b = e * l"
   873     unfolding dvd_def by blast
   874   with assms have "gcd (d * k) (e * l) = 1"
   875     by simp
   876   then have "gcd (d * k) e = 1"
   877     by (rule coprime_lmult)
   878   also have "gcd (d * k) e = gcd e (d * k)"
   879     by (simp add: ac_simps)
   880   finally have "gcd e d = 1"
   881     by (rule coprime_lmult)
   882   then show ?thesis
   883     by (simp add: ac_simps)
   884 qed
   885 
   886 lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
   887   by (simp add: lcm_gcd)
   888 
   889 declare unit_factor_lcm [simp]
   890 
   891 lemma lcmI:
   892   assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
   893     and "normalize c = c"
   894   shows "c = lcm a b"
   895   by (rule associated_eqI) (auto simp: assms intro: lcm_least)
   896 
   897 lemma gcd_dvd_lcm [simp]: "gcd a b dvd lcm a b"
   898   using gcd_dvd2 by (rule dvd_lcmI2)
   899 
   900 lemmas lcm_0 = lcm_0_right
   901 
   902 lemma lcm_unique:
   903   "a dvd d \<and> b dvd d \<and> normalize d = d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   904   by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
   905 
   906 lemma lcm_coprime: "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
   907   by (subst lcm_gcd) simp
   908 
   909 lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a"
   910   apply (cases "a = 0")
   911    apply simp
   912   apply (rule sym)
   913   apply (rule lcmI)
   914      apply simp_all
   915   done
   916 
   917 lemma lcm_proj2_if_dvd: "a dvd b \<Longrightarrow> lcm a b = normalize b"
   918   using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
   919 
   920 lemma lcm_proj1_iff: "lcm m n = normalize m \<longleftrightarrow> n dvd m"
   921 proof
   922   assume *: "lcm m n = normalize m"
   923   show "n dvd m"
   924   proof (cases "m = 0")
   925     case True
   926     then show ?thesis by simp
   927   next
   928     case [simp]: False
   929     from * have **: "m = lcm m n * unit_factor m"
   930       by (simp add: unit_eq_div2)
   931     show ?thesis by (subst **) simp
   932   qed
   933 next
   934   assume "n dvd m"
   935   then show "lcm m n = normalize m"
   936     by (rule lcm_proj1_if_dvd)
   937 qed
   938 
   939 lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
   940   using lcm_proj1_iff [of n m] by (simp add: ac_simps)
   941 
   942 lemma dvd_productE:
   943   assumes "p dvd (a * b)"
   944   obtains x y where "p = x * y" "x dvd a" "y dvd b"
   945 proof (cases "a = 0")
   946   case True
   947   thus ?thesis by (intro that[of p 1]) simp_all
   948 next
   949   case False
   950   define x y where "x = gcd a p" and "y = p div x"
   951   have "p = x * y" by (simp add: x_def y_def)
   952   moreover have "x dvd a" by (simp add: x_def)
   953   moreover from assms have "p dvd gcd (b * a) (b * p)"
   954     by (intro gcd_greatest) (simp_all add: mult.commute)
   955   hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
   956   with False have "y dvd b" 
   957     by (simp add: x_def y_def div_dvd_iff_mult assms)
   958   ultimately show ?thesis by (rule that)
   959 qed
   960 
   961 end
   962 
   963 class ring_gcd = comm_ring_1 + semiring_gcd
   964 begin
   965 
   966 lemma coprime_minus_one: "coprime (n - 1) n"
   967   using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute)
   968 
   969 lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
   970   by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
   971 
   972 lemma gcd_neg2 [simp]: "gcd a (-b) = gcd a b"
   973   by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
   974 
   975 lemma gcd_neg_numeral_1 [simp]: "gcd (- numeral n) a = gcd (numeral n) a"
   976   by (fact gcd_neg1)
   977 
   978 lemma gcd_neg_numeral_2 [simp]: "gcd a (- numeral n) = gcd a (numeral n)"
   979   by (fact gcd_neg2)
   980 
   981 lemma gcd_diff1: "gcd (m - n) n = gcd m n"
   982   by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp)
   983 
   984 lemma gcd_diff2: "gcd (n - m) n = gcd m n"
   985   by (subst gcd_neg1[symmetric]) (simp only: minus_diff_eq gcd_diff1)
   986 
   987 lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b"
   988   by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)
   989 
   990 lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b"
   991   by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)
   992 
   993 lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a"
   994   by (fact lcm_neg1)
   995 
   996 lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)"
   997   by (fact lcm_neg2)
   998 
   999 end
  1000 
  1001 class semiring_Gcd = semiring_gcd + Gcd +
  1002   assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
  1003     and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A"
  1004     and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
  1005   assumes dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
  1006     and Lcm_least: "(\<And>b. b \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> Lcm A dvd a"
  1007     and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A"
  1008 begin
  1009 
  1010 lemma Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
  1011   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
  1012 
  1013 lemma Gcd_Lcm: "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
  1014   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
  1015 
  1016 lemma Gcd_empty [simp]: "Gcd {} = 0"
  1017   by (rule dvd_0_left, rule Gcd_greatest) simp
  1018 
  1019 lemma Lcm_empty [simp]: "Lcm {} = 1"
  1020   by (auto intro: associated_eqI Lcm_least)
  1021 
  1022 lemma Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)"
  1023 proof -
  1024   have "Gcd (insert a A) dvd gcd a (Gcd A)"
  1025     by (auto intro: Gcd_dvd Gcd_greatest)
  1026   moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
  1027   proof (rule Gcd_greatest)
  1028     fix b
  1029     assume "b \<in> insert a A"
  1030     then show "gcd a (Gcd A) dvd b"
  1031     proof
  1032       assume "b = a"
  1033       then show ?thesis
  1034         by simp
  1035     next
  1036       assume "b \<in> A"
  1037       then have "Gcd A dvd b"
  1038         by (rule Gcd_dvd)
  1039       moreover have "gcd a (Gcd A) dvd Gcd A"
  1040         by simp
  1041       ultimately show ?thesis
  1042         by (blast intro: dvd_trans)
  1043     qed
  1044   qed
  1045   ultimately show ?thesis
  1046     by (auto intro: associated_eqI)
  1047 qed
  1048 
  1049 lemma Lcm_insert [simp]: "Lcm (insert a A) = lcm a (Lcm A)"
  1050 proof (rule sym)
  1051   have "lcm a (Lcm A) dvd Lcm (insert a A)"
  1052     by (auto intro: dvd_Lcm Lcm_least)
  1053   moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
  1054   proof (rule Lcm_least)
  1055     fix b
  1056     assume "b \<in> insert a A"
  1057     then show "b dvd lcm a (Lcm A)"
  1058     proof
  1059       assume "b = a"
  1060       then show ?thesis by simp
  1061     next
  1062       assume "b \<in> A"
  1063       then have "b dvd Lcm A"
  1064         by (rule dvd_Lcm)
  1065       moreover have "Lcm A dvd lcm a (Lcm A)"
  1066         by simp
  1067       ultimately show ?thesis
  1068         by (blast intro: dvd_trans)
  1069     qed
  1070   qed
  1071   ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
  1072     by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
  1073 qed
  1074 
  1075 lemma LcmI:
  1076   assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b"
  1077     and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
  1078     and "normalize b = b"
  1079   shows "b = Lcm A"
  1080   by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least)
  1081 
  1082 lemma Lcm_subset: "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
  1083   by (blast intro: Lcm_least dvd_Lcm)
  1084 
  1085 lemma Lcm_Un: "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
  1086   apply (rule lcmI)
  1087      apply (blast intro: Lcm_subset)
  1088     apply (blast intro: Lcm_subset)
  1089    apply (intro Lcm_least ballI, elim UnE)
  1090     apply (rule dvd_trans, erule dvd_Lcm, assumption)
  1091    apply (rule dvd_trans, erule dvd_Lcm, assumption)
  1092   apply simp
  1093   done
  1094 
  1095 lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
  1096   (is "?P \<longleftrightarrow> ?Q")
  1097 proof
  1098   assume ?P
  1099   show ?Q
  1100   proof
  1101     fix a
  1102     assume "a \<in> A"
  1103     then have "Gcd A dvd a"
  1104       by (rule Gcd_dvd)
  1105     with \<open>?P\<close> have "a = 0"
  1106       by simp
  1107     then show "a \<in> {0}"
  1108       by simp
  1109   qed
  1110 next
  1111   assume ?Q
  1112   have "0 dvd Gcd A"
  1113   proof (rule Gcd_greatest)
  1114     fix a
  1115     assume "a \<in> A"
  1116     with \<open>?Q\<close> have "a = 0"
  1117       by auto
  1118     then show "0 dvd a"
  1119       by simp
  1120   qed
  1121   then show ?P
  1122     by simp
  1123 qed
  1124 
  1125 lemma Lcm_1_iff [simp]: "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)"
  1126   (is "?P \<longleftrightarrow> ?Q")
  1127 proof
  1128   assume ?P
  1129   show ?Q
  1130   proof
  1131     fix a
  1132     assume "a \<in> A"
  1133     then have "a dvd Lcm A"
  1134       by (rule dvd_Lcm)
  1135     with \<open>?P\<close> show "is_unit a"
  1136       by simp
  1137   qed
  1138 next
  1139   assume ?Q
  1140   then have "is_unit (Lcm A)"
  1141     by (blast intro: Lcm_least)
  1142   then have "normalize (Lcm A) = 1"
  1143     by (rule is_unit_normalize)
  1144   then show ?P
  1145     by simp
  1146 qed
  1147 
  1148 lemma unit_factor_Lcm: "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
  1149 proof (cases "Lcm A = 0")
  1150   case True
  1151   then show ?thesis
  1152     by simp
  1153 next
  1154   case False
  1155   with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
  1156     by blast
  1157   with False show ?thesis
  1158     by simp
  1159 qed
  1160 
  1161 lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
  1162   by (simp add: Gcd_Lcm unit_factor_Lcm)
  1163 
  1164 lemma GcdI:
  1165   assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a"
  1166     and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
  1167     and "normalize b = b"
  1168   shows "b = Gcd A"
  1169   by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest)
  1170 
  1171 lemma Gcd_eq_1_I:
  1172   assumes "is_unit a" and "a \<in> A"
  1173   shows "Gcd A = 1"
  1174 proof -
  1175   from assms have "is_unit (Gcd A)"
  1176     by (blast intro: Gcd_dvd dvd_unit_imp_unit)
  1177   then have "normalize (Gcd A) = 1"
  1178     by (rule is_unit_normalize)
  1179   then show ?thesis
  1180     by simp
  1181 qed
  1182 
  1183 lemma Lcm_eq_0_I:
  1184   assumes "0 \<in> A"
  1185   shows "Lcm A = 0"
  1186 proof -
  1187   from assms have "0 dvd Lcm A"
  1188     by (rule dvd_Lcm)
  1189   then show ?thesis
  1190     by simp
  1191 qed
  1192 
  1193 lemma Gcd_UNIV [simp]: "Gcd UNIV = 1"
  1194   using dvd_refl by (rule Gcd_eq_1_I) simp
  1195 
  1196 lemma Lcm_UNIV [simp]: "Lcm UNIV = 0"
  1197   by (rule Lcm_eq_0_I) simp
  1198 
  1199 lemma Lcm_0_iff:
  1200   assumes "finite A"
  1201   shows "Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
  1202 proof (cases "A = {}")
  1203   case True
  1204   then show ?thesis by simp
  1205 next
  1206   case False
  1207   with assms show ?thesis
  1208     by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff)
  1209 qed
  1210 
  1211 lemma Gcd_finite:
  1212   assumes "finite A"
  1213   shows "Gcd A = Finite_Set.fold gcd 0 A"
  1214   by (induct rule: finite.induct[OF \<open>finite A\<close>])
  1215     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
  1216 
  1217 lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as"
  1218   by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd]
  1219       foldl_conv_fold gcd.commute)
  1220 
  1221 lemma Lcm_finite:
  1222   assumes "finite A"
  1223   shows "Lcm A = Finite_Set.fold lcm 1 A"
  1224   by (induct rule: finite.induct[OF \<open>finite A\<close>])
  1225     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
  1226 
  1227 lemma Lcm_set [code_unfold]: "Lcm (set as) = foldl lcm 1 as"
  1228   by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm]
  1229       foldl_conv_fold lcm.commute)
  1230 
  1231 lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
  1232 proof -
  1233   have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
  1234   proof -
  1235     from that obtain B where "A = insert a B"
  1236       by blast
  1237     moreover have "gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
  1238       by (rule gcd_dvd1)
  1239     ultimately show "Gcd (normalize ` A) dvd a"
  1240       by simp
  1241   qed
  1242   then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
  1243     by (auto intro!: Gcd_greatest intro: Gcd_dvd)
  1244   then show ?thesis
  1245     by (auto intro: associated_eqI)
  1246 qed
  1247 
  1248 lemma Gcd_eqI:
  1249   assumes "normalize a = a"
  1250   assumes "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
  1251     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> c dvd b) \<Longrightarrow> c dvd a"
  1252   shows "Gcd A = a"
  1253   using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd)
  1254 
  1255 lemma dvd_GcdD: "x dvd Gcd A \<Longrightarrow> y \<in> A \<Longrightarrow> x dvd y"
  1256   using Gcd_dvd dvd_trans by blast
  1257 
  1258 lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
  1259   by (blast dest: dvd_GcdD intro: Gcd_greatest)
  1260 
  1261 lemma Gcd_mult: "Gcd (op * c ` A) = normalize c * Gcd A"
  1262 proof (cases "c = 0")
  1263   case True
  1264   then show ?thesis by auto
  1265 next
  1266   case [simp]: False
  1267   have "Gcd (op * c ` A) div c dvd Gcd A"
  1268     by (intro Gcd_greatest, subst div_dvd_iff_mult)
  1269        (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
  1270   then have "Gcd (op * c ` A) dvd c * Gcd A"
  1271     by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
  1272   also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
  1273     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
  1274   also have "Gcd (op * c ` A) dvd \<dots> \<longleftrightarrow> Gcd (op * c ` A) dvd normalize c * Gcd A"
  1275     by (simp add: dvd_mult_unit_iff)
  1276   finally have "Gcd (op * c ` A) dvd normalize c * Gcd A" .
  1277   moreover have "normalize c * Gcd A dvd Gcd (op * c ` A)"
  1278     by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
  1279   ultimately have "normalize (Gcd (op * c ` A)) = normalize (normalize c * Gcd A)"
  1280     by (rule associatedI)
  1281   then show ?thesis
  1282     by (simp add: normalize_mult)
  1283 qed
  1284 
  1285 lemma Lcm_eqI:
  1286   assumes "normalize a = a"
  1287     and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
  1288     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> b dvd c) \<Longrightarrow> a dvd c"
  1289   shows "Lcm A = a"
  1290   using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
  1291 
  1292 lemma Lcm_dvdD: "Lcm A dvd x \<Longrightarrow> y \<in> A \<Longrightarrow> y dvd x"
  1293   using dvd_Lcm dvd_trans by blast
  1294 
  1295 lemma Lcm_dvd_iff: "Lcm A dvd x \<longleftrightarrow> (\<forall>y\<in>A. y dvd x)"
  1296   by (blast dest: Lcm_dvdD intro: Lcm_least)
  1297 
  1298 lemma Lcm_mult:
  1299   assumes "A \<noteq> {}"
  1300   shows "Lcm (op * c ` A) = normalize c * Lcm A"
  1301 proof (cases "c = 0")
  1302   case True
  1303   with assms have "op * c ` A = {0}"
  1304     by auto
  1305   with True show ?thesis by auto
  1306 next
  1307   case [simp]: False
  1308   from assms obtain x where x: "x \<in> A"
  1309     by blast
  1310   have "c dvd c * x"
  1311     by simp
  1312   also from x have "c * x dvd Lcm (op * c ` A)"
  1313     by (intro dvd_Lcm) auto
  1314   finally have dvd: "c dvd Lcm (op * c ` A)" .
  1315 
  1316   have "Lcm A dvd Lcm (op * c ` A) div c"
  1317     by (intro Lcm_least dvd_mult_imp_div)
  1318       (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
  1319   then have "c * Lcm A dvd Lcm (op * c ` A)"
  1320     by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
  1321   also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
  1322     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
  1323   also have "\<dots> dvd Lcm (op * c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (op * c ` A)"
  1324     by (simp add: mult_unit_dvd_iff)
  1325   finally have "normalize c * Lcm A dvd Lcm (op * c ` A)" .
  1326   moreover have "Lcm (op * c ` A) dvd normalize c * Lcm A"
  1327     by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
  1328   ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (op * c ` A))"
  1329     by (rule associatedI)
  1330   then show ?thesis
  1331     by (simp add: normalize_mult)
  1332 qed
  1333 
  1334 lemma Lcm_no_units: "Lcm A = Lcm (A - {a. is_unit a})"
  1335 proof -
  1336   have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A"
  1337     by blast
  1338   then have "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
  1339     by (simp add: Lcm_Un [symmetric])
  1340   also have "Lcm {a\<in>A. is_unit a} = 1"
  1341     by simp
  1342   finally show ?thesis
  1343     by simp
  1344 qed
  1345 
  1346 lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> (\<nexists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
  1347   by (metis Lcm_least dvd_0_left dvd_Lcm)
  1348 
  1349 lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not> a dvd m)) \<Longrightarrow> Lcm A = 0"
  1350   by (auto simp: Lcm_0_iff')
  1351 
  1352 lemma Lcm_singleton [simp]: "Lcm {a} = normalize a"
  1353   by simp
  1354 
  1355 lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
  1356   by simp
  1357 
  1358 lemma Lcm_coprime:
  1359   assumes "finite A"
  1360     and "A \<noteq> {}"
  1361     and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
  1362   shows "Lcm A = normalize (\<Prod>A)"
  1363   using assms
  1364 proof (induct rule: finite_ne_induct)
  1365   case singleton
  1366   then show ?case by simp
  1367 next
  1368   case (insert a A)
  1369   have "Lcm (insert a A) = lcm a (Lcm A)"
  1370     by simp
  1371   also from insert have "Lcm A = normalize (\<Prod>A)"
  1372     by blast
  1373   also have "lcm a \<dots> = lcm a (\<Prod>A)"
  1374     by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
  1375   also from insert have "gcd a (\<Prod>A) = 1"
  1376     by (subst gcd.commute, intro prod_coprime) auto
  1377   with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
  1378     by (simp add: lcm_coprime)
  1379   finally show ?case .
  1380 qed
  1381 
  1382 lemma Lcm_coprime':
  1383   "card A \<noteq> 0 \<Longrightarrow>
  1384     (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) \<Longrightarrow>
  1385     Lcm A = normalize (\<Prod>A)"
  1386   by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
  1387 
  1388 lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1"
  1389   by (auto intro!: Gcd_eq_1_I)
  1390 
  1391 lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
  1392   by simp
  1393 
  1394 lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
  1395   by simp
  1396 
  1397 
  1398 definition pairwise_coprime
  1399   where "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
  1400 
  1401 lemma pairwise_coprimeI [intro?]:
  1402   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
  1403   by (simp add: pairwise_coprime_def)
  1404 
  1405 lemma pairwise_coprimeD:
  1406   "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
  1407   by (simp add: pairwise_coprime_def)
  1408 
  1409 lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
  1410   by (force simp: pairwise_coprime_def)
  1411 
  1412 end
  1413 
  1414 
  1415 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
  1416 
  1417 instantiation nat :: gcd
  1418 begin
  1419 
  1420 fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  1421   where "gcd_nat x y = (if y = 0 then x else gcd y (x mod y))"
  1422 
  1423 definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  1424   where "lcm_nat x y = x * y div (gcd x y)"
  1425 
  1426 instance ..
  1427 
  1428 end
  1429 
  1430 instantiation int :: gcd
  1431 begin
  1432 
  1433 definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
  1434   where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
  1435 
  1436 definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
  1437   where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
  1438 
  1439 instance ..
  1440 
  1441 end
  1442 
  1443 text \<open>Transfer setup\<close>
  1444 
  1445 lemma transfer_nat_int_gcd:
  1446   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
  1447   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
  1448   for x y :: int
  1449   unfolding gcd_int_def lcm_int_def by auto
  1450 
  1451 lemma transfer_nat_int_gcd_closures:
  1452   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
  1453   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
  1454   for x y :: int
  1455   by (auto simp add: gcd_int_def lcm_int_def)
  1456 
  1457 declare transfer_morphism_nat_int
  1458   [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
  1459 
  1460 lemma transfer_int_nat_gcd:
  1461   "gcd (int x) (int y) = int (gcd x y)"
  1462   "lcm (int x) (int y) = int (lcm x y)"
  1463   by (auto simp: gcd_int_def lcm_int_def)
  1464 
  1465 lemma transfer_int_nat_gcd_closures:
  1466   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
  1467   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
  1468   by (auto simp: gcd_int_def lcm_int_def)
  1469 
  1470 declare transfer_morphism_int_nat
  1471   [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
  1472 
  1473 lemma gcd_nat_induct:
  1474   fixes m n :: nat
  1475   assumes "\<And>m. P m 0"
  1476     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
  1477   shows "P m n"
  1478   apply (rule gcd_nat.induct)
  1479   apply (case_tac "y = 0")
  1480   using assms
  1481    apply simp_all
  1482   done
  1483 
  1484 
  1485 text \<open>Specific to \<open>int\<close>.\<close>
  1486 
  1487 lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
  1488   by (simp add: gcd_int_def)
  1489 
  1490 lemma lcm_eq_int_iff: "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
  1491   by (simp add: lcm_int_def)
  1492 
  1493 lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
  1494   for x y :: int
  1495   by (simp add: gcd_int_def)
  1496 
  1497 lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y"
  1498   for x y :: int
  1499   by (simp add: gcd_int_def)
  1500 
  1501 lemma abs_gcd_int [simp]: "\<bar>gcd x y\<bar> = gcd x y"
  1502   for x y :: int
  1503   by (simp add: gcd_int_def)
  1504 
  1505 lemma gcd_abs_int: "gcd x y = gcd \<bar>x\<bar> \<bar>y\<bar>"
  1506   for x y :: int
  1507   by (simp add: gcd_int_def)
  1508 
  1509 lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> y = gcd x y"
  1510   for x y :: int
  1511   by (metis abs_idempotent gcd_abs_int)
  1512 
  1513 lemma gcd_abs2_int [simp]: "gcd x \<bar>y\<bar> = gcd x y"
  1514   for x y :: int
  1515   by (metis abs_idempotent gcd_abs_int)
  1516 
  1517 lemma gcd_cases_int:
  1518   fixes x y :: int
  1519   assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd x y)"
  1520     and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd x (- y))"
  1521     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd (- x) y)"
  1522     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd (- x) (- y))"
  1523   shows "P (gcd x y)"
  1524   using assms by auto arith
  1525 
  1526 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
  1527   for x y :: int
  1528   by (simp add: gcd_int_def)
  1529 
  1530 lemma lcm_neg1_int: "lcm (- x) y = lcm x y"
  1531   for x y :: int
  1532   by (simp add: lcm_int_def)
  1533 
  1534 lemma lcm_neg2_int: "lcm x (- y) = lcm x y"
  1535   for x y :: int
  1536   by (simp add: lcm_int_def)
  1537 
  1538 lemma lcm_abs_int: "lcm x y = lcm \<bar>x\<bar> \<bar>y\<bar>"
  1539   for x y :: int
  1540   by (simp add: lcm_int_def)
  1541 
  1542 lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
  1543   for i j :: int
  1544   by (simp add:lcm_int_def)
  1545 
  1546 lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> y = lcm x y"
  1547   for x y :: int
  1548   by (metis abs_idempotent lcm_int_def)
  1549 
  1550 lemma lcm_abs2_int [simp]: "lcm x \<bar>y\<bar> = lcm x y"
  1551   for x y :: int
  1552   by (metis abs_idempotent lcm_int_def)
  1553 
  1554 lemma lcm_cases_int:
  1555   fixes x y :: int
  1556   assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm x y)"
  1557     and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm x (- y))"
  1558     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm (- x) y)"
  1559     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm (- x) (- y))"
  1560   shows "P (lcm x y)"
  1561   using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
  1562 
  1563 lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
  1564   for x y :: int
  1565   by (simp add: lcm_int_def)
  1566 
  1567 lemma gcd_0_nat: "gcd x 0 = x"
  1568   for x :: nat
  1569   by simp
  1570 
  1571 lemma gcd_0_int [simp]: "gcd x 0 = \<bar>x\<bar>"
  1572   for x :: int
  1573   by (auto simp: gcd_int_def)
  1574 
  1575 lemma gcd_0_left_nat: "gcd 0 x = x"
  1576   for x :: nat
  1577   by simp
  1578 
  1579 lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>"
  1580   for x :: int
  1581   by (auto simp:gcd_int_def)
  1582 
  1583 lemma gcd_red_nat: "gcd x y = gcd y (x mod y)"
  1584   for x y :: nat
  1585   by (cases "y = 0") auto
  1586 
  1587 
  1588 text \<open>Weaker, but useful for the simplifier.\<close>
  1589 
  1590 lemma gcd_non_0_nat: "y \<noteq> 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
  1591   for x y :: nat
  1592   by simp
  1593 
  1594 lemma gcd_1_nat [simp]: "gcd m 1 = 1"
  1595   for m :: nat
  1596   by simp
  1597 
  1598 lemma gcd_Suc_0 [simp]: "gcd m (Suc 0) = Suc 0"
  1599   for m :: nat
  1600   by simp
  1601 
  1602 lemma gcd_1_int [simp]: "gcd m 1 = 1"
  1603   for m :: int
  1604   by (simp add: gcd_int_def)
  1605 
  1606 lemma gcd_idem_nat: "gcd x x = x"
  1607   for x :: nat
  1608   by simp
  1609 
  1610 lemma gcd_idem_int: "gcd x x = \<bar>x\<bar>"
  1611   for x :: int
  1612   by (auto simp add: gcd_int_def)
  1613 
  1614 declare gcd_nat.simps [simp del]
  1615 
  1616 text \<open>
  1617   \<^medskip> @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.
  1618   The conjunctions don't seem provable separately.
  1619 \<close>
  1620 
  1621 instance nat :: semiring_gcd
  1622 proof
  1623   fix m n :: nat
  1624   show "gcd m n dvd m" and "gcd m n dvd n"
  1625   proof (induct m n rule: gcd_nat_induct)
  1626     fix m n :: nat
  1627     assume "gcd n (m mod n) dvd m mod n"
  1628       and "gcd n (m mod n) dvd n"
  1629     then have "gcd n (m mod n) dvd m"
  1630       by (rule dvd_mod_imp_dvd)
  1631     moreover assume "0 < n"
  1632     ultimately show "gcd m n dvd m"
  1633       by (simp add: gcd_non_0_nat)
  1634   qed (simp_all add: gcd_0_nat gcd_non_0_nat)
  1635 next
  1636   fix m n k :: nat
  1637   assume "k dvd m" and "k dvd n"
  1638   then show "k dvd gcd m n"
  1639     by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
  1640 qed (simp_all add: lcm_nat_def)
  1641 
  1642 instance int :: ring_gcd
  1643   by standard
  1644     (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def
  1645       zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
  1646 
  1647 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a"
  1648   for a b :: nat
  1649   by (rule dvd_imp_le) auto
  1650 
  1651 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd a b \<le> b"
  1652   for a b :: nat
  1653   by (rule dvd_imp_le) auto
  1654 
  1655 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd a b \<le> a"
  1656   for a b :: int
  1657   by (rule zdvd_imp_le) auto
  1658 
  1659 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd a b \<le> b"
  1660   for a b :: int
  1661   by (rule zdvd_imp_le) auto
  1662 
  1663 lemma gcd_pos_nat [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
  1664   for m n :: nat
  1665   using gcd_eq_0_iff [of m n] by arith
  1666 
  1667 lemma gcd_pos_int [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
  1668   for m n :: int
  1669   using gcd_eq_0_iff [of m n] gcd_ge_0_int [of m n] by arith
  1670 
  1671 lemma gcd_unique_nat: "d dvd a \<and> d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
  1672   for d a :: nat
  1673   apply auto
  1674   apply (rule dvd_antisym)
  1675    apply (erule (1) gcd_greatest)
  1676   apply auto
  1677   done
  1678 
  1679 lemma gcd_unique_int:
  1680   "d \<ge> 0 \<and> d dvd a \<and> d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
  1681   for d a :: int
  1682   apply (cases "d = 0")
  1683    apply simp
  1684   apply (rule iffI)
  1685    apply (rule zdvd_antisym_nonneg)
  1686       apply (auto intro: gcd_greatest)
  1687   done
  1688 
  1689 interpretation gcd_nat:
  1690   semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
  1691   by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
  1692 
  1693 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
  1694   for x y :: int
  1695   by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
  1696 
  1697 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>"
  1698   for x y :: int
  1699   by (metis gcd_proj1_if_dvd_int gcd.commute)
  1700 
  1701 
  1702 text \<open>\<^medskip> Multiplication laws.\<close>
  1703 
  1704 lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
  1705   for k m n :: nat
  1706   \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
  1707   apply (induct m n rule: gcd_nat_induct)
  1708    apply simp
  1709   apply (cases "k = 0")
  1710    apply (simp_all add: gcd_non_0_nat)
  1711   done
  1712 
  1713 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
  1714   for k m n :: int
  1715   apply (subst (1 2) gcd_abs_int)
  1716   apply (subst (1 2) abs_mult)
  1717   apply (rule gcd_mult_distrib_nat [transferred])
  1718     apply auto
  1719   done
  1720 
  1721 lemma coprime_crossproduct_nat:
  1722   fixes a b c d :: nat
  1723   assumes "coprime a d" and "coprime b c"
  1724   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
  1725   using assms coprime_crossproduct [of a d b c] by simp
  1726 
  1727 lemma coprime_crossproduct_int:
  1728   fixes a b c d :: int
  1729   assumes "coprime a d" and "coprime b c"
  1730   shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
  1731   using assms coprime_crossproduct [of a d b c] by simp
  1732 
  1733 
  1734 text \<open>\medskip Addition laws.\<close>
  1735 
  1736 (* TODO: add the other variations? *)
  1737 
  1738 lemma gcd_diff1_nat: "m \<ge> n \<Longrightarrow> gcd (m - n) n = gcd m n"
  1739   for m n :: nat
  1740   by (subst gcd_add1 [symmetric]) auto
  1741 
  1742 lemma gcd_diff2_nat: "n \<ge> m \<Longrightarrow> gcd (n - m) n = gcd m n"
  1743   for m n :: nat
  1744   apply (subst gcd.commute)
  1745   apply (subst gcd_diff1_nat [symmetric])
  1746    apply auto
  1747   apply (subst gcd.commute)
  1748   apply (subst gcd_diff1_nat)
  1749    apply assumption
  1750   apply (rule gcd.commute)
  1751   done
  1752 
  1753 lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
  1754   for x y :: int
  1755   apply (frule_tac b = y and a = x in pos_mod_sign)
  1756   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
  1757   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
  1758   apply (frule_tac a = x in pos_mod_bound)
  1759   apply (subst (1 2) gcd.commute)
  1760   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
  1761   done
  1762 
  1763 lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
  1764   for x y :: int
  1765   apply (cases "y = 0")
  1766    apply force
  1767   apply (cases "y > 0")
  1768    apply (subst gcd_non_0_int, auto)
  1769   apply (insert gcd_non_0_int [of "- y" "- x"])
  1770   apply auto
  1771   done
  1772 
  1773 (* TODO: differences, and all variations of addition rules
  1774     as simplification rules for nat and int *)
  1775 
  1776 (* TODO: add the three variations of these, and for ints? *)
  1777 
  1778 lemma finite_divisors_nat [simp]: (* FIXME move *)
  1779   fixes m :: nat
  1780   assumes "m > 0"
  1781   shows "finite {d. d dvd m}"
  1782 proof-
  1783   from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}"
  1784     by (auto dest: dvd_imp_le)
  1785   then show ?thesis
  1786     using finite_Collect_le_nat by (rule finite_subset)
  1787 qed
  1788 
  1789 lemma finite_divisors_int [simp]:
  1790   fixes i :: int
  1791   assumes "i \<noteq> 0"
  1792   shows "finite {d. d dvd i}"
  1793 proof -
  1794   have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}"
  1795     by (auto simp: abs_if)
  1796   then have "finite {d. \<bar>d\<bar> \<le> \<bar>i\<bar>}"
  1797     by simp
  1798   from finite_subset [OF _ this] show ?thesis
  1799     using assms by (simp add: dvd_imp_le_int subset_iff)
  1800 qed
  1801 
  1802 lemma Max_divisors_self_nat [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::nat. d dvd n} = n"
  1803   apply (rule antisym)
  1804    apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
  1805   apply simp
  1806   done
  1807 
  1808 lemma Max_divisors_self_int [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::int. d dvd n} = \<bar>n\<bar>"
  1809   apply (rule antisym)
  1810    apply (rule Max_le_iff [THEN iffD2])
  1811      apply (auto intro: abs_le_D1 dvd_imp_le_int)
  1812   done
  1813 
  1814 lemma gcd_is_Max_divisors_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
  1815   for m n :: nat
  1816   apply (rule Max_eqI[THEN sym])
  1817     apply (metis finite_Collect_conjI finite_divisors_nat)
  1818    apply simp
  1819    apply (metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
  1820   apply simp
  1821   done
  1822 
  1823 lemma gcd_is_Max_divisors_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
  1824   for m n :: int
  1825   apply (rule Max_eqI[THEN sym])
  1826     apply (metis finite_Collect_conjI finite_divisors_int)
  1827    apply simp
  1828    apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
  1829   apply simp
  1830   done
  1831 
  1832 lemma gcd_code_int [code]: "gcd k l = \<bar>if l = 0 then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  1833   for k l :: int
  1834   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
  1835 
  1836 
  1837 subsection \<open>Coprimality\<close>
  1838 
  1839 lemma coprime_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1840   for a b :: nat
  1841   using coprime [of a b] by simp
  1842 
  1843 lemma coprime_Suc_0_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
  1844   for a b :: nat
  1845   using coprime_nat by simp
  1846 
  1847 lemma coprime_int: "coprime a b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1848   for a b :: int
  1849   using gcd_unique_int [of 1 a b]
  1850   apply clarsimp
  1851   apply (erule subst)
  1852   apply (rule iffI)
  1853    apply force
  1854   using abs_dvd_iff abs_ge_zero apply blast
  1855   done
  1856 
  1857 lemma pow_divides_eq_nat [simp]: "n > 0 \<Longrightarrow> a^n dvd b^n \<longleftrightarrow> a dvd b"
  1858   for a b n :: nat
  1859   using pow_divs_eq[of n] by simp
  1860 
  1861 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
  1862   using coprime_plus_one[of n] by simp
  1863 
  1864 lemma coprime_minus_one_nat: "n \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
  1865   for n :: nat
  1866   using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
  1867 
  1868 lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
  1869   for a b :: nat
  1870   by (metis gcd_greatest_iff nat_dvd_1_iff_1)
  1871 
  1872 lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
  1873   for a b :: int
  1874   using gcd_greatest_iff [of x a b] by auto
  1875 
  1876 lemma invertible_coprime_nat: "x * y mod m = 1 \<Longrightarrow> coprime x m"
  1877   for m x y :: nat
  1878   by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
  1879 
  1880 lemma invertible_coprime_int: "x * y mod m = 1 \<Longrightarrow> coprime x m"
  1881   for m x y :: int
  1882   by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
  1883 
  1884 
  1885 subsection \<open>Bezout's theorem\<close>
  1886 
  1887 text \<open>
  1888   Function \<open>bezw\<close> returns a pair of witnesses to Bezout's theorem --
  1889   see the theorems that follow the definition.
  1890 \<close>
  1891 
  1892 fun bezw :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1893   where "bezw x y =
  1894     (if y = 0 then (1, 0)
  1895      else
  1896       (snd (bezw y (x mod y)),
  1897        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1898 
  1899 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)"
  1900   by simp
  1901 
  1902 lemma bezw_non_0:
  1903   "y > 0 \<Longrightarrow> bezw x y =
  1904     (snd (bezw y (x mod y)), fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1905   by simp
  1906 
  1907 declare bezw.simps [simp del]
  1908 
  1909 lemma bezw_aux: "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1910 proof (induct x y rule: gcd_nat_induct)
  1911   fix m :: nat
  1912   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1913     by auto
  1914 next
  1915   fix m n :: nat
  1916   assume ngt0: "n > 0"
  1917     and ih: "fst (bezw n (m mod n)) * int n + snd (bezw n (m mod n)) * int (m mod n) =
  1918       int (gcd n (m mod n))"
  1919   then show "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1920     apply (simp add: bezw_non_0 gcd_non_0_nat)
  1921     apply (erule subst)
  1922     apply (simp add: field_simps)
  1923     apply (subst div_mult_mod_eq [of m n, symmetric])
  1924       (* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *)
  1925     apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
  1926     done
  1927 qed
  1928 
  1929 lemma bezout_int: "\<exists>u v. u * x + v * y = gcd x y"
  1930   for x y :: int
  1931 proof -
  1932   have aux: "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> \<exists>u v. u * x + v * y = gcd x y" for x y :: int
  1933     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1934     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1935     apply (unfold gcd_int_def)
  1936     apply simp
  1937     apply (subst bezw_aux [symmetric])
  1938     apply auto
  1939     done
  1940   consider "x \<ge> 0" "y \<ge> 0" | "x \<ge> 0" "y \<le> 0" | "x \<le> 0" "y \<ge> 0" | "x \<le> 0" "y \<le> 0"
  1941     by atomize_elim auto
  1942   then show ?thesis
  1943   proof cases
  1944     case 1
  1945     then show ?thesis by (rule aux)
  1946   next
  1947     case 2
  1948     then show ?thesis
  1949       apply -
  1950       apply (insert aux [of x "-y"])
  1951       apply auto
  1952       apply (rule_tac x = u in exI)
  1953       apply (rule_tac x = "-v" in exI)
  1954       apply (subst gcd_neg2_int [symmetric])
  1955       apply auto
  1956       done
  1957   next
  1958     case 3
  1959     then show ?thesis
  1960       apply -
  1961       apply (insert aux [of "-x" y])
  1962       apply auto
  1963       apply (rule_tac x = "-u" in exI)
  1964       apply (rule_tac x = v in exI)
  1965       apply (subst gcd_neg1_int [symmetric])
  1966       apply auto
  1967       done
  1968   next
  1969     case 4
  1970     then show ?thesis
  1971       apply -
  1972       apply (insert aux [of "-x" "-y"])
  1973       apply auto
  1974       apply (rule_tac x = "-u" in exI)
  1975       apply (rule_tac x = "-v" in exI)
  1976       apply (subst gcd_neg1_int [symmetric])
  1977       apply (subst gcd_neg2_int [symmetric])
  1978       apply auto
  1979       done
  1980   qed
  1981 qed
  1982 
  1983 
  1984 text \<open>Versions of Bezout for \<open>nat\<close>, by Amine Chaieb.\<close>
  1985 
  1986 lemma ind_euclid:
  1987   fixes P :: "nat \<Rightarrow> nat \<Rightarrow> bool"
  1988   assumes c: " \<forall>a b. P a b \<longleftrightarrow> P b a"
  1989     and z: "\<forall>a. P a 0"
  1990     and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1991   shows "P a b"
  1992 proof (induct "a + b" arbitrary: a b rule: less_induct)
  1993   case less
  1994   consider (eq) "a = b" | (lt) "a < b" "a + b - a < a + b" | "b = 0" | "b + a - b < a + b"
  1995     by arith
  1996   show ?case
  1997   proof (cases a b rule: linorder_cases)
  1998     case equal
  1999     with add [rule_format, OF z [rule_format, of a]] show ?thesis by simp
  2000   next
  2001     case lt: less
  2002     then consider "a = 0" | "a + b - a < a + b" by arith
  2003     then show ?thesis
  2004     proof cases
  2005       case 1
  2006       with z c show ?thesis by blast
  2007     next
  2008       case 2
  2009       also have *: "a + b - a = a + (b - a)" using lt by arith
  2010       finally have "a + (b - a) < a + b" .
  2011       then have "P a (a + (b - a))" by (rule add [rule_format, OF less])
  2012       then show ?thesis by (simp add: *[symmetric])
  2013     qed
  2014   next
  2015     case gt: greater
  2016     then consider "b = 0" | "b + a - b < a + b" by arith
  2017     then show ?thesis
  2018     proof cases
  2019       case 1
  2020       with z c show ?thesis by blast
  2021     next
  2022       case 2
  2023       also have *: "b + a - b = b + (a - b)" using gt by arith
  2024       finally have "b + (a - b) < a + b" .
  2025       then have "P b (b + (a - b))" by (rule add [rule_format, OF less])
  2026       then have "P b a" by (simp add: *[symmetric])
  2027       with c show ?thesis by blast
  2028     qed
  2029   qed
  2030 qed
  2031 
  2032 lemma bezout_lemma_nat:
  2033   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  2034     (a * x = b * y + d \<or> b * x = a * y + d)"
  2035   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  2036     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  2037   using ex
  2038   apply clarsimp
  2039   apply (rule_tac x="d" in exI)
  2040   apply simp
  2041   apply (case_tac "a * x = b * y + d")
  2042    apply simp_all
  2043    apply (rule_tac x="x + y" in exI)
  2044    apply (rule_tac x="y" in exI)
  2045    apply algebra
  2046   apply (rule_tac x="x" in exI)
  2047   apply (rule_tac x="x + y" in exI)
  2048   apply algebra
  2049   done
  2050 
  2051 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  2052     (a * x = b * y + d \<or> b * x = a * y + d)"
  2053   apply (induct a b rule: ind_euclid)
  2054     apply blast
  2055    apply clarify
  2056    apply (rule_tac x="a" in exI)
  2057    apply simp
  2058   apply clarsimp
  2059   apply (rule_tac x="d" in exI)
  2060   apply (case_tac "a * x = b * y + d")
  2061    apply simp_all
  2062    apply (rule_tac x="x+y" in exI)
  2063    apply (rule_tac x="y" in exI)
  2064    apply algebra
  2065   apply (rule_tac x="x" in exI)
  2066   apply (rule_tac x="x+y" in exI)
  2067   apply algebra
  2068   done
  2069 
  2070 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  2071     (a * x - b * y = d \<or> b * x - a * y = d)"
  2072   using bezout_add_nat[of a b]
  2073   apply clarsimp
  2074   apply (rule_tac x="d" in exI)
  2075   apply simp
  2076   apply (rule_tac x="x" in exI)
  2077   apply (rule_tac x="y" in exI)
  2078   apply auto
  2079   done
  2080 
  2081 lemma bezout_add_strong_nat:
  2082   fixes a b :: nat
  2083   assumes a: "a \<noteq> 0"
  2084   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  2085 proof -
  2086   consider d x y where "d dvd a" "d dvd b" "a * x = b * y + d"
  2087     | d x y where "d dvd a" "d dvd b" "b * x = a * y + d"
  2088     using bezout_add_nat [of a b] by blast
  2089   then show ?thesis
  2090   proof cases
  2091     case 1
  2092     then show ?thesis by blast
  2093   next
  2094     case H: 2
  2095     show ?thesis
  2096     proof (cases "b = 0")
  2097       case True
  2098       with H show ?thesis by simp
  2099     next
  2100       case False
  2101       then have bp: "b > 0" by simp
  2102       with dvd_imp_le [OF H(2)] consider "d = b" | "d < b"
  2103         by atomize_elim auto
  2104       then show ?thesis
  2105       proof cases
  2106         case 1
  2107         with a H show ?thesis
  2108           apply simp
  2109           apply (rule exI[where x = b])
  2110           apply simp
  2111           apply (rule exI[where x = b])
  2112           apply (rule exI[where x = "a - 1"])
  2113           apply (simp add: diff_mult_distrib2)
  2114           done
  2115       next
  2116         case 2
  2117         show ?thesis
  2118         proof (cases "x = 0")
  2119           case True
  2120           with a H show ?thesis by simp
  2121         next
  2122           case x0: False
  2123           then have xp: "x > 0" by simp
  2124           from \<open>d < b\<close> have "d \<le> b - 1" by simp
  2125           then have "d * b \<le> b * (b - 1)" by simp
  2126           with xp mult_mono[of "1" "x" "d * b" "b * (b - 1)"]
  2127           have dble: "d * b \<le> x * b * (b - 1)" using bp by simp
  2128           from H(3) have "d + (b - 1) * (b * x) = d + (b - 1) * (a * y + d)"
  2129             by simp
  2130           then have "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  2131             by (simp only: mult.assoc distrib_left)
  2132           then have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x * b * (b - 1)"
  2133             by algebra
  2134           then have "a * ((b - 1) * y) = d + x * b * (b - 1) - d * b"
  2135             using bp by simp
  2136           then have "a * ((b - 1) * y) = d + (x * b * (b - 1) - d * b)"
  2137             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  2138           then have "a * ((b - 1) * y) = b * (x * (b - 1) - d) + d"
  2139             by (simp only: diff_mult_distrib2 ac_simps)
  2140           with H(1,2) show ?thesis
  2141             apply -
  2142             apply (rule exI [where x = d])
  2143             apply simp
  2144             apply (rule exI [where x = "(b - 1) * y"])
  2145             apply (rule exI [where x = "x * (b - 1) - d"])
  2146             apply simp
  2147             done
  2148         qed
  2149       qed
  2150     qed
  2151   qed
  2152 qed
  2153 
  2154 lemma bezout_nat:
  2155   fixes a :: nat
  2156   assumes a: "a \<noteq> 0"
  2157   shows "\<exists>x y. a * x = b * y + gcd a b"
  2158 proof -
  2159   obtain d x y where d: "d dvd a" "d dvd b" and eq: "a * x = b * y + d"
  2160     using bezout_add_strong_nat [OF a, of b] by blast
  2161   from d have "d dvd gcd a b"
  2162     by simp
  2163   then obtain k where k: "gcd a b = d * k"
  2164     unfolding dvd_def by blast
  2165   from eq have "a * x * k = (b * y + d) * k"
  2166     by auto
  2167   then have "a * (x * k) = b * (y * k) + gcd a b"
  2168     by (algebra add: k)
  2169   then show ?thesis
  2170     by blast
  2171 qed
  2172 
  2173 
  2174 subsection \<open>LCM properties on @{typ nat} and @{typ int}\<close>
  2175 
  2176 lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  2177   for a b :: int
  2178   by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
  2179 
  2180 lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
  2181   for m n :: nat
  2182   unfolding lcm_nat_def
  2183   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
  2184 
  2185 lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
  2186   for m n :: int
  2187   unfolding lcm_int_def gcd_int_def
  2188   apply (subst of_nat_mult [symmetric])
  2189   apply (subst prod_gcd_lcm_nat [symmetric])
  2190   apply (subst nat_abs_mult_distrib [symmetric])
  2191   apply (simp add: abs_mult)
  2192   done
  2193 
  2194 lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
  2195   for m n :: nat
  2196   by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  2197 
  2198 lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
  2199   for m n :: int
  2200   apply (subst lcm_abs_int)
  2201   apply (rule lcm_pos_nat [transferred])
  2202      apply auto
  2203   done
  2204 
  2205 lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
  2206   for m n :: nat
  2207   by (cases m) auto
  2208 
  2209 lemma lcm_unique_nat:
  2210   "a dvd d \<and> b dvd d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  2211   for a b d :: nat
  2212   by (auto intro: dvd_antisym lcm_least)
  2213 
  2214 lemma lcm_unique_int:
  2215   "d \<ge> 0 \<and> a dvd d \<and> b dvd d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  2216   for a b d :: int
  2217   using lcm_least zdvd_antisym_nonneg by auto
  2218 
  2219 lemma lcm_proj2_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm x y = y"
  2220   for x y :: nat
  2221   apply (rule sym)
  2222   apply (subst lcm_unique_nat [symmetric])
  2223   apply auto
  2224   done
  2225 
  2226 lemma lcm_proj2_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
  2227   for x y :: int
  2228   apply (rule sym)
  2229   apply (subst lcm_unique_int [symmetric])
  2230   apply auto
  2231   done
  2232 
  2233 lemma lcm_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm y x = y"
  2234   for x y :: nat
  2235   by (subst lcm.commute) (erule lcm_proj2_if_dvd_nat)
  2236 
  2237 lemma lcm_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
  2238   for x y :: int
  2239   by (subst lcm.commute) (erule lcm_proj2_if_dvd_int)
  2240 
  2241 lemma lcm_proj1_iff_nat [simp]: "lcm m n = m \<longleftrightarrow> n dvd m"
  2242   for m n :: nat
  2243   by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  2244 
  2245 lemma lcm_proj2_iff_nat [simp]: "lcm m n = n \<longleftrightarrow> m dvd n"
  2246   for m n :: nat
  2247   by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  2248 
  2249 lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m\<bar> \<longleftrightarrow> n dvd m"
  2250   for m n :: int
  2251   by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  2252 
  2253 lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n\<bar> \<longleftrightarrow> m dvd n"
  2254   for m n :: int
  2255   by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  2256 
  2257 lemma lcm_1_iff_nat [simp]: "lcm m n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
  2258   for m n :: nat
  2259   using lcm_eq_1_iff [of m n] by simp
  2260 
  2261 lemma lcm_1_iff_int [simp]: "lcm m n = 1 \<longleftrightarrow> (m = 1 \<or> m = -1) \<and> (n = 1 \<or> n = -1)"
  2262   for m n :: int
  2263   by auto
  2264 
  2265 
  2266 subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
  2267 
  2268 text \<open>
  2269   Lifting \<open>gcd\<close> and \<open>lcm\<close> to sets (\<open>Gcd\<close> / \<open>Lcm\<close>).
  2270   \<open>Gcd\<close> is defined via \<open>Lcm\<close> to facilitate the proof that we have a complete lattice.
  2271 \<close>
  2272 
  2273 instantiation nat :: semiring_Gcd
  2274 begin
  2275 
  2276 interpretation semilattice_neutr_set lcm "1::nat"
  2277   by standard simp_all
  2278 
  2279 definition "Lcm M = (if finite M then F M else 0)" for M :: "nat set"
  2280 
  2281 lemma Lcm_nat_empty: "Lcm {} = (1::nat)"
  2282   by (simp add: Lcm_nat_def del: One_nat_def)
  2283 
  2284 lemma Lcm_nat_insert: "Lcm (insert n M) = lcm n (Lcm M)" for n :: nat
  2285   by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
  2286 
  2287 lemma Lcm_nat_infinite: "infinite M \<Longrightarrow> Lcm M = 0" for M :: "nat set"
  2288   by (simp add: Lcm_nat_def)
  2289 
  2290 lemma dvd_Lcm_nat [simp]:
  2291   fixes M :: "nat set"
  2292   assumes "m \<in> M"
  2293   shows "m dvd Lcm M"
  2294 proof -
  2295   from assms have "insert m M = M"
  2296     by auto
  2297   moreover have "m dvd Lcm (insert m M)"
  2298     by (simp add: Lcm_nat_insert)
  2299   ultimately show ?thesis
  2300     by simp
  2301 qed
  2302 
  2303 lemma Lcm_dvd_nat [simp]:
  2304   fixes M :: "nat set"
  2305   assumes "\<forall>m\<in>M. m dvd n"
  2306   shows "Lcm M dvd n"
  2307 proof (cases "n > 0")
  2308   case False
  2309   then show ?thesis by simp
  2310 next
  2311   case True
  2312   then have "finite {d. d dvd n}"
  2313     by (rule finite_divisors_nat)
  2314   moreover have "M \<subseteq> {d. d dvd n}"
  2315     using assms by fast
  2316   ultimately have "finite M"
  2317     by (rule rev_finite_subset)
  2318   then show ?thesis
  2319     using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
  2320 qed
  2321 
  2322 definition "Gcd M = Lcm {d. \<forall>m\<in>M. d dvd m}" for M :: "nat set"
  2323 
  2324 instance
  2325 proof
  2326   fix N :: "nat set"
  2327   fix n :: nat
  2328   show "Gcd N dvd n" if "n \<in> N"
  2329     using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
  2330   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m"
  2331     using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
  2332   show "n dvd Lcm N" if "n \<in> N"
  2333     using that by (induct N rule: infinite_finite_induct) auto
  2334   show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n"
  2335     using that by (induct N rule: infinite_finite_induct) auto
  2336   show "normalize (Gcd N) = Gcd N" and "normalize (Lcm N) = Lcm N"
  2337     by simp_all
  2338 qed
  2339 
  2340 end
  2341 
  2342 lemma Gcd_nat_eq_one: "1 \<in> N \<Longrightarrow> Gcd N = 1"
  2343   for N :: "nat set"
  2344   by (rule Gcd_eq_1_I) auto
  2345 
  2346 
  2347 text \<open>Alternative characterizations of Gcd:\<close>
  2348 
  2349 lemma Gcd_eq_Max:
  2350   fixes M :: "nat set"
  2351   assumes "finite (M::nat set)" and "M \<noteq> {}" and "0 \<notin> M"
  2352   shows "Gcd M = Max (\<Inter>m\<in>M. {d. d dvd m})"
  2353 proof (rule antisym)
  2354   from assms obtain m where "m \<in> M" and "m > 0"
  2355     by auto
  2356   from \<open>m > 0\<close> have "finite {d. d dvd m}"
  2357     by (blast intro: finite_divisors_nat)
  2358   with \<open>m \<in> M\<close> have fin: "finite (\<Inter>m\<in>M. {d. d dvd m})"
  2359     by blast
  2360   from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
  2361     by (auto intro: Max_ge Gcd_dvd)
  2362   from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
  2363     apply (rule Max.boundedI)
  2364      apply auto
  2365     apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
  2366     done
  2367 qed
  2368 
  2369 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0})"
  2370   for M :: "nat set"
  2371   apply (induct pred: finite)
  2372    apply simp
  2373   apply (case_tac "x = 0")
  2374    apply simp
  2375   apply (subgoal_tac "insert x F - {0} = insert x (F - {0})")
  2376    apply simp
  2377   apply blast
  2378   done
  2379 
  2380 lemma Lcm_in_lcm_closed_set_nat:
  2381   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> \<forall>m n. m \<in> M \<longrightarrow> n \<in> M \<longrightarrow> lcm m n \<in> M \<Longrightarrow> Lcm M \<in> M"
  2382   for M :: "nat set"
  2383   apply (induct rule: finite_linorder_min_induct)
  2384    apply simp
  2385   apply simp
  2386   apply (subgoal_tac "\<forall>m n. m \<in> A \<longrightarrow> n \<in> A \<longrightarrow> lcm m n \<in> A")
  2387    apply simp
  2388    apply(case_tac "A = {}")
  2389     apply simp
  2390    apply simp
  2391   apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  2392   done
  2393 
  2394 lemma Lcm_eq_Max_nat:
  2395   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> \<forall>m n. m \<in> M \<longrightarrow> n \<in> M \<longrightarrow> lcm m n \<in> M \<Longrightarrow> Lcm M = Max M"
  2396   for M :: "nat set"
  2397   apply (rule antisym)
  2398    apply (rule Max_ge)
  2399     apply assumption
  2400    apply (erule (2) Lcm_in_lcm_closed_set_nat)
  2401   apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
  2402   done
  2403 
  2404 lemma mult_inj_if_coprime_nat:
  2405   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>B. coprime (f a) (g b) \<Longrightarrow>
  2406     inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)"
  2407   for f :: "'a \<Rightarrow> nat" and g :: "'b \<Rightarrow> nat"
  2408   by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
  2409 
  2410 
  2411 text \<open>Nitpick:\<close>
  2412 
  2413 lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
  2414   by (induct x y rule: nat_gcd.induct)
  2415     (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  2416 
  2417 lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
  2418   by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  2419 
  2420 
  2421 subsubsection \<open>Setwise GCD and LCM for integers\<close>
  2422 
  2423 instantiation int :: semiring_Gcd
  2424 begin
  2425 
  2426 definition "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
  2427 
  2428 definition "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
  2429 
  2430 instance
  2431   by standard
  2432     (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
  2433       Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
  2434 
  2435 end
  2436 
  2437 lemma abs_Gcd [simp]: "\<bar>Gcd K\<bar> = Gcd K"
  2438   for K :: "int set"
  2439   using normalize_Gcd [of K] by simp
  2440 
  2441 lemma abs_Lcm [simp]: "\<bar>Lcm K\<bar> = Lcm K"
  2442   for K :: "int set"
  2443   using normalize_Lcm [of K] by simp
  2444 
  2445 lemma Gcm_eq_int_iff: "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
  2446   by (simp add: Gcd_int_def comp_def image_image)
  2447 
  2448 lemma Lcm_eq_int_iff: "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
  2449   by (simp add: Lcm_int_def comp_def image_image)
  2450 
  2451 
  2452 subsection \<open>GCD and LCM on @{typ integer}\<close>
  2453 
  2454 instantiation integer :: gcd
  2455 begin
  2456 
  2457 context
  2458   includes integer.lifting
  2459 begin
  2460 
  2461 lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
  2462 
  2463 lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
  2464 
  2465 end
  2466 
  2467 instance ..
  2468 
  2469 end
  2470 
  2471 lifting_update integer.lifting
  2472 lifting_forget integer.lifting
  2473 
  2474 context
  2475   includes integer.lifting
  2476 begin
  2477 
  2478 lemma gcd_code_integer [code]: "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  2479   by transfer (fact gcd_code_int)
  2480 
  2481 lemma lcm_code_integer [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  2482   for a b :: integer
  2483   by transfer (fact lcm_altdef_int)
  2484 
  2485 end
  2486 
  2487 code_printing
  2488   constant "gcd :: integer \<Rightarrow> _" \<rightharpoonup>
  2489     (OCaml) "Big'_int.gcd'_big'_int"
  2490   and (Haskell) "Prelude.gcd"
  2491   and (Scala) "_.gcd'((_)')"
  2492   \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
  2493 
  2494 text \<open>Some code equations\<close>
  2495 
  2496 lemmas Lcm_set_nat [code, code_unfold] = Lcm_set[where ?'a = nat]
  2497 lemmas Gcd_set_nat [code] = Gcd_set[where ?'a = nat]
  2498 lemmas Lcm_set_int [code, code_unfold] = Lcm_set[where ?'a = int]
  2499 lemmas Gcd_set_int [code] = Gcd_set[where ?'a = int]
  2500 
  2501 
  2502 text \<open>Fact aliases.\<close>
  2503 
  2504 lemma lcm_0_iff_nat [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
  2505   for m n :: nat
  2506   by (fact lcm_eq_0_iff)
  2507 
  2508 lemma lcm_0_iff_int [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
  2509   for m n :: int
  2510   by (fact lcm_eq_0_iff)
  2511 
  2512 lemma dvd_lcm_I1_nat [simp]: "k dvd m \<Longrightarrow> k dvd lcm m n"
  2513   for k m n :: nat
  2514   by (fact dvd_lcmI1)
  2515 
  2516 lemma dvd_lcm_I2_nat [simp]: "k dvd n \<Longrightarrow> k dvd lcm m n"
  2517   for k m n :: nat
  2518   by (fact dvd_lcmI2)
  2519 
  2520 lemma dvd_lcm_I1_int [simp]: "i dvd m \<Longrightarrow> i dvd lcm m n"
  2521   for i m n :: int
  2522   by (fact dvd_lcmI1)
  2523 
  2524 lemma dvd_lcm_I2_int [simp]: "i dvd n \<Longrightarrow> i dvd lcm m n"
  2525   for i m n :: int
  2526   by (fact dvd_lcmI2)
  2527 
  2528 lemma coprime_exp2_nat [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
  2529   for a b :: nat
  2530   by (fact coprime_exp2)
  2531 
  2532 lemma coprime_exp2_int [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
  2533   for a b :: int
  2534   by (fact coprime_exp2)
  2535 
  2536 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
  2537 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
  2538 lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
  2539 lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int]
  2540 
  2541 lemma dvd_Lcm_int [simp]: "m \<in> M \<Longrightarrow> m dvd Lcm M"
  2542   for M :: "int set"
  2543   by (fact dvd_Lcm)
  2544 
  2545 lemma gcd_neg_numeral_1_int [simp]: "gcd (- numeral n :: int) x = gcd (numeral n) x"
  2546   by (fact gcd_neg1_int)
  2547 
  2548 lemma gcd_neg_numeral_2_int [simp]: "gcd x (- numeral n :: int) = gcd x (numeral n)"
  2549   by (fact gcd_neg2_int)
  2550 
  2551 lemma gcd_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> gcd x y = x"
  2552   for x y :: nat
  2553   by (fact gcd_nat.absorb1)
  2554 
  2555 lemma gcd_proj2_if_dvd_nat [simp]: "y dvd x \<Longrightarrow> gcd x y = y"
  2556   for x y :: nat
  2557   by (fact gcd_nat.absorb2)
  2558 
  2559 lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]
  2560 lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat]
  2561 lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int]
  2562 
  2563 end