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