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