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