src/HOL/GCD.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63882 018998c00003
child 63924 f91766530e13
permissions -rw-r--r--
tuned proofs;
     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_divide_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 setprod_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 end
   943 
   944 class ring_gcd = comm_ring_1 + semiring_gcd
   945 begin
   946 
   947 lemma coprime_minus_one: "coprime (n - 1) n"
   948   using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute)
   949 
   950 lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
   951   by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
   952 
   953 lemma gcd_neg2 [simp]: "gcd a (-b) = gcd a b"
   954   by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
   955 
   956 lemma gcd_neg_numeral_1 [simp]: "gcd (- numeral n) a = gcd (numeral n) a"
   957   by (fact gcd_neg1)
   958 
   959 lemma gcd_neg_numeral_2 [simp]: "gcd a (- numeral n) = gcd a (numeral n)"
   960   by (fact gcd_neg2)
   961 
   962 lemma gcd_diff1: "gcd (m - n) n = gcd m n"
   963   by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp)
   964 
   965 lemma gcd_diff2: "gcd (n - m) n = gcd m n"
   966   by (subst gcd_neg1[symmetric]) (simp only: minus_diff_eq gcd_diff1)
   967 
   968 lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b"
   969   by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)
   970 
   971 lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b"
   972   by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)
   973 
   974 lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a"
   975   by (fact lcm_neg1)
   976 
   977 lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)"
   978   by (fact lcm_neg2)
   979 
   980 end
   981 
   982 class semiring_Gcd = semiring_gcd + Gcd +
   983   assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
   984     and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A"
   985     and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
   986   assumes dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
   987     and Lcm_least: "(\<And>b. b \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> Lcm A dvd a"
   988     and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A"
   989 begin
   990 
   991 lemma Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
   992   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
   993 
   994 lemma Gcd_Lcm: "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
   995   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
   996 
   997 lemma Gcd_empty [simp]: "Gcd {} = 0"
   998   by (rule dvd_0_left, rule Gcd_greatest) simp
   999 
  1000 lemma Lcm_empty [simp]: "Lcm {} = 1"
  1001   by (auto intro: associated_eqI Lcm_least)
  1002 
  1003 lemma Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)"
  1004 proof -
  1005   have "Gcd (insert a A) dvd gcd a (Gcd A)"
  1006     by (auto intro: Gcd_dvd Gcd_greatest)
  1007   moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
  1008   proof (rule Gcd_greatest)
  1009     fix b
  1010     assume "b \<in> insert a A"
  1011     then show "gcd a (Gcd A) dvd b"
  1012     proof
  1013       assume "b = a"
  1014       then show ?thesis
  1015         by simp
  1016     next
  1017       assume "b \<in> A"
  1018       then have "Gcd A dvd b"
  1019         by (rule Gcd_dvd)
  1020       moreover have "gcd a (Gcd A) dvd Gcd A"
  1021         by simp
  1022       ultimately show ?thesis
  1023         by (blast intro: dvd_trans)
  1024     qed
  1025   qed
  1026   ultimately show ?thesis
  1027     by (auto intro: associated_eqI)
  1028 qed
  1029 
  1030 lemma Lcm_insert [simp]: "Lcm (insert a A) = lcm a (Lcm A)"
  1031 proof (rule sym)
  1032   have "lcm a (Lcm A) dvd Lcm (insert a A)"
  1033     by (auto intro: dvd_Lcm Lcm_least)
  1034   moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
  1035   proof (rule Lcm_least)
  1036     fix b
  1037     assume "b \<in> insert a A"
  1038     then show "b dvd lcm a (Lcm A)"
  1039     proof
  1040       assume "b = a"
  1041       then show ?thesis by simp
  1042     next
  1043       assume "b \<in> A"
  1044       then have "b dvd Lcm A"
  1045         by (rule dvd_Lcm)
  1046       moreover have "Lcm A dvd lcm a (Lcm A)"
  1047         by simp
  1048       ultimately show ?thesis
  1049         by (blast intro: dvd_trans)
  1050     qed
  1051   qed
  1052   ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
  1053     by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
  1054 qed
  1055 
  1056 lemma LcmI:
  1057   assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b"
  1058     and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
  1059     and "normalize b = b"
  1060   shows "b = Lcm A"
  1061   by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least)
  1062 
  1063 lemma Lcm_subset: "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
  1064   by (blast intro: Lcm_least dvd_Lcm)
  1065 
  1066 lemma Lcm_Un: "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
  1067   apply (rule lcmI)
  1068      apply (blast intro: Lcm_subset)
  1069     apply (blast intro: Lcm_subset)
  1070    apply (intro Lcm_least ballI, elim UnE)
  1071     apply (rule dvd_trans, erule dvd_Lcm, assumption)
  1072    apply (rule dvd_trans, erule dvd_Lcm, assumption)
  1073   apply simp
  1074   done
  1075 
  1076 lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
  1077   (is "?P \<longleftrightarrow> ?Q")
  1078 proof
  1079   assume ?P
  1080   show ?Q
  1081   proof
  1082     fix a
  1083     assume "a \<in> A"
  1084     then have "Gcd A dvd a"
  1085       by (rule Gcd_dvd)
  1086     with \<open>?P\<close> have "a = 0"
  1087       by simp
  1088     then show "a \<in> {0}"
  1089       by simp
  1090   qed
  1091 next
  1092   assume ?Q
  1093   have "0 dvd Gcd A"
  1094   proof (rule Gcd_greatest)
  1095     fix a
  1096     assume "a \<in> A"
  1097     with \<open>?Q\<close> have "a = 0"
  1098       by auto
  1099     then show "0 dvd a"
  1100       by simp
  1101   qed
  1102   then show ?P
  1103     by simp
  1104 qed
  1105 
  1106 lemma Lcm_1_iff [simp]: "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)"
  1107   (is "?P \<longleftrightarrow> ?Q")
  1108 proof
  1109   assume ?P
  1110   show ?Q
  1111   proof
  1112     fix a
  1113     assume "a \<in> A"
  1114     then have "a dvd Lcm A"
  1115       by (rule dvd_Lcm)
  1116     with \<open>?P\<close> show "is_unit a"
  1117       by simp
  1118   qed
  1119 next
  1120   assume ?Q
  1121   then have "is_unit (Lcm A)"
  1122     by (blast intro: Lcm_least)
  1123   then have "normalize (Lcm A) = 1"
  1124     by (rule is_unit_normalize)
  1125   then show ?P
  1126     by simp
  1127 qed
  1128 
  1129 lemma unit_factor_Lcm: "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
  1130 proof (cases "Lcm A = 0")
  1131   case True
  1132   then show ?thesis
  1133     by simp
  1134 next
  1135   case False
  1136   with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
  1137     by blast
  1138   with False show ?thesis
  1139     by simp
  1140 qed
  1141 
  1142 lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
  1143   by (simp add: Gcd_Lcm unit_factor_Lcm)
  1144 
  1145 lemma GcdI:
  1146   assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a"
  1147     and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
  1148     and "normalize b = b"
  1149   shows "b = Gcd A"
  1150   by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest)
  1151 
  1152 lemma Gcd_eq_1_I:
  1153   assumes "is_unit a" and "a \<in> A"
  1154   shows "Gcd A = 1"
  1155 proof -
  1156   from assms have "is_unit (Gcd A)"
  1157     by (blast intro: Gcd_dvd dvd_unit_imp_unit)
  1158   then have "normalize (Gcd A) = 1"
  1159     by (rule is_unit_normalize)
  1160   then show ?thesis
  1161     by simp
  1162 qed
  1163 
  1164 lemma Lcm_eq_0_I:
  1165   assumes "0 \<in> A"
  1166   shows "Lcm A = 0"
  1167 proof -
  1168   from assms have "0 dvd Lcm A"
  1169     by (rule dvd_Lcm)
  1170   then show ?thesis
  1171     by simp
  1172 qed
  1173 
  1174 lemma Gcd_UNIV [simp]: "Gcd UNIV = 1"
  1175   using dvd_refl by (rule Gcd_eq_1_I) simp
  1176 
  1177 lemma Lcm_UNIV [simp]: "Lcm UNIV = 0"
  1178   by (rule Lcm_eq_0_I) simp
  1179 
  1180 lemma Lcm_0_iff:
  1181   assumes "finite A"
  1182   shows "Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
  1183 proof (cases "A = {}")
  1184   case True
  1185   then show ?thesis by simp
  1186 next
  1187   case False
  1188   with assms show ?thesis
  1189     by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff)
  1190 qed
  1191 
  1192 lemma Gcd_finite:
  1193   assumes "finite A"
  1194   shows "Gcd A = Finite_Set.fold gcd 0 A"
  1195   by (induct rule: finite.induct[OF \<open>finite A\<close>])
  1196     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
  1197 
  1198 lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as"
  1199   by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd]
  1200       foldl_conv_fold gcd.commute)
  1201 
  1202 lemma Lcm_finite:
  1203   assumes "finite A"
  1204   shows "Lcm A = Finite_Set.fold lcm 1 A"
  1205   by (induct rule: finite.induct[OF \<open>finite A\<close>])
  1206     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
  1207 
  1208 lemma Lcm_set [code_unfold]: "Lcm (set as) = foldl lcm 1 as"
  1209   by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm]
  1210       foldl_conv_fold lcm.commute)
  1211 
  1212 lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
  1213 proof -
  1214   have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
  1215   proof -
  1216     from that obtain B where "A = insert a B"
  1217       by blast
  1218     moreover have "gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
  1219       by (rule gcd_dvd1)
  1220     ultimately show "Gcd (normalize ` A) dvd a"
  1221       by simp
  1222   qed
  1223   then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
  1224     by (auto intro!: Gcd_greatest intro: Gcd_dvd)
  1225   then show ?thesis
  1226     by (auto intro: associated_eqI)
  1227 qed
  1228 
  1229 lemma Gcd_eqI:
  1230   assumes "normalize a = a"
  1231   assumes "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
  1232     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> c dvd b) \<Longrightarrow> c dvd a"
  1233   shows "Gcd A = a"
  1234   using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd)
  1235 
  1236 lemma dvd_GcdD: "x dvd Gcd A \<Longrightarrow> y \<in> A \<Longrightarrow> x dvd y"
  1237   using Gcd_dvd dvd_trans by blast
  1238 
  1239 lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
  1240   by (blast dest: dvd_GcdD intro: Gcd_greatest)
  1241 
  1242 lemma Gcd_mult: "Gcd (op * c ` A) = normalize c * Gcd A"
  1243 proof (cases "c = 0")
  1244   case True
  1245   then show ?thesis by auto
  1246 next
  1247   case [simp]: False
  1248   have "Gcd (op * c ` A) div c dvd Gcd A"
  1249     by (intro Gcd_greatest, subst div_dvd_iff_mult)
  1250        (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
  1251   then have "Gcd (op * c ` A) dvd c * Gcd A"
  1252     by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
  1253   also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
  1254     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
  1255   also have "Gcd (op * c ` A) dvd \<dots> \<longleftrightarrow> Gcd (op * c ` A) dvd normalize c * Gcd A"
  1256     by (simp add: dvd_mult_unit_iff)
  1257   finally have "Gcd (op * c ` A) dvd normalize c * Gcd A" .
  1258   moreover have "normalize c * Gcd A dvd Gcd (op * c ` A)"
  1259     by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
  1260   ultimately have "normalize (Gcd (op * c ` A)) = normalize (normalize c * Gcd A)"
  1261     by (rule associatedI)
  1262   then show ?thesis
  1263     by (simp add: normalize_mult)
  1264 qed
  1265 
  1266 lemma Lcm_eqI:
  1267   assumes "normalize a = a"
  1268     and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
  1269     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> b dvd c) \<Longrightarrow> a dvd c"
  1270   shows "Lcm A = a"
  1271   using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
  1272 
  1273 lemma Lcm_dvdD: "Lcm A dvd x \<Longrightarrow> y \<in> A \<Longrightarrow> y dvd x"
  1274   using dvd_Lcm dvd_trans by blast
  1275 
  1276 lemma Lcm_dvd_iff: "Lcm A dvd x \<longleftrightarrow> (\<forall>y\<in>A. y dvd x)"
  1277   by (blast dest: Lcm_dvdD intro: Lcm_least)
  1278 
  1279 lemma Lcm_mult:
  1280   assumes "A \<noteq> {}"
  1281   shows "Lcm (op * c ` A) = normalize c * Lcm A"
  1282 proof (cases "c = 0")
  1283   case True
  1284   with assms have "op * c ` A = {0}"
  1285     by auto
  1286   with True show ?thesis by auto
  1287 next
  1288   case [simp]: False
  1289   from assms obtain x where x: "x \<in> A"
  1290     by blast
  1291   have "c dvd c * x"
  1292     by simp
  1293   also from x have "c * x dvd Lcm (op * c ` A)"
  1294     by (intro dvd_Lcm) auto
  1295   finally have dvd: "c dvd Lcm (op * c ` A)" .
  1296 
  1297   have "Lcm A dvd Lcm (op * c ` A) div c"
  1298     by (intro Lcm_least dvd_mult_imp_div)
  1299       (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
  1300   then have "c * Lcm A dvd Lcm (op * c ` A)"
  1301     by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
  1302   also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
  1303     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
  1304   also have "\<dots> dvd Lcm (op * c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (op * c ` A)"
  1305     by (simp add: mult_unit_dvd_iff)
  1306   finally have "normalize c * Lcm A dvd Lcm (op * c ` A)" .
  1307   moreover have "Lcm (op * c ` A) dvd normalize c * Lcm A"
  1308     by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
  1309   ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (op * c ` A))"
  1310     by (rule associatedI)
  1311   then show ?thesis
  1312     by (simp add: normalize_mult)
  1313 qed
  1314 
  1315 lemma Lcm_no_units: "Lcm A = Lcm (A - {a. is_unit a})"
  1316 proof -
  1317   have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A"
  1318     by blast
  1319   then have "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
  1320     by (simp add: Lcm_Un [symmetric])
  1321   also have "Lcm {a\<in>A. is_unit a} = 1"
  1322     by simp
  1323   finally show ?thesis
  1324     by simp
  1325 qed
  1326 
  1327 lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> (\<nexists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
  1328   by (metis Lcm_least dvd_0_left dvd_Lcm)
  1329 
  1330 lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not> a dvd m)) \<Longrightarrow> Lcm A = 0"
  1331   by (auto simp: Lcm_0_iff')
  1332 
  1333 lemma Lcm_singleton [simp]: "Lcm {a} = normalize a"
  1334   by simp
  1335 
  1336 lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
  1337   by simp
  1338 
  1339 lemma Lcm_coprime:
  1340   assumes "finite A"
  1341     and "A \<noteq> {}"
  1342     and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
  1343   shows "Lcm A = normalize (\<Prod>A)"
  1344   using assms
  1345 proof (induct rule: finite_ne_induct)
  1346   case singleton
  1347   then show ?case by simp
  1348 next
  1349   case (insert a A)
  1350   have "Lcm (insert a A) = lcm a (Lcm A)"
  1351     by simp
  1352   also from insert have "Lcm A = normalize (\<Prod>A)"
  1353     by blast
  1354   also have "lcm a \<dots> = lcm a (\<Prod>A)"
  1355     by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
  1356   also from insert have "gcd a (\<Prod>A) = 1"
  1357     by (subst gcd.commute, intro setprod_coprime) auto
  1358   with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
  1359     by (simp add: lcm_coprime)
  1360   finally show ?case .
  1361 qed
  1362 
  1363 lemma Lcm_coprime':
  1364   "card A \<noteq> 0 \<Longrightarrow>
  1365     (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) \<Longrightarrow>
  1366     Lcm A = normalize (\<Prod>A)"
  1367   by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
  1368 
  1369 lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1"
  1370   by (auto intro!: Gcd_eq_1_I)
  1371 
  1372 lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
  1373   by simp
  1374 
  1375 lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
  1376   by simp
  1377 
  1378 
  1379 definition pairwise_coprime
  1380   where "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
  1381 
  1382 lemma pairwise_coprimeI [intro?]:
  1383   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
  1384   by (simp add: pairwise_coprime_def)
  1385 
  1386 lemma pairwise_coprimeD:
  1387   "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
  1388   by (simp add: pairwise_coprime_def)
  1389 
  1390 lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
  1391   by (force simp: pairwise_coprime_def)
  1392 
  1393 end
  1394 
  1395 
  1396 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
  1397 
  1398 instantiation nat :: gcd
  1399 begin
  1400 
  1401 fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  1402   where "gcd_nat x y = (if y = 0 then x else gcd y (x mod y))"
  1403 
  1404 definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  1405   where "lcm_nat x y = x * y div (gcd x y)"
  1406 
  1407 instance ..
  1408 
  1409 end
  1410 
  1411 instantiation int :: gcd
  1412 begin
  1413 
  1414 definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
  1415   where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
  1416 
  1417 definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
  1418   where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
  1419 
  1420 instance ..
  1421 
  1422 end
  1423 
  1424 text \<open>Transfer setup\<close>
  1425 
  1426 lemma transfer_nat_int_gcd:
  1427   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
  1428   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
  1429   for x y :: int
  1430   unfolding gcd_int_def lcm_int_def by auto
  1431 
  1432 lemma transfer_nat_int_gcd_closures:
  1433   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
  1434   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
  1435   for x y :: int
  1436   by (auto simp add: gcd_int_def lcm_int_def)
  1437 
  1438 declare transfer_morphism_nat_int
  1439   [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
  1440 
  1441 lemma transfer_int_nat_gcd:
  1442   "gcd (int x) (int y) = int (gcd x y)"
  1443   "lcm (int x) (int y) = int (lcm x y)"
  1444   by (auto simp: gcd_int_def lcm_int_def)
  1445 
  1446 lemma transfer_int_nat_gcd_closures:
  1447   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
  1448   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
  1449   by (auto simp: gcd_int_def lcm_int_def)
  1450 
  1451 declare transfer_morphism_int_nat
  1452   [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
  1453 
  1454 lemma gcd_nat_induct:
  1455   fixes m n :: nat
  1456   assumes "\<And>m. P m 0"
  1457     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
  1458   shows "P m n"
  1459   apply (rule gcd_nat.induct)
  1460   apply (case_tac "y = 0")
  1461   using assms
  1462    apply simp_all
  1463   done
  1464 
  1465 
  1466 text \<open>Specific to \<open>int\<close>.\<close>
  1467 
  1468 lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
  1469   by (simp add: gcd_int_def)
  1470 
  1471 lemma lcm_eq_int_iff: "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
  1472   by (simp add: lcm_int_def)
  1473 
  1474 lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
  1475   for x y :: int
  1476   by (simp add: gcd_int_def)
  1477 
  1478 lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y"
  1479   for x y :: int
  1480   by (simp add: gcd_int_def)
  1481 
  1482 lemma abs_gcd_int [simp]: "\<bar>gcd x y\<bar> = gcd x y"
  1483   for x y :: int
  1484   by (simp add: gcd_int_def)
  1485 
  1486 lemma gcd_abs_int: "gcd x y = gcd \<bar>x\<bar> \<bar>y\<bar>"
  1487   for x y :: int
  1488   by (simp add: gcd_int_def)
  1489 
  1490 lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> y = gcd x y"
  1491   for x y :: int
  1492   by (metis abs_idempotent gcd_abs_int)
  1493 
  1494 lemma gcd_abs2_int [simp]: "gcd x \<bar>y\<bar> = gcd x y"
  1495   for x y :: int
  1496   by (metis abs_idempotent gcd_abs_int)
  1497 
  1498 lemma gcd_cases_int:
  1499   fixes x y :: int
  1500   assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd x y)"
  1501     and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd x (- y))"
  1502     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd (- x) y)"
  1503     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd (- x) (- y))"
  1504   shows "P (gcd x y)"
  1505   using assms by auto arith
  1506 
  1507 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
  1508   for x y :: int
  1509   by (simp add: gcd_int_def)
  1510 
  1511 lemma lcm_neg1_int: "lcm (- x) y = lcm x y"
  1512   for x y :: int
  1513   by (simp add: lcm_int_def)
  1514 
  1515 lemma lcm_neg2_int: "lcm x (- y) = lcm x y"
  1516   for x y :: int
  1517   by (simp add: lcm_int_def)
  1518 
  1519 lemma lcm_abs_int: "lcm x y = lcm \<bar>x\<bar> \<bar>y\<bar>"
  1520   for x y :: int
  1521   by (simp add: lcm_int_def)
  1522 
  1523 lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
  1524   for i j :: int
  1525   by (simp add:lcm_int_def)
  1526 
  1527 lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> y = lcm x y"
  1528   for x y :: int
  1529   by (metis abs_idempotent lcm_int_def)
  1530 
  1531 lemma lcm_abs2_int [simp]: "lcm x \<bar>y\<bar> = lcm x y"
  1532   for x y :: int
  1533   by (metis abs_idempotent lcm_int_def)
  1534 
  1535 lemma lcm_cases_int:
  1536   fixes x y :: int
  1537   assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm x y)"
  1538     and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm x (- y))"
  1539     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm (- x) y)"
  1540     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm (- x) (- y))"
  1541   shows "P (lcm x y)"
  1542   using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
  1543 
  1544 lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
  1545   for x y :: int
  1546   by (simp add: lcm_int_def)
  1547 
  1548 lemma gcd_0_nat: "gcd x 0 = x"
  1549   for x :: nat
  1550   by simp
  1551 
  1552 lemma gcd_0_int [simp]: "gcd x 0 = \<bar>x\<bar>"
  1553   for x :: int
  1554   by (auto simp: gcd_int_def)
  1555 
  1556 lemma gcd_0_left_nat: "gcd 0 x = x"
  1557   for x :: nat
  1558   by simp
  1559 
  1560 lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>"
  1561   for x :: int
  1562   by (auto simp:gcd_int_def)
  1563 
  1564 lemma gcd_red_nat: "gcd x y = gcd y (x mod y)"
  1565   for x y :: nat
  1566   by (cases "y = 0") auto
  1567 
  1568 
  1569 text \<open>Weaker, but useful for the simplifier.\<close>
  1570 
  1571 lemma gcd_non_0_nat: "y \<noteq> 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
  1572   for x y :: nat
  1573   by simp
  1574 
  1575 lemma gcd_1_nat [simp]: "gcd m 1 = 1"
  1576   for m :: nat
  1577   by simp
  1578 
  1579 lemma gcd_Suc_0 [simp]: "gcd m (Suc 0) = Suc 0"
  1580   for m :: nat
  1581   by simp
  1582 
  1583 lemma gcd_1_int [simp]: "gcd m 1 = 1"
  1584   for m :: int
  1585   by (simp add: gcd_int_def)
  1586 
  1587 lemma gcd_idem_nat: "gcd x x = x"
  1588   for x :: nat
  1589   by simp
  1590 
  1591 lemma gcd_idem_int: "gcd x x = \<bar>x\<bar>"
  1592   for x :: int
  1593   by (auto simp add: gcd_int_def)
  1594 
  1595 declare gcd_nat.simps [simp del]
  1596 
  1597 text \<open>
  1598   \<^medskip> @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.
  1599   The conjunctions don't seem provable separately.
  1600 \<close>
  1601 
  1602 instance nat :: semiring_gcd
  1603 proof
  1604   fix m n :: nat
  1605   show "gcd m n dvd m" and "gcd m n dvd n"
  1606   proof (induct m n rule: gcd_nat_induct)
  1607     fix m n :: nat
  1608     assume "gcd n (m mod n) dvd m mod n"
  1609       and "gcd n (m mod n) dvd n"
  1610     then have "gcd n (m mod n) dvd m"
  1611       by (rule dvd_mod_imp_dvd)
  1612     moreover assume "0 < n"
  1613     ultimately show "gcd m n dvd m"
  1614       by (simp add: gcd_non_0_nat)
  1615   qed (simp_all add: gcd_0_nat gcd_non_0_nat)
  1616 next
  1617   fix m n k :: nat
  1618   assume "k dvd m" and "k dvd n"
  1619   then show "k dvd gcd m n"
  1620     by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
  1621 qed (simp_all add: lcm_nat_def)
  1622 
  1623 instance int :: ring_gcd
  1624   by standard
  1625     (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def
  1626       zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
  1627 
  1628 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a"
  1629   for a b :: nat
  1630   by (rule dvd_imp_le) auto
  1631 
  1632 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd a b \<le> b"
  1633   for a b :: nat
  1634   by (rule dvd_imp_le) auto
  1635 
  1636 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd a b \<le> a"
  1637   for a b :: int
  1638   by (rule zdvd_imp_le) auto
  1639 
  1640 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd a b \<le> b"
  1641   for a b :: int
  1642   by (rule zdvd_imp_le) auto
  1643 
  1644 lemma gcd_pos_nat [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
  1645   for m n :: nat
  1646   using gcd_eq_0_iff [of m n] by arith
  1647 
  1648 lemma gcd_pos_int [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
  1649   for m n :: int
  1650   using gcd_eq_0_iff [of m n] gcd_ge_0_int [of m n] by arith
  1651 
  1652 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"
  1653   for d a :: nat
  1654   apply auto
  1655   apply (rule dvd_antisym)
  1656    apply (erule (1) gcd_greatest)
  1657   apply auto
  1658   done
  1659 
  1660 lemma gcd_unique_int:
  1661   "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"
  1662   for d a :: int
  1663   apply (cases "d = 0")
  1664    apply simp
  1665   apply (rule iffI)
  1666    apply (rule zdvd_antisym_nonneg)
  1667       apply (auto intro: gcd_greatest)
  1668   done
  1669 
  1670 interpretation gcd_nat:
  1671   semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
  1672   by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
  1673 
  1674 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
  1675   for x y :: int
  1676   by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
  1677 
  1678 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>"
  1679   for x y :: int
  1680   by (metis gcd_proj1_if_dvd_int gcd.commute)
  1681 
  1682 
  1683 text \<open>\<^medskip> Multiplication laws.\<close>
  1684 
  1685 lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
  1686   for k m n :: nat
  1687   \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
  1688   apply (induct m n rule: gcd_nat_induct)
  1689    apply simp
  1690   apply (cases "k = 0")
  1691    apply (simp_all add: gcd_non_0_nat)
  1692   done
  1693 
  1694 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
  1695   for k m n :: int
  1696   apply (subst (1 2) gcd_abs_int)
  1697   apply (subst (1 2) abs_mult)
  1698   apply (rule gcd_mult_distrib_nat [transferred])
  1699     apply auto
  1700   done
  1701 
  1702 lemma coprime_crossproduct_nat:
  1703   fixes a b c d :: nat
  1704   assumes "coprime a d" and "coprime b c"
  1705   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
  1706   using assms coprime_crossproduct [of a d b c] by simp
  1707 
  1708 lemma coprime_crossproduct_int:
  1709   fixes a b c d :: int
  1710   assumes "coprime a d" and "coprime b c"
  1711   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>"
  1712   using assms coprime_crossproduct [of a d b c] by simp
  1713 
  1714 
  1715 text \<open>\medskip Addition laws.\<close>
  1716 
  1717 (* TODO: add the other variations? *)
  1718 
  1719 lemma gcd_diff1_nat: "m \<ge> n \<Longrightarrow> gcd (m - n) n = gcd m n"
  1720   for m n :: nat
  1721   by (subst gcd_add1 [symmetric]) auto
  1722 
  1723 lemma gcd_diff2_nat: "n \<ge> m \<Longrightarrow> gcd (n - m) n = gcd m n"
  1724   for m n :: nat
  1725   apply (subst gcd.commute)
  1726   apply (subst gcd_diff1_nat [symmetric])
  1727    apply auto
  1728   apply (subst gcd.commute)
  1729   apply (subst gcd_diff1_nat)
  1730    apply assumption
  1731   apply (rule gcd.commute)
  1732   done
  1733 
  1734 lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
  1735   for x y :: int
  1736   apply (frule_tac b = y and a = x in pos_mod_sign)
  1737   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
  1738   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
  1739   apply (frule_tac a = x in pos_mod_bound)
  1740   apply (subst (1 2) gcd.commute)
  1741   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
  1742   done
  1743 
  1744 lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
  1745   for x y :: int
  1746   apply (cases "y = 0")
  1747    apply force
  1748   apply (cases "y > 0")
  1749    apply (subst gcd_non_0_int, auto)
  1750   apply (insert gcd_non_0_int [of "- y" "- x"])
  1751   apply auto
  1752   done
  1753 
  1754 (* TODO: differences, and all variations of addition rules
  1755     as simplification rules for nat and int *)
  1756 
  1757 (* TODO: add the three variations of these, and for ints? *)
  1758 
  1759 lemma finite_divisors_nat [simp]: (* FIXME move *)
  1760   fixes m :: nat
  1761   assumes "m > 0"
  1762   shows "finite {d. d dvd m}"
  1763 proof-
  1764   from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}"
  1765     by (auto dest: dvd_imp_le)
  1766   then show ?thesis
  1767     using finite_Collect_le_nat by (rule finite_subset)
  1768 qed
  1769 
  1770 lemma finite_divisors_int [simp]:
  1771   fixes i :: int
  1772   assumes "i \<noteq> 0"
  1773   shows "finite {d. d dvd i}"
  1774 proof -
  1775   have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}"
  1776     by (auto simp: abs_if)
  1777   then have "finite {d. \<bar>d\<bar> \<le> \<bar>i\<bar>}"
  1778     by simp
  1779   from finite_subset [OF _ this] show ?thesis
  1780     using assms by (simp add: dvd_imp_le_int subset_iff)
  1781 qed
  1782 
  1783 lemma Max_divisors_self_nat [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::nat. d dvd n} = n"
  1784   apply (rule antisym)
  1785    apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
  1786   apply simp
  1787   done
  1788 
  1789 lemma Max_divisors_self_int [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::int. d dvd n} = \<bar>n\<bar>"
  1790   apply (rule antisym)
  1791    apply (rule Max_le_iff [THEN iffD2])
  1792      apply (auto intro: abs_le_D1 dvd_imp_le_int)
  1793   done
  1794 
  1795 lemma gcd_is_Max_divisors_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
  1796   for m n :: nat
  1797   apply (rule Max_eqI[THEN sym])
  1798     apply (metis finite_Collect_conjI finite_divisors_nat)
  1799    apply simp
  1800    apply (metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
  1801   apply simp
  1802   done
  1803 
  1804 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}"
  1805   for m n :: int
  1806   apply (rule Max_eqI[THEN sym])
  1807     apply (metis finite_Collect_conjI finite_divisors_int)
  1808    apply simp
  1809    apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
  1810   apply simp
  1811   done
  1812 
  1813 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>"
  1814   for k l :: int
  1815   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
  1816 
  1817 
  1818 subsection \<open>Coprimality\<close>
  1819 
  1820 lemma coprime_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1821   for a b :: nat
  1822   using coprime [of a b] by simp
  1823 
  1824 lemma coprime_Suc_0_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
  1825   for a b :: nat
  1826   using coprime_nat by simp
  1827 
  1828 lemma coprime_int: "coprime a b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1829   for a b :: int
  1830   using gcd_unique_int [of 1 a b]
  1831   apply clarsimp
  1832   apply (erule subst)
  1833   apply (rule iffI)
  1834    apply force
  1835   using abs_dvd_iff abs_ge_zero apply blast
  1836   done
  1837 
  1838 lemma pow_divides_eq_nat [simp]: "n > 0 \<Longrightarrow> a^n dvd b^n \<longleftrightarrow> a dvd b"
  1839   for a b n :: nat
  1840   using pow_divs_eq[of n] by simp
  1841 
  1842 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
  1843   using coprime_plus_one[of n] by simp
  1844 
  1845 lemma coprime_minus_one_nat: "n \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
  1846   for n :: nat
  1847   using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
  1848 
  1849 lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
  1850   for a b :: nat
  1851   by (metis gcd_greatest_iff nat_dvd_1_iff_1)
  1852 
  1853 lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
  1854   for a b :: int
  1855   using gcd_greatest_iff [of x a b] by auto
  1856 
  1857 lemma invertible_coprime_nat: "x * y mod m = 1 \<Longrightarrow> coprime x m"
  1858   for m x y :: nat
  1859   by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
  1860 
  1861 lemma invertible_coprime_int: "x * y mod m = 1 \<Longrightarrow> coprime x m"
  1862   for m x y :: int
  1863   by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
  1864 
  1865 
  1866 subsection \<open>Bezout's theorem\<close>
  1867 
  1868 text \<open>
  1869   Function \<open>bezw\<close> returns a pair of witnesses to Bezout's theorem --
  1870   see the theorems that follow the definition.
  1871 \<close>
  1872 
  1873 fun bezw :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1874   where "bezw x y =
  1875     (if y = 0 then (1, 0)
  1876      else
  1877       (snd (bezw y (x mod y)),
  1878        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1879 
  1880 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)"
  1881   by simp
  1882 
  1883 lemma bezw_non_0:
  1884   "y > 0 \<Longrightarrow> bezw x y =
  1885     (snd (bezw y (x mod y)), fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1886   by simp
  1887 
  1888 declare bezw.simps [simp del]
  1889 
  1890 lemma bezw_aux: "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1891 proof (induct x y rule: gcd_nat_induct)
  1892   fix m :: nat
  1893   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1894     by auto
  1895 next
  1896   fix m n :: nat
  1897   assume ngt0: "n > 0"
  1898     and ih: "fst (bezw n (m mod n)) * int n + snd (bezw n (m mod n)) * int (m mod n) =
  1899       int (gcd n (m mod n))"
  1900   then show "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1901     apply (simp add: bezw_non_0 gcd_non_0_nat)
  1902     apply (erule subst)
  1903     apply (simp add: field_simps)
  1904     apply (subst mod_div_equality [of m n, symmetric])
  1905       (* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *)
  1906     apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
  1907     done
  1908 qed
  1909 
  1910 lemma bezout_int: "\<exists>u v. u * x + v * y = gcd x y"
  1911   for x y :: int
  1912 proof -
  1913   have aux: "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> \<exists>u v. u * x + v * y = gcd x y" for x y :: int
  1914     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1915     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1916     apply (unfold gcd_int_def)
  1917     apply simp
  1918     apply (subst bezw_aux [symmetric])
  1919     apply auto
  1920     done
  1921   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"
  1922     by atomize_elim auto
  1923   then show ?thesis
  1924   proof cases
  1925     case 1
  1926     then show ?thesis by (rule aux)
  1927   next
  1928     case 2
  1929     then show ?thesis
  1930       apply -
  1931       apply (insert aux [of x "-y"])
  1932       apply auto
  1933       apply (rule_tac x = u in exI)
  1934       apply (rule_tac x = "-v" in exI)
  1935       apply (subst gcd_neg2_int [symmetric])
  1936       apply auto
  1937       done
  1938   next
  1939     case 3
  1940     then show ?thesis
  1941       apply -
  1942       apply (insert aux [of "-x" y])
  1943       apply auto
  1944       apply (rule_tac x = "-u" in exI)
  1945       apply (rule_tac x = v in exI)
  1946       apply (subst gcd_neg1_int [symmetric])
  1947       apply auto
  1948       done
  1949   next
  1950     case 4
  1951     then show ?thesis
  1952       apply -
  1953       apply (insert aux [of "-x" "-y"])
  1954       apply auto
  1955       apply (rule_tac x = "-u" in exI)
  1956       apply (rule_tac x = "-v" in exI)
  1957       apply (subst gcd_neg1_int [symmetric])
  1958       apply (subst gcd_neg2_int [symmetric])
  1959       apply auto
  1960       done
  1961   qed
  1962 qed
  1963 
  1964 
  1965 text \<open>Versions of Bezout for \<open>nat\<close>, by Amine Chaieb.\<close>
  1966 
  1967 lemma ind_euclid:
  1968   fixes P :: "nat \<Rightarrow> nat \<Rightarrow> bool"
  1969   assumes c: " \<forall>a b. P a b \<longleftrightarrow> P b a"
  1970     and z: "\<forall>a. P a 0"
  1971     and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1972   shows "P a b"
  1973 proof (induct "a + b" arbitrary: a b rule: less_induct)
  1974   case less
  1975   consider (eq) "a = b" | (lt) "a < b" "a + b - a < a + b" | "b = 0" | "b + a - b < a + b"
  1976     by arith
  1977   show ?case
  1978   proof (cases a b rule: linorder_cases)
  1979     case equal
  1980     with add [rule_format, OF z [rule_format, of a]] show ?thesis by simp
  1981   next
  1982     case lt: less
  1983     then consider "a = 0" | "a + b - a < a + b" by arith
  1984     then show ?thesis
  1985     proof cases
  1986       case 1
  1987       with z c show ?thesis by blast
  1988     next
  1989       case 2
  1990       also have *: "a + b - a = a + (b - a)" using lt by arith
  1991       finally have "a + (b - a) < a + b" .
  1992       then have "P a (a + (b - a))" by (rule add [rule_format, OF less])
  1993       then show ?thesis by (simp add: *[symmetric])
  1994     qed
  1995   next
  1996     case gt: greater
  1997     then consider "b = 0" | "b + a - b < a + b" by arith
  1998     then show ?thesis
  1999     proof cases
  2000       case 1
  2001       with z c show ?thesis by blast
  2002     next
  2003       case 2
  2004       also have *: "b + a - b = b + (a - b)" using gt by arith
  2005       finally have "b + (a - b) < a + b" .
  2006       then have "P b (b + (a - b))" by (rule add [rule_format, OF less])
  2007       then have "P b a" by (simp add: *[symmetric])
  2008       with c show ?thesis by blast
  2009     qed
  2010   qed
  2011 qed
  2012 
  2013 lemma bezout_lemma_nat:
  2014   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  2015     (a * x = b * y + d \<or> b * x = a * y + d)"
  2016   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  2017     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  2018   using ex
  2019   apply clarsimp
  2020   apply (rule_tac x="d" in exI)
  2021   apply simp
  2022   apply (case_tac "a * x = b * y + d")
  2023    apply simp_all
  2024    apply (rule_tac x="x + y" in exI)
  2025    apply (rule_tac x="y" in exI)
  2026    apply algebra
  2027   apply (rule_tac x="x" in exI)
  2028   apply (rule_tac x="x + y" in exI)
  2029   apply algebra
  2030   done
  2031 
  2032 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  2033     (a * x = b * y + d \<or> b * x = a * y + d)"
  2034   apply (induct a b rule: ind_euclid)
  2035     apply blast
  2036    apply clarify
  2037    apply (rule_tac x="a" in exI)
  2038    apply simp
  2039   apply clarsimp
  2040   apply (rule_tac x="d" in exI)
  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 bezout1_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   using bezout_add_nat[of a b]
  2054   apply clarsimp
  2055   apply (rule_tac x="d" in exI)
  2056   apply simp
  2057   apply (rule_tac x="x" in exI)
  2058   apply (rule_tac x="y" in exI)
  2059   apply auto
  2060   done
  2061 
  2062 lemma bezout_add_strong_nat:
  2063   fixes a b :: nat
  2064   assumes a: "a \<noteq> 0"
  2065   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  2066 proof -
  2067   consider d x y where "d dvd a" "d dvd b" "a * x = b * y + d"
  2068     | d x y where "d dvd a" "d dvd b" "b * x = a * y + d"
  2069     using bezout_add_nat [of a b] by blast
  2070   then show ?thesis
  2071   proof cases
  2072     case 1
  2073     then show ?thesis by blast
  2074   next
  2075     case H: 2
  2076     show ?thesis
  2077     proof (cases "b = 0")
  2078       case True
  2079       with H show ?thesis by simp
  2080     next
  2081       case False
  2082       then have bp: "b > 0" by simp
  2083       with dvd_imp_le [OF H(2)] consider "d = b" | "d < b"
  2084         by atomize_elim auto
  2085       then show ?thesis
  2086       proof cases
  2087         case 1
  2088         with a H show ?thesis
  2089           apply simp
  2090           apply (rule exI[where x = b])
  2091           apply simp
  2092           apply (rule exI[where x = b])
  2093           apply (rule exI[where x = "a - 1"])
  2094           apply (simp add: diff_mult_distrib2)
  2095           done
  2096       next
  2097         case 2
  2098         show ?thesis
  2099         proof (cases "x = 0")
  2100           case True
  2101           with a H show ?thesis by simp
  2102         next
  2103           case x0: False
  2104           then have xp: "x > 0" by simp
  2105           from \<open>d < b\<close> have "d \<le> b - 1" by simp
  2106           then have "d * b \<le> b * (b - 1)" by simp
  2107           with xp mult_mono[of "1" "x" "d * b" "b * (b - 1)"]
  2108           have dble: "d * b \<le> x * b * (b - 1)" using bp by simp
  2109           from H(3) have "d + (b - 1) * (b * x) = d + (b - 1) * (a * y + d)"
  2110             by simp
  2111           then have "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  2112             by (simp only: mult.assoc distrib_left)
  2113           then have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x * b * (b - 1)"
  2114             by algebra
  2115           then have "a * ((b - 1) * y) = d + x * b * (b - 1) - d * b"
  2116             using bp by simp
  2117           then have "a * ((b - 1) * y) = d + (x * b * (b - 1) - d * b)"
  2118             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  2119           then have "a * ((b - 1) * y) = b * (x * (b - 1) - d) + d"
  2120             by (simp only: diff_mult_distrib2 ac_simps)
  2121           with H(1,2) show ?thesis
  2122             apply -
  2123             apply (rule exI [where x = d])
  2124             apply simp
  2125             apply (rule exI [where x = "(b - 1) * y"])
  2126             apply (rule exI [where x = "x * (b - 1) - d"])
  2127             apply simp
  2128             done
  2129         qed
  2130       qed
  2131     qed
  2132   qed
  2133 qed
  2134 
  2135 lemma bezout_nat:
  2136   fixes a :: nat
  2137   assumes a: "a \<noteq> 0"
  2138   shows "\<exists>x y. a * x = b * y + gcd a b"
  2139 proof -
  2140   obtain d x y where d: "d dvd a" "d dvd b" and eq: "a * x = b * y + d"
  2141     using bezout_add_strong_nat [OF a, of b] by blast
  2142   from d have "d dvd gcd a b"
  2143     by simp
  2144   then obtain k where k: "gcd a b = d * k"
  2145     unfolding dvd_def by blast
  2146   from eq have "a * x * k = (b * y + d) * k"
  2147     by auto
  2148   then have "a * (x * k) = b * (y * k) + gcd a b"
  2149     by (algebra add: k)
  2150   then show ?thesis
  2151     by blast
  2152 qed
  2153 
  2154 
  2155 subsection \<open>LCM properties on @{typ nat} and @{typ int}\<close>
  2156 
  2157 lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  2158   for a b :: int
  2159   by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
  2160 
  2161 lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
  2162   for m n :: nat
  2163   unfolding lcm_nat_def
  2164   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
  2165 
  2166 lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
  2167   for m n :: int
  2168   unfolding lcm_int_def gcd_int_def
  2169   apply (subst of_nat_mult [symmetric])
  2170   apply (subst prod_gcd_lcm_nat [symmetric])
  2171   apply (subst nat_abs_mult_distrib [symmetric])
  2172   apply (simp add: abs_mult)
  2173   done
  2174 
  2175 lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
  2176   for m n :: nat
  2177   by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  2178 
  2179 lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
  2180   for m n :: int
  2181   apply (subst lcm_abs_int)
  2182   apply (rule lcm_pos_nat [transferred])
  2183      apply auto
  2184   done
  2185 
  2186 lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
  2187   for m n :: nat
  2188   by (cases m) auto
  2189 
  2190 lemma lcm_unique_nat:
  2191   "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"
  2192   for a b d :: nat
  2193   by (auto intro: dvd_antisym lcm_least)
  2194 
  2195 lemma lcm_unique_int:
  2196   "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"
  2197   for a b d :: int
  2198   using lcm_least zdvd_antisym_nonneg by auto
  2199 
  2200 lemma lcm_proj2_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm x y = y"
  2201   for x y :: nat
  2202   apply (rule sym)
  2203   apply (subst lcm_unique_nat [symmetric])
  2204   apply auto
  2205   done
  2206 
  2207 lemma lcm_proj2_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
  2208   for x y :: int
  2209   apply (rule sym)
  2210   apply (subst lcm_unique_int [symmetric])
  2211   apply auto
  2212   done
  2213 
  2214 lemma lcm_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm y x = y"
  2215   for x y :: nat
  2216   by (subst lcm.commute) (erule lcm_proj2_if_dvd_nat)
  2217 
  2218 lemma lcm_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
  2219   for x y :: int
  2220   by (subst lcm.commute) (erule lcm_proj2_if_dvd_int)
  2221 
  2222 lemma lcm_proj1_iff_nat [simp]: "lcm m n = m \<longleftrightarrow> n dvd m"
  2223   for m n :: nat
  2224   by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  2225 
  2226 lemma lcm_proj2_iff_nat [simp]: "lcm m n = n \<longleftrightarrow> m dvd n"
  2227   for m n :: nat
  2228   by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  2229 
  2230 lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m\<bar> \<longleftrightarrow> n dvd m"
  2231   for m n :: int
  2232   by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  2233 
  2234 lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n\<bar> \<longleftrightarrow> m dvd n"
  2235   for m n :: int
  2236   by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  2237 
  2238 lemma lcm_1_iff_nat [simp]: "lcm m n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
  2239   for m n :: nat
  2240   using lcm_eq_1_iff [of m n] by simp
  2241 
  2242 lemma lcm_1_iff_int [simp]: "lcm m n = 1 \<longleftrightarrow> (m = 1 \<or> m = -1) \<and> (n = 1 \<or> n = -1)"
  2243   for m n :: int
  2244   by auto
  2245 
  2246 
  2247 subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
  2248 
  2249 text \<open>
  2250   Lifting \<open>gcd\<close> and \<open>lcm\<close> to sets (\<open>Gcd\<close> / \<open>Lcm\<close>).
  2251   \<open>Gcd\<close> is defined via \<open>Lcm\<close> to facilitate the proof that we have a complete lattice.
  2252 \<close>
  2253 
  2254 instantiation nat :: semiring_Gcd
  2255 begin
  2256 
  2257 interpretation semilattice_neutr_set lcm "1::nat"
  2258   by standard simp_all
  2259 
  2260 definition "Lcm M = (if finite M then F M else 0)" for M :: "nat set"
  2261 
  2262 lemma Lcm_nat_empty: "Lcm {} = (1::nat)"
  2263   by (simp add: Lcm_nat_def del: One_nat_def)
  2264 
  2265 lemma Lcm_nat_insert: "Lcm (insert n M) = lcm n (Lcm M)" for n :: nat
  2266   by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
  2267 
  2268 lemma Lcm_nat_infinite: "infinite M \<Longrightarrow> Lcm M = 0" for M :: "nat set"
  2269   by (simp add: Lcm_nat_def)
  2270 
  2271 lemma dvd_Lcm_nat [simp]:
  2272   fixes M :: "nat set"
  2273   assumes "m \<in> M"
  2274   shows "m dvd Lcm M"
  2275 proof -
  2276   from assms have "insert m M = M"
  2277     by auto
  2278   moreover have "m dvd Lcm (insert m M)"
  2279     by (simp add: Lcm_nat_insert)
  2280   ultimately show ?thesis
  2281     by simp
  2282 qed
  2283 
  2284 lemma Lcm_dvd_nat [simp]:
  2285   fixes M :: "nat set"
  2286   assumes "\<forall>m\<in>M. m dvd n"
  2287   shows "Lcm M dvd n"
  2288 proof (cases "n > 0")
  2289   case False
  2290   then show ?thesis by simp
  2291 next
  2292   case True
  2293   then have "finite {d. d dvd n}"
  2294     by (rule finite_divisors_nat)
  2295   moreover have "M \<subseteq> {d. d dvd n}"
  2296     using assms by fast
  2297   ultimately have "finite M"
  2298     by (rule rev_finite_subset)
  2299   then show ?thesis
  2300     using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
  2301 qed
  2302 
  2303 definition "Gcd M = Lcm {d. \<forall>m\<in>M. d dvd m}" for M :: "nat set"
  2304 
  2305 instance
  2306 proof
  2307   fix N :: "nat set"
  2308   fix n :: nat
  2309   show "Gcd N dvd n" if "n \<in> N"
  2310     using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
  2311   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m"
  2312     using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
  2313   show "n dvd Lcm N" if "n \<in> N"
  2314     using that by (induct N rule: infinite_finite_induct) auto
  2315   show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n"
  2316     using that by (induct N rule: infinite_finite_induct) auto
  2317   show "normalize (Gcd N) = Gcd N" and "normalize (Lcm N) = Lcm N"
  2318     by simp_all
  2319 qed
  2320 
  2321 end
  2322 
  2323 lemma Gcd_nat_eq_one: "1 \<in> N \<Longrightarrow> Gcd N = 1"
  2324   for N :: "nat set"
  2325   by (rule Gcd_eq_1_I) auto
  2326 
  2327 
  2328 text \<open>Alternative characterizations of Gcd:\<close>
  2329 
  2330 lemma Gcd_eq_Max:
  2331   fixes M :: "nat set"
  2332   assumes "finite (M::nat set)" and "M \<noteq> {}" and "0 \<notin> M"
  2333   shows "Gcd M = Max (\<Inter>m\<in>M. {d. d dvd m})"
  2334 proof (rule antisym)
  2335   from assms obtain m where "m \<in> M" and "m > 0"
  2336     by auto
  2337   from \<open>m > 0\<close> have "finite {d. d dvd m}"
  2338     by (blast intro: finite_divisors_nat)
  2339   with \<open>m \<in> M\<close> have fin: "finite (\<Inter>m\<in>M. {d. d dvd m})"
  2340     by blast
  2341   from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
  2342     by (auto intro: Max_ge Gcd_dvd)
  2343   from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
  2344     apply (rule Max.boundedI)
  2345      apply auto
  2346     apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
  2347     done
  2348 qed
  2349 
  2350 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0})"
  2351   for M :: "nat set"
  2352   apply (induct pred: finite)
  2353    apply simp
  2354   apply (case_tac "x = 0")
  2355    apply simp
  2356   apply (subgoal_tac "insert x F - {0} = insert x (F - {0})")
  2357    apply simp
  2358   apply blast
  2359   done
  2360 
  2361 lemma Lcm_in_lcm_closed_set_nat:
  2362   "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"
  2363   for M :: "nat set"
  2364   apply (induct rule: finite_linorder_min_induct)
  2365    apply simp
  2366   apply simp
  2367   apply (subgoal_tac "\<forall>m n. m \<in> A \<longrightarrow> n \<in> A \<longrightarrow> lcm m n \<in> A")
  2368    apply simp
  2369    apply(case_tac "A = {}")
  2370     apply simp
  2371    apply simp
  2372   apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  2373   done
  2374 
  2375 lemma Lcm_eq_Max_nat:
  2376   "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"
  2377   for M :: "nat set"
  2378   apply (rule antisym)
  2379    apply (rule Max_ge)
  2380     apply assumption
  2381    apply (erule (2) Lcm_in_lcm_closed_set_nat)
  2382   apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
  2383   done
  2384 
  2385 lemma mult_inj_if_coprime_nat:
  2386   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>B. coprime (f a) (g b) \<Longrightarrow>
  2387     inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)"
  2388   for f :: "'a \<Rightarrow> nat" and g :: "'b \<Rightarrow> nat"
  2389   by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
  2390 
  2391 
  2392 text \<open>Nitpick:\<close>
  2393 
  2394 lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
  2395   by (induct x y rule: nat_gcd.induct)
  2396     (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  2397 
  2398 lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
  2399   by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  2400 
  2401 
  2402 subsubsection \<open>Setwise GCD and LCM for integers\<close>
  2403 
  2404 instantiation int :: semiring_Gcd
  2405 begin
  2406 
  2407 definition "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
  2408 
  2409 definition "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
  2410 
  2411 instance
  2412   by standard
  2413     (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
  2414       Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
  2415 
  2416 end
  2417 
  2418 lemma abs_Gcd [simp]: "\<bar>Gcd K\<bar> = Gcd K"
  2419   for K :: "int set"
  2420   using normalize_Gcd [of K] by simp
  2421 
  2422 lemma abs_Lcm [simp]: "\<bar>Lcm K\<bar> = Lcm K"
  2423   for K :: "int set"
  2424   using normalize_Lcm [of K] by simp
  2425 
  2426 lemma Gcm_eq_int_iff: "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
  2427   by (simp add: Gcd_int_def comp_def image_image)
  2428 
  2429 lemma Lcm_eq_int_iff: "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
  2430   by (simp add: Lcm_int_def comp_def image_image)
  2431 
  2432 
  2433 subsection \<open>GCD and LCM on @{typ integer}\<close>
  2434 
  2435 instantiation integer :: gcd
  2436 begin
  2437 
  2438 context
  2439   includes integer.lifting
  2440 begin
  2441 
  2442 lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
  2443 
  2444 lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
  2445 
  2446 end
  2447 
  2448 instance ..
  2449 
  2450 end
  2451 
  2452 lifting_update integer.lifting
  2453 lifting_forget integer.lifting
  2454 
  2455 context
  2456   includes integer.lifting
  2457 begin
  2458 
  2459 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>"
  2460   by transfer (fact gcd_code_int)
  2461 
  2462 lemma lcm_code_integer [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  2463   for a b :: integer
  2464   by transfer (fact lcm_altdef_int)
  2465 
  2466 end
  2467 
  2468 code_printing
  2469   constant "gcd :: integer \<Rightarrow> _" \<rightharpoonup>
  2470     (OCaml) "Big'_int.gcd'_big'_int"
  2471   and (Haskell) "Prelude.gcd"
  2472   and (Scala) "_.gcd'((_)')"
  2473   \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
  2474 
  2475 text \<open>Some code equations\<close>
  2476 
  2477 lemmas Lcm_set_nat [code, code_unfold] = Lcm_set[where ?'a = nat]
  2478 lemmas Gcd_set_nat [code] = Gcd_set[where ?'a = nat]
  2479 lemmas Lcm_set_int [code, code_unfold] = Lcm_set[where ?'a = int]
  2480 lemmas Gcd_set_int [code] = Gcd_set[where ?'a = int]
  2481 
  2482 
  2483 text \<open>Fact aliases.\<close>
  2484 
  2485 lemma lcm_0_iff_nat [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
  2486   for m n :: nat
  2487   by (fact lcm_eq_0_iff)
  2488 
  2489 lemma lcm_0_iff_int [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
  2490   for m n :: int
  2491   by (fact lcm_eq_0_iff)
  2492 
  2493 lemma dvd_lcm_I1_nat [simp]: "k dvd m \<Longrightarrow> k dvd lcm m n"
  2494   for k m n :: nat
  2495   by (fact dvd_lcmI1)
  2496 
  2497 lemma dvd_lcm_I2_nat [simp]: "k dvd n \<Longrightarrow> k dvd lcm m n"
  2498   for k m n :: nat
  2499   by (fact dvd_lcmI2)
  2500 
  2501 lemma dvd_lcm_I1_int [simp]: "i dvd m \<Longrightarrow> i dvd lcm m n"
  2502   for i m n :: int
  2503   by (fact dvd_lcmI1)
  2504 
  2505 lemma dvd_lcm_I2_int [simp]: "i dvd n \<Longrightarrow> i dvd lcm m n"
  2506   for i m n :: int
  2507   by (fact dvd_lcmI2)
  2508 
  2509 lemma coprime_exp2_nat [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
  2510   for a b :: nat
  2511   by (fact coprime_exp2)
  2512 
  2513 lemma coprime_exp2_int [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
  2514   for a b :: int
  2515   by (fact coprime_exp2)
  2516 
  2517 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
  2518 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
  2519 lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
  2520 lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int]
  2521 
  2522 lemma dvd_Lcm_int [simp]: "m \<in> M \<Longrightarrow> m dvd Lcm M"
  2523   for M :: "int set"
  2524   by (fact dvd_Lcm)
  2525 
  2526 lemma gcd_neg_numeral_1_int [simp]: "gcd (- numeral n :: int) x = gcd (numeral n) x"
  2527   by (fact gcd_neg1_int)
  2528 
  2529 lemma gcd_neg_numeral_2_int [simp]: "gcd x (- numeral n :: int) = gcd x (numeral n)"
  2530   by (fact gcd_neg2_int)
  2531 
  2532 lemma gcd_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> gcd x y = x"
  2533   for x y :: nat
  2534   by (fact gcd_nat.absorb1)
  2535 
  2536 lemma gcd_proj2_if_dvd_nat [simp]: "y dvd x \<Longrightarrow> gcd x y = y"
  2537   for x y :: nat
  2538   by (fact gcd_nat.absorb2)
  2539 
  2540 lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]
  2541 lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat]
  2542 lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int]
  2543 
  2544 end