src/HOL/GCD.thy
author haftmann
Mon Apr 18 20:56:13 2016 +0200 (2016-04-18)
changeset 63025 92680537201f
parent 62429 25271ff79171
child 63145 703edebd1d92
permissions -rw-r--r--
capitalized GCD and LCM syntax
     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 Lcm_eqI:
  1192   assumes "normalize a = a"
  1193   assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
  1194     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> b dvd c) \<Longrightarrow> a dvd c"
  1195   shows "Lcm A = a"
  1196   using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
  1197 
  1198 
  1199 lemma Lcm_no_units:
  1200   "Lcm A = Lcm (A - {a. is_unit a})"
  1201 proof -
  1202   have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A" by blast
  1203   hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
  1204     by (simp add: Lcm_Un [symmetric])
  1205   also have "Lcm {a\<in>A. is_unit a} = 1" by (simp add: Lcm_1_iff)
  1206   finally show ?thesis by simp
  1207 qed
  1208 
  1209 lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
  1210   by (metis Lcm_least dvd_0_left dvd_Lcm)
  1211 
  1212 lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0"
  1213   by (auto simp: Lcm_0_iff')
  1214 
  1215 lemma Lcm_singleton [simp]:
  1216   "Lcm {a} = normalize a"
  1217   by simp
  1218 
  1219 lemma Lcm_2 [simp]:
  1220   "Lcm {a,b} = lcm a b"
  1221   by simp
  1222 
  1223 lemma Lcm_coprime:
  1224   assumes "finite A" and "A \<noteq> {}" 
  1225   assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
  1226   shows "Lcm A = normalize (\<Prod>A)"
  1227 using assms proof (induct rule: finite_ne_induct)
  1228   case (insert a A)
  1229   have "Lcm (insert a A) = lcm a (Lcm A)" by simp
  1230   also from insert have "Lcm A = normalize (\<Prod>A)" by blast
  1231   also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
  1232   also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto
  1233   with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
  1234     by (simp add: lcm_coprime)
  1235   finally show ?case .
  1236 qed simp
  1237       
  1238 lemma Lcm_coprime':
  1239   "card A \<noteq> 0 \<Longrightarrow> (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1)
  1240     \<Longrightarrow> Lcm A = normalize (\<Prod>A)"
  1241   by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
  1242 
  1243 lemma Gcd_1:
  1244   "1 \<in> A \<Longrightarrow> Gcd A = 1"
  1245   by (auto intro!: Gcd_eq_1_I)
  1246 
  1247 lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
  1248   by simp
  1249 
  1250 lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
  1251   by simp
  1252 
  1253 
  1254 definition pairwise_coprime where
  1255   "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
  1256 
  1257 lemma pairwise_coprimeI [intro?]:
  1258   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
  1259   by (simp add: pairwise_coprime_def)
  1260 
  1261 lemma pairwise_coprimeD:
  1262   "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
  1263   by (simp add: pairwise_coprime_def)
  1264 
  1265 lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
  1266   by (force simp: pairwise_coprime_def)
  1267 
  1268 end
  1269 
  1270 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
  1271 
  1272 instantiation nat :: gcd
  1273 begin
  1274 
  1275 fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  1276 where "gcd_nat x y =
  1277   (if y = 0 then x else gcd y (x mod y))"
  1278 
  1279 definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  1280 where
  1281   "lcm_nat x y = x * y div (gcd x y)"
  1282 
  1283 instance proof qed
  1284 
  1285 end
  1286 
  1287 instantiation int :: gcd
  1288 begin
  1289 
  1290 definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
  1291   where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
  1292 
  1293 definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
  1294   where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
  1295 
  1296 instance ..
  1297 
  1298 end
  1299 
  1300 text \<open>Transfer setup\<close>
  1301 
  1302 lemma transfer_nat_int_gcd:
  1303   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
  1304   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
  1305   unfolding gcd_int_def lcm_int_def
  1306   by auto
  1307 
  1308 lemma transfer_nat_int_gcd_closures:
  1309   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
  1310   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
  1311   by (auto simp add: gcd_int_def lcm_int_def)
  1312 
  1313 declare transfer_morphism_nat_int[transfer add return:
  1314     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
  1315 
  1316 lemma transfer_int_nat_gcd:
  1317   "gcd (int x) (int y) = int (gcd x y)"
  1318   "lcm (int x) (int y) = int (lcm x y)"
  1319   by (unfold gcd_int_def lcm_int_def, auto)
  1320 
  1321 lemma transfer_int_nat_gcd_closures:
  1322   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
  1323   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
  1324   by (auto simp add: gcd_int_def lcm_int_def)
  1325 
  1326 declare transfer_morphism_int_nat[transfer add return:
  1327     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
  1328 
  1329 lemma gcd_nat_induct:
  1330   fixes m n :: nat
  1331   assumes "\<And>m. P m 0"
  1332     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
  1333   shows "P m n"
  1334   apply (rule gcd_nat.induct)
  1335   apply (case_tac "y = 0")
  1336   using assms apply simp_all
  1337 done
  1338 
  1339 (* specific to int *)
  1340 
  1341 lemma gcd_eq_int_iff:
  1342   "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
  1343   by (simp add: gcd_int_def)
  1344 
  1345 lemma lcm_eq_int_iff:
  1346   "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
  1347   by (simp add: lcm_int_def)
  1348 
  1349 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
  1350   by (simp add: gcd_int_def)
  1351 
  1352 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
  1353   by (simp add: gcd_int_def)
  1354 
  1355 lemma abs_gcd_int [simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
  1356 by(simp add: gcd_int_def)
  1357 
  1358 lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
  1359 by (simp add: gcd_int_def)
  1360 
  1361 lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
  1362 by (metis abs_idempotent gcd_abs_int)
  1363 
  1364 lemma gcd_abs2_int [simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
  1365 by (metis abs_idempotent gcd_abs_int)
  1366 
  1367 lemma gcd_cases_int:
  1368   fixes x :: int and y
  1369   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
  1370       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
  1371       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
  1372       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
  1373   shows "P (gcd x y)"
  1374   by (insert assms, auto, arith)
  1375 
  1376 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
  1377   by (simp add: gcd_int_def)
  1378 
  1379 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
  1380   by (simp add: lcm_int_def)
  1381 
  1382 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
  1383   by (simp add: lcm_int_def)
  1384 
  1385 lemma lcm_abs_int: "lcm (x::int) y = lcm \<bar>x\<bar> \<bar>y\<bar>"
  1386   by (simp add: lcm_int_def)
  1387 
  1388 lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
  1389   by (simp add:lcm_int_def)
  1390 
  1391 lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
  1392   by (metis abs_idempotent lcm_int_def)
  1393 
  1394 lemma lcm_abs2_int [simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
  1395   by (metis abs_idempotent lcm_int_def)
  1396 
  1397 lemma lcm_cases_int:
  1398   fixes x :: int and y
  1399   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
  1400       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
  1401       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
  1402       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
  1403   shows "P (lcm x y)"
  1404   using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
  1405 
  1406 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
  1407   by (simp add: lcm_int_def)
  1408 
  1409 lemma gcd_0_nat: "gcd (x::nat) 0 = x"
  1410   by simp
  1411 
  1412 lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
  1413   by (unfold gcd_int_def, auto)
  1414 
  1415 lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
  1416   by simp
  1417 
  1418 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = \<bar>x\<bar>"
  1419   by (unfold gcd_int_def, auto)
  1420 
  1421 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
  1422   by (case_tac "y = 0", auto)
  1423 
  1424 (* weaker, but useful for the simplifier *)
  1425 
  1426 lemma gcd_non_0_nat: "y \<noteq> (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
  1427   by simp
  1428 
  1429 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
  1430   by simp
  1431 
  1432 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
  1433   by simp
  1434 
  1435 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
  1436   by (simp add: gcd_int_def)
  1437 
  1438 lemma gcd_idem_nat: "gcd (x::nat) x = x"
  1439 by simp
  1440 
  1441 lemma gcd_idem_int: "gcd (x::int) x = \<bar>x\<bar>"
  1442 by (auto simp add: gcd_int_def)
  1443 
  1444 declare gcd_nat.simps [simp del]
  1445 
  1446 text \<open>
  1447   \medskip @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.  The
  1448   conjunctions don't seem provable separately.
  1449 \<close>
  1450 
  1451 instance nat :: semiring_gcd
  1452 proof
  1453   fix m n :: nat
  1454   show "gcd m n dvd m" and "gcd m n dvd n"
  1455   proof (induct m n rule: gcd_nat_induct)
  1456     fix m n :: nat
  1457     assume "gcd n (m mod n) dvd m mod n" and "gcd n (m mod n) dvd n"
  1458     then have "gcd n (m mod n) dvd m"
  1459       by (rule dvd_mod_imp_dvd)
  1460     moreover assume "0 < n"
  1461     ultimately show "gcd m n dvd m"
  1462       by (simp add: gcd_non_0_nat)
  1463   qed (simp_all add: gcd_0_nat gcd_non_0_nat)
  1464 next
  1465   fix m n k :: nat
  1466   assume "k dvd m" and "k dvd n"
  1467   then show "k dvd gcd m n"
  1468     by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
  1469 qed (simp_all add: lcm_nat_def)
  1470 
  1471 instance int :: ring_gcd
  1472   by standard
  1473     (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)
  1474 
  1475 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
  1476   by (rule dvd_imp_le, auto)
  1477 
  1478 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
  1479   by (rule dvd_imp_le, auto)
  1480 
  1481 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
  1482   by (rule zdvd_imp_le, auto)
  1483 
  1484 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
  1485   by (rule zdvd_imp_le, auto)
  1486 
  1487 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
  1488   by (insert gcd_eq_0_iff [of m n], arith)
  1489 
  1490 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
  1491   by (insert gcd_eq_0_iff [of m n], insert gcd_ge_0_int [of m n], arith)
  1492 
  1493 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
  1494     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
  1495   apply auto
  1496   apply (rule dvd_antisym)
  1497   apply (erule (1) gcd_greatest)
  1498   apply auto
  1499 done
  1500 
  1501 lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
  1502     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
  1503 apply (case_tac "d = 0")
  1504  apply simp
  1505 apply (rule iffI)
  1506  apply (rule zdvd_antisym_nonneg)
  1507  apply (auto intro: gcd_greatest)
  1508 done
  1509 
  1510 interpretation gcd_nat:
  1511   semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
  1512   by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
  1513 
  1514 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>"
  1515   by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
  1516 
  1517 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>"
  1518   by (metis gcd_proj1_if_dvd_int gcd.commute)
  1519 
  1520 text \<open>
  1521   \medskip Multiplication laws
  1522 \<close>
  1523 
  1524 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
  1525     \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
  1526   apply (induct m n rule: gcd_nat_induct)
  1527   apply simp
  1528   apply (case_tac "k = 0")
  1529   apply (simp_all add: gcd_non_0_nat)
  1530 done
  1531 
  1532 lemma gcd_mult_distrib_int: "\<bar>k::int\<bar> * gcd m n = gcd (k * m) (k * n)"
  1533   apply (subst (1 2) gcd_abs_int)
  1534   apply (subst (1 2) abs_mult)
  1535   apply (rule gcd_mult_distrib_nat [transferred])
  1536   apply auto
  1537 done
  1538 
  1539 lemma coprime_crossproduct_nat:
  1540   fixes a b c d :: nat
  1541   assumes "coprime a d" and "coprime b c"
  1542   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
  1543   using assms coprime_crossproduct [of a d b c] by simp
  1544 
  1545 lemma coprime_crossproduct_int:
  1546   fixes a b c d :: int
  1547   assumes "coprime a d" and "coprime b c"
  1548   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>"
  1549   using assms coprime_crossproduct [of a d b c] by simp
  1550 
  1551 text \<open>\medskip Addition laws\<close>
  1552 
  1553 (* to do: add the other variations? *)
  1554 
  1555 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
  1556   by (subst gcd_add1 [symmetric]) auto
  1557 
  1558 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
  1559   apply (subst gcd.commute)
  1560   apply (subst gcd_diff1_nat [symmetric])
  1561   apply auto
  1562   apply (subst gcd.commute)
  1563   apply (subst gcd_diff1_nat)
  1564   apply assumption
  1565   apply (rule gcd.commute)
  1566   done
  1567 
  1568 lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
  1569   apply (frule_tac b = y and a = x in pos_mod_sign)
  1570   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
  1571   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
  1572     zmod_zminus1_eq_if)
  1573   apply (frule_tac a = x in pos_mod_bound)
  1574   apply (subst (1 2) gcd.commute)
  1575   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
  1576     nat_le_eq_zle)
  1577   done
  1578 
  1579 lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
  1580   apply (case_tac "y = 0")
  1581   apply force
  1582   apply (case_tac "y > 0")
  1583   apply (subst gcd_non_0_int, auto)
  1584   apply (insert gcd_non_0_int [of "-y" "-x"])
  1585   apply auto
  1586 done
  1587 
  1588 (* to do: differences, and all variations of addition rules
  1589     as simplification rules for nat and int *)
  1590 
  1591 (* to do: add the three variations of these, and for ints? *)
  1592 
  1593 lemma finite_divisors_nat [simp]: -- \<open>FIXME move\<close>
  1594   fixes m :: nat
  1595   assumes "m > 0" 
  1596   shows "finite {d. d dvd m}"
  1597 proof-
  1598   from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}"
  1599     by (auto dest: dvd_imp_le)
  1600   then show ?thesis
  1601     using finite_Collect_le_nat by (rule finite_subset)
  1602 qed
  1603 
  1604 lemma finite_divisors_int [simp]:
  1605   fixes i :: int
  1606   assumes "i \<noteq> 0"
  1607   shows "finite {d. d dvd i}"
  1608 proof -
  1609   have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}"
  1610     by (auto simp: abs_if)
  1611   then have "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}"
  1612     by simp
  1613   from finite_subset [OF _ this] show ?thesis using assms
  1614     by (simp add: dvd_imp_le_int subset_iff)
  1615 qed
  1616 
  1617 lemma Max_divisors_self_nat [simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
  1618 apply(rule antisym)
  1619  apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
  1620 apply simp
  1621 done
  1622 
  1623 lemma Max_divisors_self_int [simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
  1624 apply(rule antisym)
  1625  apply(rule Max_le_iff [THEN iffD2])
  1626   apply (auto intro: abs_le_D1 dvd_imp_le_int)
  1627 done
  1628 
  1629 lemma gcd_is_Max_divisors_nat:
  1630   "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd (m::nat) n = Max {d. d dvd m \<and> d dvd n}"
  1631 apply(rule Max_eqI[THEN sym])
  1632   apply (metis finite_Collect_conjI finite_divisors_nat)
  1633  apply simp
  1634  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
  1635 apply simp
  1636 done
  1637 
  1638 lemma gcd_is_Max_divisors_int:
  1639   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
  1640 apply(rule Max_eqI[THEN sym])
  1641   apply (metis finite_Collect_conjI finite_divisors_int)
  1642  apply simp
  1643  apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
  1644 apply simp
  1645 done
  1646 
  1647 lemma gcd_code_int [code]:
  1648   "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  1649   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
  1650 
  1651 
  1652 subsection \<open>Coprimality\<close>
  1653 
  1654 lemma coprime_nat:
  1655   "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1656   using coprime [of a b] by simp
  1657 
  1658 lemma coprime_Suc_0_nat:
  1659   "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
  1660   using coprime_nat by simp
  1661 
  1662 lemma coprime_int:
  1663   "coprime (a::int) b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1664   using gcd_unique_int [of 1 a b]
  1665   apply clarsimp
  1666   apply (erule subst)
  1667   apply (rule iffI)
  1668   apply force
  1669   using abs_dvd_iff abs_ge_zero apply blast
  1670   done
  1671 
  1672 lemma pow_divides_eq_nat [simp]:
  1673   "n > 0 \<Longrightarrow> (a::nat) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
  1674   using pow_divs_eq[of n] by simp
  1675 
  1676 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
  1677   using coprime_plus_one[of n] by simp
  1678 
  1679 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
  1680   using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
  1681 
  1682 lemma coprime_common_divisor_nat: 
  1683   "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
  1684   by (metis gcd_greatest_iff nat_dvd_1_iff_1)
  1685 
  1686 lemma coprime_common_divisor_int:
  1687   "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
  1688   using gcd_greatest_iff [of x a b] by auto
  1689 
  1690 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1691 by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
  1692 
  1693 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1694 by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
  1695 
  1696 
  1697 subsection \<open>Bezout's theorem\<close>
  1698 
  1699 (* Function bezw returns a pair of witnesses to Bezout's theorem --
  1700    see the theorems that follow the definition. *)
  1701 fun
  1702   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1703 where
  1704   "bezw x y =
  1705   (if y = 0 then (1, 0) else
  1706       (snd (bezw y (x mod y)),
  1707        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1708 
  1709 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1710 
  1711 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1712        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1713   by simp
  1714 
  1715 declare bezw.simps [simp del]
  1716 
  1717 lemma bezw_aux [rule_format]:
  1718     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1719 proof (induct x y rule: gcd_nat_induct)
  1720   fix m :: nat
  1721   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1722     by auto
  1723   next fix m :: nat and n
  1724     assume ngt0: "n > 0" and
  1725       ih: "fst (bezw n (m mod n)) * int n +
  1726         snd (bezw n (m mod n)) * int (m mod n) =
  1727         int (gcd n (m mod n))"
  1728     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1729       apply (simp add: bezw_non_0 gcd_non_0_nat)
  1730       apply (erule subst)
  1731       apply (simp add: field_simps)
  1732       apply (subst mod_div_equality [of m n, symmetric])
  1733       (* applying simp here undoes the last substitution!
  1734          what is procedure cancel_div_mod? *)
  1735       apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
  1736       done
  1737 qed
  1738 
  1739 lemma bezout_int:
  1740   fixes x y
  1741   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1742 proof -
  1743   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1744       EX u v. u * x + v * y = gcd x y"
  1745     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1746     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1747     apply (unfold gcd_int_def)
  1748     apply simp
  1749     apply (subst bezw_aux [symmetric])
  1750     apply auto
  1751     done
  1752   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1753       (x \<le> 0 \<and> y \<le> 0)"
  1754     by auto
  1755   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1756     by (erule (1) bezout_aux)
  1757   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1758     apply (insert bezout_aux [of x "-y"])
  1759     apply auto
  1760     apply (rule_tac x = u in exI)
  1761     apply (rule_tac x = "-v" in exI)
  1762     apply (subst gcd_neg2_int [symmetric])
  1763     apply auto
  1764     done
  1765   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1766     apply (insert bezout_aux [of "-x" y])
  1767     apply auto
  1768     apply (rule_tac x = "-u" in exI)
  1769     apply (rule_tac x = v in exI)
  1770     apply (subst gcd_neg1_int [symmetric])
  1771     apply auto
  1772     done
  1773   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1774     apply (insert bezout_aux [of "-x" "-y"])
  1775     apply auto
  1776     apply (rule_tac x = "-u" in exI)
  1777     apply (rule_tac x = "-v" in exI)
  1778     apply (subst gcd_neg1_int [symmetric])
  1779     apply (subst gcd_neg2_int [symmetric])
  1780     apply auto
  1781     done
  1782   ultimately show ?thesis by blast
  1783 qed
  1784 
  1785 text \<open>versions of Bezout for nat, by Amine Chaieb\<close>
  1786 
  1787 lemma ind_euclid:
  1788   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1789   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1790   shows "P a b"
  1791 proof(induct "a + b" arbitrary: a b rule: less_induct)
  1792   case less
  1793   have "a = b \<or> a < b \<or> b < a" by arith
  1794   moreover {assume eq: "a= b"
  1795     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1796     by simp}
  1797   moreover
  1798   {assume lt: "a < b"
  1799     hence "a + b - a < a + b \<or> a = 0" by arith
  1800     moreover
  1801     {assume "a =0" with z c have "P a b" by blast }
  1802     moreover
  1803     {assume "a + b - a < a + b"
  1804       also have th0: "a + b - a = a + (b - a)" using lt by arith
  1805       finally have "a + (b - a) < a + b" .
  1806       then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
  1807       then have "P a b" by (simp add: th0[symmetric])}
  1808     ultimately have "P a b" by blast}
  1809   moreover
  1810   {assume lt: "a > b"
  1811     hence "b + a - b < a + b \<or> b = 0" by arith
  1812     moreover
  1813     {assume "b =0" with z c have "P a b" by blast }
  1814     moreover
  1815     {assume "b + a - b < a + b"
  1816       also have th0: "b + a - b = b + (a - b)" using lt by arith
  1817       finally have "b + (a - b) < a + b" .
  1818       then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
  1819       then have "P b a" by (simp add: th0[symmetric])
  1820       hence "P a b" using c by blast }
  1821     ultimately have "P a b" by blast}
  1822 ultimately  show "P a b" by blast
  1823 qed
  1824 
  1825 lemma bezout_lemma_nat:
  1826   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1827     (a * x = b * y + d \<or> b * x = a * y + d)"
  1828   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1829     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1830   using ex
  1831   apply clarsimp
  1832   apply (rule_tac x="d" in exI, simp)
  1833   apply (case_tac "a * x = b * y + d" , simp_all)
  1834   apply (rule_tac x="x + y" in exI)
  1835   apply (rule_tac x="y" in exI)
  1836   apply algebra
  1837   apply (rule_tac x="x" in exI)
  1838   apply (rule_tac x="x + y" in exI)
  1839   apply algebra
  1840 done
  1841 
  1842 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1843     (a * x = b * y + d \<or> b * x = a * y + d)"
  1844   apply(induct a b rule: ind_euclid)
  1845   apply blast
  1846   apply clarify
  1847   apply (rule_tac x="a" in exI, simp)
  1848   apply clarsimp
  1849   apply (rule_tac x="d" in exI)
  1850   apply (case_tac "a * x = b * y + d", simp_all)
  1851   apply (rule_tac x="x+y" in exI)
  1852   apply (rule_tac x="y" in exI)
  1853   apply algebra
  1854   apply (rule_tac x="x" in exI)
  1855   apply (rule_tac x="x+y" in exI)
  1856   apply algebra
  1857 done
  1858 
  1859 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1860     (a * x - b * y = d \<or> b * x - a * y = d)"
  1861   using bezout_add_nat[of a b]
  1862   apply clarsimp
  1863   apply (rule_tac x="d" in exI, simp)
  1864   apply (rule_tac x="x" in exI)
  1865   apply (rule_tac x="y" in exI)
  1866   apply auto
  1867 done
  1868 
  1869 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1870   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1871 proof-
  1872  from nz have ap: "a > 0" by simp
  1873  from bezout_add_nat[of a b]
  1874  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1875    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1876  moreover
  1877     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1878      from H have ?thesis by blast }
  1879  moreover
  1880  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1881    {assume b0: "b = 0" with H  have ?thesis by simp}
  1882    moreover
  1883    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1884      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1885        by auto
  1886      moreover
  1887      {assume db: "d=b"
  1888        with nz H have ?thesis apply simp
  1889          apply (rule exI[where x = b], simp)
  1890          apply (rule exI[where x = b])
  1891         by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1892     moreover
  1893     {assume db: "d < b"
  1894         {assume "x=0" hence ?thesis using nz H by simp }
  1895         moreover
  1896         {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1897           from db have "d \<le> b - 1" by simp
  1898           hence "d*b \<le> b*(b - 1)" by simp
  1899           with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1900           have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1901           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1902             by simp
  1903           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1904             by (simp only: mult.assoc distrib_left)
  1905           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1906             by algebra
  1907           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1908           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1909             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1910           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1911             by (simp only: diff_mult_distrib2 ac_simps)
  1912           hence ?thesis using H(1,2)
  1913             apply -
  1914             apply (rule exI[where x=d], simp)
  1915             apply (rule exI[where x="(b - 1) * y"])
  1916             by (rule exI[where x="x*(b - 1) - d"], simp)}
  1917         ultimately have ?thesis by blast}
  1918     ultimately have ?thesis by blast}
  1919   ultimately have ?thesis by blast}
  1920  ultimately show ?thesis by blast
  1921 qed
  1922 
  1923 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1924   shows "\<exists>x y. a * x = b * y + gcd a b"
  1925 proof-
  1926   let ?g = "gcd a b"
  1927   from bezout_add_strong_nat[OF a, of b]
  1928   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1929   from d(1,2) have "d dvd ?g" by simp
  1930   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1931   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1932   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1933   thus ?thesis by blast
  1934 qed
  1935 
  1936 
  1937 subsection \<open>LCM properties  on @{typ nat} and @{typ int}\<close>
  1938 
  1939 lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  1940   by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
  1941 
  1942 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1943   unfolding lcm_nat_def
  1944   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
  1945 
  1946 lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
  1947   unfolding lcm_int_def gcd_int_def
  1948   apply (subst of_nat_mult [symmetric])
  1949   apply (subst prod_gcd_lcm_nat [symmetric])
  1950   apply (subst nat_abs_mult_distrib [symmetric])
  1951   apply (simp, simp add: abs_mult)
  1952 done
  1953 
  1954 lemma lcm_pos_nat:
  1955   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1956 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1957 
  1958 lemma lcm_pos_int:
  1959   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1960   apply (subst lcm_abs_int)
  1961   apply (rule lcm_pos_nat [transferred])
  1962   apply auto
  1963   done
  1964 
  1965 lemma dvd_pos_nat: -- \<open>FIXME move\<close>
  1966   fixes n m :: nat
  1967   assumes "n > 0" and "m dvd n"
  1968   shows "m > 0"
  1969   using assms by (cases m) auto
  1970 
  1971 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1972     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1973   by (auto intro: dvd_antisym lcm_least)
  1974 
  1975 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1976     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1977   using lcm_least zdvd_antisym_nonneg by auto
  1978 
  1979 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1980   apply (rule sym)
  1981   apply (subst lcm_unique_nat [symmetric])
  1982   apply auto
  1983 done
  1984 
  1985 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
  1986   apply (rule sym)
  1987   apply (subst lcm_unique_int [symmetric])
  1988   apply auto
  1989 done
  1990 
  1991 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1992 by (subst lcm.commute, erule lcm_proj2_if_dvd_nat)
  1993 
  1994 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
  1995 by (subst lcm.commute, erule lcm_proj2_if_dvd_int)
  1996 
  1997 lemma lcm_proj1_iff_nat [simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1998 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1999 
  2000 lemma lcm_proj2_iff_nat [simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  2001 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  2002 
  2003 lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
  2004 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  2005 
  2006 lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
  2007 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  2008 
  2009 lemma lcm_1_iff_nat [simp]:
  2010   "lcm (m::nat) n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
  2011   using lcm_eq_1_iff [of m n] by simp
  2012   
  2013 lemma lcm_1_iff_int [simp]:
  2014   "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  2015   by auto
  2016 
  2017 
  2018 subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
  2019 
  2020 text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
  2021 Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
  2022 \<close>
  2023 
  2024 instantiation nat :: semiring_Gcd
  2025 begin
  2026 
  2027 interpretation semilattice_neutr_set lcm "1::nat"
  2028   by standard simp_all
  2029 
  2030 definition
  2031   "Lcm (M::nat set) = (if finite M then F M else 0)"
  2032 
  2033 lemma Lcm_nat_empty:
  2034   "Lcm {} = (1::nat)"
  2035   by (simp add: Lcm_nat_def del: One_nat_def)
  2036 
  2037 lemma Lcm_nat_insert:
  2038   "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
  2039   by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
  2040 
  2041 lemma Lcm_nat_infinite:
  2042   "infinite M \<Longrightarrow> Lcm M = (0::nat)"
  2043   by (simp add: Lcm_nat_def)
  2044 
  2045 lemma dvd_Lcm_nat [simp]:
  2046   fixes M :: "nat set"
  2047   assumes "m \<in> M"
  2048   shows "m dvd Lcm M"
  2049 proof -
  2050   from assms have "insert m M = M" by auto
  2051   moreover have "m dvd Lcm (insert m M)"
  2052     by (simp add: Lcm_nat_insert)
  2053   ultimately show ?thesis by simp
  2054 qed
  2055 
  2056 lemma Lcm_dvd_nat [simp]:
  2057   fixes M :: "nat set"
  2058   assumes "\<forall>m\<in>M. m dvd n"
  2059   shows "Lcm M dvd n"
  2060 proof (cases "n > 0")
  2061   case False then show ?thesis by simp
  2062 next
  2063   case True
  2064   then have "finite {d. d dvd n}" by (rule finite_divisors_nat)
  2065   moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
  2066   ultimately have "finite M" by (rule rev_finite_subset)
  2067   then show ?thesis using assms
  2068     by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
  2069 qed
  2070 
  2071 definition
  2072   "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
  2073 
  2074 instance proof
  2075   show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
  2076   using that by (induct N rule: infinite_finite_induct)
  2077     (auto simp add: Gcd_nat_def)
  2078   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
  2079   using that by (induct N rule: infinite_finite_induct)
  2080     (auto simp add: Gcd_nat_def)
  2081   show "n dvd Lcm N" if "n \<in> N" for N and n ::nat
  2082   using that by (induct N rule: infinite_finite_induct)
  2083     auto
  2084   show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n" for N and n ::nat
  2085   using that by (induct N rule: infinite_finite_induct)
  2086     auto
  2087 qed simp_all
  2088 
  2089 end
  2090 
  2091 lemma Gcd_nat_eq_one:
  2092   "1 \<in> N \<Longrightarrow> Gcd N = (1::nat)"
  2093   by (rule Gcd_eq_1_I) auto
  2094 
  2095 text\<open>Alternative characterizations of Gcd:\<close>
  2096 
  2097 lemma Gcd_eq_Max:
  2098   fixes M :: "nat set"
  2099   assumes "finite (M::nat set)" and "M \<noteq> {}" and "0 \<notin> M"
  2100   shows "Gcd M = Max (\<Inter>m\<in>M. {d. d dvd m})"
  2101 proof (rule antisym)
  2102   from assms obtain m where "m \<in> M" and "m > 0"
  2103     by auto
  2104   from \<open>m > 0\<close> have "finite {d. d dvd m}"
  2105     by (blast intro: finite_divisors_nat)
  2106   with \<open>m \<in> M\<close> have fin: "finite (\<Inter>m\<in>M. {d. d dvd m})"
  2107     by blast
  2108   from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
  2109     by (auto intro: Max_ge Gcd_dvd)
  2110   from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
  2111     apply (rule Max.boundedI)
  2112     apply auto
  2113     apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
  2114     done
  2115 qed
  2116 
  2117 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
  2118 apply(induct pred:finite)
  2119  apply simp
  2120 apply(case_tac "x=0")
  2121  apply simp
  2122 apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
  2123  apply simp
  2124 apply blast
  2125 done
  2126 
  2127 lemma Lcm_in_lcm_closed_set_nat:
  2128   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
  2129 apply(induct rule:finite_linorder_min_induct)
  2130  apply simp
  2131 apply simp
  2132 apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
  2133  apply simp
  2134  apply(case_tac "A={}")
  2135   apply simp
  2136  apply simp
  2137 apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  2138 done
  2139 
  2140 lemma Lcm_eq_Max_nat:
  2141   "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"
  2142 apply(rule antisym)
  2143  apply(rule Max_ge, assumption)
  2144  apply(erule (2) Lcm_in_lcm_closed_set_nat)
  2145 apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
  2146 done
  2147 
  2148 lemma mult_inj_if_coprime_nat:
  2149   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
  2150    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
  2151   by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
  2152 
  2153 text\<open>Nitpick:\<close>
  2154 
  2155 lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
  2156 by (induct x y rule: nat_gcd.induct)
  2157    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  2158 
  2159 lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
  2160 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  2161 
  2162 
  2163 subsubsection \<open>Setwise gcd and lcm for integers\<close>
  2164 
  2165 instantiation int :: semiring_Gcd
  2166 begin
  2167 
  2168 definition
  2169   "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
  2170 
  2171 definition
  2172   "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
  2173 
  2174 instance by standard
  2175   (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
  2176     Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
  2177 
  2178 end
  2179 
  2180 lemma abs_Gcd [simp]:
  2181   fixes K :: "int set"
  2182   shows "\<bar>Gcd K\<bar> = Gcd K"
  2183   using normalize_Gcd [of K] by simp
  2184 
  2185 lemma abs_Lcm [simp]:
  2186   fixes K :: "int set"
  2187   shows "\<bar>Lcm K\<bar> = Lcm K"
  2188   using normalize_Lcm [of K] by simp
  2189 
  2190 lemma Gcm_eq_int_iff:
  2191   "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
  2192   by (simp add: Gcd_int_def comp_def image_image)
  2193 
  2194 lemma Lcm_eq_int_iff:
  2195   "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
  2196   by (simp add: Lcm_int_def comp_def image_image)
  2197 
  2198 
  2199 subsection \<open>GCD and LCM on @{typ integer}\<close>
  2200 
  2201 instantiation integer :: gcd
  2202 begin
  2203 
  2204 context
  2205   includes integer.lifting
  2206 begin
  2207 
  2208 lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
  2209   is gcd .
  2210 lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
  2211   is lcm .
  2212 
  2213 end
  2214 instance ..
  2215 
  2216 end
  2217 
  2218 lifting_update integer.lifting
  2219 lifting_forget integer.lifting
  2220 
  2221 context
  2222   includes integer.lifting
  2223 begin
  2224 
  2225 lemma gcd_code_integer [code]:
  2226   "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  2227   by transfer (fact gcd_code_int)
  2228 
  2229 lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  2230   by transfer (fact lcm_altdef_int)
  2231 
  2232 end
  2233 
  2234 code_printing constant "gcd :: integer \<Rightarrow> _"
  2235   \<rightharpoonup> (OCaml) "Big'_int.gcd'_big'_int"
  2236   and (Haskell) "Prelude.gcd"
  2237   and (Scala) "_.gcd'((_)')"
  2238   \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
  2239 
  2240 text \<open>Some code equations\<close>
  2241 
  2242 lemmas Lcm_set_nat [code, code_unfold] = Lcm_set[where ?'a = nat]
  2243 lemmas Gcd_set_nat [code] = Gcd_set[where ?'a = nat]
  2244 lemmas Lcm_set_int [code, code_unfold] = Lcm_set[where ?'a = int]
  2245 lemmas Gcd_set_int [code] = Gcd_set[where ?'a = int]
  2246 
  2247 
  2248 text \<open>Fact aliasses\<close>
  2249 
  2250 lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
  2251   by (fact lcm_eq_0_iff)
  2252 
  2253 lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
  2254   by (fact lcm_eq_0_iff)
  2255 
  2256 lemma dvd_lcm_I1_nat [simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  2257   by (fact dvd_lcmI1)
  2258 
  2259 lemma dvd_lcm_I2_nat [simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  2260   by (fact dvd_lcmI2)
  2261 
  2262 lemma dvd_lcm_I1_int [simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  2263   by (fact dvd_lcmI1)
  2264 
  2265 lemma dvd_lcm_I2_int [simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  2266   by (fact dvd_lcmI2)
  2267 
  2268 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
  2269   by (fact coprime_exp2)
  2270 
  2271 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
  2272   by (fact coprime_exp2)
  2273 
  2274 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
  2275 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
  2276 lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
  2277 lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int]
  2278 
  2279 lemma dvd_Lcm_int [simp]:
  2280   fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
  2281   using assms by (fact dvd_Lcm)
  2282 
  2283 lemma gcd_neg_numeral_1_int [simp]:
  2284   "gcd (- numeral n :: int) x = gcd (numeral n) x"
  2285   by (fact gcd_neg1_int)
  2286 
  2287 lemma gcd_neg_numeral_2_int [simp]:
  2288   "gcd x (- numeral n :: int) = gcd x (numeral n)"
  2289   by (fact gcd_neg2_int)
  2290 
  2291 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
  2292   by (fact gcd_nat.absorb1)
  2293 
  2294 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
  2295   by (fact gcd_nat.absorb2)
  2296 
  2297 lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]
  2298 lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat]
  2299 lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int]
  2300 
  2301 end