src/HOL/GCD.thy
author haftmann
Wed Feb 17 21:51:56 2016 +0100 (2016-02-17)
changeset 62345 e66d7841d5a2
parent 62344 759d684c0e60
child 62346 97f2ed240431
permissions -rw-r--r--
further generalization and polishing
     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 
    50 class semiring_gcd = normalization_semidom + gcd +
    51   assumes gcd_dvd1 [iff]: "gcd a b dvd a"
    52     and gcd_dvd2 [iff]: "gcd a b dvd b"
    53     and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
    54     and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
    55     and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
    56 begin    
    57 
    58 lemma gcd_greatest_iff [simp]:
    59   "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
    60   by (blast intro!: gcd_greatest intro: dvd_trans)
    61 
    62 lemma gcd_dvdI1:
    63   "a dvd c \<Longrightarrow> gcd a b dvd c"
    64   by (rule dvd_trans) (rule gcd_dvd1)
    65 
    66 lemma gcd_dvdI2:
    67   "b dvd c \<Longrightarrow> gcd a b dvd c"
    68   by (rule dvd_trans) (rule gcd_dvd2)
    69 
    70 lemma dvd_gcdD1:
    71   "a dvd gcd b c \<Longrightarrow> a dvd b"
    72   using gcd_dvd1 [of b c] by (blast intro: dvd_trans)
    73 
    74 lemma dvd_gcdD2:
    75   "a dvd gcd b c \<Longrightarrow> a dvd c"
    76   using gcd_dvd2 [of b c] by (blast intro: dvd_trans)
    77 
    78 lemma gcd_0_left [simp]:
    79   "gcd 0 a = normalize a"
    80   by (rule associated_eqI) simp_all
    81 
    82 lemma gcd_0_right [simp]:
    83   "gcd a 0 = normalize a"
    84   by (rule associated_eqI) simp_all
    85   
    86 lemma gcd_eq_0_iff [simp]:
    87   "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" (is "?P \<longleftrightarrow> ?Q")
    88 proof
    89   assume ?P then have "0 dvd gcd a b" by simp
    90   then have "0 dvd a" and "0 dvd b" by (blast intro: dvd_trans)+
    91   then show ?Q by simp
    92 next
    93   assume ?Q then show ?P by simp
    94 qed
    95 
    96 lemma unit_factor_gcd:
    97   "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)"
    98 proof (cases "gcd a b = 0")
    99   case True then show ?thesis by simp
   100 next
   101   case False
   102   have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b"
   103     by (rule unit_factor_mult_normalize)
   104   then have "unit_factor (gcd a b) * gcd a b = gcd a b"
   105     by simp
   106   then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b"
   107     by simp
   108   with False show ?thesis by simp
   109 qed
   110 
   111 lemma is_unit_gcd [simp]:
   112   "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
   113   by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
   114 
   115 sublocale gcd: abel_semigroup gcd
   116 proof
   117   fix a b c
   118   show "gcd a b = gcd b a"
   119     by (rule associated_eqI) simp_all
   120   from gcd_dvd1 have "gcd (gcd a b) c dvd a"
   121     by (rule dvd_trans) simp
   122   moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
   123     by (rule dvd_trans) simp
   124   ultimately have P1: "gcd (gcd a b) c dvd gcd a (gcd b c)"
   125     by (auto intro!: gcd_greatest)
   126   from gcd_dvd2 have "gcd a (gcd b c) dvd b"
   127     by (rule dvd_trans) simp
   128   moreover from gcd_dvd2 have "gcd a (gcd b c) dvd c"
   129     by (rule dvd_trans) simp
   130   ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
   131     by (auto intro!: gcd_greatest)
   132   from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)"
   133     by (rule associated_eqI) simp_all
   134 qed
   135 
   136 lemma gcd_self [simp]:
   137   "gcd a a = normalize a"
   138 proof -
   139   have "a dvd gcd a a"
   140     by (rule gcd_greatest) simp_all
   141   then show ?thesis
   142     by (auto intro: associated_eqI)
   143 qed
   144 
   145 lemma gcd_left_idem [simp]:
   146   "gcd a (gcd a b) = gcd a b"
   147   by (auto intro: associated_eqI)
   148 
   149 lemma gcd_right_idem [simp]:
   150   "gcd (gcd a b) b = gcd a b"
   151   unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
   152 
   153 lemma coprime_1_left [simp]:
   154   "coprime 1 a"
   155   by (rule associated_eqI) simp_all
   156 
   157 lemma coprime_1_right [simp]:
   158   "coprime a 1"
   159   using coprime_1_left [of a] by (simp add: ac_simps)
   160 
   161 lemma gcd_mult_left:
   162   "gcd (c * a) (c * b) = normalize c * gcd a b"
   163 proof (cases "c = 0")
   164   case True then show ?thesis by simp
   165 next
   166   case False
   167   then have "c * gcd a b dvd gcd (c * a) (c * b)"
   168     by (auto intro: gcd_greatest)
   169   moreover from calculation False have "gcd (c * a) (c * b) dvd c * gcd a b"
   170     by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
   171   ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
   172     by (auto intro: associated_eqI)
   173   then show ?thesis by (simp add: normalize_mult)
   174 qed
   175 
   176 lemma gcd_mult_right:
   177   "gcd (a * c) (b * c) = gcd b a * normalize c"
   178   using gcd_mult_left [of c a b] by (simp add: ac_simps)
   179 
   180 lemma mult_gcd_left:
   181   "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
   182   by (simp add: gcd_mult_left mult.assoc [symmetric])
   183 
   184 lemma mult_gcd_right:
   185   "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
   186   using mult_gcd_left [of c a b] by (simp add: ac_simps)
   187 
   188 lemma dvd_lcm1 [iff]:
   189   "a dvd lcm a b"
   190 proof -
   191   have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
   192     by (simp add: lcm_gcd normalize_mult div_mult_swap)
   193   then show ?thesis
   194     by (simp add: lcm_gcd)
   195 qed
   196   
   197 lemma dvd_lcm2 [iff]:
   198   "b dvd lcm a b"
   199 proof -
   200   have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
   201     by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
   202   then show ?thesis
   203     by (simp add: lcm_gcd)
   204 qed
   205 
   206 lemma dvd_lcmI1:
   207   "a dvd b \<Longrightarrow> a dvd lcm b c"
   208   by (rule dvd_trans) (assumption, blast) 
   209 
   210 lemma dvd_lcmI2:
   211   "a dvd c \<Longrightarrow> a dvd lcm b c"
   212   by (rule dvd_trans) (assumption, blast)
   213 
   214 lemma lcm_dvdD1:
   215   "lcm a b dvd c \<Longrightarrow> a dvd c"
   216   using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
   217 
   218 lemma lcm_dvdD2:
   219   "lcm a b dvd c \<Longrightarrow> b dvd c"
   220   using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
   221 
   222 lemma lcm_least:
   223   assumes "a dvd c" and "b dvd c"
   224   shows "lcm a b dvd c"
   225 proof (cases "c = 0")
   226   case True then show ?thesis by simp
   227 next
   228   case False then have U: "is_unit (unit_factor c)" by simp
   229   show ?thesis
   230   proof (cases "gcd a b = 0")
   231     case True with assms show ?thesis by simp
   232   next
   233     case False then have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
   234     with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b"
   235       by (simp_all add: mult_dvd_mono)
   236     then have "normalize (a * b) dvd gcd (a * c) (b * c)"
   237       by (auto intro: gcd_greatest simp add: ac_simps)
   238     then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
   239       using U by (simp add: dvd_mult_unit_iff)
   240     then have "normalize (a * b) dvd gcd a b * c"
   241       by (simp add: mult_gcd_right [of a b c])
   242     then have "normalize (a * b) div gcd a b dvd c"
   243       using False by (simp add: div_dvd_iff_mult ac_simps)
   244     then show ?thesis by (simp add: lcm_gcd)
   245   qed
   246 qed
   247 
   248 lemma lcm_least_iff [simp]:
   249   "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
   250   by (blast intro!: lcm_least intro: dvd_trans)
   251 
   252 lemma normalize_lcm [simp]:
   253   "normalize (lcm a b) = lcm a b"
   254   by (simp add: lcm_gcd dvd_normalize_div)
   255 
   256 lemma lcm_0_left [simp]:
   257   "lcm 0 a = 0"
   258   by (simp add: lcm_gcd)
   259   
   260 lemma lcm_0_right [simp]:
   261   "lcm a 0 = 0"
   262   by (simp add: lcm_gcd)
   263 
   264 lemma lcm_eq_0_iff:
   265   "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" (is "?P \<longleftrightarrow> ?Q")
   266 proof
   267   assume ?P then have "0 dvd lcm a b" by simp
   268   then have "0 dvd normalize (a * b) div gcd a b"
   269     by (simp add: lcm_gcd)
   270   then have "0 * gcd a b dvd normalize (a * b)"
   271     using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
   272   then have "normalize (a * b) = 0"
   273     by simp
   274   then show ?Q by simp
   275 next
   276   assume ?Q then show ?P by auto
   277 qed
   278 
   279 lemma lcm_eq_1_iff [simp]:
   280   "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
   281   by (auto intro: associated_eqI)
   282 
   283 lemma unit_factor_lcm :
   284   "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
   285   by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
   286 
   287 sublocale lcm: abel_semigroup lcm
   288 proof
   289   fix a b c
   290   show "lcm a b = lcm b a"
   291     by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
   292   have "lcm (lcm a b) c dvd lcm a (lcm b c)"
   293     and "lcm a (lcm b c) dvd lcm (lcm a b) c"
   294     by (auto intro: lcm_least
   295       dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
   296       dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
   297       dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
   298       dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
   299   then show "lcm (lcm a b) c = lcm a (lcm b c)"
   300     by (rule associated_eqI) simp_all
   301 qed
   302 
   303 lemma lcm_self [simp]:
   304   "lcm a a = normalize a"
   305 proof -
   306   have "lcm a a dvd a"
   307     by (rule lcm_least) simp_all
   308   then show ?thesis
   309     by (auto intro: associated_eqI)
   310 qed
   311 
   312 lemma lcm_left_idem [simp]:
   313   "lcm a (lcm a b) = lcm a b"
   314   by (auto intro: associated_eqI)
   315 
   316 lemma lcm_right_idem [simp]:
   317   "lcm (lcm a b) b = lcm a b"
   318   unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
   319 
   320 lemma gcd_mult_lcm [simp]:
   321   "gcd a b * lcm a b = normalize a * normalize b"
   322   by (simp add: lcm_gcd normalize_mult)
   323 
   324 lemma lcm_mult_gcd [simp]:
   325   "lcm a b * gcd a b = normalize a * normalize b"
   326   using gcd_mult_lcm [of a b] by (simp add: ac_simps) 
   327 
   328 lemma gcd_lcm:
   329   assumes "a \<noteq> 0" and "b \<noteq> 0"
   330   shows "gcd a b = normalize (a * b) div lcm a b"
   331 proof -
   332   from assms have "lcm a b \<noteq> 0"
   333     by (simp add: lcm_eq_0_iff)
   334   have "gcd a b * lcm a b = normalize a * normalize b" by simp
   335   then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
   336     by (simp_all add: normalize_mult)
   337   with \<open>lcm a b \<noteq> 0\<close> show ?thesis
   338     using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp
   339 qed
   340 
   341 lemma lcm_1_left [simp]:
   342   "lcm 1 a = normalize a"
   343   by (simp add: lcm_gcd)
   344 
   345 lemma lcm_1_right [simp]:
   346   "lcm a 1 = normalize a"
   347   by (simp add: lcm_gcd)
   348   
   349 lemma lcm_mult_left:
   350   "lcm (c * a) (c * b) = normalize c * lcm a b"
   351   by (cases "c = 0")
   352     (simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
   353       simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
   354 
   355 lemma lcm_mult_right:
   356   "lcm (a * c) (b * c) = lcm b a * normalize c"
   357   using lcm_mult_left [of c a b] by (simp add: ac_simps)
   358 
   359 lemma mult_lcm_left:
   360   "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
   361   by (simp add: lcm_mult_left mult.assoc [symmetric])
   362 
   363 lemma mult_lcm_right:
   364   "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
   365   using mult_lcm_left [of c a b] by (simp add: ac_simps)
   366   
   367 end
   368 
   369 class ring_gcd = comm_ring_1 + semiring_gcd
   370 
   371 class semiring_Gcd = semiring_gcd + Gcd +
   372   assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
   373     and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A"
   374     and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
   375   assumes dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
   376     and Lcm_least: "(\<And>b. b \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> Lcm A dvd a"
   377     and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A"
   378 begin
   379 
   380 lemma Lcm_Gcd:
   381   "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
   382   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
   383 
   384 lemma Gcd_Lcm:
   385   "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
   386   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
   387 
   388 lemma Gcd_empty [simp]:
   389   "Gcd {} = 0"
   390   by (rule dvd_0_left, rule Gcd_greatest) simp
   391 
   392 lemma Lcm_empty [simp]:
   393   "Lcm {} = 1"
   394   by (auto intro: associated_eqI Lcm_least)
   395 
   396 lemma Gcd_insert [simp]:
   397   "Gcd (insert a A) = gcd a (Gcd A)"
   398 proof -
   399   have "Gcd (insert a A) dvd gcd a (Gcd A)"
   400     by (auto intro: Gcd_dvd Gcd_greatest)
   401   moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
   402   proof (rule Gcd_greatest)
   403     fix b
   404     assume "b \<in> insert a A"
   405     then show "gcd a (Gcd A) dvd b"
   406     proof
   407       assume "b = a" then show ?thesis by simp
   408     next
   409       assume "b \<in> A"
   410       then have "Gcd A dvd b" by (rule Gcd_dvd)
   411       moreover have "gcd a (Gcd A) dvd Gcd A" by simp
   412       ultimately show ?thesis by (blast intro: dvd_trans)
   413     qed
   414   qed
   415   ultimately show ?thesis
   416     by (auto intro: associated_eqI)
   417 qed
   418 
   419 lemma Lcm_insert [simp]:
   420   "Lcm (insert a A) = lcm a (Lcm A)"
   421 proof (rule sym)
   422   have "lcm a (Lcm A) dvd Lcm (insert a A)"
   423     by (auto intro: dvd_Lcm Lcm_least)
   424   moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
   425   proof (rule Lcm_least)
   426     fix b
   427     assume "b \<in> insert a A"
   428     then show "b dvd lcm a (Lcm A)"
   429     proof
   430       assume "b = a" then show ?thesis by simp
   431     next
   432       assume "b \<in> A"
   433       then have "b dvd Lcm A" by (rule dvd_Lcm)
   434       moreover have "Lcm A dvd lcm a (Lcm A)" by simp
   435       ultimately show ?thesis by (blast intro: dvd_trans)
   436     qed
   437   qed
   438   ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
   439     by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
   440 qed
   441 
   442 lemma Gcd_0_iff [simp]:
   443   "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
   444 proof
   445   assume ?P
   446   show ?Q
   447   proof
   448     fix a
   449     assume "a \<in> A"
   450     then have "Gcd A dvd a" by (rule Gcd_dvd)
   451     with \<open>?P\<close> have "a = 0" by simp
   452     then show "a \<in> {0}" by simp
   453   qed
   454 next
   455   assume ?Q
   456   have "0 dvd Gcd A"
   457   proof (rule Gcd_greatest)
   458     fix a
   459     assume "a \<in> A"
   460     with \<open>?Q\<close> have "a = 0" by auto
   461     then show "0 dvd a" by simp
   462   qed
   463   then show ?P by simp
   464 qed
   465 
   466 lemma Lcm_1_iff [simp]:
   467   "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" (is "?P \<longleftrightarrow> ?Q")
   468 proof
   469   assume ?P
   470   show ?Q
   471   proof
   472     fix a
   473     assume "a \<in> A"
   474     then have "a dvd Lcm A"
   475       by (rule dvd_Lcm)
   476     with \<open>?P\<close> show "is_unit a"
   477       by simp
   478   qed
   479 next
   480   assume ?Q
   481   then have "is_unit (Lcm A)"
   482     by (blast intro: Lcm_least)
   483   then have "normalize (Lcm A) = 1"
   484     by (rule is_unit_normalize)
   485   then show ?P
   486     by simp
   487 qed
   488 
   489 lemma unit_factor_Gcd:
   490   "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
   491 proof (cases "Gcd A = 0")
   492   case True then show ?thesis by auto
   493 next
   494   case False
   495   from unit_factor_mult_normalize
   496   have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" .
   497   then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
   498   then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
   499   with False have "unit_factor (Gcd A) = 1" by simp
   500   with False show ?thesis by auto
   501 qed
   502 
   503 lemma unit_factor_Lcm:
   504   "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
   505 proof (cases "Lcm A = 0")
   506   case True then show ?thesis by simp
   507 next
   508   case False
   509   with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
   510     by blast
   511   with False show ?thesis
   512     by simp
   513 qed
   514 
   515 lemma Gcd_eq_1_I:
   516   assumes "is_unit a" and "a \<in> A"
   517   shows "Gcd A = 1"
   518 proof -
   519   from assms have "is_unit (Gcd A)"
   520     by (blast intro: Gcd_dvd dvd_unit_imp_unit)
   521   then have "normalize (Gcd A) = 1"
   522     by (rule is_unit_normalize)
   523   then show ?thesis
   524     by simp
   525 qed
   526 
   527 lemma Lcm_eq_0_I:
   528   assumes "0 \<in> A"
   529   shows "Lcm A = 0"
   530 proof -
   531   from assms have "0 dvd Lcm A"
   532     by (rule dvd_Lcm)
   533   then show ?thesis
   534     by simp
   535 qed
   536 
   537 lemma Gcd_UNIV [simp]:
   538   "Gcd UNIV = 1"
   539   using dvd_refl by (rule Gcd_eq_1_I) simp
   540 
   541 lemma Lcm_UNIV [simp]:
   542   "Lcm UNIV = 0"
   543   by (rule Lcm_eq_0_I) simp
   544 
   545 lemma Lcm_0_iff:
   546   assumes "finite A"
   547   shows "Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
   548 proof (cases "A = {}")
   549   case True then show ?thesis by simp
   550 next
   551   case False with assms show ?thesis
   552     by (induct A rule: finite_ne_induct)
   553       (auto simp add: lcm_eq_0_iff)
   554 qed
   555 
   556 lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close>
   557   "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
   558   by (blast intro: Gcd_greatest)
   559 
   560 lemma Gcd_set [code_unfold]:
   561   "Gcd (set as) = foldr gcd as 0"
   562   by (induct as) simp_all
   563 
   564 lemma Lcm_set [code_unfold]:
   565   "Lcm (set as) = foldr lcm as 1"
   566   by (induct as) simp_all
   567 
   568 lemma Gcd_image_normalize [simp]:
   569   "Gcd (normalize ` A) = Gcd A"
   570 proof -
   571   have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
   572   proof -
   573     from that obtain B where "A = insert a B" by blast
   574     moreover have " gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
   575       by (rule gcd_dvd1)
   576     ultimately show "Gcd (normalize ` A) dvd a"
   577       by simp
   578   qed
   579   then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
   580     by (auto intro!: Gcd_greatest intro: Gcd_dvd)
   581   then show ?thesis
   582     by (auto intro: associated_eqI)
   583 qed
   584 
   585 end  
   586 
   587 
   588 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
   589 
   590 instantiation nat :: gcd
   591 begin
   592 
   593 fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   594 where "gcd_nat x y =
   595   (if y = 0 then x else gcd y (x mod y))"
   596 
   597 definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   598 where
   599   "lcm_nat x y = x * y div (gcd x y)"
   600 
   601 instance proof qed
   602 
   603 end
   604 
   605 instantiation int :: gcd
   606 begin
   607 
   608 definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
   609   where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   610 
   611 definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
   612   where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   613 
   614 instance ..
   615 
   616 end
   617 
   618 text \<open>Transfer setup\<close>
   619 
   620 lemma transfer_nat_int_gcd:
   621   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   622   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   623   unfolding gcd_int_def lcm_int_def
   624   by auto
   625 
   626 lemma transfer_nat_int_gcd_closures:
   627   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
   628   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   629   by (auto simp add: gcd_int_def lcm_int_def)
   630 
   631 declare transfer_morphism_nat_int[transfer add return:
   632     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   633 
   634 lemma transfer_int_nat_gcd:
   635   "gcd (int x) (int y) = int (gcd x y)"
   636   "lcm (int x) (int y) = int (lcm x y)"
   637   by (unfold gcd_int_def lcm_int_def, auto)
   638 
   639 lemma transfer_int_nat_gcd_closures:
   640   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   641   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   642   by (auto simp add: gcd_int_def lcm_int_def)
   643 
   644 declare transfer_morphism_int_nat[transfer add return:
   645     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   646 
   647 lemma gcd_nat_induct:
   648   fixes m n :: nat
   649   assumes "\<And>m. P m 0"
   650     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   651   shows "P m n"
   652   apply (rule gcd_nat.induct)
   653   apply (case_tac "y = 0")
   654   using assms apply simp_all
   655 done
   656 
   657 (* specific to int *)
   658 
   659 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
   660   by (simp add: gcd_int_def)
   661 
   662 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
   663   by (simp add: gcd_int_def)
   664 
   665 lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
   666 by(simp add: gcd_int_def)
   667 
   668 lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
   669 by (simp add: gcd_int_def)
   670 
   671 lemma gcd_abs1_int[simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
   672 by (metis abs_idempotent gcd_abs_int)
   673 
   674 lemma gcd_abs2_int[simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
   675 by (metis abs_idempotent gcd_abs_int)
   676 
   677 lemma gcd_cases_int:
   678   fixes x :: int and y
   679   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   680       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   681       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   682       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   683   shows "P (gcd x y)"
   684   by (insert assms, auto, arith)
   685 
   686 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   687   by (simp add: gcd_int_def)
   688 
   689 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
   690   by (simp add: lcm_int_def)
   691 
   692 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
   693   by (simp add: lcm_int_def)
   694 
   695 lemma lcm_abs_int: "lcm (x::int) y = lcm \<bar>x\<bar> \<bar>y\<bar>"
   696   by (simp add: lcm_int_def)
   697 
   698 lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
   699   by (simp add:lcm_int_def)
   700 
   701 lemma lcm_abs1_int[simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
   702   by (metis abs_idempotent lcm_int_def)
   703 
   704 lemma lcm_abs2_int[simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
   705   by (metis abs_idempotent lcm_int_def)
   706 
   707 lemma lcm_cases_int:
   708   fixes x :: int and y
   709   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   710       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   711       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   712       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   713   shows "P (lcm x y)"
   714   using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
   715 
   716 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   717   by (simp add: lcm_int_def)
   718 
   719 lemma gcd_0_nat: "gcd (x::nat) 0 = x"
   720   by simp
   721 
   722 lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
   723   by (unfold gcd_int_def, auto)
   724 
   725 lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
   726   by simp
   727 
   728 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = \<bar>x\<bar>"
   729   by (unfold gcd_int_def, auto)
   730 
   731 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
   732   by (case_tac "y = 0", auto)
   733 
   734 (* weaker, but useful for the simplifier *)
   735 
   736 lemma gcd_non_0_nat: "y \<noteq> (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   737   by simp
   738 
   739 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   740   by simp
   741 
   742 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   743   by simp
   744 
   745 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   746   by (simp add: gcd_int_def)
   747 
   748 lemma gcd_idem_nat: "gcd (x::nat) x = x"
   749 by simp
   750 
   751 lemma gcd_idem_int: "gcd (x::int) x = \<bar>x\<bar>"
   752 by (auto simp add: gcd_int_def)
   753 
   754 declare gcd_nat.simps [simp del]
   755 
   756 text \<open>
   757   \medskip @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.  The
   758   conjunctions don't seem provable separately.
   759 \<close>
   760 
   761 instance nat :: semiring_gcd
   762 proof
   763   fix m n :: nat
   764   show "gcd m n dvd m" and "gcd m n dvd n"
   765   proof (induct m n rule: gcd_nat_induct)
   766     fix m n :: nat
   767     assume "gcd n (m mod n) dvd m mod n" and "gcd n (m mod n) dvd n"
   768     then have "gcd n (m mod n) dvd m"
   769       by (rule dvd_mod_imp_dvd)
   770     moreover assume "0 < n"
   771     ultimately show "gcd m n dvd m"
   772       by (simp add: gcd_non_0_nat)
   773   qed (simp_all add: gcd_0_nat gcd_non_0_nat)
   774 next
   775   fix m n k :: nat
   776   assume "k dvd m" and "k dvd n"
   777   then show "k dvd gcd m n"
   778     by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
   779 qed (simp_all add: lcm_nat_def)
   780 
   781 instance int :: ring_gcd
   782   by standard
   783     (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)
   784 
   785 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   786   by (rule dvd_imp_le, auto)
   787 
   788 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   789   by (rule dvd_imp_le, auto)
   790 
   791 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   792   by (rule zdvd_imp_le, auto)
   793 
   794 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   795   by (rule zdvd_imp_le, auto)
   796 
   797 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   798   by (insert gcd_eq_0_iff [of m n], arith)
   799 
   800 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   801   by (insert gcd_eq_0_iff [of m n], insert gcd_ge_0_int [of m n], arith)
   802 
   803 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
   804     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   805   apply auto
   806   apply (rule dvd_antisym)
   807   apply (erule (1) gcd_greatest)
   808   apply auto
   809 done
   810 
   811 lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   812     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   813 apply (case_tac "d = 0")
   814  apply simp
   815 apply (rule iffI)
   816  apply (rule zdvd_antisym_nonneg)
   817  apply (auto intro: gcd_greatest)
   818 done
   819 
   820 interpretation gcd_nat:
   821   semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
   822   by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
   823 
   824 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>"
   825   by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
   826 
   827 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>"
   828   by (metis gcd_proj1_if_dvd_int gcd.commute)
   829 
   830 text \<open>
   831   \medskip Multiplication laws
   832 \<close>
   833 
   834 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   835     \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
   836   apply (induct m n rule: gcd_nat_induct)
   837   apply simp
   838   apply (case_tac "k = 0")
   839   apply (simp_all add: gcd_non_0_nat)
   840 done
   841 
   842 lemma gcd_mult_distrib_int: "\<bar>k::int\<bar> * gcd m n = gcd (k * m) (k * n)"
   843   apply (subst (1 2) gcd_abs_int)
   844   apply (subst (1 2) abs_mult)
   845   apply (rule gcd_mult_distrib_nat [transferred])
   846   apply auto
   847 done
   848 
   849 context semiring_gcd
   850 begin
   851 
   852 lemma coprime_dvd_mult:
   853   assumes "coprime a b" and "a dvd c * b"
   854   shows "a dvd c"
   855 proof (cases "c = 0")
   856   case True then show ?thesis by simp
   857 next
   858   case False
   859   then have unit: "is_unit (unit_factor c)" by simp
   860   from \<open>coprime a b\<close> mult_gcd_left [of c a b]
   861   have "gcd (c * a) (c * b) * unit_factor c = c"
   862     by (simp add: ac_simps)
   863   moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
   864     by (simp add: dvd_mult_unit_iff unit)
   865   ultimately show ?thesis by simp
   866 qed
   867 
   868 lemma coprime_dvd_mult_iff:
   869   assumes "coprime a c"
   870   shows "a dvd b * c \<longleftrightarrow> a dvd b"
   871   using assms by (auto intro: coprime_dvd_mult)
   872 
   873 lemma gcd_mult_cancel:
   874   "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   875   apply (rule associated_eqI)
   876   apply (rule gcd_greatest)
   877   apply (rule_tac b = c in coprime_dvd_mult)
   878   apply (simp add: gcd.assoc)
   879   apply (simp_all add: ac_simps)
   880   done
   881 
   882 lemma coprime_crossproduct:
   883   fixes a b c d
   884   assumes "coprime a d" and "coprime b c"
   885   shows "normalize a * normalize c = normalize b * normalize d
   886     \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs")
   887 proof
   888   assume ?rhs then show ?lhs by simp
   889 next
   890   assume ?lhs
   891   from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
   892     by (auto intro: dvdI dest: sym)
   893   with \<open>coprime a d\<close> have "a dvd b"
   894     by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   895   from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
   896     by (auto intro: dvdI dest: sym)
   897   with \<open>coprime b c\<close> have "b dvd a"
   898     by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   899   from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
   900     by (auto intro: dvdI dest: sym simp add: mult.commute)
   901   with \<open>coprime b c\<close> have "c dvd d"
   902     by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   903   from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
   904     by (auto intro: dvdI dest: sym simp add: mult.commute)
   905   with \<open>coprime a d\<close> have "d dvd c"
   906     by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   907   from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
   908     by (rule associatedI)
   909   moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
   910     by (rule associatedI)
   911   ultimately show ?rhs ..
   912 qed
   913 
   914 end
   915 
   916 lemma coprime_crossproduct_nat:
   917   fixes a b c d :: nat
   918   assumes "coprime a d" and "coprime b c"
   919   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
   920   using assms coprime_crossproduct [of a d b c] by simp
   921 
   922 lemma coprime_crossproduct_int:
   923   fixes a b c d :: int
   924   assumes "coprime a d" and "coprime b c"
   925   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>"
   926   using assms coprime_crossproduct [of a d b c] by simp
   927 
   928 text \<open>\medskip Addition laws\<close>
   929 
   930 lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   931   apply (case_tac "n = 0")
   932   apply (simp_all add: gcd_non_0_nat)
   933   done
   934 
   935 lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   936   apply (subst (1 2) gcd.commute)
   937   apply (subst add.commute)
   938   apply simp
   939   done
   940 
   941 (* to do: add the other variations? *)
   942 
   943 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   944   by (subst gcd_add1_nat [symmetric]) auto
   945 
   946 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   947   apply (subst gcd.commute)
   948   apply (subst gcd_diff1_nat [symmetric])
   949   apply auto
   950   apply (subst gcd.commute)
   951   apply (subst gcd_diff1_nat)
   952   apply assumption
   953   apply (rule gcd.commute)
   954   done
   955 
   956 lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   957   apply (frule_tac b = y and a = x in pos_mod_sign)
   958   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   959   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
   960     zmod_zminus1_eq_if)
   961   apply (frule_tac a = x in pos_mod_bound)
   962   apply (subst (1 2) gcd.commute)
   963   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   964     nat_le_eq_zle)
   965   done
   966 
   967 lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
   968   apply (case_tac "y = 0")
   969   apply force
   970   apply (case_tac "y > 0")
   971   apply (subst gcd_non_0_int, auto)
   972   apply (insert gcd_non_0_int [of "-y" "-x"])
   973   apply auto
   974 done
   975 
   976 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
   977 by (metis gcd_red_int mod_add_self1 add.commute)
   978 
   979 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   980 by (metis gcd_add1_int gcd.commute add.commute)
   981 
   982 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   983 by (metis mod_mult_self3 gcd.commute gcd_red_nat)
   984 
   985 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   986 by (metis gcd.commute gcd_red_int mod_mult_self1 add.commute)
   987 
   988 
   989 (* to do: differences, and all variations of addition rules
   990     as simplification rules for nat and int *)
   991 
   992 lemma gcd_dvd_prod_nat: "gcd (m::nat) n dvd k * n"
   993   using mult_dvd_mono [of 1] by auto
   994 
   995 (* to do: add the three variations of these, and for ints? *)
   996 
   997 lemma finite_divisors_nat[simp]:
   998   assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
   999 proof-
  1000   have "finite{d. d <= m}"
  1001     by (blast intro: bounded_nat_set_is_finite)
  1002   from finite_subset[OF _ this] show ?thesis using assms
  1003     by (metis Collect_mono dvd_imp_le neq0_conv)
  1004 qed
  1005 
  1006 lemma finite_divisors_int[simp]:
  1007   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
  1008 proof-
  1009   have "{d. \<bar>d\<bar> <= \<bar>i\<bar>} = {- \<bar>i\<bar> .. \<bar>i\<bar>}" by(auto simp:abs_if)
  1010   hence "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}" by simp
  1011   from finite_subset[OF _ this] show ?thesis using assms
  1012     by (simp add: dvd_imp_le_int subset_iff)
  1013 qed
  1014 
  1015 lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
  1016 apply(rule antisym)
  1017  apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
  1018 apply simp
  1019 done
  1020 
  1021 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
  1022 apply(rule antisym)
  1023  apply(rule Max_le_iff [THEN iffD2])
  1024   apply (auto intro: abs_le_D1 dvd_imp_le_int)
  1025 done
  1026 
  1027 lemma gcd_is_Max_divisors_nat:
  1028   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
  1029 apply(rule Max_eqI[THEN sym])
  1030   apply (metis finite_Collect_conjI finite_divisors_nat)
  1031  apply simp
  1032  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
  1033 apply simp
  1034 done
  1035 
  1036 lemma gcd_is_Max_divisors_int:
  1037   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
  1038 apply(rule Max_eqI[THEN sym])
  1039   apply (metis finite_Collect_conjI finite_divisors_int)
  1040  apply simp
  1041  apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
  1042 apply simp
  1043 done
  1044 
  1045 lemma gcd_code_int [code]:
  1046   "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  1047   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
  1048 
  1049 
  1050 subsection \<open>Coprimality\<close>
  1051 
  1052 context semiring_gcd
  1053 begin
  1054 
  1055 lemma div_gcd_coprime:
  1056   assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
  1057   shows "coprime (a div gcd a b) (b div gcd a b)"
  1058 proof -
  1059   let ?g = "gcd a b"
  1060   let ?a' = "a div ?g"
  1061   let ?b' = "b div ?g"
  1062   let ?g' = "gcd ?a' ?b'"
  1063   have dvdg: "?g dvd a" "?g dvd b" by simp_all
  1064   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
  1065   from dvdg dvdg' obtain ka kb ka' kb' where
  1066       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
  1067     unfolding dvd_def by blast
  1068   from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
  1069     by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
  1070   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
  1071     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
  1072       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
  1073   have "?g \<noteq> 0" using nz by simp
  1074   moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
  1075   thm dvd_mult_cancel_left
  1076   ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
  1077 qed
  1078 
  1079 lemma coprime:
  1080   "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)" (is "?P \<longleftrightarrow> ?Q")
  1081 proof
  1082   assume ?P then show ?Q by auto
  1083 next
  1084   assume ?Q
  1085   then have "is_unit (gcd a b) \<longleftrightarrow> gcd a b dvd a \<and> gcd a b dvd b"
  1086     by blast
  1087   then have "is_unit (gcd a b)"
  1088     by simp
  1089   then show ?P
  1090     by simp
  1091 qed
  1092 
  1093 end
  1094 
  1095 lemma coprime_nat:
  1096   "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1097   using coprime [of a b] by simp
  1098 
  1099 lemma coprime_Suc_0_nat:
  1100   "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
  1101   using coprime_nat by simp
  1102 
  1103 lemma coprime_int:
  1104   "coprime (a::int) b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1105   using gcd_unique_int [of 1 a b]
  1106   apply clarsimp
  1107   apply (erule subst)
  1108   apply (rule iffI)
  1109   apply force
  1110   using abs_dvd_iff abs_ge_zero apply blast
  1111   done
  1112 
  1113 lemma gcd_coprime_nat:
  1114   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
  1115     b: "b = b' * gcd a b"
  1116   shows    "coprime a' b'"
  1117 
  1118   apply (subgoal_tac "a' = a div gcd a b")
  1119   apply (erule ssubst)
  1120   apply (subgoal_tac "b' = b div gcd a b")
  1121   apply (erule ssubst)
  1122   apply (rule div_gcd_coprime)
  1123   using z apply force
  1124   apply (subst (1) b)
  1125   using z apply force
  1126   apply (subst (1) a)
  1127   using z apply force
  1128   done
  1129 
  1130 lemma gcd_coprime_int:
  1131   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
  1132     b: "b = b' * gcd a b"
  1133   shows    "coprime a' b'"
  1134   apply (subgoal_tac "a' = a div gcd a b")
  1135   apply (erule ssubst)
  1136   apply (subgoal_tac "b' = b div gcd a b")
  1137   apply (erule ssubst)
  1138   apply (rule div_gcd_coprime)
  1139   using z apply force
  1140   apply (subst (1) b)
  1141   using z apply force
  1142   apply (subst (1) a)
  1143   using z apply force
  1144   done
  1145 
  1146 context semiring_gcd
  1147 begin
  1148 
  1149 lemma coprime_mult:
  1150   assumes da: "coprime d a" and db: "coprime d b"
  1151   shows "coprime d (a * b)"
  1152   apply (subst gcd.commute)
  1153   using da apply (subst gcd_mult_cancel)
  1154   apply (subst gcd.commute, assumption)
  1155   apply (subst gcd.commute, rule db)
  1156   done
  1157 
  1158 end
  1159 
  1160 lemma coprime_lmult_nat:
  1161   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
  1162 proof -
  1163   have "gcd d a dvd gcd d (a * b)"
  1164     by (rule gcd_greatest, auto)
  1165   with dab show ?thesis
  1166     by auto
  1167 qed
  1168 
  1169 lemma coprime_lmult_int:
  1170   assumes "coprime (d::int) (a * b)" shows "coprime d a"
  1171 proof -
  1172   have "gcd d a dvd gcd d (a * b)"
  1173     by (rule gcd_greatest, auto)
  1174   with assms show ?thesis
  1175     by auto
  1176 qed
  1177 
  1178 lemma coprime_rmult_nat:
  1179   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
  1180 proof -
  1181   have "gcd d b dvd gcd d (a * b)"
  1182     by (rule gcd_greatest, auto intro: dvd_mult)
  1183   with assms show ?thesis
  1184     by auto
  1185 qed
  1186 
  1187 lemma coprime_rmult_int:
  1188   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
  1189 proof -
  1190   have "gcd d b dvd gcd d (a * b)"
  1191     by (rule gcd_greatest, auto intro: dvd_mult)
  1192   with dab show ?thesis
  1193     by auto
  1194 qed
  1195 
  1196 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
  1197     coprime d a \<and>  coprime d b"
  1198   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
  1199     coprime_mult [of d a b]
  1200   by blast
  1201 
  1202 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
  1203     coprime d a \<and>  coprime d b"
  1204   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
  1205     coprime_mult [of d a b]
  1206   by blast
  1207 
  1208 lemma coprime_power_int:
  1209   assumes "0 < n" shows "coprime (a :: int) (b ^ n) \<longleftrightarrow> coprime a b"
  1210   using assms
  1211 proof (induct n)
  1212   case (Suc n) then show ?case
  1213     by (cases n) (simp_all add: coprime_mul_eq_int)
  1214 qed simp
  1215 
  1216 lemma gcd_coprime_exists_nat:
  1217     assumes nz: "gcd (a::nat) b \<noteq> 0"
  1218     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
  1219   apply (rule_tac x = "a div gcd a b" in exI)
  1220   apply (rule_tac x = "b div gcd a b" in exI)
  1221   using nz apply (auto simp add: div_gcd_coprime dvd_div_mult)
  1222 done
  1223 
  1224 lemma gcd_coprime_exists_int:
  1225     assumes nz: "gcd (a::int) b \<noteq> 0"
  1226     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
  1227   apply (rule_tac x = "a div gcd a b" in exI)
  1228   apply (rule_tac x = "b div gcd a b" in exI)
  1229   using nz apply (auto simp add: div_gcd_coprime)
  1230 done
  1231 
  1232 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
  1233   by (induct n) (simp_all add: coprime_mult)
  1234 
  1235 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
  1236   by (induct n) (simp_all add: coprime_mult)
  1237 
  1238 context semiring_gcd
  1239 begin
  1240 
  1241 lemma coprime_exp_left:
  1242   assumes "coprime a b"
  1243   shows "coprime (a ^ n) b"
  1244   using assms by (induct n) (simp_all add: gcd_mult_cancel)
  1245 
  1246 lemma coprime_exp2:
  1247   assumes "coprime a b"
  1248   shows "coprime (a ^ n) (b ^ m)"
  1249 proof (rule coprime_exp_left)
  1250   from assms show "coprime a (b ^ m)"
  1251     by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
  1252 qed
  1253 
  1254 end
  1255 
  1256 lemma gcd_exp_nat:
  1257   "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
  1258 proof (cases "a = 0 \<and> b = 0")
  1259   case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power)
  1260 next
  1261   case False
  1262   then have "coprime (a div gcd a b) (b div gcd a b)"
  1263     by (auto simp: div_gcd_coprime)
  1264   then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
  1265     by (simp add: coprime_exp2)
  1266   then have "gcd ((a div gcd a b)^n * (gcd a b)^n)
  1267       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
  1268     by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
  1269   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
  1270     by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
  1271   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
  1272     by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
  1273   finally show ?thesis .
  1274 qed
  1275 
  1276 lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
  1277   apply (subst (1 2) gcd_abs_int)
  1278   apply (subst (1 2) power_abs)
  1279   apply (rule gcd_exp_nat [where n = n, transferred])
  1280   apply auto
  1281 done
  1282 
  1283 lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
  1284   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  1285 proof-
  1286   let ?g = "gcd a b"
  1287   {assume "?g = 0" with dc have ?thesis by auto}
  1288   moreover
  1289   {assume z: "?g \<noteq> 0"
  1290     from gcd_coprime_exists_nat[OF z]
  1291     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1292       by blast
  1293     have thb: "?g dvd b" by auto
  1294     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
  1295     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
  1296     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
  1297     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
  1298     with z have th_1: "a' dvd b' * c" by auto
  1299     from coprime_dvd_mult [OF ab'(3)] th_1
  1300     have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
  1301     from ab' have "a = ?g*a'" by algebra
  1302     with thb thc have ?thesis by blast }
  1303   ultimately show ?thesis by blast
  1304 qed
  1305 
  1306 lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
  1307   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  1308 proof-
  1309   let ?g = "gcd a b"
  1310   {assume "?g = 0" with dc have ?thesis by auto}
  1311   moreover
  1312   {assume z: "?g \<noteq> 0"
  1313     from gcd_coprime_exists_int[OF z]
  1314     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1315       by blast
  1316     have thb: "?g dvd b" by auto
  1317     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
  1318     with dc have th0: "a' dvd b*c"
  1319       using dvd_trans[of a' a "b*c"] by simp
  1320     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
  1321     hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
  1322     with z have th_1: "a' dvd b' * c" by auto
  1323     from coprime_dvd_mult [OF ab'(3)] th_1
  1324     have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
  1325     from ab' have "a = ?g*a'" by algebra
  1326     with thb thc have ?thesis by blast }
  1327   ultimately show ?thesis by blast
  1328 qed
  1329 
  1330 lemma pow_divides_pow_nat:
  1331   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
  1332   shows "a dvd b"
  1333 proof-
  1334   let ?g = "gcd a b"
  1335   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
  1336   {assume "?g = 0" with ab n have ?thesis by auto }
  1337   moreover
  1338   {assume z: "?g \<noteq> 0"
  1339     hence zn: "?g ^ n \<noteq> 0" using n by simp
  1340     from gcd_coprime_exists_nat[OF z]
  1341     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1342       by blast
  1343     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
  1344       by (simp add: ab'(1,2)[symmetric])
  1345     hence "?g^n*a'^n dvd ?g^n *b'^n"
  1346       by (simp only: power_mult_distrib mult.commute)
  1347     then have th0: "a'^n dvd b'^n"
  1348       using zn by auto
  1349     have "a' dvd a'^n" by (simp add: m)
  1350     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
  1351     hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
  1352     from coprime_dvd_mult [OF coprime_exp_nat [OF ab'(3), of m]] th1
  1353     have "a' dvd b'" by (subst (asm) mult.commute, blast)
  1354     hence "a'*?g dvd b'*?g" by simp
  1355     with ab'(1,2)  have ?thesis by simp }
  1356   ultimately show ?thesis by blast
  1357 qed
  1358 
  1359 lemma pow_divides_pow_int:
  1360   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
  1361   shows "a dvd b"
  1362 proof-
  1363   let ?g = "gcd a b"
  1364   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
  1365   {assume "?g = 0" with ab n have ?thesis by auto }
  1366   moreover
  1367   {assume z: "?g \<noteq> 0"
  1368     hence zn: "?g ^ n \<noteq> 0" using n by simp
  1369     from gcd_coprime_exists_int[OF z]
  1370     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1371       by blast
  1372     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
  1373       by (simp add: ab'(1,2)[symmetric])
  1374     hence "?g^n*a'^n dvd ?g^n *b'^n"
  1375       by (simp only: power_mult_distrib mult.commute)
  1376     with zn z n have th0:"a'^n dvd b'^n" by auto
  1377     have "a' dvd a'^n" by (simp add: m)
  1378     with th0 have "a' dvd b'^n"
  1379       using dvd_trans[of a' "a'^n" "b'^n"] by simp
  1380     hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
  1381     from coprime_dvd_mult [OF coprime_exp_int [OF ab'(3), of m]] th1
  1382     have "a' dvd b'" by (subst (asm) mult.commute, blast)
  1383     hence "a'*?g dvd b'*?g" by simp
  1384     with ab'(1,2)  have ?thesis by simp }
  1385   ultimately show ?thesis by blast
  1386 qed
  1387 
  1388 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
  1389   by (auto intro: pow_divides_pow_nat dvd_power_same)
  1390 
  1391 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
  1392   by (auto intro: pow_divides_pow_int dvd_power_same)
  1393 
  1394 lemma divides_mult_nat:
  1395   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
  1396   shows "m * n dvd r"
  1397 proof-
  1398   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
  1399     unfolding dvd_def by blast
  1400   from mr n' have "m dvd n'*n" by (simp add: mult.commute)
  1401   hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
  1402   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
  1403   from n' k show ?thesis unfolding dvd_def by auto
  1404 qed
  1405 
  1406 lemma divides_mult_int:
  1407   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
  1408   shows "m * n dvd r"
  1409 proof-
  1410   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
  1411     unfolding dvd_def by blast
  1412   from mr n' have "m dvd n'*n" by (simp add: mult.commute)
  1413   hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
  1414   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
  1415   from n' k show ?thesis unfolding dvd_def by auto
  1416 qed
  1417 
  1418 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
  1419   by (simp add: gcd.commute del: One_nat_def)
  1420 
  1421 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
  1422   using coprime_plus_one_nat by simp
  1423 
  1424 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
  1425   by (simp add: gcd.commute)
  1426 
  1427 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
  1428   using coprime_plus_one_nat [of "n - 1"]
  1429     gcd.commute [of "n - 1" n] by auto
  1430 
  1431 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
  1432   using coprime_plus_one_int [of "n - 1"]
  1433     gcd.commute [of "n - 1" n] by auto
  1434 
  1435 lemma setprod_coprime_nat:
  1436   fixes x :: nat
  1437   shows "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>A. f i) x"
  1438   by (induct A rule: infinite_finite_induct)
  1439     (auto simp add: gcd_mult_cancel One_nat_def [symmetric] simp del: One_nat_def)
  1440 
  1441 lemma setprod_coprime_int:
  1442   fixes x :: int
  1443   shows "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>A. f i) x"
  1444   by (induct A rule: infinite_finite_induct)
  1445     (auto simp add: gcd_mult_cancel)
  1446 
  1447 lemma coprime_common_divisor_nat: 
  1448   "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
  1449   by (metis gcd_greatest_iff nat_dvd_1_iff_1)
  1450 
  1451 lemma coprime_common_divisor_int:
  1452   "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
  1453   using gcd_greatest_iff [of x a b] by auto
  1454 
  1455 lemma coprime_divisors_nat:
  1456     "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
  1457   by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
  1458 
  1459 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1460 by (metis coprime_lmult_nat gcd_1_nat gcd.commute gcd_red_nat)
  1461 
  1462 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1463 by (metis coprime_lmult_int gcd_1_int gcd.commute gcd_red_int)
  1464 
  1465 
  1466 subsection \<open>Bezout's theorem\<close>
  1467 
  1468 (* Function bezw returns a pair of witnesses to Bezout's theorem --
  1469    see the theorems that follow the definition. *)
  1470 fun
  1471   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1472 where
  1473   "bezw x y =
  1474   (if y = 0 then (1, 0) else
  1475       (snd (bezw y (x mod y)),
  1476        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1477 
  1478 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1479 
  1480 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1481        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1482   by simp
  1483 
  1484 declare bezw.simps [simp del]
  1485 
  1486 lemma bezw_aux [rule_format]:
  1487     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1488 proof (induct x y rule: gcd_nat_induct)
  1489   fix m :: nat
  1490   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1491     by auto
  1492   next fix m :: nat and n
  1493     assume ngt0: "n > 0" and
  1494       ih: "fst (bezw n (m mod n)) * int n +
  1495         snd (bezw n (m mod n)) * int (m mod n) =
  1496         int (gcd n (m mod n))"
  1497     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1498       apply (simp add: bezw_non_0 gcd_non_0_nat)
  1499       apply (erule subst)
  1500       apply (simp add: field_simps)
  1501       apply (subst mod_div_equality [of m n, symmetric])
  1502       (* applying simp here undoes the last substitution!
  1503          what is procedure cancel_div_mod? *)
  1504       apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
  1505       done
  1506 qed
  1507 
  1508 lemma bezout_int:
  1509   fixes x y
  1510   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1511 proof -
  1512   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1513       EX u v. u * x + v * y = gcd x y"
  1514     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1515     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1516     apply (unfold gcd_int_def)
  1517     apply simp
  1518     apply (subst bezw_aux [symmetric])
  1519     apply auto
  1520     done
  1521   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1522       (x \<le> 0 \<and> y \<le> 0)"
  1523     by auto
  1524   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1525     by (erule (1) bezout_aux)
  1526   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1527     apply (insert bezout_aux [of x "-y"])
  1528     apply auto
  1529     apply (rule_tac x = u in exI)
  1530     apply (rule_tac x = "-v" in exI)
  1531     apply (subst gcd_neg2_int [symmetric])
  1532     apply auto
  1533     done
  1534   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1535     apply (insert bezout_aux [of "-x" y])
  1536     apply auto
  1537     apply (rule_tac x = "-u" in exI)
  1538     apply (rule_tac x = v in exI)
  1539     apply (subst gcd_neg1_int [symmetric])
  1540     apply auto
  1541     done
  1542   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1543     apply (insert bezout_aux [of "-x" "-y"])
  1544     apply auto
  1545     apply (rule_tac x = "-u" in exI)
  1546     apply (rule_tac x = "-v" in exI)
  1547     apply (subst gcd_neg1_int [symmetric])
  1548     apply (subst gcd_neg2_int [symmetric])
  1549     apply auto
  1550     done
  1551   ultimately show ?thesis by blast
  1552 qed
  1553 
  1554 text \<open>versions of Bezout for nat, by Amine Chaieb\<close>
  1555 
  1556 lemma ind_euclid:
  1557   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1558   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1559   shows "P a b"
  1560 proof(induct "a + b" arbitrary: a b rule: less_induct)
  1561   case less
  1562   have "a = b \<or> a < b \<or> b < a" by arith
  1563   moreover {assume eq: "a= b"
  1564     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1565     by simp}
  1566   moreover
  1567   {assume lt: "a < b"
  1568     hence "a + b - a < a + b \<or> a = 0" by arith
  1569     moreover
  1570     {assume "a =0" with z c have "P a b" by blast }
  1571     moreover
  1572     {assume "a + b - a < a + b"
  1573       also have th0: "a + b - a = a + (b - a)" using lt by arith
  1574       finally have "a + (b - a) < a + b" .
  1575       then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
  1576       then have "P a b" by (simp add: th0[symmetric])}
  1577     ultimately have "P a b" by blast}
  1578   moreover
  1579   {assume lt: "a > b"
  1580     hence "b + a - b < a + b \<or> b = 0" by arith
  1581     moreover
  1582     {assume "b =0" with z c have "P a b" by blast }
  1583     moreover
  1584     {assume "b + a - b < a + b"
  1585       also have th0: "b + a - b = b + (a - b)" using lt by arith
  1586       finally have "b + (a - b) < a + b" .
  1587       then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
  1588       then have "P b a" by (simp add: th0[symmetric])
  1589       hence "P a b" using c by blast }
  1590     ultimately have "P a b" by blast}
  1591 ultimately  show "P a b" by blast
  1592 qed
  1593 
  1594 lemma bezout_lemma_nat:
  1595   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1596     (a * x = b * y + d \<or> b * x = a * y + d)"
  1597   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1598     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1599   using ex
  1600   apply clarsimp
  1601   apply (rule_tac x="d" in exI, simp)
  1602   apply (case_tac "a * x = b * y + d" , simp_all)
  1603   apply (rule_tac x="x + y" in exI)
  1604   apply (rule_tac x="y" in exI)
  1605   apply algebra
  1606   apply (rule_tac x="x" in exI)
  1607   apply (rule_tac x="x + y" in exI)
  1608   apply algebra
  1609 done
  1610 
  1611 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1612     (a * x = b * y + d \<or> b * x = a * y + d)"
  1613   apply(induct a b rule: ind_euclid)
  1614   apply blast
  1615   apply clarify
  1616   apply (rule_tac x="a" in exI, simp)
  1617   apply clarsimp
  1618   apply (rule_tac x="d" in exI)
  1619   apply (case_tac "a * x = b * y + d", simp_all)
  1620   apply (rule_tac x="x+y" in exI)
  1621   apply (rule_tac x="y" in exI)
  1622   apply algebra
  1623   apply (rule_tac x="x" in exI)
  1624   apply (rule_tac x="x+y" in exI)
  1625   apply algebra
  1626 done
  1627 
  1628 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1629     (a * x - b * y = d \<or> b * x - a * y = d)"
  1630   using bezout_add_nat[of a b]
  1631   apply clarsimp
  1632   apply (rule_tac x="d" in exI, simp)
  1633   apply (rule_tac x="x" in exI)
  1634   apply (rule_tac x="y" in exI)
  1635   apply auto
  1636 done
  1637 
  1638 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1639   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1640 proof-
  1641  from nz have ap: "a > 0" by simp
  1642  from bezout_add_nat[of a b]
  1643  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1644    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1645  moreover
  1646     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1647      from H have ?thesis by blast }
  1648  moreover
  1649  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1650    {assume b0: "b = 0" with H  have ?thesis by simp}
  1651    moreover
  1652    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1653      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1654        by auto
  1655      moreover
  1656      {assume db: "d=b"
  1657        with nz H have ?thesis apply simp
  1658          apply (rule exI[where x = b], simp)
  1659          apply (rule exI[where x = b])
  1660         by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1661     moreover
  1662     {assume db: "d < b"
  1663         {assume "x=0" hence ?thesis using nz H by simp }
  1664         moreover
  1665         {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1666           from db have "d \<le> b - 1" by simp
  1667           hence "d*b \<le> b*(b - 1)" by simp
  1668           with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1669           have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1670           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1671             by simp
  1672           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1673             by (simp only: mult.assoc distrib_left)
  1674           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1675             by algebra
  1676           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1677           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1678             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1679           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1680             by (simp only: diff_mult_distrib2 ac_simps)
  1681           hence ?thesis using H(1,2)
  1682             apply -
  1683             apply (rule exI[where x=d], simp)
  1684             apply (rule exI[where x="(b - 1) * y"])
  1685             by (rule exI[where x="x*(b - 1) - d"], simp)}
  1686         ultimately have ?thesis by blast}
  1687     ultimately have ?thesis by blast}
  1688   ultimately have ?thesis by blast}
  1689  ultimately show ?thesis by blast
  1690 qed
  1691 
  1692 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1693   shows "\<exists>x y. a * x = b * y + gcd a b"
  1694 proof-
  1695   let ?g = "gcd a b"
  1696   from bezout_add_strong_nat[OF a, of b]
  1697   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1698   from d(1,2) have "d dvd ?g" by simp
  1699   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1700   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1701   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1702   thus ?thesis by blast
  1703 qed
  1704 
  1705 
  1706 subsection \<open>LCM properties  on @{typ nat} and @{typ int}\<close>
  1707 
  1708 lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  1709   by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
  1710 
  1711 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1712   unfolding lcm_nat_def
  1713   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1714 
  1715 lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
  1716   unfolding lcm_int_def gcd_int_def
  1717   apply (subst int_mult [symmetric])
  1718   apply (subst prod_gcd_lcm_nat [symmetric])
  1719   apply (subst nat_abs_mult_distrib [symmetric])
  1720   apply (simp, simp add: abs_mult)
  1721 done
  1722 
  1723 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1724   unfolding lcm_nat_def by simp
  1725 
  1726 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1727   unfolding lcm_int_def by simp
  1728 
  1729 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1730   unfolding lcm_nat_def by simp
  1731 
  1732 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1733   unfolding lcm_int_def by simp
  1734 
  1735 lemma lcm_pos_nat:
  1736   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1737 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1738 
  1739 lemma lcm_pos_int:
  1740   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1741   apply (subst lcm_abs_int)
  1742   apply (rule lcm_pos_nat [transferred])
  1743   apply auto
  1744   done
  1745 
  1746 lemma dvd_pos_nat:
  1747   fixes n m :: nat
  1748   assumes "n > 0" and "m dvd n"
  1749   shows "m > 0"
  1750   using assms by (cases m) auto
  1751 
  1752 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1753     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1754   by (auto intro: dvd_antisym lcm_least)
  1755 
  1756 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1757     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1758   using lcm_least zdvd_antisym_nonneg by auto
  1759 
  1760 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1761   apply (rule sym)
  1762   apply (subst lcm_unique_nat [symmetric])
  1763   apply auto
  1764 done
  1765 
  1766 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
  1767   apply (rule sym)
  1768   apply (subst lcm_unique_int [symmetric])
  1769   apply auto
  1770 done
  1771 
  1772 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1773 by (subst lcm.commute, erule lcm_proj2_if_dvd_nat)
  1774 
  1775 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
  1776 by (subst lcm.commute, erule lcm_proj2_if_dvd_int)
  1777 
  1778 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1779 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1780 
  1781 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1782 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1783 
  1784 lemma lcm_proj1_iff_int[simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
  1785 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1786 
  1787 lemma lcm_proj2_iff_int[simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
  1788 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1789 
  1790 lemma (in semiring_gcd) comp_fun_idem_gcd:
  1791   "comp_fun_idem gcd"
  1792   by standard (simp_all add: fun_eq_iff ac_simps)
  1793 
  1794 lemma (in semiring_gcd) comp_fun_idem_lcm:
  1795   "comp_fun_idem lcm"
  1796   by standard (simp_all add: fun_eq_iff ac_simps)
  1797 
  1798 lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
  1799   by (simp only: lcm_eq_1_iff) simp
  1800   
  1801 lemma lcm_1_iff_int [simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  1802   by auto
  1803 
  1804 
  1805 subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
  1806 
  1807 text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
  1808 Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
  1809 \<close>
  1810 
  1811 instantiation nat :: semiring_Gcd
  1812 begin
  1813 
  1814 interpretation semilattice_neutr_set lcm "1::nat"
  1815   by standard simp_all
  1816 
  1817 definition
  1818   "Lcm (M::nat set) = (if finite M then F M else 0)"
  1819 
  1820 lemma Lcm_nat_empty:
  1821   "Lcm {} = (1::nat)"
  1822   by (simp add: Lcm_nat_def del: One_nat_def)
  1823 
  1824 lemma Lcm_nat_insert:
  1825   "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
  1826   by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
  1827 
  1828 lemma Lcm_nat_infinite:
  1829   "infinite M \<Longrightarrow> Lcm M = (0::nat)"
  1830   by (simp add: Lcm_nat_def)
  1831 
  1832 lemma dvd_Lcm_nat [simp]:
  1833   fixes M :: "nat set"
  1834   assumes "m \<in> M"
  1835   shows "m dvd Lcm M"
  1836 proof -
  1837   from assms have "insert m M = M" by auto
  1838   moreover have "m dvd Lcm (insert m M)"
  1839     by (simp add: Lcm_nat_insert)
  1840   ultimately show ?thesis by simp
  1841 qed
  1842 
  1843 lemma Lcm_dvd_nat [simp]:
  1844   fixes M :: "nat set"
  1845   assumes "\<forall>m\<in>M. m dvd n"
  1846   shows "Lcm M dvd n"
  1847 proof (cases "n = 0")
  1848   case True then show ?thesis by simp
  1849 next
  1850   case False
  1851   then have "finite {d. d dvd n}" by (rule finite_divisors_nat)
  1852   moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
  1853   ultimately have "finite M" by (rule rev_finite_subset)
  1854   then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
  1855 qed
  1856 
  1857 definition
  1858   "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
  1859 
  1860 instance proof
  1861   show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
  1862   using that by (induct N rule: infinite_finite_induct)
  1863     (auto simp add: Gcd_nat_def)
  1864   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
  1865   using that by (induct N rule: infinite_finite_induct)
  1866     (auto simp add: Gcd_nat_def)
  1867   show "n dvd Lcm N" if "n \<in> N" for N and n ::nat
  1868   using that by (induct N rule: infinite_finite_induct)
  1869     auto
  1870   show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n" for N and n ::nat
  1871   using that by (induct N rule: infinite_finite_induct)
  1872     auto
  1873 qed simp_all
  1874 
  1875 end
  1876 
  1877 text\<open>Alternative characterizations of Gcd:\<close>
  1878 
  1879 lemma Gcd_eq_Max: "finite(M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> Gcd M = Max(\<Inter>m\<in>M. {d. d dvd m})"
  1880 apply(rule antisym)
  1881  apply(rule Max_ge)
  1882   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1883  apply (simp add: Gcd_dvd)
  1884 apply (rule Max_le_iff[THEN iffD2])
  1885   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1886  apply fastforce
  1887 apply clarsimp
  1888 apply (metis Gcd_dvd Max_in dvd_0_left dvd_Gcd dvd_imp_le linorder_antisym_conv3 not_less0)
  1889 done
  1890 
  1891 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
  1892 apply(induct pred:finite)
  1893  apply simp
  1894 apply(case_tac "x=0")
  1895  apply simp
  1896 apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
  1897  apply simp
  1898 apply blast
  1899 done
  1900 
  1901 lemma Lcm_in_lcm_closed_set_nat:
  1902   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
  1903 apply(induct rule:finite_linorder_min_induct)
  1904  apply simp
  1905 apply simp
  1906 apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
  1907  apply simp
  1908  apply(case_tac "A={}")
  1909   apply simp
  1910  apply simp
  1911 apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  1912 done
  1913 
  1914 lemma Lcm_eq_Max_nat:
  1915   "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"
  1916 apply(rule antisym)
  1917  apply(rule Max_ge, assumption)
  1918  apply(erule (2) Lcm_in_lcm_closed_set_nat)
  1919 apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
  1920 done
  1921 
  1922 lemma mult_inj_if_coprime_nat:
  1923   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
  1924    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
  1925   by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
  1926 
  1927 text\<open>Nitpick:\<close>
  1928 
  1929 lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
  1930 by (induct x y rule: nat_gcd.induct)
  1931    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  1932 
  1933 lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
  1934 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  1935 
  1936 
  1937 subsubsection \<open>Setwise gcd and lcm for integers\<close>
  1938 
  1939 instantiation int :: semiring_Gcd
  1940 begin
  1941 
  1942 definition
  1943   "Lcm M = int (Lcm (nat ` abs ` M))"
  1944 
  1945 definition
  1946   "Gcd M = int (Gcd (nat ` abs ` M))"
  1947 
  1948 instance by standard
  1949   (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
  1950     Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
  1951 
  1952 end
  1953 
  1954 
  1955 subsection \<open>GCD and LCM on @{typ integer}\<close>
  1956 
  1957 instantiation integer :: gcd
  1958 begin
  1959 
  1960 context
  1961   includes integer.lifting
  1962 begin
  1963 
  1964 lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
  1965   is gcd .
  1966 lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
  1967   is lcm .
  1968 
  1969 end
  1970 instance ..
  1971 
  1972 end
  1973 
  1974 lifting_update integer.lifting
  1975 lifting_forget integer.lifting
  1976 
  1977 context
  1978   includes integer.lifting
  1979 begin
  1980 
  1981 lemma gcd_code_integer [code]:
  1982   "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  1983   by transfer (fact gcd_code_int)
  1984 
  1985 lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  1986   by transfer (fact lcm_altdef_int)
  1987 
  1988 end
  1989 
  1990 code_printing constant "gcd :: integer \<Rightarrow> _"
  1991   \<rightharpoonup> (OCaml) "Big'_int.gcd'_big'_int"
  1992   and (Haskell) "Prelude.gcd"
  1993   and (Scala) "_.gcd'((_)')"
  1994   \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
  1995 
  1996 text \<open>Some code equations\<close>
  1997 
  1998 lemma Lcm_set_nat [code, code_unfold]:
  1999   "Lcm (set ns) = fold lcm ns (1::nat)"
  2000   using Lcm_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  2001 
  2002 lemma Gcd_set_nat [code]:
  2003   "Gcd (set ns) = fold gcd ns (0::nat)"
  2004   using Gcd_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  2005 
  2006 lemma Lcm_set_int [code, code_unfold]:
  2007   "Lcm (set xs) = fold lcm xs (1::int)"
  2008   using Lcm_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  2009 
  2010 lemma Gcd_set_int [code]:
  2011   "Gcd (set xs) = fold gcd xs (0::int)"
  2012   using Gcd_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  2013 
  2014 text \<open>Fact aliasses\<close>
  2015 
  2016 lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
  2017   by (fact dvd_int_unfold_dvd_nat)
  2018 
  2019 lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
  2020 lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
  2021 lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
  2022 lemmas gcd_commute_int = gcd.commute [where ?'a = int]
  2023 lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
  2024 lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
  2025 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
  2026 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
  2027 lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
  2028 lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
  2029 lemmas gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
  2030 lemmas gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
  2031 lemmas gcd_greatest_nat = gcd_greatest [where ?'a = nat]
  2032 lemmas gcd_greatest_int = gcd_greatest [where ?'a = int]
  2033 lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
  2034 lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
  2035 lemmas gcd_greatest_iff_nat = gcd_greatest_iff [where ?'a = nat]
  2036 lemmas gcd_greatest_iff_int = gcd_greatest_iff [where ?'a = int]
  2037 lemmas gcd_zero_nat = gcd_eq_0_iff [where ?'a = nat]
  2038 lemmas gcd_zero_int = gcd_eq_0_iff [where ?'a = int]
  2039 
  2040 lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
  2041 lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
  2042 lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
  2043 lemmas lcm_commute_int = lcm.commute [where ?'a = int]
  2044 lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
  2045 lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
  2046 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  2047 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  2048 lemmas lcm_dvd1_nat = dvd_lcm1 [where ?'a = nat]
  2049 lemmas lcm_dvd1_int = dvd_lcm1 [where ?'a = int]
  2050 lemmas lcm_dvd2_nat = dvd_lcm2 [where ?'a = nat]
  2051 lemmas lcm_dvd2_int = dvd_lcm2 [where ?'a = int]
  2052 lemmas lcm_least_nat = lcm_least [where ?'a = nat]
  2053 lemmas lcm_least_int = lcm_least [where ?'a = int]
  2054 
  2055 lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n= 0"
  2056   by (fact lcm_eq_0_iff)
  2057 
  2058 lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
  2059   by (fact lcm_eq_0_iff)
  2060 
  2061 lemma dvd_lcm_I1_nat [simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  2062   by (fact dvd_lcmI1)
  2063 
  2064 lemma dvd_lcm_I2_nat [simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  2065   by (fact dvd_lcmI2)
  2066 
  2067 lemma dvd_lcm_I1_int [simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  2068   by (fact dvd_lcmI1)
  2069 
  2070 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  2071   by (fact dvd_lcmI2)
  2072 
  2073 lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
  2074 lemmas coprime_mult_int = coprime_mult [where ?'a = int]
  2075 lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
  2076 lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
  2077 lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
  2078 lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
  2079 
  2080 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
  2081     (k dvd m * n) = (k dvd m)"
  2082   by (fact coprime_dvd_mult_iff)
  2083 
  2084 lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
  2085     (k dvd m * n) = (k dvd m)"
  2086   by (fact coprime_dvd_mult_iff)
  2087 
  2088 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
  2089   by (fact coprime_exp2)
  2090 
  2091 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
  2092   by (fact coprime_exp2)
  2093 
  2094 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
  2095 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
  2096 lemmas dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
  2097 lemmas dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
  2098 lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
  2099 lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
  2100 lemmas Gcd_insert_nat = Gcd_insert [where ?'a = nat]
  2101 lemmas Gcd_insert_int = Gcd_insert [where ?'a = int]
  2102 
  2103 lemma dvd_Lcm_int [simp]:
  2104   fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
  2105   using assms by (fact dvd_Lcm)
  2106 
  2107 lemma Lcm_empty_nat:
  2108   "Lcm {} = (1::nat)"
  2109   by (fact Lcm_empty)
  2110 
  2111 lemma Lcm_empty_int:
  2112   "Lcm {} = (1::int)"
  2113   by (fact Lcm_empty)
  2114 
  2115 lemma Lcm_insert_nat:
  2116   "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
  2117   by (fact Lcm_insert)
  2118 
  2119 lemma Lcm_insert_int:
  2120   "Lcm (insert (n::int) N) = lcm n (Lcm N)"
  2121   by (fact Lcm_insert)
  2122 
  2123 lemma gcd_neg_numeral_1_int [simp]:
  2124   "gcd (- numeral n :: int) x = gcd (numeral n) x"
  2125   by (fact gcd_neg1_int)
  2126 
  2127 lemma gcd_neg_numeral_2_int [simp]:
  2128   "gcd x (- numeral n :: int) = gcd x (numeral n)"
  2129   by (fact gcd_neg2_int)
  2130 
  2131 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
  2132   by (fact gcd_nat.absorb1)
  2133 
  2134 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
  2135   by (fact gcd_nat.absorb2)
  2136 
  2137 lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  2138   by (fact comp_fun_idem_gcd)
  2139 
  2140 lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  2141   by (fact comp_fun_idem_gcd)
  2142 
  2143 lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  2144   by (fact comp_fun_idem_lcm)
  2145 
  2146 lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  2147   by (fact comp_fun_idem_lcm)
  2148 
  2149 lemma Lcm_eq_0 [simp]:
  2150   "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
  2151   by (rule Lcm_eq_0_I)
  2152 
  2153 lemma Lcm0_iff [simp]:
  2154   fixes M :: "nat set"
  2155   assumes "finite M" and "M \<noteq> {}"
  2156   shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
  2157   using assms by (simp add: Lcm_0_iff)
  2158 
  2159 lemma Lcm_dvd_int [simp]:
  2160   fixes M :: "int set"
  2161   assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
  2162   using assms by (auto intro: Lcm_least)
  2163 
  2164 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
  2165   by (fact dvd_gcdD1)
  2166 
  2167 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
  2168   by (fact dvd_gcdD2)
  2169 
  2170 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
  2171   by (fact dvd_gcdD1)
  2172 
  2173 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
  2174   by (fact dvd_gcdD2)
  2175 
  2176 interpretation dvd:
  2177   order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> m \<noteq> n"
  2178   by standard (auto intro: dvd_refl dvd_trans dvd_antisym)
  2179 
  2180 interpretation gcd_semilattice_nat:
  2181   semilattice_inf gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
  2182   by standard (auto dest: dvd_antisym dvd_trans)
  2183 
  2184 interpretation lcm_semilattice_nat:
  2185   semilattice_sup lcm Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
  2186   by standard simp_all
  2187 
  2188 interpretation gcd_lcm_lattice_nat:
  2189   lattice gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n" lcm
  2190   ..
  2191 
  2192 interpretation gcd_lcm_complete_lattice_nat:
  2193   complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n" lcm 1 "0::nat"
  2194   by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
  2195 
  2196 end