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