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