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