src/HOL/GCD.thy
author haftmann
Wed Feb 17 21:51:56 2016 +0100 (2016-02-17)
changeset 62346 97f2ed240431
parent 62345 e66d7841d5a2
child 62347 2230b7047376
permissions -rw-r--r--
more theorems concerning gcd/lcm/Gcd/Lcm
     1 (*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     2                 Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
     3 
     4 
     5 This file deals with the functions gcd and lcm.  Definitions and
     6 lemmas are proved uniformly for the natural numbers and integers.
     7 
     8 This file combines and revises a number of prior developments.
     9 
    10 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    11 and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
    12 gcd, lcm, and prime for the natural numbers.
    13 
    14 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    15 extended gcd, lcm, primes to the integers. Amine Chaieb provided
    16 another extension of the notions to the integers, and added a number
    17 of results to "Primes" and "GCD". IntPrimes also defined and developed
    18 the congruence relations on the integers. The notion was extended to
    19 the natural numbers by Chaieb.
    20 
    21 Jeremy Avigad combined all of these, made everything uniform for the
    22 natural numbers and the integers, and added a number of new theorems.
    23 
    24 Tobias Nipkow cleaned up a lot.
    25 *)
    26 
    27 
    28 section \<open>Greatest common divisor and least common multiple\<close>
    29 
    30 theory GCD
    31 imports Main
    32 begin
    33 
    34 subsection \<open>Abstract GCD and LCM\<close>
    35 
    36 class gcd = zero + one + dvd +
    37   fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    38     and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    39 begin
    40 
    41 abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    42   where "coprime x y \<equiv> gcd x y = 1"
    43 
    44 end
    45 
    46 class Gcd = gcd +
    47   fixes Gcd :: "'a set \<Rightarrow> 'a"
    48     and Lcm :: "'a set \<Rightarrow> 'a"
    49 
    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 lemma Gcd_eqI:
   586   assumes "normalize a = a"
   587   assumes "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
   588     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> c dvd b) \<Longrightarrow> c dvd a"
   589   shows "Gcd A = a"
   590   using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd)
   591 
   592 lemma Lcm_eqI:
   593   assumes "normalize a = a"
   594   assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
   595     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> b dvd c) \<Longrightarrow> a dvd c"
   596   shows "Lcm A = a"
   597   using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
   598 
   599 end  
   600 
   601 
   602 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
   603 
   604 instantiation nat :: gcd
   605 begin
   606 
   607 fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   608 where "gcd_nat x y =
   609   (if y = 0 then x else gcd y (x mod y))"
   610 
   611 definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   612 where
   613   "lcm_nat x y = x * y div (gcd x y)"
   614 
   615 instance proof qed
   616 
   617 end
   618 
   619 instantiation int :: gcd
   620 begin
   621 
   622 definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
   623   where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   624 
   625 definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
   626   where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   627 
   628 instance ..
   629 
   630 end
   631 
   632 text \<open>Transfer setup\<close>
   633 
   634 lemma transfer_nat_int_gcd:
   635   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   636   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   637   unfolding gcd_int_def lcm_int_def
   638   by auto
   639 
   640 lemma transfer_nat_int_gcd_closures:
   641   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
   642   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   643   by (auto simp add: gcd_int_def lcm_int_def)
   644 
   645 declare transfer_morphism_nat_int[transfer add return:
   646     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   647 
   648 lemma transfer_int_nat_gcd:
   649   "gcd (int x) (int y) = int (gcd x y)"
   650   "lcm (int x) (int y) = int (lcm x y)"
   651   by (unfold gcd_int_def lcm_int_def, auto)
   652 
   653 lemma transfer_int_nat_gcd_closures:
   654   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   655   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   656   by (auto simp add: gcd_int_def lcm_int_def)
   657 
   658 declare transfer_morphism_int_nat[transfer add return:
   659     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   660 
   661 lemma gcd_nat_induct:
   662   fixes m n :: nat
   663   assumes "\<And>m. P m 0"
   664     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   665   shows "P m n"
   666   apply (rule gcd_nat.induct)
   667   apply (case_tac "y = 0")
   668   using assms apply simp_all
   669 done
   670 
   671 (* specific to int *)
   672 
   673 lemma gcd_eq_int_iff:
   674   "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
   675   by (simp add: gcd_int_def)
   676 
   677 lemma lcm_eq_int_iff:
   678   "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
   679   by (simp add: lcm_int_def)
   680 
   681 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
   682   by (simp add: gcd_int_def)
   683 
   684 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
   685   by (simp add: gcd_int_def)
   686 
   687 lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
   688 by(simp add: gcd_int_def)
   689 
   690 lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
   691 by (simp add: gcd_int_def)
   692 
   693 lemma gcd_abs1_int[simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
   694 by (metis abs_idempotent gcd_abs_int)
   695 
   696 lemma gcd_abs2_int[simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
   697 by (metis abs_idempotent gcd_abs_int)
   698 
   699 lemma gcd_cases_int:
   700   fixes x :: int and y
   701   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   702       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   703       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   704       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   705   shows "P (gcd x y)"
   706   by (insert assms, auto, arith)
   707 
   708 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   709   by (simp add: gcd_int_def)
   710 
   711 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
   712   by (simp add: lcm_int_def)
   713 
   714 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
   715   by (simp add: lcm_int_def)
   716 
   717 lemma lcm_abs_int: "lcm (x::int) y = lcm \<bar>x\<bar> \<bar>y\<bar>"
   718   by (simp add: lcm_int_def)
   719 
   720 lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
   721   by (simp add:lcm_int_def)
   722 
   723 lemma lcm_abs1_int[simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
   724   by (metis abs_idempotent lcm_int_def)
   725 
   726 lemma lcm_abs2_int[simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
   727   by (metis abs_idempotent lcm_int_def)
   728 
   729 lemma lcm_cases_int:
   730   fixes x :: int and y
   731   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   732       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   733       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   734       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   735   shows "P (lcm x y)"
   736   using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
   737 
   738 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   739   by (simp add: lcm_int_def)
   740 
   741 lemma gcd_0_nat: "gcd (x::nat) 0 = x"
   742   by simp
   743 
   744 lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
   745   by (unfold gcd_int_def, auto)
   746 
   747 lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
   748   by simp
   749 
   750 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = \<bar>x\<bar>"
   751   by (unfold gcd_int_def, auto)
   752 
   753 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
   754   by (case_tac "y = 0", auto)
   755 
   756 (* weaker, but useful for the simplifier *)
   757 
   758 lemma gcd_non_0_nat: "y \<noteq> (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   759   by simp
   760 
   761 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   762   by simp
   763 
   764 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   765   by simp
   766 
   767 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   768   by (simp add: gcd_int_def)
   769 
   770 lemma gcd_idem_nat: "gcd (x::nat) x = x"
   771 by simp
   772 
   773 lemma gcd_idem_int: "gcd (x::int) x = \<bar>x\<bar>"
   774 by (auto simp add: gcd_int_def)
   775 
   776 declare gcd_nat.simps [simp del]
   777 
   778 text \<open>
   779   \medskip @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.  The
   780   conjunctions don't seem provable separately.
   781 \<close>
   782 
   783 instance nat :: semiring_gcd
   784 proof
   785   fix m n :: nat
   786   show "gcd m n dvd m" and "gcd m n dvd n"
   787   proof (induct m n rule: gcd_nat_induct)
   788     fix m n :: nat
   789     assume "gcd n (m mod n) dvd m mod n" and "gcd n (m mod n) dvd n"
   790     then have "gcd n (m mod n) dvd m"
   791       by (rule dvd_mod_imp_dvd)
   792     moreover assume "0 < n"
   793     ultimately show "gcd m n dvd m"
   794       by (simp add: gcd_non_0_nat)
   795   qed (simp_all add: gcd_0_nat gcd_non_0_nat)
   796 next
   797   fix m n k :: nat
   798   assume "k dvd m" and "k dvd n"
   799   then show "k dvd gcd m n"
   800     by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
   801 qed (simp_all add: lcm_nat_def)
   802 
   803 instance int :: ring_gcd
   804   by standard
   805     (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)
   806 
   807 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   808   by (rule dvd_imp_le, auto)
   809 
   810 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   811   by (rule dvd_imp_le, auto)
   812 
   813 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   814   by (rule zdvd_imp_le, auto)
   815 
   816 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   817   by (rule zdvd_imp_le, auto)
   818 
   819 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   820   by (insert gcd_eq_0_iff [of m n], arith)
   821 
   822 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   823   by (insert gcd_eq_0_iff [of m n], insert gcd_ge_0_int [of m n], arith)
   824 
   825 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
   826     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   827   apply auto
   828   apply (rule dvd_antisym)
   829   apply (erule (1) gcd_greatest)
   830   apply auto
   831 done
   832 
   833 lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   834     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   835 apply (case_tac "d = 0")
   836  apply simp
   837 apply (rule iffI)
   838  apply (rule zdvd_antisym_nonneg)
   839  apply (auto intro: gcd_greatest)
   840 done
   841 
   842 interpretation gcd_nat:
   843   semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
   844   by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
   845 
   846 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>"
   847   by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
   848 
   849 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>"
   850   by (metis gcd_proj1_if_dvd_int gcd.commute)
   851 
   852 text \<open>
   853   \medskip Multiplication laws
   854 \<close>
   855 
   856 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   857     \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
   858   apply (induct m n rule: gcd_nat_induct)
   859   apply simp
   860   apply (case_tac "k = 0")
   861   apply (simp_all add: gcd_non_0_nat)
   862 done
   863 
   864 lemma gcd_mult_distrib_int: "\<bar>k::int\<bar> * gcd m n = gcd (k * m) (k * n)"
   865   apply (subst (1 2) gcd_abs_int)
   866   apply (subst (1 2) abs_mult)
   867   apply (rule gcd_mult_distrib_nat [transferred])
   868   apply auto
   869 done
   870 
   871 context semiring_gcd
   872 begin
   873 
   874 lemma coprime_dvd_mult:
   875   assumes "coprime a b" and "a dvd c * b"
   876   shows "a dvd c"
   877 proof (cases "c = 0")
   878   case True then show ?thesis by simp
   879 next
   880   case False
   881   then have unit: "is_unit (unit_factor c)" by simp
   882   from \<open>coprime a b\<close> mult_gcd_left [of c a b]
   883   have "gcd (c * a) (c * b) * unit_factor c = c"
   884     by (simp add: ac_simps)
   885   moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
   886     by (simp add: dvd_mult_unit_iff unit)
   887   ultimately show ?thesis by simp
   888 qed
   889 
   890 lemma coprime_dvd_mult_iff:
   891   assumes "coprime a c"
   892   shows "a dvd b * c \<longleftrightarrow> a dvd b"
   893   using assms by (auto intro: coprime_dvd_mult)
   894 
   895 lemma gcd_mult_cancel:
   896   "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   897   apply (rule associated_eqI)
   898   apply (rule gcd_greatest)
   899   apply (rule_tac b = c in coprime_dvd_mult)
   900   apply (simp add: gcd.assoc)
   901   apply (simp_all add: ac_simps)
   902   done
   903 
   904 lemma coprime_crossproduct:
   905   fixes a b c d
   906   assumes "coprime a d" and "coprime b c"
   907   shows "normalize a * normalize c = normalize b * normalize d
   908     \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs")
   909 proof
   910   assume ?rhs then show ?lhs by simp
   911 next
   912   assume ?lhs
   913   from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
   914     by (auto intro: dvdI dest: sym)
   915   with \<open>coprime a d\<close> have "a dvd b"
   916     by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   917   from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
   918     by (auto intro: dvdI dest: sym)
   919   with \<open>coprime b c\<close> have "b dvd a"
   920     by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   921   from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
   922     by (auto intro: dvdI dest: sym simp add: mult.commute)
   923   with \<open>coprime b c\<close> have "c dvd d"
   924     by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   925   from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
   926     by (auto intro: dvdI dest: sym simp add: mult.commute)
   927   with \<open>coprime a d\<close> have "d dvd c"
   928     by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   929   from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
   930     by (rule associatedI)
   931   moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
   932     by (rule associatedI)
   933   ultimately show ?rhs ..
   934 qed
   935 
   936 end
   937 
   938 lemma coprime_crossproduct_nat:
   939   fixes a b c d :: nat
   940   assumes "coprime a d" and "coprime b c"
   941   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
   942   using assms coprime_crossproduct [of a d b c] by simp
   943 
   944 lemma coprime_crossproduct_int:
   945   fixes a b c d :: int
   946   assumes "coprime a d" and "coprime b c"
   947   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>"
   948   using assms coprime_crossproduct [of a d b c] by simp
   949 
   950 text \<open>\medskip Addition laws\<close>
   951 
   952 lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   953   apply (case_tac "n = 0")
   954   apply (simp_all add: gcd_non_0_nat)
   955   done
   956 
   957 lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   958   apply (subst (1 2) gcd.commute)
   959   apply (subst add.commute)
   960   apply simp
   961   done
   962 
   963 (* to do: add the other variations? *)
   964 
   965 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   966   by (subst gcd_add1_nat [symmetric]) auto
   967 
   968 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   969   apply (subst gcd.commute)
   970   apply (subst gcd_diff1_nat [symmetric])
   971   apply auto
   972   apply (subst gcd.commute)
   973   apply (subst gcd_diff1_nat)
   974   apply assumption
   975   apply (rule gcd.commute)
   976   done
   977 
   978 lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   979   apply (frule_tac b = y and a = x in pos_mod_sign)
   980   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   981   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
   982     zmod_zminus1_eq_if)
   983   apply (frule_tac a = x in pos_mod_bound)
   984   apply (subst (1 2) gcd.commute)
   985   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   986     nat_le_eq_zle)
   987   done
   988 
   989 lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
   990   apply (case_tac "y = 0")
   991   apply force
   992   apply (case_tac "y > 0")
   993   apply (subst gcd_non_0_int, auto)
   994   apply (insert gcd_non_0_int [of "-y" "-x"])
   995   apply auto
   996 done
   997 
   998 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
   999 by (metis gcd_red_int mod_add_self1 add.commute)
  1000 
  1001 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
  1002 by (metis gcd_add1_int gcd.commute add.commute)
  1003 
  1004 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
  1005 by (metis mod_mult_self3 gcd.commute gcd_red_nat)
  1006 
  1007 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
  1008 by (metis gcd.commute gcd_red_int mod_mult_self1 add.commute)
  1009 
  1010 
  1011 (* to do: differences, and all variations of addition rules
  1012     as simplification rules for nat and int *)
  1013 
  1014 lemma gcd_dvd_prod_nat: "gcd (m::nat) n dvd k * n"
  1015   using mult_dvd_mono [of 1] by auto
  1016 
  1017 (* to do: add the three variations of these, and for ints? *)
  1018 
  1019 lemma finite_divisors_nat[simp]:
  1020   assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
  1021 proof-
  1022   have "finite{d. d <= m}"
  1023     by (blast intro: bounded_nat_set_is_finite)
  1024   from finite_subset[OF _ this] show ?thesis using assms
  1025     by (metis Collect_mono dvd_imp_le neq0_conv)
  1026 qed
  1027 
  1028 lemma finite_divisors_int[simp]:
  1029   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
  1030 proof-
  1031   have "{d. \<bar>d\<bar> <= \<bar>i\<bar>} = {- \<bar>i\<bar> .. \<bar>i\<bar>}" by(auto simp:abs_if)
  1032   hence "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}" by simp
  1033   from finite_subset[OF _ this] show ?thesis using assms
  1034     by (simp add: dvd_imp_le_int subset_iff)
  1035 qed
  1036 
  1037 lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
  1038 apply(rule antisym)
  1039  apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
  1040 apply simp
  1041 done
  1042 
  1043 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
  1044 apply(rule antisym)
  1045  apply(rule Max_le_iff [THEN iffD2])
  1046   apply (auto intro: abs_le_D1 dvd_imp_le_int)
  1047 done
  1048 
  1049 lemma gcd_is_Max_divisors_nat:
  1050   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
  1051 apply(rule Max_eqI[THEN sym])
  1052   apply (metis finite_Collect_conjI finite_divisors_nat)
  1053  apply simp
  1054  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
  1055 apply simp
  1056 done
  1057 
  1058 lemma gcd_is_Max_divisors_int:
  1059   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
  1060 apply(rule Max_eqI[THEN sym])
  1061   apply (metis finite_Collect_conjI finite_divisors_int)
  1062  apply simp
  1063  apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
  1064 apply simp
  1065 done
  1066 
  1067 lemma gcd_code_int [code]:
  1068   "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  1069   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
  1070 
  1071 
  1072 subsection \<open>Coprimality\<close>
  1073 
  1074 context semiring_gcd
  1075 begin
  1076 
  1077 lemma div_gcd_coprime:
  1078   assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
  1079   shows "coprime (a div gcd a b) (b div gcd a b)"
  1080 proof -
  1081   let ?g = "gcd a b"
  1082   let ?a' = "a div ?g"
  1083   let ?b' = "b div ?g"
  1084   let ?g' = "gcd ?a' ?b'"
  1085   have dvdg: "?g dvd a" "?g dvd b" by simp_all
  1086   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
  1087   from dvdg dvdg' obtain ka kb ka' kb' where
  1088       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
  1089     unfolding dvd_def by blast
  1090   from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
  1091     by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
  1092   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
  1093     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
  1094       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
  1095   have "?g \<noteq> 0" using nz by simp
  1096   moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
  1097   thm dvd_mult_cancel_left
  1098   ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
  1099 qed
  1100 
  1101 lemma coprime:
  1102   "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)" (is "?P \<longleftrightarrow> ?Q")
  1103 proof
  1104   assume ?P then show ?Q by auto
  1105 next
  1106   assume ?Q
  1107   then have "is_unit (gcd a b) \<longleftrightarrow> gcd a b dvd a \<and> gcd a b dvd b"
  1108     by blast
  1109   then have "is_unit (gcd a b)"
  1110     by simp
  1111   then show ?P
  1112     by simp
  1113 qed
  1114 
  1115 end
  1116 
  1117 lemma coprime_nat:
  1118   "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1119   using coprime [of a b] by simp
  1120 
  1121 lemma coprime_Suc_0_nat:
  1122   "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
  1123   using coprime_nat by simp
  1124 
  1125 lemma coprime_int:
  1126   "coprime (a::int) b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1127   using gcd_unique_int [of 1 a b]
  1128   apply clarsimp
  1129   apply (erule subst)
  1130   apply (rule iffI)
  1131   apply force
  1132   using abs_dvd_iff abs_ge_zero apply blast
  1133   done
  1134 
  1135 lemma gcd_coprime_nat:
  1136   assumes z: "gcd (a::nat) 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 lemma gcd_coprime_int:
  1153   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
  1154     b: "b = b' * gcd a b"
  1155   shows    "coprime a' b'"
  1156   apply (subgoal_tac "a' = a div gcd a b")
  1157   apply (erule ssubst)
  1158   apply (subgoal_tac "b' = b div gcd a b")
  1159   apply (erule ssubst)
  1160   apply (rule div_gcd_coprime)
  1161   using z apply force
  1162   apply (subst (1) b)
  1163   using z apply force
  1164   apply (subst (1) a)
  1165   using z apply force
  1166   done
  1167 
  1168 context semiring_gcd
  1169 begin
  1170 
  1171 lemma coprime_mult:
  1172   assumes da: "coprime d a" and db: "coprime d b"
  1173   shows "coprime d (a * b)"
  1174   apply (subst gcd.commute)
  1175   using da apply (subst gcd_mult_cancel)
  1176   apply (subst gcd.commute, assumption)
  1177   apply (subst gcd.commute, rule db)
  1178   done
  1179 
  1180 end
  1181 
  1182 lemma coprime_lmult_nat:
  1183   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
  1184 proof -
  1185   have "gcd d a dvd gcd d (a * b)"
  1186     by (rule gcd_greatest, auto)
  1187   with dab show ?thesis
  1188     by auto
  1189 qed
  1190 
  1191 lemma coprime_lmult_int:
  1192   assumes "coprime (d::int) (a * b)" shows "coprime d a"
  1193 proof -
  1194   have "gcd d a dvd gcd d (a * b)"
  1195     by (rule gcd_greatest, auto)
  1196   with assms show ?thesis
  1197     by auto
  1198 qed
  1199 
  1200 lemma coprime_rmult_nat:
  1201   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
  1202 proof -
  1203   have "gcd d b dvd gcd d (a * b)"
  1204     by (rule gcd_greatest, auto intro: dvd_mult)
  1205   with assms show ?thesis
  1206     by auto
  1207 qed
  1208 
  1209 lemma coprime_rmult_int:
  1210   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
  1211 proof -
  1212   have "gcd d b dvd gcd d (a * b)"
  1213     by (rule gcd_greatest, auto intro: dvd_mult)
  1214   with dab show ?thesis
  1215     by auto
  1216 qed
  1217 
  1218 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
  1219     coprime d a \<and>  coprime d b"
  1220   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
  1221     coprime_mult [of d a b]
  1222   by blast
  1223 
  1224 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
  1225     coprime d a \<and>  coprime d b"
  1226   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
  1227     coprime_mult [of d a b]
  1228   by blast
  1229 
  1230 lemma coprime_power_int:
  1231   assumes "0 < n" shows "coprime (a :: int) (b ^ n) \<longleftrightarrow> coprime a b"
  1232   using assms
  1233 proof (induct n)
  1234   case (Suc n) then show ?case
  1235     by (cases n) (simp_all add: coprime_mul_eq_int)
  1236 qed simp
  1237 
  1238 lemma gcd_coprime_exists_nat:
  1239     assumes nz: "gcd (a::nat) b \<noteq> 0"
  1240     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
  1241   apply (rule_tac x = "a div gcd a b" in exI)
  1242   apply (rule_tac x = "b div gcd a b" in exI)
  1243   using nz apply (auto simp add: div_gcd_coprime dvd_div_mult)
  1244 done
  1245 
  1246 lemma gcd_coprime_exists_int:
  1247     assumes nz: "gcd (a::int) b \<noteq> 0"
  1248     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
  1249   apply (rule_tac x = "a div gcd a b" in exI)
  1250   apply (rule_tac x = "b div gcd a b" in exI)
  1251   using nz apply (auto simp add: div_gcd_coprime)
  1252 done
  1253 
  1254 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
  1255   by (induct n) (simp_all add: coprime_mult)
  1256 
  1257 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
  1258   by (induct n) (simp_all add: coprime_mult)
  1259 
  1260 context semiring_gcd
  1261 begin
  1262 
  1263 lemma coprime_exp_left:
  1264   assumes "coprime a b"
  1265   shows "coprime (a ^ n) b"
  1266   using assms by (induct n) (simp_all add: gcd_mult_cancel)
  1267 
  1268 lemma coprime_exp2:
  1269   assumes "coprime a b"
  1270   shows "coprime (a ^ n) (b ^ m)"
  1271 proof (rule coprime_exp_left)
  1272   from assms show "coprime a (b ^ m)"
  1273     by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
  1274 qed
  1275 
  1276 end
  1277 
  1278 lemma gcd_exp_nat:
  1279   "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
  1280 proof (cases "a = 0 \<and> b = 0")
  1281   case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power)
  1282 next
  1283   case False
  1284   then have "coprime (a div gcd a b) (b div gcd a b)"
  1285     by (auto simp: div_gcd_coprime)
  1286   then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
  1287     by (simp add: coprime_exp2)
  1288   then have "gcd ((a div gcd a b)^n * (gcd a b)^n)
  1289       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
  1290     by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
  1291   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
  1292     by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
  1293   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
  1294     by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
  1295   finally show ?thesis .
  1296 qed
  1297 
  1298 lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
  1299   apply (subst (1 2) gcd_abs_int)
  1300   apply (subst (1 2) power_abs)
  1301   apply (rule gcd_exp_nat [where n = n, transferred])
  1302   apply auto
  1303 done
  1304 
  1305 lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
  1306   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  1307 proof-
  1308   let ?g = "gcd a b"
  1309   {assume "?g = 0" with dc have ?thesis by auto}
  1310   moreover
  1311   {assume z: "?g \<noteq> 0"
  1312     from gcd_coprime_exists_nat[OF z]
  1313     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1314       by blast
  1315     have thb: "?g dvd b" by auto
  1316     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
  1317     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
  1318     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
  1319     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
  1320     with z have th_1: "a' dvd b' * c" by auto
  1321     from coprime_dvd_mult [OF ab'(3)] th_1
  1322     have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
  1323     from ab' have "a = ?g*a'" by algebra
  1324     with thb thc have ?thesis by blast }
  1325   ultimately show ?thesis by blast
  1326 qed
  1327 
  1328 lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
  1329   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  1330 proof-
  1331   let ?g = "gcd a b"
  1332   {assume "?g = 0" with dc have ?thesis by auto}
  1333   moreover
  1334   {assume z: "?g \<noteq> 0"
  1335     from gcd_coprime_exists_int[OF z]
  1336     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1337       by blast
  1338     have thb: "?g dvd b" by auto
  1339     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
  1340     with dc have th0: "a' dvd b*c"
  1341       using dvd_trans[of a' a "b*c"] by simp
  1342     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
  1343     hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
  1344     with z have th_1: "a' dvd b' * c" by auto
  1345     from coprime_dvd_mult [OF ab'(3)] th_1
  1346     have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
  1347     from ab' have "a = ?g*a'" by algebra
  1348     with thb thc have ?thesis by blast }
  1349   ultimately show ?thesis by blast
  1350 qed
  1351 
  1352 lemma pow_divides_pow_nat:
  1353   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
  1354   shows "a dvd b"
  1355 proof-
  1356   let ?g = "gcd a b"
  1357   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
  1358   {assume "?g = 0" with ab n have ?thesis by auto }
  1359   moreover
  1360   {assume z: "?g \<noteq> 0"
  1361     hence zn: "?g ^ n \<noteq> 0" using n by simp
  1362     from gcd_coprime_exists_nat[OF z]
  1363     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1364       by blast
  1365     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
  1366       by (simp add: ab'(1,2)[symmetric])
  1367     hence "?g^n*a'^n dvd ?g^n *b'^n"
  1368       by (simp only: power_mult_distrib mult.commute)
  1369     then have th0: "a'^n dvd b'^n"
  1370       using zn by auto
  1371     have "a' dvd a'^n" by (simp add: m)
  1372     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
  1373     hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
  1374     from coprime_dvd_mult [OF coprime_exp_nat [OF ab'(3), of m]] th1
  1375     have "a' dvd b'" by (subst (asm) mult.commute, blast)
  1376     hence "a'*?g dvd b'*?g" by simp
  1377     with ab'(1,2)  have ?thesis by simp }
  1378   ultimately show ?thesis by blast
  1379 qed
  1380 
  1381 lemma pow_divides_pow_int:
  1382   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
  1383   shows "a dvd b"
  1384 proof-
  1385   let ?g = "gcd a b"
  1386   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
  1387   {assume "?g = 0" with ab n have ?thesis by auto }
  1388   moreover
  1389   {assume z: "?g \<noteq> 0"
  1390     hence zn: "?g ^ n \<noteq> 0" using n by simp
  1391     from gcd_coprime_exists_int[OF z]
  1392     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1393       by blast
  1394     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
  1395       by (simp add: ab'(1,2)[symmetric])
  1396     hence "?g^n*a'^n dvd ?g^n *b'^n"
  1397       by (simp only: power_mult_distrib mult.commute)
  1398     with zn z n have th0:"a'^n dvd b'^n" by auto
  1399     have "a' dvd a'^n" by (simp add: m)
  1400     with th0 have "a' dvd b'^n"
  1401       using dvd_trans[of a' "a'^n" "b'^n"] by simp
  1402     hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
  1403     from coprime_dvd_mult [OF coprime_exp_int [OF ab'(3), of m]] th1
  1404     have "a' dvd b'" by (subst (asm) mult.commute, blast)
  1405     hence "a'*?g dvd b'*?g" by simp
  1406     with ab'(1,2)  have ?thesis by simp }
  1407   ultimately show ?thesis by blast
  1408 qed
  1409 
  1410 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
  1411   by (auto intro: pow_divides_pow_nat dvd_power_same)
  1412 
  1413 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
  1414   by (auto intro: pow_divides_pow_int dvd_power_same)
  1415 
  1416 lemma divides_mult_nat:
  1417   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
  1418   shows "m * n dvd r"
  1419 proof-
  1420   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
  1421     unfolding dvd_def by blast
  1422   from mr n' have "m dvd n'*n" by (simp add: mult.commute)
  1423   hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
  1424   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
  1425   from n' k show ?thesis unfolding dvd_def by auto
  1426 qed
  1427 
  1428 lemma divides_mult_int:
  1429   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
  1430   shows "m * n dvd r"
  1431 proof-
  1432   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
  1433     unfolding dvd_def by blast
  1434   from mr n' have "m dvd n'*n" by (simp add: mult.commute)
  1435   hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
  1436   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
  1437   from n' k show ?thesis unfolding dvd_def by auto
  1438 qed
  1439 
  1440 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
  1441   by (simp add: gcd.commute del: One_nat_def)
  1442 
  1443 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
  1444   using coprime_plus_one_nat by simp
  1445 
  1446 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
  1447   by (simp add: gcd.commute)
  1448 
  1449 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
  1450   using coprime_plus_one_nat [of "n - 1"]
  1451     gcd.commute [of "n - 1" n] by auto
  1452 
  1453 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
  1454   using coprime_plus_one_int [of "n - 1"]
  1455     gcd.commute [of "n - 1" n] by auto
  1456 
  1457 lemma setprod_coprime_nat:
  1458   fixes x :: nat
  1459   shows "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>A. f i) x"
  1460   by (induct A rule: infinite_finite_induct)
  1461     (auto simp add: gcd_mult_cancel One_nat_def [symmetric] simp del: One_nat_def)
  1462 
  1463 lemma setprod_coprime_int:
  1464   fixes x :: int
  1465   shows "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>A. f i) x"
  1466   by (induct A rule: infinite_finite_induct)
  1467     (auto simp add: gcd_mult_cancel)
  1468 
  1469 lemma coprime_common_divisor_nat: 
  1470   "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
  1471   by (metis gcd_greatest_iff nat_dvd_1_iff_1)
  1472 
  1473 lemma coprime_common_divisor_int:
  1474   "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
  1475   using gcd_greatest_iff [of x a b] by auto
  1476 
  1477 lemma coprime_divisors_nat:
  1478     "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
  1479   by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
  1480 
  1481 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1482 by (metis coprime_lmult_nat gcd_1_nat gcd.commute gcd_red_nat)
  1483 
  1484 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1485 by (metis coprime_lmult_int gcd_1_int gcd.commute gcd_red_int)
  1486 
  1487 
  1488 subsection \<open>Bezout's theorem\<close>
  1489 
  1490 (* Function bezw returns a pair of witnesses to Bezout's theorem --
  1491    see the theorems that follow the definition. *)
  1492 fun
  1493   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1494 where
  1495   "bezw x y =
  1496   (if y = 0 then (1, 0) else
  1497       (snd (bezw y (x mod y)),
  1498        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1499 
  1500 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1501 
  1502 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1503        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1504   by simp
  1505 
  1506 declare bezw.simps [simp del]
  1507 
  1508 lemma bezw_aux [rule_format]:
  1509     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1510 proof (induct x y rule: gcd_nat_induct)
  1511   fix m :: nat
  1512   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1513     by auto
  1514   next fix m :: nat and n
  1515     assume ngt0: "n > 0" and
  1516       ih: "fst (bezw n (m mod n)) * int n +
  1517         snd (bezw n (m mod n)) * int (m mod n) =
  1518         int (gcd n (m mod n))"
  1519     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1520       apply (simp add: bezw_non_0 gcd_non_0_nat)
  1521       apply (erule subst)
  1522       apply (simp add: field_simps)
  1523       apply (subst mod_div_equality [of m n, symmetric])
  1524       (* applying simp here undoes the last substitution!
  1525          what is procedure cancel_div_mod? *)
  1526       apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
  1527       done
  1528 qed
  1529 
  1530 lemma bezout_int:
  1531   fixes x y
  1532   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1533 proof -
  1534   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1535       EX u v. u * x + v * y = gcd x y"
  1536     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1537     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1538     apply (unfold gcd_int_def)
  1539     apply simp
  1540     apply (subst bezw_aux [symmetric])
  1541     apply auto
  1542     done
  1543   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1544       (x \<le> 0 \<and> y \<le> 0)"
  1545     by auto
  1546   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1547     by (erule (1) bezout_aux)
  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_neg2_int [symmetric])
  1554     apply auto
  1555     done
  1556   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1557     apply (insert bezout_aux [of "-x" y])
  1558     apply auto
  1559     apply (rule_tac x = "-u" in exI)
  1560     apply (rule_tac x = v in exI)
  1561     apply (subst gcd_neg1_int [symmetric])
  1562     apply auto
  1563     done
  1564   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1565     apply (insert bezout_aux [of "-x" "-y"])
  1566     apply auto
  1567     apply (rule_tac x = "-u" in exI)
  1568     apply (rule_tac x = "-v" in exI)
  1569     apply (subst gcd_neg1_int [symmetric])
  1570     apply (subst gcd_neg2_int [symmetric])
  1571     apply auto
  1572     done
  1573   ultimately show ?thesis by blast
  1574 qed
  1575 
  1576 text \<open>versions of Bezout for nat, by Amine Chaieb\<close>
  1577 
  1578 lemma ind_euclid:
  1579   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1580   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1581   shows "P a b"
  1582 proof(induct "a + b" arbitrary: a b rule: less_induct)
  1583   case less
  1584   have "a = b \<or> a < b \<or> b < a" by arith
  1585   moreover {assume eq: "a= b"
  1586     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1587     by simp}
  1588   moreover
  1589   {assume lt: "a < b"
  1590     hence "a + b - a < a + b \<or> a = 0" by arith
  1591     moreover
  1592     {assume "a =0" with z c have "P a b" by blast }
  1593     moreover
  1594     {assume "a + b - a < a + b"
  1595       also have th0: "a + b - a = a + (b - a)" using lt by arith
  1596       finally have "a + (b - a) < a + b" .
  1597       then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
  1598       then have "P a b" by (simp add: th0[symmetric])}
  1599     ultimately have "P a b" by blast}
  1600   moreover
  1601   {assume lt: "a > b"
  1602     hence "b + a - b < a + b \<or> b = 0" by arith
  1603     moreover
  1604     {assume "b =0" with z c have "P a b" by blast }
  1605     moreover
  1606     {assume "b + a - b < a + b"
  1607       also have th0: "b + a - b = b + (a - b)" using lt by arith
  1608       finally have "b + (a - b) < a + b" .
  1609       then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
  1610       then have "P b a" by (simp add: th0[symmetric])
  1611       hence "P a b" using c by blast }
  1612     ultimately have "P a b" by blast}
  1613 ultimately  show "P a b" by blast
  1614 qed
  1615 
  1616 lemma bezout_lemma_nat:
  1617   assumes ex: "\<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   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1620     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1621   using ex
  1622   apply clarsimp
  1623   apply (rule_tac x="d" in exI, simp)
  1624   apply (case_tac "a * x = b * y + d" , simp_all)
  1625   apply (rule_tac x="x + y" in exI)
  1626   apply (rule_tac x="y" in exI)
  1627   apply algebra
  1628   apply (rule_tac x="x" in exI)
  1629   apply (rule_tac x="x + y" in exI)
  1630   apply algebra
  1631 done
  1632 
  1633 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1634     (a * x = b * y + d \<or> b * x = a * y + d)"
  1635   apply(induct a b rule: ind_euclid)
  1636   apply blast
  1637   apply clarify
  1638   apply (rule_tac x="a" in exI, simp)
  1639   apply clarsimp
  1640   apply (rule_tac x="d" in exI)
  1641   apply (case_tac "a * x = b * y + d", simp_all)
  1642   apply (rule_tac x="x+y" in exI)
  1643   apply (rule_tac x="y" in exI)
  1644   apply algebra
  1645   apply (rule_tac x="x" in exI)
  1646   apply (rule_tac x="x+y" in exI)
  1647   apply algebra
  1648 done
  1649 
  1650 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1651     (a * x - b * y = d \<or> b * x - a * y = d)"
  1652   using bezout_add_nat[of a b]
  1653   apply clarsimp
  1654   apply (rule_tac x="d" in exI, simp)
  1655   apply (rule_tac x="x" in exI)
  1656   apply (rule_tac x="y" in exI)
  1657   apply auto
  1658 done
  1659 
  1660 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1661   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1662 proof-
  1663  from nz have ap: "a > 0" by simp
  1664  from bezout_add_nat[of a b]
  1665  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1666    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1667  moreover
  1668     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1669      from H have ?thesis by blast }
  1670  moreover
  1671  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1672    {assume b0: "b = 0" with H  have ?thesis by simp}
  1673    moreover
  1674    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1675      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1676        by auto
  1677      moreover
  1678      {assume db: "d=b"
  1679        with nz H have ?thesis apply simp
  1680          apply (rule exI[where x = b], simp)
  1681          apply (rule exI[where x = b])
  1682         by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1683     moreover
  1684     {assume db: "d < b"
  1685         {assume "x=0" hence ?thesis using nz H by simp }
  1686         moreover
  1687         {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1688           from db have "d \<le> b - 1" by simp
  1689           hence "d*b \<le> b*(b - 1)" by simp
  1690           with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1691           have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1692           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1693             by simp
  1694           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1695             by (simp only: mult.assoc distrib_left)
  1696           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1697             by algebra
  1698           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1699           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1700             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1701           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1702             by (simp only: diff_mult_distrib2 ac_simps)
  1703           hence ?thesis using H(1,2)
  1704             apply -
  1705             apply (rule exI[where x=d], simp)
  1706             apply (rule exI[where x="(b - 1) * y"])
  1707             by (rule exI[where x="x*(b - 1) - d"], simp)}
  1708         ultimately have ?thesis by blast}
  1709     ultimately have ?thesis by blast}
  1710   ultimately have ?thesis by blast}
  1711  ultimately show ?thesis by blast
  1712 qed
  1713 
  1714 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1715   shows "\<exists>x y. a * x = b * y + gcd a b"
  1716 proof-
  1717   let ?g = "gcd a b"
  1718   from bezout_add_strong_nat[OF a, of b]
  1719   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1720   from d(1,2) have "d dvd ?g" by simp
  1721   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1722   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1723   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1724   thus ?thesis by blast
  1725 qed
  1726 
  1727 
  1728 subsection \<open>LCM properties  on @{typ nat} and @{typ int}\<close>
  1729 
  1730 lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  1731   by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
  1732 
  1733 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1734   unfolding lcm_nat_def
  1735   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1736 
  1737 lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
  1738   unfolding lcm_int_def gcd_int_def
  1739   apply (subst int_mult [symmetric])
  1740   apply (subst prod_gcd_lcm_nat [symmetric])
  1741   apply (subst nat_abs_mult_distrib [symmetric])
  1742   apply (simp, simp add: abs_mult)
  1743 done
  1744 
  1745 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1746   unfolding lcm_nat_def by simp
  1747 
  1748 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1749   unfolding lcm_int_def by simp
  1750 
  1751 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1752   unfolding lcm_nat_def by simp
  1753 
  1754 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1755   unfolding lcm_int_def by simp
  1756 
  1757 lemma lcm_pos_nat:
  1758   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1759 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1760 
  1761 lemma lcm_pos_int:
  1762   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1763   apply (subst lcm_abs_int)
  1764   apply (rule lcm_pos_nat [transferred])
  1765   apply auto
  1766   done
  1767 
  1768 lemma dvd_pos_nat:
  1769   fixes n m :: nat
  1770   assumes "n > 0" and "m dvd n"
  1771   shows "m > 0"
  1772   using assms by (cases m) auto
  1773 
  1774 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1775     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1776   by (auto intro: dvd_antisym lcm_least)
  1777 
  1778 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1779     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1780   using lcm_least zdvd_antisym_nonneg by auto
  1781 
  1782 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1783   apply (rule sym)
  1784   apply (subst lcm_unique_nat [symmetric])
  1785   apply auto
  1786 done
  1787 
  1788 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
  1789   apply (rule sym)
  1790   apply (subst lcm_unique_int [symmetric])
  1791   apply auto
  1792 done
  1793 
  1794 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1795 by (subst lcm.commute, erule lcm_proj2_if_dvd_nat)
  1796 
  1797 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
  1798 by (subst lcm.commute, erule lcm_proj2_if_dvd_int)
  1799 
  1800 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1801 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1802 
  1803 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1804 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1805 
  1806 lemma lcm_proj1_iff_int[simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
  1807 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1808 
  1809 lemma lcm_proj2_iff_int[simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
  1810 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1811 
  1812 lemma (in semiring_gcd) comp_fun_idem_gcd:
  1813   "comp_fun_idem gcd"
  1814   by standard (simp_all add: fun_eq_iff ac_simps)
  1815 
  1816 lemma (in semiring_gcd) comp_fun_idem_lcm:
  1817   "comp_fun_idem lcm"
  1818   by standard (simp_all add: fun_eq_iff ac_simps)
  1819 
  1820 lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
  1821   by (simp only: lcm_eq_1_iff) simp
  1822   
  1823 lemma lcm_1_iff_int [simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  1824   by auto
  1825 
  1826 
  1827 subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
  1828 
  1829 text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
  1830 Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
  1831 \<close>
  1832 
  1833 instantiation nat :: semiring_Gcd
  1834 begin
  1835 
  1836 interpretation semilattice_neutr_set lcm "1::nat"
  1837   by standard simp_all
  1838 
  1839 definition
  1840   "Lcm (M::nat set) = (if finite M then F M else 0)"
  1841 
  1842 lemma Lcm_nat_empty:
  1843   "Lcm {} = (1::nat)"
  1844   by (simp add: Lcm_nat_def del: One_nat_def)
  1845 
  1846 lemma Lcm_nat_insert:
  1847   "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
  1848   by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
  1849 
  1850 lemma Lcm_nat_infinite:
  1851   "infinite M \<Longrightarrow> Lcm M = (0::nat)"
  1852   by (simp add: Lcm_nat_def)
  1853 
  1854 lemma dvd_Lcm_nat [simp]:
  1855   fixes M :: "nat set"
  1856   assumes "m \<in> M"
  1857   shows "m dvd Lcm M"
  1858 proof -
  1859   from assms have "insert m M = M" by auto
  1860   moreover have "m dvd Lcm (insert m M)"
  1861     by (simp add: Lcm_nat_insert)
  1862   ultimately show ?thesis by simp
  1863 qed
  1864 
  1865 lemma Lcm_dvd_nat [simp]:
  1866   fixes M :: "nat set"
  1867   assumes "\<forall>m\<in>M. m dvd n"
  1868   shows "Lcm M dvd n"
  1869 proof (cases "n = 0")
  1870   case True then show ?thesis by simp
  1871 next
  1872   case False
  1873   then have "finite {d. d dvd n}" by (rule finite_divisors_nat)
  1874   moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
  1875   ultimately have "finite M" by (rule rev_finite_subset)
  1876   then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
  1877 qed
  1878 
  1879 definition
  1880   "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
  1881 
  1882 instance proof
  1883   show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
  1884   using that by (induct N rule: infinite_finite_induct)
  1885     (auto simp add: Gcd_nat_def)
  1886   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
  1887   using that by (induct N rule: infinite_finite_induct)
  1888     (auto simp add: Gcd_nat_def)
  1889   show "n dvd Lcm N" if "n \<in> N" for N and n ::nat
  1890   using that by (induct N rule: infinite_finite_induct)
  1891     auto
  1892   show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n" for N and n ::nat
  1893   using that by (induct N rule: infinite_finite_induct)
  1894     auto
  1895 qed simp_all
  1896 
  1897 end
  1898 
  1899 lemma Gcd_nat_eq_one:
  1900   "1 \<in> N \<Longrightarrow> Gcd N = (1::nat)"
  1901   by (rule Gcd_eq_1_I) auto
  1902 
  1903 text\<open>Alternative characterizations of Gcd:\<close>
  1904 
  1905 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})"
  1906 apply(rule antisym)
  1907  apply(rule Max_ge)
  1908   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1909  apply (simp add: Gcd_dvd)
  1910 apply (rule Max_le_iff[THEN iffD2])
  1911   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1912  apply fastforce
  1913 apply clarsimp
  1914 apply (metis Gcd_dvd Max_in dvd_0_left dvd_Gcd dvd_imp_le linorder_antisym_conv3 not_less0)
  1915 done
  1916 
  1917 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
  1918 apply(induct pred:finite)
  1919  apply simp
  1920 apply(case_tac "x=0")
  1921  apply simp
  1922 apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
  1923  apply simp
  1924 apply blast
  1925 done
  1926 
  1927 lemma Lcm_in_lcm_closed_set_nat:
  1928   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
  1929 apply(induct rule:finite_linorder_min_induct)
  1930  apply simp
  1931 apply simp
  1932 apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
  1933  apply simp
  1934  apply(case_tac "A={}")
  1935   apply simp
  1936  apply simp
  1937 apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  1938 done
  1939 
  1940 lemma Lcm_eq_Max_nat:
  1941   "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"
  1942 apply(rule antisym)
  1943  apply(rule Max_ge, assumption)
  1944  apply(erule (2) Lcm_in_lcm_closed_set_nat)
  1945 apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
  1946 done
  1947 
  1948 lemma mult_inj_if_coprime_nat:
  1949   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
  1950    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
  1951   by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
  1952 
  1953 text\<open>Nitpick:\<close>
  1954 
  1955 lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
  1956 by (induct x y rule: nat_gcd.induct)
  1957    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  1958 
  1959 lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
  1960 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  1961 
  1962 
  1963 subsubsection \<open>Setwise gcd and lcm for integers\<close>
  1964 
  1965 instantiation int :: semiring_Gcd
  1966 begin
  1967 
  1968 definition
  1969   "Lcm M = int (Lcm m\<in>M. (nat \<circ> abs) m)"
  1970 
  1971 definition
  1972   "Gcd M = int (Gcd m\<in>M. (nat \<circ> abs) m)"
  1973 
  1974 instance by standard
  1975   (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
  1976     Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
  1977 
  1978 end
  1979 
  1980 lemma abs_Gcd [simp]:
  1981   fixes K :: "int set"
  1982   shows "\<bar>Gcd K\<bar> = Gcd K"
  1983   using normalize_Gcd [of K] by simp
  1984 
  1985 lemma abs_Lcm [simp]:
  1986   fixes K :: "int set"
  1987   shows "\<bar>Lcm K\<bar> = Lcm K"
  1988   using normalize_Lcm [of K] by simp
  1989 
  1990 lemma Gcm_eq_int_iff:
  1991   "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
  1992   by (simp add: Gcd_int_def comp_def image_image)
  1993 
  1994 lemma Lcm_eq_int_iff:
  1995   "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
  1996   by (simp add: Lcm_int_def comp_def image_image)
  1997 
  1998 
  1999 subsection \<open>GCD and LCM on @{typ integer}\<close>
  2000 
  2001 instantiation integer :: gcd
  2002 begin
  2003 
  2004 context
  2005   includes integer.lifting
  2006 begin
  2007 
  2008 lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
  2009   is gcd .
  2010 lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
  2011   is lcm .
  2012 
  2013 end
  2014 instance ..
  2015 
  2016 end
  2017 
  2018 lifting_update integer.lifting
  2019 lifting_forget integer.lifting
  2020 
  2021 context
  2022   includes integer.lifting
  2023 begin
  2024 
  2025 lemma gcd_code_integer [code]:
  2026   "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  2027   by transfer (fact gcd_code_int)
  2028 
  2029 lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  2030   by transfer (fact lcm_altdef_int)
  2031 
  2032 end
  2033 
  2034 code_printing constant "gcd :: integer \<Rightarrow> _"
  2035   \<rightharpoonup> (OCaml) "Big'_int.gcd'_big'_int"
  2036   and (Haskell) "Prelude.gcd"
  2037   and (Scala) "_.gcd'((_)')"
  2038   \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
  2039 
  2040 text \<open>Some code equations\<close>
  2041 
  2042 lemma Lcm_set_nat [code, code_unfold]:
  2043   "Lcm (set ns) = fold lcm ns (1::nat)"
  2044   using Lcm_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  2045 
  2046 lemma Gcd_set_nat [code]:
  2047   "Gcd (set ns) = fold gcd ns (0::nat)"
  2048   using Gcd_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  2049 
  2050 lemma Lcm_set_int [code, code_unfold]:
  2051   "Lcm (set xs) = fold lcm xs (1::int)"
  2052   using Lcm_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  2053 
  2054 lemma Gcd_set_int [code]:
  2055   "Gcd (set xs) = fold gcd xs (0::int)"
  2056   using Gcd_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  2057 
  2058 text \<open>Fact aliasses\<close>
  2059 
  2060 lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
  2061   by (fact dvd_int_unfold_dvd_nat)
  2062 
  2063 lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
  2064 lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
  2065 lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
  2066 lemmas gcd_commute_int = gcd.commute [where ?'a = int]
  2067 lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
  2068 lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
  2069 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
  2070 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
  2071 lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
  2072 lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
  2073 lemmas gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
  2074 lemmas gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
  2075 lemmas gcd_greatest_nat = gcd_greatest [where ?'a = nat]
  2076 lemmas gcd_greatest_int = gcd_greatest [where ?'a = int]
  2077 lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
  2078 lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
  2079 lemmas gcd_greatest_iff_nat = gcd_greatest_iff [where ?'a = nat]
  2080 lemmas gcd_greatest_iff_int = gcd_greatest_iff [where ?'a = int]
  2081 lemmas gcd_zero_nat = gcd_eq_0_iff [where ?'a = nat]
  2082 lemmas gcd_zero_int = gcd_eq_0_iff [where ?'a = int]
  2083 
  2084 lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
  2085 lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
  2086 lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
  2087 lemmas lcm_commute_int = lcm.commute [where ?'a = int]
  2088 lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
  2089 lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
  2090 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  2091 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  2092 lemmas lcm_dvd1_nat = dvd_lcm1 [where ?'a = nat]
  2093 lemmas lcm_dvd1_int = dvd_lcm1 [where ?'a = int]
  2094 lemmas lcm_dvd2_nat = dvd_lcm2 [where ?'a = nat]
  2095 lemmas lcm_dvd2_int = dvd_lcm2 [where ?'a = int]
  2096 lemmas lcm_least_nat = lcm_least [where ?'a = nat]
  2097 lemmas lcm_least_int = lcm_least [where ?'a = int]
  2098 
  2099 lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n= 0"
  2100   by (fact lcm_eq_0_iff)
  2101 
  2102 lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
  2103   by (fact lcm_eq_0_iff)
  2104 
  2105 lemma dvd_lcm_I1_nat [simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  2106   by (fact dvd_lcmI1)
  2107 
  2108 lemma dvd_lcm_I2_nat [simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  2109   by (fact dvd_lcmI2)
  2110 
  2111 lemma dvd_lcm_I1_int [simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  2112   by (fact dvd_lcmI1)
  2113 
  2114 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  2115   by (fact dvd_lcmI2)
  2116 
  2117 lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
  2118 lemmas coprime_mult_int = coprime_mult [where ?'a = int]
  2119 lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
  2120 lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
  2121 lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
  2122 lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
  2123 
  2124 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
  2125     (k dvd m * n) = (k dvd m)"
  2126   by (fact coprime_dvd_mult_iff)
  2127 
  2128 lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
  2129     (k dvd m * n) = (k dvd m)"
  2130   by (fact coprime_dvd_mult_iff)
  2131 
  2132 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
  2133   by (fact coprime_exp2)
  2134 
  2135 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
  2136   by (fact coprime_exp2)
  2137 
  2138 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
  2139 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
  2140 lemmas dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
  2141 lemmas dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
  2142 lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
  2143 lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
  2144 lemmas Gcd_insert_nat = Gcd_insert [where ?'a = nat]
  2145 lemmas Gcd_insert_int = Gcd_insert [where ?'a = int]
  2146 
  2147 lemma dvd_Lcm_int [simp]:
  2148   fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
  2149   using assms by (fact dvd_Lcm)
  2150 
  2151 lemma Lcm_empty_nat:
  2152   "Lcm {} = (1::nat)"
  2153   by (fact Lcm_empty)
  2154 
  2155 lemma Lcm_empty_int:
  2156   "Lcm {} = (1::int)"
  2157   by (fact Lcm_empty)
  2158 
  2159 lemma Lcm_insert_nat:
  2160   "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
  2161   by (fact Lcm_insert)
  2162 
  2163 lemma Lcm_insert_int:
  2164   "Lcm (insert (n::int) N) = lcm n (Lcm N)"
  2165   by (fact Lcm_insert)
  2166 
  2167 lemma gcd_neg_numeral_1_int [simp]:
  2168   "gcd (- numeral n :: int) x = gcd (numeral n) x"
  2169   by (fact gcd_neg1_int)
  2170 
  2171 lemma gcd_neg_numeral_2_int [simp]:
  2172   "gcd x (- numeral n :: int) = gcd x (numeral n)"
  2173   by (fact gcd_neg2_int)
  2174 
  2175 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
  2176   by (fact gcd_nat.absorb1)
  2177 
  2178 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
  2179   by (fact gcd_nat.absorb2)
  2180 
  2181 lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  2182   by (fact comp_fun_idem_gcd)
  2183 
  2184 lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  2185   by (fact comp_fun_idem_gcd)
  2186 
  2187 lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  2188   by (fact comp_fun_idem_lcm)
  2189 
  2190 lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  2191   by (fact comp_fun_idem_lcm)
  2192 
  2193 lemma Lcm_eq_0 [simp]:
  2194   "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
  2195   by (rule Lcm_eq_0_I)
  2196 
  2197 lemma Lcm0_iff [simp]:
  2198   fixes M :: "nat set"
  2199   assumes "finite M" and "M \<noteq> {}"
  2200   shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
  2201   using assms by (simp add: Lcm_0_iff)
  2202 
  2203 lemma Lcm_dvd_int [simp]:
  2204   fixes M :: "int set"
  2205   assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
  2206   using assms by (auto intro: Lcm_least)
  2207 
  2208 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
  2209   by (fact dvd_gcdD1)
  2210 
  2211 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
  2212   by (fact dvd_gcdD2)
  2213 
  2214 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
  2215   by (fact dvd_gcdD1)
  2216 
  2217 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
  2218   by (fact dvd_gcdD2)
  2219 
  2220 interpretation dvd:
  2221   order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> m \<noteq> n"
  2222   by standard (auto intro: dvd_refl dvd_trans dvd_antisym)
  2223 
  2224 interpretation gcd_semilattice_nat:
  2225   semilattice_inf gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
  2226   by standard (auto dest: dvd_antisym dvd_trans)
  2227 
  2228 interpretation lcm_semilattice_nat:
  2229   semilattice_sup lcm Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
  2230   by standard simp_all
  2231 
  2232 interpretation gcd_lcm_lattice_nat:
  2233   lattice gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n" lcm
  2234   ..
  2235 
  2236 interpretation gcd_lcm_complete_lattice_nat:
  2237   complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n" lcm 1 "0::nat"
  2238   by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
  2239 
  2240 end