src/HOL/GCD.thy
author haftmann
Sun Mar 10 15:16:45 2019 +0000 (6 weeks ago)
changeset 69906 55534affe445
parent 69785 9e326f6f8a24
permissions -rw-r--r--
migrated from Nums to Zarith as library for OCaml integer arithmetic
     1 (*  Title:      HOL/GCD.thy
     2     Author:     Christophe Tabacznyj
     3     Author:     Lawrence C. Paulson
     4     Author:     Amine Chaieb
     5     Author:     Thomas M. Rasmussen
     6     Author:     Jeremy Avigad
     7     Author:     Tobias Nipkow
     8 
     9 This file deals with the functions gcd and lcm.  Definitions and
    10 lemmas are proved uniformly for the natural numbers and integers.
    11 
    12 This file combines and revises a number of prior developments.
    13 
    14 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    15 and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
    16 gcd, lcm, and prime for the natural numbers.
    17 
    18 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    19 extended gcd, lcm, primes to the integers. Amine Chaieb provided
    20 another extension of the notions to the integers, and added a number
    21 of results to "Primes" and "GCD". IntPrimes also defined and developed
    22 the congruence relations on the integers. The notion was extended to
    23 the natural numbers by Chaieb.
    24 
    25 Jeremy Avigad combined all of these, made everything uniform for the
    26 natural numbers and the integers, and added a number of new theorems.
    27 
    28 Tobias Nipkow cleaned up a lot.
    29 *)
    30 
    31 section \<open>Greatest common divisor and least common multiple\<close>
    32 
    33 theory GCD
    34   imports Groups_List 
    35 begin
    36 
    37 subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
    38 
    39 locale bounded_quasi_semilattice = abel_semigroup +
    40   fixes top :: 'a  ("\<^bold>\<top>") and bot :: 'a  ("\<^bold>\<bottom>")
    41     and normalize :: "'a \<Rightarrow> 'a"
    42   assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
    43     and normalize_left_idem [simp]: "normalize a \<^bold>* b = a \<^bold>* b"
    44     and normalize_idem [simp]: "normalize (a \<^bold>* b) = a \<^bold>* b"
    45     and normalize_top [simp]: "normalize \<^bold>\<top> = \<^bold>\<top>"
    46     and normalize_bottom [simp]: "normalize \<^bold>\<bottom> = \<^bold>\<bottom>"
    47     and top_left_normalize [simp]: "\<^bold>\<top> \<^bold>* a = normalize a"
    48     and bottom_left_bottom [simp]: "\<^bold>\<bottom> \<^bold>* a = \<^bold>\<bottom>"
    49 begin
    50 
    51 lemma left_idem [simp]:
    52   "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
    53   using assoc [of a a b, symmetric] by simp
    54 
    55 lemma right_idem [simp]:
    56   "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
    57   using left_idem [of b a] by (simp add: ac_simps)
    58 
    59 lemma comp_fun_idem: "comp_fun_idem f"
    60   by standard (simp_all add: fun_eq_iff ac_simps)
    61 
    62 interpretation comp_fun_idem f
    63   by (fact comp_fun_idem)
    64 
    65 lemma top_right_normalize [simp]:
    66   "a \<^bold>* \<^bold>\<top> = normalize a"
    67   using top_left_normalize [of a] by (simp add: ac_simps)
    68 
    69 lemma bottom_right_bottom [simp]:
    70   "a \<^bold>* \<^bold>\<bottom> = \<^bold>\<bottom>"
    71   using bottom_left_bottom [of a] by (simp add: ac_simps)
    72 
    73 lemma normalize_right_idem [simp]:
    74   "a \<^bold>* normalize b = a \<^bold>* b"
    75   using normalize_left_idem [of b a] by (simp add: ac_simps)
    76 
    77 end
    78 
    79 locale bounded_quasi_semilattice_set = bounded_quasi_semilattice
    80 begin
    81 
    82 interpretation comp_fun_idem f
    83   by (fact comp_fun_idem)
    84 
    85 definition F :: "'a set \<Rightarrow> 'a"
    86 where
    87   eq_fold: "F A = (if finite A then Finite_Set.fold f \<^bold>\<top> A else \<^bold>\<bottom>)"
    88 
    89 lemma infinite [simp]:
    90   "infinite A \<Longrightarrow> F A = \<^bold>\<bottom>"
    91   by (simp add: eq_fold)
    92 
    93 lemma set_eq_fold [code]:
    94   "F (set xs) = fold f xs \<^bold>\<top>"
    95   by (simp add: eq_fold fold_set_fold)
    96 
    97 lemma empty [simp]:
    98   "F {} = \<^bold>\<top>"
    99   by (simp add: eq_fold)
   100 
   101 lemma insert [simp]:
   102   "F (insert a A) = a \<^bold>* F A"
   103   by (cases "finite A") (simp_all add: eq_fold)
   104 
   105 lemma normalize [simp]:
   106   "normalize (F A) = F A"
   107   by (induct A rule: infinite_finite_induct) simp_all
   108 
   109 lemma in_idem:
   110   assumes "a \<in> A"
   111   shows "a \<^bold>* F A = F A"
   112   using assms by (induct A rule: infinite_finite_induct)
   113     (auto simp: left_commute [of a])
   114 
   115 lemma union:
   116   "F (A \<union> B) = F A \<^bold>* F B"
   117   by (induct A rule: infinite_finite_induct)
   118     (simp_all add: ac_simps)
   119 
   120 lemma remove:
   121   assumes "a \<in> A"
   122   shows "F A = a \<^bold>* F (A - {a})"
   123 proof -
   124   from assms obtain B where "A = insert a B" and "a \<notin> B"
   125     by (blast dest: mk_disjoint_insert)
   126   with assms show ?thesis by simp
   127 qed
   128 
   129 lemma insert_remove:
   130   "F (insert a A) = a \<^bold>* F (A - {a})"
   131   by (cases "a \<in> A") (simp_all add: insert_absorb remove)
   132 
   133 lemma subset:
   134   assumes "B \<subseteq> A"
   135   shows "F B \<^bold>* F A = F A"
   136   using assms by (simp add: union [symmetric] Un_absorb1)
   137 
   138 end
   139 
   140 subsection \<open>Abstract GCD and LCM\<close>
   141 
   142 class gcd = zero + one + dvd +
   143   fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   144     and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   145 
   146 class Gcd = gcd +
   147   fixes Gcd :: "'a set \<Rightarrow> 'a"
   148     and Lcm :: "'a set \<Rightarrow> 'a"
   149 
   150 syntax
   151   "_GCD1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3GCD _./ _)" [0, 10] 10)
   152   "_GCD"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3GCD _\<in>_./ _)" [0, 0, 10] 10)
   153   "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3LCM _./ _)" [0, 10] 10)
   154   "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
   155 
   156 translations
   157   "GCD x y. f"   \<rightleftharpoons> "GCD x. GCD y. f"
   158   "GCD x. f"     \<rightleftharpoons> "CONST Gcd (CONST range (\<lambda>x. f))"
   159   "GCD x\<in>A. f"   \<rightleftharpoons> "CONST Gcd ((\<lambda>x. f) ` A)"
   160   "LCM x y. f"   \<rightleftharpoons> "LCM x. LCM y. f"
   161   "LCM x. f"     \<rightleftharpoons> "CONST Lcm (CONST range (\<lambda>x. f))"
   162   "LCM x\<in>A. f"   \<rightleftharpoons> "CONST Lcm ((\<lambda>x. f) ` A)"
   163 
   164 class semiring_gcd = normalization_semidom + gcd +
   165   assumes gcd_dvd1 [iff]: "gcd a b dvd a"
   166     and gcd_dvd2 [iff]: "gcd a b dvd b"
   167     and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
   168     and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
   169     and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
   170 begin
   171 
   172 lemma gcd_greatest_iff [simp]: "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
   173   by (blast intro!: gcd_greatest intro: dvd_trans)
   174 
   175 lemma gcd_dvdI1: "a dvd c \<Longrightarrow> gcd a b dvd c"
   176   by (rule dvd_trans) (rule gcd_dvd1)
   177 
   178 lemma gcd_dvdI2: "b dvd c \<Longrightarrow> gcd a b dvd c"
   179   by (rule dvd_trans) (rule gcd_dvd2)
   180 
   181 lemma dvd_gcdD1: "a dvd gcd b c \<Longrightarrow> a dvd b"
   182   using gcd_dvd1 [of b c] by (blast intro: dvd_trans)
   183 
   184 lemma dvd_gcdD2: "a dvd gcd b c \<Longrightarrow> a dvd c"
   185   using gcd_dvd2 [of b c] by (blast intro: dvd_trans)
   186 
   187 lemma gcd_0_left [simp]: "gcd 0 a = normalize a"
   188   by (rule associated_eqI) simp_all
   189 
   190 lemma gcd_0_right [simp]: "gcd a 0 = normalize a"
   191   by (rule associated_eqI) simp_all
   192 
   193 lemma gcd_eq_0_iff [simp]: "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
   194   (is "?P \<longleftrightarrow> ?Q")
   195 proof
   196   assume ?P
   197   then have "0 dvd gcd a b"
   198     by simp
   199   then have "0 dvd a" and "0 dvd b"
   200     by (blast intro: dvd_trans)+
   201   then show ?Q
   202     by simp
   203 next
   204   assume ?Q
   205   then show ?P
   206     by simp
   207 qed
   208 
   209 lemma unit_factor_gcd: "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)"
   210 proof (cases "gcd a b = 0")
   211   case True
   212   then show ?thesis by simp
   213 next
   214   case False
   215   have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b"
   216     by (rule unit_factor_mult_normalize)
   217   then have "unit_factor (gcd a b) * gcd a b = gcd a b"
   218     by simp
   219   then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b"
   220     by simp
   221   with False show ?thesis
   222     by simp
   223 qed
   224 
   225 lemma is_unit_gcd_iff [simp]:
   226   "is_unit (gcd a b) \<longleftrightarrow> gcd a b = 1"
   227   by (cases "a = 0 \<and> b = 0") (auto simp: unit_factor_gcd dest: is_unit_unit_factor)
   228 
   229 sublocale gcd: abel_semigroup gcd
   230 proof
   231   fix a b c
   232   show "gcd a b = gcd b a"
   233     by (rule associated_eqI) simp_all
   234   from gcd_dvd1 have "gcd (gcd a b) c dvd a"
   235     by (rule dvd_trans) simp
   236   moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
   237     by (rule dvd_trans) simp
   238   ultimately have P1: "gcd (gcd a b) c dvd gcd a (gcd b c)"
   239     by (auto intro!: gcd_greatest)
   240   from gcd_dvd2 have "gcd a (gcd b c) dvd b"
   241     by (rule dvd_trans) simp
   242   moreover from gcd_dvd2 have "gcd a (gcd b c) dvd c"
   243     by (rule dvd_trans) simp
   244   ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
   245     by (auto intro!: gcd_greatest)
   246   from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)"
   247     by (rule associated_eqI) simp_all
   248 qed
   249 
   250 sublocale gcd: bounded_quasi_semilattice gcd 0 1 normalize
   251 proof
   252   show "gcd a a = normalize a" for a
   253   proof -
   254     have "a dvd gcd a a"
   255       by (rule gcd_greatest) simp_all
   256     then show ?thesis
   257       by (auto intro: associated_eqI)
   258   qed
   259   show "gcd (normalize a) b = gcd a b" for a b
   260     using gcd_dvd1 [of "normalize a" b]
   261     by (auto intro: associated_eqI)
   262   show "gcd 1 a = 1" for a
   263     by (rule associated_eqI) simp_all
   264 qed simp_all
   265 
   266 lemma gcd_self: "gcd a a = normalize a"
   267   by (fact gcd.idem_normalize)
   268 
   269 lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b"
   270   by (fact gcd.left_idem)
   271 
   272 lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
   273   by (fact gcd.right_idem)
   274 
   275 lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
   276 proof (cases "c = 0")
   277   case True
   278   then show ?thesis by simp
   279 next
   280   case False
   281   then have *: "c * gcd a b dvd gcd (c * a) (c * b)"
   282     by (auto intro: gcd_greatest)
   283   moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b"
   284     by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
   285   ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
   286     by (auto intro: associated_eqI)
   287   then show ?thesis
   288     by (simp add: normalize_mult)
   289 qed
   290 
   291 lemma gcd_mult_right: "gcd (a * c) (b * c) = gcd b a * normalize c"
   292   using gcd_mult_left [of c a b] by (simp add: ac_simps)
   293 
   294 lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
   295   by (simp add: gcd_mult_left mult.assoc [symmetric])
   296 
   297 lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
   298   using mult_gcd_left [of c a b] by (simp add: ac_simps)
   299 
   300 lemma dvd_lcm1 [iff]: "a dvd lcm a b"
   301 proof -
   302   have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
   303     by (simp add: lcm_gcd normalize_mult div_mult_swap)
   304   then show ?thesis
   305     by (simp add: lcm_gcd)
   306 qed
   307 
   308 lemma dvd_lcm2 [iff]: "b dvd lcm a b"
   309 proof -
   310   have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
   311     by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
   312   then show ?thesis
   313     by (simp add: lcm_gcd)
   314 qed
   315 
   316 lemma dvd_lcmI1: "a dvd b \<Longrightarrow> a dvd lcm b c"
   317   by (rule dvd_trans) (assumption, blast)
   318 
   319 lemma dvd_lcmI2: "a dvd c \<Longrightarrow> a dvd lcm b c"
   320   by (rule dvd_trans) (assumption, blast)
   321 
   322 lemma lcm_dvdD1: "lcm a b dvd c \<Longrightarrow> a dvd c"
   323   using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
   324 
   325 lemma lcm_dvdD2: "lcm a b dvd c \<Longrightarrow> b dvd c"
   326   using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
   327 
   328 lemma lcm_least:
   329   assumes "a dvd c" and "b dvd c"
   330   shows "lcm a b dvd c"
   331 proof (cases "c = 0")
   332   case True
   333   then show ?thesis by simp
   334 next
   335   case False
   336   then have *: "is_unit (unit_factor c)"
   337     by simp
   338   show ?thesis
   339   proof (cases "gcd a b = 0")
   340     case True
   341     with assms show ?thesis by simp
   342   next
   343     case False
   344     then have "a \<noteq> 0 \<or> b \<noteq> 0"
   345       by simp
   346     with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b"
   347       by (simp_all add: mult_dvd_mono)
   348     then have "normalize (a * b) dvd gcd (a * c) (b * c)"
   349       by (auto intro: gcd_greatest simp add: ac_simps)
   350     then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
   351       using * by (simp add: dvd_mult_unit_iff)
   352     then have "normalize (a * b) dvd gcd a b * c"
   353       by (simp add: mult_gcd_right [of a b c])
   354     then have "normalize (a * b) div gcd a b dvd c"
   355       using False by (simp add: div_dvd_iff_mult ac_simps)
   356     then show ?thesis
   357       by (simp add: lcm_gcd)
   358   qed
   359 qed
   360 
   361 lemma lcm_least_iff [simp]: "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
   362   by (blast intro!: lcm_least intro: dvd_trans)
   363 
   364 lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b"
   365   by (simp add: lcm_gcd dvd_normalize_div)
   366 
   367 lemma lcm_0_left [simp]: "lcm 0 a = 0"
   368   by (simp add: lcm_gcd)
   369 
   370 lemma lcm_0_right [simp]: "lcm a 0 = 0"
   371   by (simp add: lcm_gcd)
   372 
   373 lemma lcm_eq_0_iff: "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   374   (is "?P \<longleftrightarrow> ?Q")
   375 proof
   376   assume ?P
   377   then have "0 dvd lcm a b"
   378     by simp
   379   then have "0 dvd normalize (a * b) div gcd a b"
   380     by (simp add: lcm_gcd)
   381   then have "0 * gcd a b dvd normalize (a * b)"
   382     using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
   383   then have "normalize (a * b) = 0"
   384     by simp
   385   then show ?Q
   386     by simp
   387 next
   388   assume ?Q
   389   then show ?P
   390     by auto
   391 qed
   392 
   393 lemma lcm_eq_1_iff [simp]: "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
   394   by (auto intro: associated_eqI)
   395 
   396 lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
   397   by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
   398 
   399 sublocale lcm: abel_semigroup lcm
   400 proof
   401   fix a b c
   402   show "lcm a b = lcm b a"
   403     by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
   404   have "lcm (lcm a b) c dvd lcm a (lcm b c)"
   405     and "lcm a (lcm b c) dvd lcm (lcm a b) c"
   406     by (auto intro: lcm_least
   407       dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
   408       dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
   409       dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
   410       dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
   411   then show "lcm (lcm a b) c = lcm a (lcm b c)"
   412     by (rule associated_eqI) simp_all
   413 qed
   414 
   415 sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
   416 proof
   417   show "lcm a a = normalize a" for a
   418   proof -
   419     have "lcm a a dvd a"
   420       by (rule lcm_least) simp_all
   421     then show ?thesis
   422       by (auto intro: associated_eqI)
   423   qed
   424   show "lcm (normalize a) b = lcm a b" for a b
   425     using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
   426     by (auto intro: associated_eqI)
   427   show "lcm 1 a = normalize a" for a
   428     by (rule associated_eqI) simp_all
   429 qed simp_all
   430 
   431 lemma lcm_self: "lcm a a = normalize a"
   432   by (fact lcm.idem_normalize)
   433 
   434 lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
   435   by (fact lcm.left_idem)
   436 
   437 lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
   438   by (fact lcm.right_idem)
   439 
   440 lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
   441   by (simp add: lcm_gcd normalize_mult)
   442 
   443 lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b"
   444   using gcd_mult_lcm [of a b] by (simp add: ac_simps)
   445 
   446 lemma gcd_lcm:
   447   assumes "a \<noteq> 0" and "b \<noteq> 0"
   448   shows "gcd a b = normalize (a * b) div lcm a b"
   449 proof -
   450   from assms have "lcm a b \<noteq> 0"
   451     by (simp add: lcm_eq_0_iff)
   452   have "gcd a b * lcm a b = normalize a * normalize b"
   453     by simp
   454   then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
   455     by (simp_all add: normalize_mult)
   456   with \<open>lcm a b \<noteq> 0\<close> show ?thesis
   457     using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
   458 qed
   459 
   460 lemma lcm_1_left: "lcm 1 a = normalize a"
   461   by (fact lcm.top_left_normalize)
   462 
   463 lemma lcm_1_right: "lcm a 1 = normalize a"
   464   by (fact lcm.top_right_normalize)
   465 
   466 lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b"
   467   by (cases "c = 0")
   468     (simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
   469       simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
   470 
   471 lemma lcm_mult_right: "lcm (a * c) (b * c) = lcm b a * normalize c"
   472   using lcm_mult_left [of c a b] by (simp add: ac_simps)
   473 
   474 lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
   475   by (simp add: lcm_mult_left mult.assoc [symmetric])
   476 
   477 lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
   478   using mult_lcm_left [of c a b] by (simp add: ac_simps)
   479 
   480 lemma gcdI:
   481   assumes "c dvd a" and "c dvd b"
   482     and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
   483     and "normalize c = c"
   484   shows "c = gcd a b"
   485   by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
   486 
   487 lemma gcd_unique:
   488   "d dvd a \<and> d dvd b \<and> normalize d = d \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   489   by rule (auto intro: gcdI simp: gcd_greatest)
   490 
   491 lemma gcd_dvd_prod: "gcd a b dvd k * b"
   492   using mult_dvd_mono [of 1] by auto
   493 
   494 lemma gcd_proj2_if_dvd: "b dvd a \<Longrightarrow> gcd a b = normalize b"
   495   by (rule gcdI [symmetric]) simp_all
   496 
   497 lemma gcd_proj1_if_dvd: "a dvd b \<Longrightarrow> gcd a b = normalize a"
   498   by (rule gcdI [symmetric]) simp_all
   499 
   500 lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n"
   501 proof
   502   assume *: "gcd m n = normalize m"
   503   show "m dvd n"
   504   proof (cases "m = 0")
   505     case True
   506     with * show ?thesis by simp
   507   next
   508     case [simp]: False
   509     from * have **: "m = gcd m n * unit_factor m"
   510       by (simp add: unit_eq_div2)
   511     show ?thesis
   512       by (subst **) (simp add: mult_unit_dvd_iff)
   513   qed
   514 next
   515   assume "m dvd n"
   516   then show "gcd m n = normalize m"
   517     by (rule gcd_proj1_if_dvd)
   518 qed
   519 
   520 lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m"
   521   using gcd_proj1_iff [of n m] by (simp add: ac_simps)
   522 
   523 lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)"
   524   by (rule gcdI) (auto simp: normalize_mult gcd_greatest mult_dvd_mono gcd_mult_left[symmetric])
   525 
   526 lemma gcd_mult_distrib: "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
   527 proof-
   528   have "normalize k * gcd a b = gcd (k * a) (k * b)"
   529     by (simp add: gcd_mult_distrib')
   530   then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
   531     by simp
   532   then have "normalize k * unit_factor k * gcd a b  = gcd (k * a) (k * b) * unit_factor k"
   533     by (simp only: ac_simps)
   534   then show ?thesis
   535     by simp
   536 qed
   537 
   538 lemma lcm_mult_unit1: "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
   539   by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
   540 
   541 lemma lcm_mult_unit2: "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
   542   using lcm_mult_unit1 [of a c b] by (simp add: ac_simps)
   543 
   544 lemma lcm_div_unit1:
   545   "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c"
   546   by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1)
   547 
   548 lemma lcm_div_unit2: "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
   549   by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
   550 
   551 lemma normalize_lcm_left: "lcm (normalize a) b = lcm a b"
   552   by (fact lcm.normalize_left_idem)
   553 
   554 lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
   555   by (fact lcm.normalize_right_idem)
   556 
   557 lemma gcd_mult_unit1: 
   558   assumes "is_unit a" shows "gcd (b * a) c = gcd b c"
   559 proof -
   560   have "gcd (b * a) c dvd b"
   561     using assms local.dvd_mult_unit_iff by blast
   562   then show ?thesis
   563     by (rule gcdI) simp_all
   564 qed
   565 
   566 lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
   567   using gcd.commute gcd_mult_unit1 by auto
   568 
   569 lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
   570   by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
   571 
   572 lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
   573   by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
   574 
   575 lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
   576   by (fact gcd.normalize_left_idem)
   577 
   578 lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
   579   by (fact gcd.normalize_right_idem)
   580 
   581 lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
   582   by standard (simp_all add: fun_eq_iff ac_simps)
   583 
   584 lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
   585   by standard (simp_all add: fun_eq_iff ac_simps)
   586 
   587 lemma gcd_dvd_antisym: "gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d"
   588 proof (rule gcdI)
   589   assume *: "gcd a b dvd gcd c d"
   590     and **: "gcd c d dvd gcd a b"
   591   have "gcd c d dvd c"
   592     by simp
   593   with * show "gcd a b dvd c"
   594     by (rule dvd_trans)
   595   have "gcd c d dvd d"
   596     by simp
   597   with * show "gcd a b dvd d"
   598     by (rule dvd_trans)
   599   show "normalize (gcd a b) = gcd a b"
   600     by simp
   601   fix l assume "l dvd c" and "l dvd d"
   602   then have "l dvd gcd c d"
   603     by (rule gcd_greatest)
   604   from this and ** show "l dvd gcd a b"
   605     by (rule dvd_trans)
   606 qed
   607 
   608 lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
   609   by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
   610 
   611 lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
   612   using gcd_add1 [of n m] by (simp add: ac_simps)
   613 
   614 lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
   615   by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
   616 
   617 lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
   618   by (simp add: lcm_gcd)
   619 
   620 declare unit_factor_lcm [simp]
   621 
   622 lemma lcmI:
   623   assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
   624     and "normalize c = c"
   625   shows "c = lcm a b"
   626   by (rule associated_eqI) (auto simp: assms intro: lcm_least)
   627 
   628 lemma gcd_dvd_lcm [simp]: "gcd a b dvd lcm a b"
   629   using gcd_dvd2 by (rule dvd_lcmI2)
   630 
   631 lemmas lcm_0 = lcm_0_right
   632 
   633 lemma lcm_unique:
   634   "a dvd d \<and> b dvd d \<and> normalize d = d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   635   by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
   636 
   637 lemma lcm_proj1_if_dvd:
   638   assumes "b dvd a" shows "lcm a b = normalize a"
   639 proof (cases "a = 0")
   640   case False
   641   then show ?thesis
   642     using assms gcd_proj2_if_dvd lcm_mult_gcd local.lcm_gcd by auto
   643 qed auto
   644 
   645 lemma lcm_proj2_if_dvd: "a dvd b \<Longrightarrow> lcm a b = normalize b"
   646   using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
   647 
   648 lemma lcm_proj1_iff: "lcm m n = normalize m \<longleftrightarrow> n dvd m"
   649 proof
   650   assume *: "lcm m n = normalize m"
   651   show "n dvd m"
   652   proof (cases "m = 0")
   653     case True
   654     then show ?thesis by simp
   655   next
   656     case [simp]: False
   657     from * have **: "m = lcm m n * unit_factor m"
   658       by (simp add: unit_eq_div2)
   659     show ?thesis by (subst **) simp
   660   qed
   661 next
   662   assume "n dvd m"
   663   then show "lcm m n = normalize m"
   664     by (rule lcm_proj1_if_dvd)
   665 qed
   666 
   667 lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
   668   using lcm_proj1_iff [of n m] by (simp add: ac_simps)
   669 
   670 lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
   671   by (rule lcmI) (auto simp: normalize_mult lcm_least mult_dvd_mono lcm_mult_left [symmetric])
   672 
   673 lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
   674 proof-
   675   have "normalize k * lcm a b = lcm (k * a) (k * b)"
   676     by (simp add: lcm_mult_distrib')
   677   then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
   678     by simp
   679   then have "normalize k * unit_factor k * lcm a b  = lcm (k * a) (k * b) * unit_factor k"
   680     by (simp only: ac_simps)
   681   then show ?thesis
   682     by simp
   683 qed
   684 
   685 lemma gcd_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> gcd a b dvd gcd c d"
   686   by (simp add: gcd_dvdI1 gcd_dvdI2)
   687 
   688 lemma lcm_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> lcm a b dvd lcm c d"
   689   by (simp add: dvd_lcmI1 dvd_lcmI2)
   690 
   691 lemma dvd_productE:
   692   assumes "p dvd a * b"
   693   obtains x y where "p = x * y" "x dvd a" "y dvd b"
   694 proof (cases "a = 0")
   695   case True
   696   thus ?thesis by (intro that[of p 1]) simp_all
   697 next
   698   case False
   699   define x y where "x = gcd a p" and "y = p div x"
   700   have "p = x * y" by (simp add: x_def y_def)
   701   moreover have "x dvd a" by (simp add: x_def)
   702   moreover from assms have "p dvd gcd (b * a) (b * p)"
   703     by (intro gcd_greatest) (simp_all add: mult.commute)
   704   hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
   705   with False have "y dvd b"
   706     by (simp add: x_def y_def div_dvd_iff_mult assms)
   707   ultimately show ?thesis by (rule that)
   708 qed
   709 
   710 end
   711 
   712 class ring_gcd = comm_ring_1 + semiring_gcd
   713 begin
   714 
   715 lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
   716   by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
   717 
   718 lemma gcd_neg2 [simp]: "gcd a (-b) = gcd a b"
   719   by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
   720 
   721 lemma gcd_neg_numeral_1 [simp]: "gcd (- numeral n) a = gcd (numeral n) a"
   722   by (fact gcd_neg1)
   723 
   724 lemma gcd_neg_numeral_2 [simp]: "gcd a (- numeral n) = gcd a (numeral n)"
   725   by (fact gcd_neg2)
   726 
   727 lemma gcd_diff1: "gcd (m - n) n = gcd m n"
   728   by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp)
   729 
   730 lemma gcd_diff2: "gcd (n - m) n = gcd m n"
   731   by (subst gcd_neg1[symmetric]) (simp only: minus_diff_eq gcd_diff1)
   732 
   733 lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b"
   734   by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)
   735 
   736 lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b"
   737   by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)
   738 
   739 lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a"
   740   by (fact lcm_neg1)
   741 
   742 lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)"
   743   by (fact lcm_neg2)
   744 
   745 end
   746 
   747 class semiring_Gcd = semiring_gcd + Gcd +
   748   assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
   749     and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A"
   750     and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
   751   assumes dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
   752     and Lcm_least: "(\<And>b. b \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> Lcm A dvd a"
   753     and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A"
   754 begin
   755 
   756 lemma Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
   757   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
   758 
   759 lemma Gcd_Lcm: "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
   760   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
   761 
   762 lemma Gcd_empty [simp]: "Gcd {} = 0"
   763   by (rule dvd_0_left, rule Gcd_greatest) simp
   764 
   765 lemma Lcm_empty [simp]: "Lcm {} = 1"
   766   by (auto intro: associated_eqI Lcm_least)
   767 
   768 lemma Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)"
   769 proof -
   770   have "Gcd (insert a A) dvd gcd a (Gcd A)"
   771     by (auto intro: Gcd_dvd Gcd_greatest)
   772   moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
   773   proof (rule Gcd_greatest)
   774     fix b
   775     assume "b \<in> insert a A"
   776     then show "gcd a (Gcd A) dvd b"
   777     proof
   778       assume "b = a"
   779       then show ?thesis
   780         by simp
   781     next
   782       assume "b \<in> A"
   783       then have "Gcd A dvd b"
   784         by (rule Gcd_dvd)
   785       moreover have "gcd a (Gcd A) dvd Gcd A"
   786         by simp
   787       ultimately show ?thesis
   788         by (blast intro: dvd_trans)
   789     qed
   790   qed
   791   ultimately show ?thesis
   792     by (auto intro: associated_eqI)
   793 qed
   794 
   795 lemma Lcm_insert [simp]: "Lcm (insert a A) = lcm a (Lcm A)"
   796 proof (rule sym)
   797   have "lcm a (Lcm A) dvd Lcm (insert a A)"
   798     by (auto intro: dvd_Lcm Lcm_least)
   799   moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
   800   proof (rule Lcm_least)
   801     fix b
   802     assume "b \<in> insert a A"
   803     then show "b dvd lcm a (Lcm A)"
   804     proof
   805       assume "b = a"
   806       then show ?thesis by simp
   807     next
   808       assume "b \<in> A"
   809       then have "b dvd Lcm A"
   810         by (rule dvd_Lcm)
   811       moreover have "Lcm A dvd lcm a (Lcm A)"
   812         by simp
   813       ultimately show ?thesis
   814         by (blast intro: dvd_trans)
   815     qed
   816   qed
   817   ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
   818     by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
   819 qed
   820 
   821 lemma LcmI:
   822   assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b"
   823     and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
   824     and "normalize b = b"
   825   shows "b = Lcm A"
   826   by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least)
   827 
   828 lemma Lcm_subset: "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
   829   by (blast intro: Lcm_least dvd_Lcm)
   830 
   831 lemma Lcm_Un: "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
   832 proof -
   833   have "\<And>d. \<lbrakk>Lcm A dvd d; Lcm B dvd d\<rbrakk> \<Longrightarrow> Lcm (A \<union> B) dvd d"
   834     by (meson UnE local.Lcm_least local.dvd_Lcm local.dvd_trans)
   835   then show ?thesis
   836     by (meson Lcm_subset local.lcm_unique local.normalize_Lcm sup.cobounded1 sup.cobounded2)
   837 qed
   838 
   839 lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
   840   (is "?P \<longleftrightarrow> ?Q")
   841 proof
   842   assume ?P
   843   show ?Q
   844   proof
   845     fix a
   846     assume "a \<in> A"
   847     then have "Gcd A dvd a"
   848       by (rule Gcd_dvd)
   849     with \<open>?P\<close> have "a = 0"
   850       by simp
   851     then show "a \<in> {0}"
   852       by simp
   853   qed
   854 next
   855   assume ?Q
   856   have "0 dvd Gcd A"
   857   proof (rule Gcd_greatest)
   858     fix a
   859     assume "a \<in> A"
   860     with \<open>?Q\<close> have "a = 0"
   861       by auto
   862     then show "0 dvd a"
   863       by simp
   864   qed
   865   then show ?P
   866     by simp
   867 qed
   868 
   869 lemma Lcm_1_iff [simp]: "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)"
   870   (is "?P \<longleftrightarrow> ?Q")
   871 proof
   872   assume ?P
   873   show ?Q
   874   proof
   875     fix a
   876     assume "a \<in> A"
   877     then have "a dvd Lcm A"
   878       by (rule dvd_Lcm)
   879     with \<open>?P\<close> show "is_unit a"
   880       by simp
   881   qed
   882 next
   883   assume ?Q
   884   then have "is_unit (Lcm A)"
   885     by (blast intro: Lcm_least)
   886   then have "normalize (Lcm A) = 1"
   887     by (rule is_unit_normalize)
   888   then show ?P
   889     by simp
   890 qed
   891 
   892 lemma unit_factor_Lcm: "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
   893 proof (cases "Lcm A = 0")
   894   case True
   895   then show ?thesis
   896     by simp
   897 next
   898   case False
   899   with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
   900     by blast
   901   with False show ?thesis
   902     by simp
   903 qed
   904 
   905 lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   906   by (simp add: Gcd_Lcm unit_factor_Lcm)
   907 
   908 lemma GcdI:
   909   assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a"
   910     and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
   911     and "normalize b = b"
   912   shows "b = Gcd A"
   913   by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest)
   914 
   915 lemma Gcd_eq_1_I:
   916   assumes "is_unit a" and "a \<in> A"
   917   shows "Gcd A = 1"
   918 proof -
   919   from assms have "is_unit (Gcd A)"
   920     by (blast intro: Gcd_dvd dvd_unit_imp_unit)
   921   then have "normalize (Gcd A) = 1"
   922     by (rule is_unit_normalize)
   923   then show ?thesis
   924     by simp
   925 qed
   926 
   927 lemma Lcm_eq_0_I:
   928   assumes "0 \<in> A"
   929   shows "Lcm A = 0"
   930 proof -
   931   from assms have "0 dvd Lcm A"
   932     by (rule dvd_Lcm)
   933   then show ?thesis
   934     by simp
   935 qed
   936 
   937 lemma Gcd_UNIV [simp]: "Gcd UNIV = 1"
   938   using dvd_refl by (rule Gcd_eq_1_I) simp
   939 
   940 lemma Lcm_UNIV [simp]: "Lcm UNIV = 0"
   941   by (rule Lcm_eq_0_I) simp
   942 
   943 lemma Lcm_0_iff:
   944   assumes "finite A"
   945   shows "Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
   946 proof (cases "A = {}")
   947   case True
   948   then show ?thesis by simp
   949 next
   950   case False
   951   with assms show ?thesis
   952     by (induct A rule: finite_ne_induct) (auto simp: lcm_eq_0_iff)
   953 qed
   954 
   955 lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
   956 proof -
   957   have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
   958   proof -
   959     from that obtain B where "A = insert a B"
   960       by blast
   961     moreover have "gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
   962       by (rule gcd_dvd1)
   963     ultimately show "Gcd (normalize ` A) dvd a"
   964       by simp
   965   qed
   966   then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
   967     by (auto intro!: Gcd_greatest intro: Gcd_dvd)
   968   then show ?thesis
   969     by (auto intro: associated_eqI)
   970 qed
   971 
   972 lemma Gcd_eqI:
   973   assumes "normalize a = a"
   974   assumes "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
   975     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> c dvd b) \<Longrightarrow> c dvd a"
   976   shows "Gcd A = a"
   977   using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd)
   978 
   979 lemma dvd_GcdD: "x dvd Gcd A \<Longrightarrow> y \<in> A \<Longrightarrow> x dvd y"
   980   using Gcd_dvd dvd_trans by blast
   981 
   982 lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
   983   by (blast dest: dvd_GcdD intro: Gcd_greatest)
   984 
   985 lemma Gcd_mult: "Gcd ((*) c ` A) = normalize c * Gcd A"
   986 proof (cases "c = 0")
   987   case True
   988   then show ?thesis by auto
   989 next
   990   case [simp]: False
   991   have "Gcd ((*) c ` A) div c dvd Gcd A"
   992     by (intro Gcd_greatest, subst div_dvd_iff_mult)
   993        (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
   994   then have "Gcd ((*) c ` A) dvd c * Gcd A"
   995     by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
   996   also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
   997     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
   998   also have "Gcd ((*) c ` A) dvd \<dots> \<longleftrightarrow> Gcd ((*) c ` A) dvd normalize c * Gcd A"
   999     by (simp add: dvd_mult_unit_iff)
  1000   finally have "Gcd ((*) c ` A) dvd normalize c * Gcd A" .
  1001   moreover have "normalize c * Gcd A dvd Gcd ((*) c ` A)"
  1002     by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
  1003   ultimately have "normalize (Gcd ((*) c ` A)) = normalize (normalize c * Gcd A)"
  1004     by (rule associatedI)
  1005   then show ?thesis
  1006     by (simp add: normalize_mult)
  1007 qed
  1008 
  1009 lemma Lcm_eqI:
  1010   assumes "normalize a = a"
  1011     and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
  1012     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> b dvd c) \<Longrightarrow> a dvd c"
  1013   shows "Lcm A = a"
  1014   using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
  1015 
  1016 lemma Lcm_dvdD: "Lcm A dvd x \<Longrightarrow> y \<in> A \<Longrightarrow> y dvd x"
  1017   using dvd_Lcm dvd_trans by blast
  1018 
  1019 lemma Lcm_dvd_iff: "Lcm A dvd x \<longleftrightarrow> (\<forall>y\<in>A. y dvd x)"
  1020   by (blast dest: Lcm_dvdD intro: Lcm_least)
  1021 
  1022 lemma Lcm_mult:
  1023   assumes "A \<noteq> {}"
  1024   shows "Lcm ((*) c ` A) = normalize c * Lcm A"
  1025 proof (cases "c = 0")
  1026   case True
  1027   with assms have "(*) c ` A = {0}"
  1028     by auto
  1029   with True show ?thesis by auto
  1030 next
  1031   case [simp]: False
  1032   from assms obtain x where x: "x \<in> A"
  1033     by blast
  1034   have "c dvd c * x"
  1035     by simp
  1036   also from x have "c * x dvd Lcm ((*) c ` A)"
  1037     by (intro dvd_Lcm) auto
  1038   finally have dvd: "c dvd Lcm ((*) c ` A)" .
  1039   moreover have "Lcm A dvd Lcm ((*) c ` A) div c"
  1040     by (intro Lcm_least dvd_mult_imp_div)
  1041       (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
  1042   ultimately have "c * Lcm A dvd Lcm ((*) c ` A)"
  1043     by auto
  1044   also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
  1045     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
  1046   also have "\<dots> dvd Lcm ((*) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm ((*) c ` A)"
  1047     by (simp add: mult_unit_dvd_iff)
  1048   finally have "normalize c * Lcm A dvd Lcm ((*) c ` A)" .
  1049   moreover have "Lcm ((*) c ` A) dvd normalize c * Lcm A"
  1050     by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
  1051   ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm ((*) c ` A))"
  1052     by (rule associatedI)
  1053   then show ?thesis
  1054     by (simp add: normalize_mult)
  1055 qed
  1056 
  1057 lemma Lcm_no_units: "Lcm A = Lcm (A - {a. is_unit a})"
  1058 proof -
  1059   have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A"
  1060     by blast
  1061   then have "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
  1062     by (simp add: Lcm_Un [symmetric])
  1063   also have "Lcm {a\<in>A. is_unit a} = 1"
  1064     by simp
  1065   finally show ?thesis
  1066     by simp
  1067 qed
  1068 
  1069 lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> (\<nexists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
  1070   by (metis Lcm_least dvd_0_left dvd_Lcm)
  1071 
  1072 lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not> a dvd m)) \<Longrightarrow> Lcm A = 0"
  1073   by (auto simp: Lcm_0_iff')
  1074 
  1075 lemma Lcm_singleton [simp]: "Lcm {a} = normalize a"
  1076   by simp
  1077 
  1078 lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
  1079   by simp
  1080 
  1081 lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1"
  1082   by (auto intro!: Gcd_eq_1_I)
  1083 
  1084 lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
  1085   by simp
  1086 
  1087 lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
  1088   by simp
  1089 
  1090 lemma Gcd_mono:
  1091   assumes "\<And>x. x \<in> A \<Longrightarrow> f x dvd g x"
  1092   shows   "(GCD x\<in>A. f x) dvd (GCD x\<in>A. g x)"
  1093 proof (intro Gcd_greatest, safe)
  1094   fix x assume "x \<in> A"
  1095   hence "(GCD x\<in>A. f x) dvd f x"
  1096     by (intro Gcd_dvd) auto
  1097   also have "f x dvd g x"
  1098     using \<open>x \<in> A\<close> assms by blast
  1099   finally show "(GCD x\<in>A. f x) dvd \<dots>" .
  1100 qed
  1101 
  1102 lemma Lcm_mono:
  1103   assumes "\<And>x. x \<in> A \<Longrightarrow> f x dvd g x"
  1104   shows   "(LCM x\<in>A. f x) dvd (LCM x\<in>A. g x)"
  1105 proof (intro Lcm_least, safe)
  1106   fix x assume "x \<in> A"
  1107   hence "f x dvd g x" by (rule assms)
  1108   also have "g x dvd (LCM x\<in>A. g x)"
  1109     using \<open>x \<in> A\<close> by (intro dvd_Lcm) auto
  1110   finally show "f x dvd \<dots>" .
  1111 qed
  1112 
  1113 end
  1114 
  1115 
  1116 subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close>
  1117 
  1118 context semiring_gcd
  1119 begin
  1120 
  1121 sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
  1122 defines
  1123   Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n") = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
  1124 
  1125 abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
  1126   where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
  1127 
  1128 sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
  1129 defines
  1130   Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n") = Lcm_fin.F ..
  1131 
  1132 abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
  1133   where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
  1134 
  1135 lemma Gcd_fin_dvd:
  1136   "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a"
  1137   by (induct A rule: infinite_finite_induct)
  1138     (auto intro: dvd_trans)
  1139 
  1140 lemma dvd_Lcm_fin:
  1141   "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A"
  1142   by (induct A rule: infinite_finite_induct)
  1143     (auto intro: dvd_trans)
  1144 
  1145 lemma Gcd_fin_greatest:
  1146   "a dvd Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
  1147   using that by (induct A) simp_all
  1148 
  1149 lemma Lcm_fin_least:
  1150   "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd a" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
  1151   using that by (induct A) simp_all
  1152 
  1153 lemma gcd_list_greatest:
  1154   "a dvd gcd_list bs" if "\<And>b. b \<in> set bs \<Longrightarrow> a dvd b"
  1155   by (rule Gcd_fin_greatest) (simp_all add: that)
  1156 
  1157 lemma lcm_list_least:
  1158   "lcm_list bs dvd a" if "\<And>b. b \<in> set bs \<Longrightarrow> b dvd a"
  1159   by (rule Lcm_fin_least) (simp_all add: that)
  1160 
  1161 lemma dvd_Gcd_fin_iff:
  1162   "b dvd Gcd\<^sub>f\<^sub>i\<^sub>n A \<longleftrightarrow> (\<forall>a\<in>A. b dvd a)" if "finite A"
  1163   using that by (auto intro: Gcd_fin_greatest Gcd_fin_dvd dvd_trans [of b "Gcd\<^sub>f\<^sub>i\<^sub>n A"])
  1164 
  1165 lemma dvd_gcd_list_iff:
  1166   "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)"
  1167   by (simp add: dvd_Gcd_fin_iff)
  1168 
  1169 lemma Lcm_fin_dvd_iff:
  1170   "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b  \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A"
  1171   using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b])
  1172 
  1173 lemma lcm_list_dvd_iff:
  1174   "lcm_list xs dvd b  \<longleftrightarrow> (\<forall>a\<in>set xs. a dvd b)"
  1175   by (simp add: Lcm_fin_dvd_iff)
  1176 
  1177 lemma Gcd_fin_mult:
  1178   "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A"
  1179 using that proof induct
  1180   case empty
  1181   then show ?case
  1182     by simp
  1183 next
  1184   case (insert a A)
  1185   have "gcd (b * a) (b * Gcd\<^sub>f\<^sub>i\<^sub>n A) = gcd (b * a) (normalize (b * Gcd\<^sub>f\<^sub>i\<^sub>n A))"
  1186     by simp
  1187   also have "\<dots> = gcd (b * a) (normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A)"
  1188     by (simp add: normalize_mult)
  1189   finally show ?case
  1190     using insert by (simp add: gcd_mult_distrib')
  1191 qed
  1192 
  1193 lemma Lcm_fin_mult:
  1194   "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A" if "A \<noteq> {}"
  1195 proof (cases "b = 0")
  1196   case True
  1197   moreover from that have "times 0 ` A = {0}"
  1198     by auto
  1199   ultimately show ?thesis
  1200     by simp
  1201 next
  1202   case False
  1203   show ?thesis proof (cases "finite A")
  1204     case False
  1205     moreover have "inj_on (times b) A"
  1206       using \<open>b \<noteq> 0\<close> by (rule inj_on_mult)
  1207     ultimately have "infinite (times b ` A)"
  1208       by (simp add: finite_image_iff)
  1209     with False show ?thesis
  1210       by simp
  1211   next
  1212     case True
  1213     then show ?thesis using that proof (induct A rule: finite_ne_induct)
  1214       case (singleton a)
  1215       then show ?case
  1216         by (simp add: normalize_mult)
  1217     next
  1218       case (insert a A)
  1219       have "lcm (b * a) (b * Lcm\<^sub>f\<^sub>i\<^sub>n A) = lcm (b * a) (normalize (b * Lcm\<^sub>f\<^sub>i\<^sub>n A))"
  1220         by simp
  1221       also have "\<dots> = lcm (b * a) (normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A)"
  1222         by (simp add: normalize_mult)
  1223       finally show ?case
  1224         using insert by (simp add: lcm_mult_distrib')
  1225     qed
  1226   qed
  1227 qed
  1228 
  1229 lemma unit_factor_Gcd_fin:
  1230   "unit_factor (Gcd\<^sub>f\<^sub>i\<^sub>n A) = of_bool (Gcd\<^sub>f\<^sub>i\<^sub>n A \<noteq> 0)"
  1231   by (rule normalize_idem_imp_unit_factor_eq) simp
  1232 
  1233 lemma unit_factor_Lcm_fin:
  1234   "unit_factor (Lcm\<^sub>f\<^sub>i\<^sub>n A) = of_bool (Lcm\<^sub>f\<^sub>i\<^sub>n A \<noteq> 0)"
  1235   by (rule normalize_idem_imp_unit_factor_eq) simp
  1236 
  1237 lemma is_unit_Gcd_fin_iff [simp]:
  1238   "is_unit (Gcd\<^sub>f\<^sub>i\<^sub>n A) \<longleftrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A = 1"
  1239   by (rule normalize_idem_imp_is_unit_iff) simp
  1240 
  1241 lemma is_unit_Lcm_fin_iff [simp]:
  1242   "is_unit (Lcm\<^sub>f\<^sub>i\<^sub>n A) \<longleftrightarrow> Lcm\<^sub>f\<^sub>i\<^sub>n A = 1"
  1243   by (rule normalize_idem_imp_is_unit_iff) simp
  1244  
  1245 lemma Gcd_fin_0_iff:
  1246   "Gcd\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> A \<subseteq> {0} \<and> finite A"
  1247   by (induct A rule: infinite_finite_induct) simp_all
  1248 
  1249 lemma Lcm_fin_0_iff:
  1250   "Lcm\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> 0 \<in> A" if "finite A"
  1251   using that by (induct A) (auto simp: lcm_eq_0_iff)
  1252 
  1253 lemma Lcm_fin_1_iff:
  1254   "Lcm\<^sub>f\<^sub>i\<^sub>n A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a) \<and> finite A"
  1255   by (induct A rule: infinite_finite_induct) simp_all
  1256 
  1257 end
  1258 
  1259 context semiring_Gcd
  1260 begin
  1261 
  1262 lemma Gcd_fin_eq_Gcd [simp]:
  1263   "Gcd\<^sub>f\<^sub>i\<^sub>n A = Gcd A" if "finite A" for A :: "'a set"
  1264   using that by induct simp_all
  1265 
  1266 lemma Gcd_set_eq_fold [code_unfold]:
  1267   "Gcd (set xs) = fold gcd xs 0"
  1268   by (simp add: Gcd_fin.set_eq_fold [symmetric])
  1269 
  1270 lemma Lcm_fin_eq_Lcm [simp]:
  1271   "Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A" if "finite A" for A :: "'a set"
  1272   using that by induct simp_all
  1273 
  1274 lemma Lcm_set_eq_fold [code_unfold]:
  1275   "Lcm (set xs) = fold lcm xs 1"
  1276   by (simp add: Lcm_fin.set_eq_fold [symmetric])
  1277 
  1278 end
  1279 
  1280 
  1281 subsection \<open>Coprimality\<close>
  1282 
  1283 context semiring_gcd
  1284 begin
  1285 
  1286 lemma coprime_imp_gcd_eq_1 [simp]:
  1287   "gcd a b = 1" if "coprime a b"
  1288 proof -
  1289   define t r s where "t = gcd a b" and "r = a div t" and "s = b div t"
  1290   then have "a = t * r" and "b = t * s"
  1291     by simp_all
  1292   with that have "coprime (t * r) (t * s)"
  1293     by simp
  1294   then show ?thesis
  1295     by (simp add: t_def)
  1296 qed
  1297 
  1298 lemma gcd_eq_1_imp_coprime [dest!]:
  1299   "coprime a b" if "gcd a b = 1"
  1300 proof (rule coprimeI)
  1301   fix c
  1302   assume "c dvd a" and "c dvd b"
  1303   then have "c dvd gcd a b"
  1304     by (rule gcd_greatest)
  1305   with that show "is_unit c"
  1306     by simp
  1307 qed
  1308 
  1309 lemma coprime_iff_gcd_eq_1 [presburger, code]:
  1310   "coprime a b \<longleftrightarrow> gcd a b = 1"
  1311   by rule (simp_all add: gcd_eq_1_imp_coprime)
  1312 
  1313 lemma is_unit_gcd [simp]:
  1314   "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
  1315   by (simp add: coprime_iff_gcd_eq_1)
  1316 
  1317 lemma coprime_add_one_left [simp]: "coprime (a + 1) a"
  1318   by (simp add: gcd_eq_1_imp_coprime ac_simps)
  1319 
  1320 lemma coprime_add_one_right [simp]: "coprime a (a + 1)"
  1321   using coprime_add_one_left [of a] by (simp add: ac_simps)
  1322 
  1323 lemma coprime_mult_left_iff [simp]:
  1324   "coprime (a * b) c \<longleftrightarrow> coprime a c \<and> coprime b c"
  1325 proof
  1326   assume "coprime (a * b) c"
  1327   with coprime_common_divisor [of "a * b" c]
  1328   have *: "is_unit d" if "d dvd a * b" and "d dvd c" for d
  1329     using that by blast
  1330   have "coprime a c"
  1331     by (rule coprimeI, rule *) simp_all
  1332   moreover have "coprime b c"
  1333     by (rule coprimeI, rule *) simp_all
  1334   ultimately show "coprime a c \<and> coprime b c" ..
  1335 next
  1336   assume "coprime a c \<and> coprime b c"
  1337   then have "coprime a c" "coprime b c"
  1338     by simp_all
  1339   show "coprime (a * b) c"
  1340   proof (rule coprimeI)
  1341     fix d
  1342     assume "d dvd a * b"
  1343     then obtain r s where d: "d = r * s" "r dvd a" "s dvd b"
  1344       by (rule dvd_productE)
  1345     assume "d dvd c"
  1346     with d have "r * s dvd c"
  1347       by simp
  1348     then have "r dvd c" "s dvd c"
  1349       by (auto intro: dvd_mult_left dvd_mult_right)
  1350     from \<open>coprime a c\<close> \<open>r dvd a\<close> \<open>r dvd c\<close>
  1351     have "is_unit r"
  1352       by (rule coprime_common_divisor)
  1353     moreover from \<open>coprime b c\<close> \<open>s dvd b\<close> \<open>s dvd c\<close>
  1354     have "is_unit s"
  1355       by (rule coprime_common_divisor)
  1356     ultimately show "is_unit d"
  1357       by (simp add: d is_unit_mult_iff)
  1358   qed
  1359 qed
  1360 
  1361 lemma coprime_mult_right_iff [simp]:
  1362   "coprime c (a * b) \<longleftrightarrow> coprime c a \<and> coprime c b"
  1363   using coprime_mult_left_iff [of a b c] by (simp add: ac_simps)
  1364 
  1365 lemma coprime_power_left_iff [simp]:
  1366   "coprime (a ^ n) b \<longleftrightarrow> coprime a b \<or> n = 0"
  1367 proof (cases "n = 0")
  1368   case True
  1369   then show ?thesis
  1370     by simp
  1371 next
  1372   case False
  1373   then have "n > 0"
  1374     by simp
  1375   then show ?thesis
  1376     by (induction n rule: nat_induct_non_zero) simp_all
  1377 qed
  1378 
  1379 lemma coprime_power_right_iff [simp]:
  1380   "coprime a (b ^ n) \<longleftrightarrow> coprime a b \<or> n = 0"
  1381   using coprime_power_left_iff [of b n a] by (simp add: ac_simps)
  1382 
  1383 lemma prod_coprime_left:
  1384   "coprime (\<Prod>i\<in>A. f i) a" if "\<And>i. i \<in> A \<Longrightarrow> coprime (f i) a"
  1385   using that by (induct A rule: infinite_finite_induct) simp_all
  1386 
  1387 lemma prod_coprime_right:
  1388   "coprime a (\<Prod>i\<in>A. f i)" if "\<And>i. i \<in> A \<Longrightarrow> coprime a (f i)"
  1389   using that prod_coprime_left [of A f a] by (simp add: ac_simps)
  1390 
  1391 lemma prod_list_coprime_left:
  1392   "coprime (prod_list xs) a" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime x a"
  1393   using that by (induct xs) simp_all
  1394 
  1395 lemma prod_list_coprime_right:
  1396   "coprime a (prod_list xs)" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime a x"
  1397   using that prod_list_coprime_left [of xs a] by (simp add: ac_simps)
  1398 
  1399 lemma coprime_dvd_mult_left_iff:
  1400   "a dvd b * c \<longleftrightarrow> a dvd b" if "coprime a c"
  1401 proof
  1402   assume "a dvd b"
  1403   then show "a dvd b * c"
  1404     by simp
  1405 next
  1406   assume "a dvd b * c"
  1407   show "a dvd b"
  1408   proof (cases "b = 0")
  1409     case True
  1410     then show ?thesis
  1411       by simp
  1412   next
  1413     case False
  1414     then have unit: "is_unit (unit_factor b)"
  1415       by simp
  1416     from \<open>coprime a c\<close> mult_gcd_left [of b a c]
  1417     have "gcd (b * a) (b * c) * unit_factor b = b"
  1418       by (simp add: ac_simps)
  1419     moreover from \<open>a dvd b * c\<close>
  1420     have "a dvd gcd (b * a) (b * c) * unit_factor b"
  1421       by (simp add: dvd_mult_unit_iff unit)
  1422     ultimately show ?thesis
  1423       by simp
  1424   qed
  1425 qed
  1426 
  1427 lemma coprime_dvd_mult_right_iff:
  1428   "a dvd c * b \<longleftrightarrow> a dvd b" if "coprime a c"
  1429   using that coprime_dvd_mult_left_iff [of a c b] by (simp add: ac_simps)
  1430 
  1431 lemma divides_mult:
  1432   "a * b dvd c" if "a dvd c" and "b dvd c" and "coprime a b"
  1433 proof -
  1434   from \<open>b dvd c\<close> obtain b' where "c = b * b'" ..
  1435   with \<open>a dvd c\<close> have "a dvd b' * b"
  1436     by (simp add: ac_simps)
  1437   with \<open>coprime a b\<close> have "a dvd b'"
  1438     by (simp add: coprime_dvd_mult_left_iff)
  1439   then obtain a' where "b' = a * a'" ..
  1440   with \<open>c = b * b'\<close> have "c = (a * b) * a'"
  1441     by (simp add: ac_simps)
  1442   then show ?thesis ..
  1443 qed
  1444 
  1445 lemma div_gcd_coprime:
  1446   assumes "a \<noteq> 0 \<or> b \<noteq> 0"
  1447   shows "coprime (a div gcd a b) (b div gcd a b)"
  1448 proof -
  1449   let ?g = "gcd a b"
  1450   let ?a' = "a div ?g"
  1451   let ?b' = "b div ?g"
  1452   let ?g' = "gcd ?a' ?b'"
  1453   have dvdg: "?g dvd a" "?g dvd b"
  1454     by simp_all
  1455   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
  1456     by simp_all
  1457   from dvdg dvdg' obtain ka kb ka' kb' where
  1458     kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
  1459     unfolding dvd_def by blast
  1460   from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
  1461     by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
  1462   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
  1463     by (auto simp: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
  1464   have "?g \<noteq> 0"
  1465     using assms by simp
  1466   moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
  1467   ultimately show ?thesis
  1468     using dvd_times_left_cancel_iff [of "gcd a b" _ 1]
  1469     by simp (simp only: coprime_iff_gcd_eq_1)
  1470 qed
  1471 
  1472 lemma gcd_coprime:
  1473   assumes c: "gcd a b \<noteq> 0"
  1474     and a: "a = a' * gcd a b"
  1475     and b: "b = b' * gcd a b"
  1476   shows "coprime a' b'"
  1477 proof -
  1478   from c have "a \<noteq> 0 \<or> b \<noteq> 0"
  1479     by simp
  1480   with div_gcd_coprime have "coprime (a div gcd a b) (b div gcd a b)" .
  1481   also from assms have "a div gcd a b = a'"
  1482     using dvd_div_eq_mult local.gcd_dvd1 by blast
  1483   also from assms have "b div gcd a b = b'"
  1484     using dvd_div_eq_mult local.gcd_dvd1 by blast
  1485   finally show ?thesis .
  1486 qed
  1487 
  1488 lemma gcd_coprime_exists:
  1489   assumes "gcd a b \<noteq> 0"
  1490   shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
  1491 proof -
  1492   have "coprime (a div gcd a b) (b div gcd a b)"
  1493     using assms div_gcd_coprime by auto
  1494   then show ?thesis
  1495     by force
  1496 qed
  1497 
  1498 lemma pow_divides_pow_iff [simp]:
  1499   "a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" if "n > 0"
  1500 proof (cases "gcd a b = 0")
  1501   case True
  1502   then show ?thesis
  1503     by simp
  1504 next
  1505   case False
  1506   show ?thesis
  1507   proof
  1508     let ?d = "gcd a b"
  1509     from \<open>n > 0\<close> obtain m where m: "n = Suc m"
  1510       by (cases n) simp_all
  1511     from False have zn: "?d ^ n \<noteq> 0"
  1512       by (rule power_not_zero)
  1513     from gcd_coprime_exists [OF False]
  1514     obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
  1515       by blast
  1516     assume "a ^ n dvd b ^ n"
  1517     then have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
  1518       by (simp add: ab'(1,2)[symmetric])
  1519     then have "?d^n * a'^n dvd ?d^n * b'^n"
  1520       by (simp only: power_mult_distrib ac_simps)
  1521     with zn have "a' ^ n dvd b' ^ n"
  1522       by simp
  1523     then have "a' dvd b' ^ n"
  1524       using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
  1525     then have "a' dvd b' ^ m * b'"
  1526       by (simp add: m ac_simps)
  1527     moreover have "coprime a' (b' ^ n)"
  1528       using \<open>coprime a' b'\<close> by simp
  1529     then have "a' dvd b'"
  1530       using \<open>a' dvd b' ^ n\<close> coprime_dvd_mult_left_iff dvd_mult by blast
  1531     then have "a' * ?d dvd b' * ?d"
  1532       by (rule mult_dvd_mono) simp
  1533     with ab'(1,2) show "a dvd b"
  1534       by simp
  1535   next
  1536     assume "a dvd b"
  1537     with \<open>n > 0\<close> show "a ^ n dvd b ^ n"
  1538       by (induction rule: nat_induct_non_zero)
  1539         (simp_all add: mult_dvd_mono)
  1540   qed
  1541 qed
  1542 
  1543 lemma coprime_crossproduct:
  1544   fixes a b c d :: 'a
  1545   assumes "coprime a d" and "coprime b c"
  1546   shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
  1547     normalize a = normalize b \<and> normalize c = normalize d"
  1548     (is "?lhs \<longleftrightarrow> ?rhs")
  1549 proof
  1550   assume ?rhs
  1551   then show ?lhs by simp
  1552 next
  1553   assume ?lhs
  1554   from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
  1555     by (auto intro: dvdI dest: sym)
  1556   with \<open>coprime a d\<close> have "a dvd b"
  1557     by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
  1558   from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
  1559     by (auto intro: dvdI dest: sym)
  1560   with \<open>coprime b c\<close> have "b dvd a"
  1561     by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
  1562   from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
  1563     by (auto intro: dvdI dest: sym simp add: mult.commute)
  1564   with \<open>coprime b c\<close> have "c dvd d"
  1565     by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
  1566   from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
  1567     by (auto intro: dvdI dest: sym simp add: mult.commute)
  1568   with \<open>coprime a d\<close> have "d dvd c"
  1569     by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
  1570   from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
  1571     by (rule associatedI)
  1572   moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
  1573     by (rule associatedI)
  1574   ultimately show ?rhs ..
  1575 qed
  1576 
  1577 lemma coprime_crossproduct':
  1578   fixes a b c d
  1579   assumes "b \<noteq> 0"
  1580   assumes unit_factors: "unit_factor b = unit_factor d"
  1581   assumes coprime: "coprime a b" "coprime c d"
  1582   shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
  1583 proof safe
  1584   assume eq: "a * d = b * c"
  1585   hence "normalize a * normalize d = normalize c * normalize b"
  1586     by (simp only: normalize_mult [symmetric] mult_ac)
  1587   with coprime have "normalize b = normalize d"
  1588     by (subst (asm) coprime_crossproduct) simp_all
  1589   from this and unit_factors show "b = d"
  1590     by (rule normalize_unit_factor_eqI)
  1591   from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
  1592   with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
  1593 qed (simp_all add: mult_ac)
  1594 
  1595 lemma gcd_mult_left_left_cancel:
  1596   "gcd (c * a) b = gcd a b" if "coprime b c"
  1597 proof -
  1598   have "coprime (gcd b (a * c)) c"
  1599     by (rule coprimeI) (auto intro: that coprime_common_divisor)
  1600   then have "gcd b (a * c) dvd a"
  1601     using coprime_dvd_mult_left_iff [of "gcd b (a * c)" c a]
  1602     by simp
  1603   then show ?thesis
  1604     by (auto intro: associated_eqI simp add: ac_simps)
  1605 qed
  1606 
  1607 lemma gcd_mult_left_right_cancel:
  1608   "gcd (a * c) b = gcd a b" if "coprime b c"
  1609   using that gcd_mult_left_left_cancel [of b c a]
  1610   by (simp add: ac_simps)
  1611 
  1612 lemma gcd_mult_right_left_cancel:
  1613   "gcd a (c * b) = gcd a b" if "coprime a c"
  1614   using that gcd_mult_left_left_cancel [of a c b]
  1615   by (simp add: ac_simps)
  1616 
  1617 lemma gcd_mult_right_right_cancel:
  1618   "gcd a (b * c) = gcd a b" if "coprime a c"
  1619   using that gcd_mult_right_left_cancel [of a c b]
  1620   by (simp add: ac_simps)
  1621 
  1622 lemma gcd_exp [simp]:
  1623   "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
  1624 proof (cases "a = 0 \<and> b = 0 \<or> n = 0")
  1625   case True
  1626   then show ?thesis
  1627     by (cases n) simp_all
  1628 next
  1629   case False
  1630   then have "coprime (a div gcd a b) (b div gcd a b)" and "n > 0"
  1631     by (auto intro: div_gcd_coprime)
  1632   then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
  1633     by simp
  1634   then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
  1635     by simp
  1636   then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
  1637     by simp
  1638   also note gcd_mult_distrib
  1639   also have "unit_factor (gcd a b ^ n) = 1"
  1640     using False by (auto simp: unit_factor_power unit_factor_gcd)
  1641   also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
  1642     by (simp add: ac_simps div_power dvd_power_same)
  1643   also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
  1644     by (simp add: ac_simps div_power dvd_power_same)
  1645   finally show ?thesis by simp
  1646 qed
  1647 
  1648 lemma division_decomp:
  1649   assumes "a dvd b * c"
  1650   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  1651 proof (cases "gcd a b = 0")
  1652   case True
  1653   then have "a = 0 \<and> b = 0"
  1654     by simp
  1655   then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
  1656     by simp
  1657   then show ?thesis by blast
  1658 next
  1659   case False
  1660   let ?d = "gcd a b"
  1661   from gcd_coprime_exists [OF False]
  1662     obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
  1663     by blast
  1664   from ab'(1) have "a' dvd a" ..
  1665   with assms have "a' dvd b * c"
  1666     using dvd_trans [of a' a "b * c"] by simp
  1667   from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
  1668     by simp
  1669   then have "?d * a' dvd ?d * (b' * c)"
  1670     by (simp add: mult_ac)
  1671   with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
  1672     by simp
  1673   then have "a' dvd c"
  1674     using \<open>coprime a' b'\<close> by (simp add: coprime_dvd_mult_right_iff)
  1675   with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
  1676     by (simp add: ac_simps)
  1677   then show ?thesis by blast
  1678 qed
  1679 
  1680 lemma lcm_coprime: "coprime a b \<Longrightarrow> lcm a b = normalize (a * b)"
  1681   by (subst lcm_gcd) simp
  1682 
  1683 end
  1684 
  1685 context ring_gcd
  1686 begin
  1687 
  1688 lemma coprime_minus_left_iff [simp]:
  1689   "coprime (- a) b \<longleftrightarrow> coprime a b"
  1690   by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
  1691 
  1692 lemma coprime_minus_right_iff [simp]:
  1693   "coprime a (- b) \<longleftrightarrow> coprime a b"
  1694   using coprime_minus_left_iff [of b a] by (simp add: ac_simps)
  1695 
  1696 lemma coprime_diff_one_left [simp]: "coprime (a - 1) a"
  1697   using coprime_add_one_right [of "a - 1"] by simp
  1698 
  1699 lemma coprime_doff_one_right [simp]: "coprime a (a - 1)"
  1700   using coprime_diff_one_left [of a] by (simp add: ac_simps)
  1701 
  1702 end
  1703 
  1704 context semiring_Gcd
  1705 begin
  1706 
  1707 lemma Lcm_coprime:
  1708   assumes "finite A"
  1709     and "A \<noteq> {}"
  1710     and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b"
  1711   shows "Lcm A = normalize (\<Prod>A)"
  1712   using assms
  1713 proof (induct rule: finite_ne_induct)
  1714   case singleton
  1715   then show ?case by simp
  1716 next
  1717   case (insert a A)
  1718   have "Lcm (insert a A) = lcm a (Lcm A)"
  1719     by simp
  1720   also from insert have "Lcm A = normalize (\<Prod>A)"
  1721     by blast
  1722   also have "lcm a \<dots> = lcm a (\<Prod>A)"
  1723     by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
  1724   also from insert have "coprime a (\<Prod>A)"
  1725     by (subst coprime_commute, intro prod_coprime_left) auto
  1726   with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
  1727     by (simp add: lcm_coprime)
  1728   finally show ?case .
  1729 qed
  1730 
  1731 lemma Lcm_coprime':
  1732   "card A \<noteq> 0 \<Longrightarrow>
  1733     (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b) \<Longrightarrow>
  1734     Lcm A = normalize (\<Prod>A)"
  1735   by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
  1736 
  1737 end
  1738 
  1739 
  1740 subsection \<open>GCD and LCM on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close>
  1741 
  1742 instantiation nat :: gcd
  1743 begin
  1744 
  1745 fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  1746   where "gcd_nat x y = (if y = 0 then x else gcd y (x mod y))"
  1747 
  1748 definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  1749   where "lcm_nat x y = x * y div (gcd x y)"
  1750 
  1751 instance ..
  1752 
  1753 end
  1754 
  1755 instantiation int :: gcd
  1756 begin
  1757 
  1758 definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
  1759   where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
  1760 
  1761 definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
  1762   where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
  1763 
  1764 instance ..
  1765 
  1766 end
  1767 
  1768 lemma gcd_int_int_eq [simp]:
  1769   "gcd (int m) (int n) = int (gcd m n)"
  1770   by (simp add: gcd_int_def)
  1771 
  1772 lemma gcd_nat_abs_left_eq [simp]:
  1773   "gcd (nat \<bar>k\<bar>) n = nat (gcd k (int n))"
  1774   by (simp add: gcd_int_def)
  1775 
  1776 lemma gcd_nat_abs_right_eq [simp]:
  1777   "gcd n (nat \<bar>k\<bar>) = nat (gcd (int n) k)"
  1778   by (simp add: gcd_int_def)
  1779 
  1780 lemma abs_gcd_int [simp]:
  1781   "\<bar>gcd x y\<bar> = gcd x y"
  1782   for x y :: int
  1783   by (simp only: gcd_int_def)
  1784 
  1785 lemma gcd_abs1_int [simp]:
  1786   "gcd \<bar>x\<bar> y = gcd x y"
  1787   for x y :: int
  1788   by (simp only: gcd_int_def) simp
  1789 
  1790 lemma gcd_abs2_int [simp]:
  1791   "gcd x \<bar>y\<bar> = gcd x y"
  1792   for x y :: int
  1793   by (simp only: gcd_int_def) simp
  1794 
  1795 lemma lcm_int_int_eq [simp]:
  1796   "lcm (int m) (int n) = int (lcm m n)"
  1797   by (simp add: lcm_int_def)
  1798 
  1799 lemma lcm_nat_abs_left_eq [simp]:
  1800   "lcm (nat \<bar>k\<bar>) n = nat (lcm k (int n))"
  1801   by (simp add: lcm_int_def)
  1802 
  1803 lemma lcm_nat_abs_right_eq [simp]:
  1804   "lcm n (nat \<bar>k\<bar>) = nat (lcm (int n) k)"
  1805   by (simp add: lcm_int_def)
  1806 
  1807 lemma lcm_abs1_int [simp]:
  1808   "lcm \<bar>x\<bar> y = lcm x y"
  1809   for x y :: int
  1810   by (simp only: lcm_int_def) simp
  1811 
  1812 lemma lcm_abs2_int [simp]:
  1813   "lcm x \<bar>y\<bar> = lcm x y"
  1814   for x y :: int
  1815   by (simp only: lcm_int_def) simp
  1816 
  1817 lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
  1818   for i j :: int
  1819   by (simp only: lcm_int_def)
  1820 
  1821 lemma gcd_nat_induct [case_names base step]:
  1822   fixes m n :: nat
  1823   assumes "\<And>m. P m 0"
  1824     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
  1825   shows "P m n"
  1826 proof (induction m n rule: gcd_nat.induct)
  1827   case (1 x y)
  1828   then show ?case
  1829     using assms neq0_conv by blast
  1830 qed
  1831 
  1832 lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
  1833   for x y :: int
  1834   by (simp only: gcd_int_def) simp
  1835 
  1836 lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y"
  1837   for x y :: int
  1838   by (simp only: gcd_int_def) simp
  1839 
  1840 lemma gcd_cases_int:
  1841   fixes x y :: int
  1842   assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd x y)"
  1843     and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd x (- y))"
  1844     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd (- x) y)"
  1845     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd (- x) (- y))"
  1846   shows "P (gcd x y)"
  1847   using assms by auto arith
  1848 
  1849 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
  1850   for x y :: int
  1851   by (simp add: gcd_int_def)
  1852 
  1853 lemma lcm_neg1_int: "lcm (- x) y = lcm x y"
  1854   for x y :: int
  1855   by (simp only: lcm_int_def) simp
  1856 
  1857 lemma lcm_neg2_int: "lcm x (- y) = lcm x y"
  1858   for x y :: int
  1859   by (simp only: lcm_int_def) simp
  1860 
  1861 lemma lcm_cases_int:
  1862   fixes x y :: int
  1863   assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm x y)"
  1864     and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm x (- y))"
  1865     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm (- x) y)"
  1866     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm (- x) (- y))"
  1867   shows "P (lcm x y)"
  1868   using assms by (auto simp: lcm_neg1_int lcm_neg2_int) arith
  1869 
  1870 lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
  1871   for x y :: int
  1872   by (simp only: lcm_int_def)
  1873 
  1874 lemma gcd_0_nat: "gcd x 0 = x"
  1875   for x :: nat
  1876   by simp
  1877 
  1878 lemma gcd_0_int [simp]: "gcd x 0 = \<bar>x\<bar>"
  1879   for x :: int
  1880   by (auto simp: gcd_int_def)
  1881 
  1882 lemma gcd_0_left_nat: "gcd 0 x = x"
  1883   for x :: nat
  1884   by simp
  1885 
  1886 lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>"
  1887   for x :: int
  1888   by (auto simp: gcd_int_def)
  1889 
  1890 lemma gcd_red_nat: "gcd x y = gcd y (x mod y)"
  1891   for x y :: nat
  1892   by (cases "y = 0") auto
  1893 
  1894 
  1895 text \<open>Weaker, but useful for the simplifier.\<close>
  1896 
  1897 lemma gcd_non_0_nat: "y \<noteq> 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
  1898   for x y :: nat
  1899   by simp
  1900 
  1901 lemma gcd_1_nat [simp]: "gcd m 1 = 1"
  1902   for m :: nat
  1903   by simp
  1904 
  1905 lemma gcd_Suc_0 [simp]: "gcd m (Suc 0) = Suc 0"
  1906   for m :: nat
  1907   by simp
  1908 
  1909 lemma gcd_1_int [simp]: "gcd m 1 = 1"
  1910   for m :: int
  1911   by (simp add: gcd_int_def)
  1912 
  1913 lemma gcd_idem_nat: "gcd x x = x"
  1914   for x :: nat
  1915   by simp
  1916 
  1917 lemma gcd_idem_int: "gcd x x = \<bar>x\<bar>"
  1918   for x :: int
  1919   by (auto simp: gcd_int_def)
  1920 
  1921 declare gcd_nat.simps [simp del]
  1922 
  1923 text \<open>
  1924   \<^medskip> \<^term>\<open>gcd m n\<close> divides \<open>m\<close> and \<open>n\<close>.
  1925   The conjunctions don't seem provable separately.
  1926 \<close>
  1927 
  1928 instance nat :: semiring_gcd
  1929 proof
  1930   fix m n :: nat
  1931   show "gcd m n dvd m" and "gcd m n dvd n"
  1932   proof (induct m n rule: gcd_nat_induct)
  1933     case (step m n)
  1934     then have "gcd n (m mod n) dvd m"
  1935       by (metis dvd_mod_imp_dvd)
  1936     with step show "gcd m n dvd m"
  1937       by (simp add: gcd_non_0_nat)
  1938   qed (simp_all add: gcd_0_nat gcd_non_0_nat)
  1939 next
  1940   fix m n k :: nat
  1941   assume "k dvd m" and "k dvd n"
  1942   then show "k dvd gcd m n"
  1943     by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
  1944 qed (simp_all add: lcm_nat_def)
  1945 
  1946 instance int :: ring_gcd
  1947 proof
  1948   fix k l r :: int
  1949   show "gcd k l dvd k" "gcd k l dvd l"
  1950     using gcd_dvd1 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
  1951       gcd_dvd2 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
  1952     by simp_all
  1953   show "lcm k l = normalize (k * l) div gcd k l"
  1954     using lcm_gcd [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
  1955     by (simp add: nat_eq_iff of_nat_div abs_mult)
  1956   assume "r dvd k" "r dvd l"
  1957   then show "r dvd gcd k l"
  1958     using gcd_greatest [of "nat \<bar>r\<bar>" "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
  1959     by simp
  1960 qed simp
  1961 
  1962 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a"
  1963   for a b :: nat
  1964   by (rule dvd_imp_le) auto
  1965 
  1966 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd a b \<le> b"
  1967   for a b :: nat
  1968   by (rule dvd_imp_le) auto
  1969 
  1970 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd a b \<le> a"
  1971   for a b :: int
  1972   by (rule zdvd_imp_le) auto
  1973 
  1974 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd a b \<le> b"
  1975   for a b :: int
  1976   by (rule zdvd_imp_le) auto
  1977 
  1978 lemma gcd_pos_nat [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
  1979   for m n :: nat
  1980   using gcd_eq_0_iff [of m n] by arith
  1981 
  1982 lemma gcd_pos_int [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
  1983   for m n :: int
  1984   using gcd_eq_0_iff [of m n] gcd_ge_0_int [of m n] by arith
  1985 
  1986 lemma gcd_unique_nat: "d dvd a \<and> d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
  1987   for d a :: nat
  1988   using gcd_unique by fastforce
  1989 
  1990 lemma gcd_unique_int:
  1991   "d \<ge> 0 \<and> d dvd a \<and> d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
  1992   for d a :: int
  1993   using zdvd_antisym_nonneg by auto
  1994 
  1995 interpretation gcd_nat:
  1996   semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
  1997   by standard (auto simp: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
  1998 
  1999 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
  2000   for x y :: int
  2001   by (metis abs_dvd_iff gcd_0_left_int gcd_unique_int)
  2002 
  2003 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>"
  2004   for x y :: int
  2005   by (metis gcd_proj1_if_dvd_int gcd.commute)
  2006 
  2007 
  2008 text \<open>\<^medskip> Multiplication laws.\<close>
  2009 
  2010 lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
  2011   for k m n :: nat
  2012   \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
  2013 proof (induct m n rule: gcd_nat_induct)
  2014   case (step m n)
  2015   then show ?case
  2016     by (metis gcd_mult_distrib' gcd_red_nat)
  2017 qed auto
  2018 
  2019 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
  2020   for k m n :: int
  2021   using gcd_mult_distrib' [of k m n] by simp
  2022 
  2023 text \<open>\medskip Addition laws.\<close>
  2024 
  2025 (* TODO: add the other variations? *)
  2026 
  2027 lemma gcd_diff1_nat: "m \<ge> n \<Longrightarrow> gcd (m - n) n = gcd m n"
  2028   for m n :: nat
  2029   by (subst gcd_add1 [symmetric]) auto
  2030 
  2031 lemma gcd_diff2_nat: "n \<ge> m \<Longrightarrow> gcd (n - m) n = gcd m n"
  2032   for m n :: nat
  2033   by (metis gcd.commute gcd_add2 gcd_diff1_nat le_add_diff_inverse2)
  2034 
  2035 lemma gcd_non_0_int: 
  2036   fixes x y :: int
  2037   assumes "y > 0" shows "gcd x y = gcd y (x mod y)"
  2038 proof (cases "x mod y = 0")
  2039   case False
  2040   then have neg: "x mod y = y - (- x) mod y"
  2041     by (simp add: zmod_zminus1_eq_if)
  2042   have xy: "0 \<le> x mod y" 
  2043     by (simp add: assms)
  2044   show ?thesis
  2045   proof (cases "x < 0")
  2046     case True
  2047     have "nat (- x mod y) \<le> nat y"
  2048       by (simp add: assms dual_order.order_iff_strict)
  2049     moreover have "gcd (nat (- x)) (nat y) = gcd (nat (- x mod y)) (nat y)"
  2050       using True assms gcd_non_0_nat nat_mod_distrib by auto
  2051     ultimately have "gcd (nat (- x)) (nat y) = gcd (nat y) (nat (x mod y))"
  2052       using assms 
  2053       by (simp add: neg nat_diff_distrib') (metis gcd.commute gcd_diff2_nat)
  2054     with assms \<open>0 \<le> x mod y\<close> show ?thesis
  2055       by (simp add: True dual_order.order_iff_strict gcd_int_def)
  2056   next
  2057     case False
  2058     with assms xy have "gcd (nat x) (nat y) = gcd (nat y) (nat x mod nat y)"
  2059       using gcd_red_nat by blast
  2060     with False assms show ?thesis
  2061       by (simp add: gcd_int_def nat_mod_distrib)
  2062   qed
  2063 qed (use assms in auto)
  2064 
  2065 lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
  2066   for x y :: int
  2067 proof (cases y "0::int" rule: linorder_cases)
  2068   case less
  2069   with gcd_non_0_int [of "- y" "- x"] show ?thesis
  2070     by auto
  2071 next
  2072   case greater
  2073   with gcd_non_0_int [of y x] show ?thesis
  2074     by auto
  2075 qed auto
  2076 
  2077 (* TODO: differences, and all variations of addition rules
  2078     as simplification rules for nat and int *)
  2079 
  2080 (* TODO: add the three variations of these, and for ints? *)
  2081 
  2082 lemma finite_divisors_nat [simp]: (* FIXME move *)
  2083   fixes m :: nat
  2084   assumes "m > 0"
  2085   shows "finite {d. d dvd m}"
  2086 proof-
  2087   from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}"
  2088     by (auto dest: dvd_imp_le)
  2089   then show ?thesis
  2090     using finite_Collect_le_nat by (rule finite_subset)
  2091 qed
  2092 
  2093 lemma finite_divisors_int [simp]:
  2094   fixes i :: int
  2095   assumes "i \<noteq> 0"
  2096   shows "finite {d. d dvd i}"
  2097 proof -
  2098   have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}"
  2099     by (auto simp: abs_if)
  2100   then have "finite {d. \<bar>d\<bar> \<le> \<bar>i\<bar>}"
  2101     by simp
  2102   from finite_subset [OF _ this] show ?thesis
  2103     using assms by (simp add: dvd_imp_le_int subset_iff)
  2104 qed
  2105 
  2106 lemma Max_divisors_self_nat [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::nat. d dvd n} = n"
  2107   by (fastforce intro: antisym Max_le_iff[THEN iffD2] simp: dvd_imp_le)
  2108 
  2109 lemma Max_divisors_self_int [simp]: 
  2110   assumes "n \<noteq> 0" shows "Max {d::int. d dvd n} = \<bar>n\<bar>"
  2111 proof (rule antisym)
  2112   show "Max {d. d dvd n} \<le> \<bar>n\<bar>"
  2113     using assms by (auto intro: abs_le_D1 dvd_imp_le_int intro!: Max_le_iff [THEN iffD2])
  2114 qed (simp add: assms)
  2115 
  2116 lemma gcd_is_Max_divisors_nat:
  2117   fixes m n :: nat
  2118   assumes "n > 0" shows "gcd m n = Max {d. d dvd m \<and> d dvd n}"
  2119 proof (rule Max_eqI[THEN sym], simp_all)
  2120   show "finite {d. d dvd m \<and> d dvd n}"
  2121     by (simp add: \<open>n > 0\<close>)
  2122   show "\<And>y. y dvd m \<and> y dvd n \<Longrightarrow> y \<le> gcd m n"
  2123     by (simp add: \<open>n > 0\<close> dvd_imp_le)
  2124 qed
  2125 
  2126 lemma gcd_is_Max_divisors_int:
  2127   fixes m n :: int
  2128   assumes "n \<noteq> 0" shows "gcd m n = Max {d. d dvd m \<and> d dvd n}"
  2129 proof (rule Max_eqI[THEN sym], simp_all)
  2130   show "finite {d. d dvd m \<and> d dvd n}"
  2131     by (simp add: \<open>n \<noteq> 0\<close>)
  2132   show "\<And>y. y dvd m \<and> y dvd n \<Longrightarrow> y \<le> gcd m n"
  2133     by (simp add: \<open>n \<noteq> 0\<close> zdvd_imp_le)
  2134 qed
  2135 
  2136 lemma gcd_code_int [code]: "gcd k l = \<bar>if l = 0 then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  2137   for k l :: int
  2138   using gcd_red_int [of "\<bar>k\<bar>" "\<bar>l\<bar>"] by simp
  2139 
  2140 lemma coprime_Suc_left_nat [simp]:
  2141   "coprime (Suc n) n"
  2142   using coprime_add_one_left [of n] by simp
  2143 
  2144 lemma coprime_Suc_right_nat [simp]:
  2145   "coprime n (Suc n)"
  2146   using coprime_Suc_left_nat [of n] by (simp add: ac_simps)
  2147 
  2148 lemma coprime_diff_one_left_nat [simp]:
  2149   "coprime (n - 1) n" if "n > 0" for n :: nat
  2150   using that coprime_Suc_right_nat [of "n - 1"] by simp
  2151 
  2152 lemma coprime_diff_one_right_nat [simp]:
  2153   "coprime n (n - 1)" if "n > 0" for n :: nat
  2154   using that coprime_diff_one_left_nat [of n] by (simp add: ac_simps)
  2155 
  2156 lemma coprime_crossproduct_nat:
  2157   fixes a b c d :: nat
  2158   assumes "coprime a d" and "coprime b c"
  2159   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
  2160   using assms coprime_crossproduct [of a d b c] by simp
  2161 
  2162 lemma coprime_crossproduct_int:
  2163   fixes a b c d :: int
  2164   assumes "coprime a d" and "coprime b c"
  2165   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>"
  2166   using assms coprime_crossproduct [of a d b c] by simp
  2167 
  2168 
  2169 subsection \<open>Bezout's theorem\<close>
  2170 
  2171 text \<open>
  2172   Function \<open>bezw\<close> returns a pair of witnesses to Bezout's theorem --
  2173   see the theorems that follow the definition.
  2174 \<close>
  2175 
  2176 fun bezw :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  2177   where "bezw x y =
  2178     (if y = 0 then (1, 0)
  2179      else
  2180       (snd (bezw y (x mod y)),
  2181        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  2182 
  2183 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)"
  2184   by simp
  2185 
  2186 lemma bezw_non_0:
  2187   "y > 0 \<Longrightarrow> bezw x y =
  2188     (snd (bezw y (x mod y)), fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  2189   by simp
  2190 
  2191 declare bezw.simps [simp del]
  2192 
  2193 
  2194 lemma bezw_aux: "int (gcd x y) = fst (bezw x y) * int x + snd (bezw x y) * int y"
  2195 proof (induct x y rule: gcd_nat_induct)
  2196   case (step m n)
  2197   then have "fst (bezw m n) * int m + snd (bezw m n) * int n - int (gcd m n) 
  2198              = int m * snd (bezw n (m mod n)) -
  2199                (int (m mod n) * snd (bezw n (m mod n)) + int n * (int (m div n) * snd (bezw n (m mod n))))"
  2200     by (simp add: bezw_non_0 gcd_non_0_nat field_simps)
  2201   also have "\<dots> = int m * snd (bezw n (m mod n)) - (int (m mod n) + int (n * (m div n))) * snd (bezw n (m mod n))"
  2202     by (simp add: distrib_right)
  2203   also have "\<dots> = 0"
  2204     by (metis cancel_comm_monoid_add_class.diff_cancel mod_mult_div_eq of_nat_add)
  2205   finally show ?case
  2206     by simp
  2207 qed auto
  2208 
  2209 
  2210 lemma bezout_int: "\<exists>u v. u * x + v * y = gcd x y"
  2211   for x y :: int
  2212 proof -
  2213   have aux: "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> \<exists>u v. u * x + v * y = gcd x y" for x y :: int
  2214     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  2215     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  2216     by (simp add: bezw_aux gcd_int_def)
  2217   consider "x \<ge> 0" "y \<ge> 0" | "x \<ge> 0" "y \<le> 0" | "x \<le> 0" "y \<ge> 0" | "x \<le> 0" "y \<le> 0"
  2218     using linear by blast
  2219   then show ?thesis
  2220   proof cases
  2221     case 1
  2222     then show ?thesis by (rule aux)
  2223   next
  2224     case 2
  2225     then show ?thesis
  2226       using aux [of x "-y"]
  2227       by (metis gcd_neg2_int mult.commute mult_minus_right neg_0_le_iff_le)
  2228   next
  2229     case 3
  2230     then show ?thesis
  2231       using aux [of "-x" y]
  2232       by (metis gcd.commute gcd_neg2_int mult.commute mult_minus_right neg_0_le_iff_le)
  2233   next
  2234     case 4
  2235     then show ?thesis
  2236       using aux [of "-x" "-y"]
  2237       by (metis diff_0 diff_ge_0_iff_ge gcd_neg1_int gcd_neg2_int mult.commute mult_minus_right)
  2238   qed
  2239 qed
  2240 
  2241 
  2242 text \<open>Versions of Bezout for \<open>nat\<close>, by Amine Chaieb.\<close>
  2243 
  2244 lemma Euclid_induct [case_names swap zero add]:
  2245   fixes P :: "nat \<Rightarrow> nat \<Rightarrow> bool"
  2246   assumes c: "\<And>a b. P a b \<longleftrightarrow> P b a"
  2247     and z: "\<And>a. P a 0"
  2248     and add: "\<And>a b. P a b \<longrightarrow> P a (a + b)"
  2249   shows "P a b"
  2250 proof (induct "a + b" arbitrary: a b rule: less_induct)
  2251   case less
  2252   consider (eq) "a = b" | (lt) "a < b" "a + b - a < a + b" | "b = 0" | "b + a - b < a + b"
  2253     by arith
  2254   show ?case
  2255   proof (cases a b rule: linorder_cases)
  2256     case equal
  2257     with add [rule_format, OF z [rule_format, of a]] show ?thesis by simp
  2258   next
  2259     case lt: less
  2260     then consider "a = 0" | "a + b - a < a + b" by arith
  2261     then show ?thesis
  2262     proof cases
  2263       case 1
  2264       with z c show ?thesis by blast
  2265     next
  2266       case 2
  2267       also have *: "a + b - a = a + (b - a)" using lt by arith
  2268       finally have "a + (b - a) < a + b" .
  2269       then have "P a (a + (b - a))" by (rule add [rule_format, OF less])
  2270       then show ?thesis by (simp add: *[symmetric])
  2271     qed
  2272   next
  2273     case gt: greater
  2274     then consider "b = 0" | "b + a - b < a + b" by arith
  2275     then show ?thesis
  2276     proof cases
  2277       case 1
  2278       with z c show ?thesis by blast
  2279     next
  2280       case 2
  2281       also have *: "b + a - b = b + (a - b)" using gt by arith
  2282       finally have "b + (a - b) < a + b" .
  2283       then have "P b (b + (a - b))" by (rule add [rule_format, OF less])
  2284       then have "P b a" by (simp add: *[symmetric])
  2285       with c show ?thesis by blast
  2286     qed
  2287   qed
  2288 qed
  2289 
  2290 lemma bezout_lemma_nat:
  2291   fixes d::nat
  2292   shows "\<lbrakk>d dvd a; d dvd b; a * x = b * y + d \<or> b * x = a * y + d\<rbrakk>
  2293     \<Longrightarrow> \<exists>x y. d dvd a \<and> d dvd a + b \<and> (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  2294   apply auto
  2295   apply (metis add_mult_distrib2 left_add_mult_distrib)
  2296   apply (rule_tac x=x in exI)
  2297   by (metis add_mult_distrib2 mult.commute add.assoc)
  2298 
  2299 lemma bezout_add_nat: 
  2300   "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> b * x = a * y + d)"
  2301 proof (induct a b rule: Euclid_induct)
  2302   case (swap a b)
  2303   then show ?case
  2304     by blast
  2305 next
  2306   case (zero a)
  2307   then show ?case
  2308     by fastforce    
  2309 next
  2310   case (add a b)
  2311   then show ?case
  2312     by (meson bezout_lemma_nat)
  2313 qed
  2314 
  2315 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x - b * y = d \<or> b * x - a * y = d)"
  2316   using bezout_add_nat[of a b]  by (metis add_diff_cancel_left')
  2317 
  2318 lemma bezout_add_strong_nat:
  2319   fixes a b :: nat
  2320   assumes a: "a \<noteq> 0"
  2321   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  2322 proof -
  2323   consider d x y where "d dvd a" "d dvd b" "a * x = b * y + d"
  2324          | d x y where "d dvd a" "d dvd b" "b * x = a * y + d"
  2325     using bezout_add_nat [of a b] by blast
  2326   then show ?thesis
  2327   proof cases
  2328     case 1
  2329     then show ?thesis by blast
  2330   next
  2331     case H: 2
  2332     show ?thesis
  2333     proof (cases "b = 0")
  2334       case True
  2335       with H show ?thesis by simp
  2336     next
  2337       case False
  2338       then have bp: "b > 0" by simp
  2339       with dvd_imp_le [OF H(2)] consider "d = b" | "d < b"
  2340         by atomize_elim auto
  2341       then show ?thesis
  2342       proof cases
  2343         case 1
  2344         with a H show ?thesis
  2345           by (metis Suc_pred add.commute mult.commute mult_Suc_right neq0_conv)
  2346       next
  2347         case 2
  2348         show ?thesis
  2349         proof (cases "x = 0")
  2350           case True
  2351           with a H show ?thesis by simp
  2352         next
  2353           case x0: False
  2354           then have xp: "x > 0" by simp
  2355           from \<open>d < b\<close> have "d \<le> b - 1" by simp
  2356           then have "d * b \<le> b * (b - 1)" by simp
  2357           with xp mult_mono[of "1" "x" "d * b" "b * (b - 1)"]
  2358           have dble: "d * b \<le> x * b * (b - 1)" using bp by simp
  2359           from H(3) have "d + (b - 1) * (b * x) = d + (b - 1) * (a * y + d)"
  2360             by simp
  2361           then have "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  2362             by (simp only: mult.assoc distrib_left)
  2363           then have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x * b * (b - 1)"
  2364             by algebra
  2365           then have "a * ((b - 1) * y) = d + x * b * (b - 1) - d * b"
  2366             using bp by simp
  2367           then have "a * ((b - 1) * y) = d + (x * b * (b - 1) - d * b)"
  2368             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  2369           then have "a * ((b - 1) * y) = b * (x * (b - 1) - d) + d"
  2370             by (simp only: diff_mult_distrib2 ac_simps)
  2371           with H(1,2) show ?thesis
  2372             by blast
  2373         qed
  2374       qed
  2375     qed
  2376   qed
  2377 qed
  2378 
  2379 lemma bezout_nat:
  2380   fixes a :: nat
  2381   assumes a: "a \<noteq> 0"
  2382   shows "\<exists>x y. a * x = b * y + gcd a b"
  2383 proof -
  2384   obtain d x y where d: "d dvd a" "d dvd b" and eq: "a * x = b * y + d"
  2385     using bezout_add_strong_nat [OF a, of b] by blast
  2386   from d have "d dvd gcd a b"
  2387     by simp
  2388   then obtain k where k: "gcd a b = d * k"
  2389     unfolding dvd_def by blast
  2390   from eq have "a * x * k = (b * y + d) * k"
  2391     by auto
  2392   then have "a * (x * k) = b * (y * k) + gcd a b"
  2393     by (algebra add: k)
  2394   then show ?thesis
  2395     by blast
  2396 qed
  2397 
  2398 
  2399 subsection \<open>LCM properties on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close>
  2400 
  2401 lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  2402   for a b :: int
  2403   by (simp add: abs_mult lcm_gcd)
  2404   
  2405 lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
  2406   for m n :: nat
  2407   by simp
  2408 
  2409 lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
  2410   for m n :: int
  2411   by simp
  2412 
  2413 lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
  2414   for m n :: nat
  2415   using lcm_eq_0_iff [of m n] by auto
  2416 
  2417 lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
  2418   for m n :: int
  2419   by (simp add: less_le lcm_eq_0_iff)
  2420 
  2421 lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
  2422   for m n :: nat
  2423   by auto
  2424 
  2425 lemma lcm_unique_nat:
  2426   "a dvd d \<and> b dvd d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  2427   for a b d :: nat
  2428   by (auto intro: dvd_antisym lcm_least)
  2429 
  2430 lemma lcm_unique_int:
  2431   "d \<ge> 0 \<and> a dvd d \<and> b dvd d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  2432   for a b d :: int
  2433   using lcm_least zdvd_antisym_nonneg by auto
  2434 
  2435 lemma lcm_proj2_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm x y = y"
  2436   for x y :: nat
  2437   by (simp add: lcm_proj2_if_dvd)
  2438 
  2439 lemma lcm_proj2_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
  2440   for x y :: int
  2441   by (simp add: lcm_proj2_if_dvd)
  2442 
  2443 lemma lcm_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm y x = y"
  2444   for x y :: nat
  2445   by (subst lcm.commute) (erule lcm_proj2_if_dvd_nat)
  2446 
  2447 lemma lcm_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
  2448   for x y :: int
  2449   by (subst lcm.commute) (erule lcm_proj2_if_dvd_int)
  2450 
  2451 lemma lcm_proj1_iff_nat [simp]: "lcm m n = m \<longleftrightarrow> n dvd m"
  2452   for m n :: nat
  2453   by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  2454 
  2455 lemma lcm_proj2_iff_nat [simp]: "lcm m n = n \<longleftrightarrow> m dvd n"
  2456   for m n :: nat
  2457   by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  2458 
  2459 lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m\<bar> \<longleftrightarrow> n dvd m"
  2460   for m n :: int
  2461   by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  2462 
  2463 lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n\<bar> \<longleftrightarrow> m dvd n"
  2464   for m n :: int
  2465   by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  2466 
  2467 lemma lcm_1_iff_nat [simp]: "lcm m n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
  2468   for m n :: nat
  2469   using lcm_eq_1_iff [of m n] by simp
  2470 
  2471 lemma lcm_1_iff_int [simp]: "lcm m n = 1 \<longleftrightarrow> (m = 1 \<or> m = -1) \<and> (n = 1 \<or> n = -1)"
  2472   for m n :: int
  2473   by auto
  2474 
  2475 
  2476 subsection \<open>The complete divisibility lattice on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close>
  2477 
  2478 text \<open>
  2479   Lifting \<open>gcd\<close> and \<open>lcm\<close> to sets (\<open>Gcd\<close> / \<open>Lcm\<close>).
  2480   \<open>Gcd\<close> is defined via \<open>Lcm\<close> to facilitate the proof that we have a complete lattice.
  2481 \<close>
  2482 
  2483 instantiation nat :: semiring_Gcd
  2484 begin
  2485 
  2486 interpretation semilattice_neutr_set lcm "1::nat"
  2487   by standard simp_all
  2488 
  2489 definition "Lcm M = (if finite M then F M else 0)" for M :: "nat set"
  2490 
  2491 lemma Lcm_nat_empty: "Lcm {} = (1::nat)"
  2492   by (simp add: Lcm_nat_def del: One_nat_def)
  2493 
  2494 lemma Lcm_nat_insert: "Lcm (insert n M) = lcm n (Lcm M)" for n :: nat
  2495   by (cases "finite M") (auto simp: Lcm_nat_def simp del: One_nat_def)
  2496 
  2497 lemma Lcm_nat_infinite: "infinite M \<Longrightarrow> Lcm M = 0" for M :: "nat set"
  2498   by (simp add: Lcm_nat_def)
  2499 
  2500 lemma dvd_Lcm_nat [simp]:
  2501   fixes M :: "nat set"
  2502   assumes "m \<in> M"
  2503   shows "m dvd Lcm M"
  2504 proof -
  2505   from assms have "insert m M = M"
  2506     by auto
  2507   moreover have "m dvd Lcm (insert m M)"
  2508     by (simp add: Lcm_nat_insert)
  2509   ultimately show ?thesis
  2510     by simp
  2511 qed
  2512 
  2513 lemma Lcm_dvd_nat [simp]:
  2514   fixes M :: "nat set"
  2515   assumes "\<forall>m\<in>M. m dvd n"
  2516   shows "Lcm M dvd n"
  2517 proof (cases "n > 0")
  2518   case False
  2519   then show ?thesis by simp
  2520 next
  2521   case True
  2522   then have "finite {d. d dvd n}"
  2523     by (rule finite_divisors_nat)
  2524   moreover have "M \<subseteq> {d. d dvd n}"
  2525     using assms by fast
  2526   ultimately have "finite M"
  2527     by (rule rev_finite_subset)
  2528   then show ?thesis
  2529     using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
  2530 qed
  2531 
  2532 definition "Gcd M = Lcm {d. \<forall>m\<in>M. d dvd m}" for M :: "nat set"
  2533 
  2534 instance
  2535 proof
  2536   fix N :: "nat set"
  2537   fix n :: nat
  2538   show "Gcd N dvd n" if "n \<in> N"
  2539     using that by (induct N rule: infinite_finite_induct) (auto simp: Gcd_nat_def)
  2540   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m"
  2541     using that by (induct N rule: infinite_finite_induct) (auto simp: Gcd_nat_def)
  2542   show "n dvd Lcm N" if "n \<in> N"
  2543     using that by (induct N rule: infinite_finite_induct) auto
  2544   show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n"
  2545     using that by (induct N rule: infinite_finite_induct) auto
  2546   show "normalize (Gcd N) = Gcd N" and "normalize (Lcm N) = Lcm N"
  2547     by simp_all
  2548 qed
  2549 
  2550 end
  2551 
  2552 lemma Gcd_nat_eq_one: "1 \<in> N \<Longrightarrow> Gcd N = 1"
  2553   for N :: "nat set"
  2554   by (rule Gcd_eq_1_I) auto
  2555 
  2556 
  2557 text \<open>Alternative characterizations of Gcd:\<close>
  2558 
  2559 lemma Gcd_eq_Max:
  2560   fixes M :: "nat set"
  2561   assumes "finite (M::nat set)" and "M \<noteq> {}" and "0 \<notin> M"
  2562   shows "Gcd M = Max (\<Inter>m\<in>M. {d. d dvd m})"
  2563 proof (rule antisym)
  2564   from assms obtain m where "m \<in> M" and "m > 0"
  2565     by auto
  2566   from \<open>m > 0\<close> have "finite {d. d dvd m}"
  2567     by (blast intro: finite_divisors_nat)
  2568   with \<open>m \<in> M\<close> have fin: "finite (\<Inter>m\<in>M. {d. d dvd m})"
  2569     by blast
  2570   from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
  2571     by (auto intro: Max_ge Gcd_dvd)
  2572   from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
  2573   proof (rule Max.boundedI, simp_all)
  2574     show "(\<Inter>m\<in>M. {d. d dvd m}) \<noteq> {}"
  2575       by auto
  2576     show "\<And>a. \<forall>x\<in>M. a dvd x \<Longrightarrow> a \<le> Gcd M"
  2577       by (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
  2578   qed
  2579 qed
  2580 
  2581 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0})"
  2582   for M :: "nat set"
  2583 proof (induct pred: finite)
  2584   case (insert x M)
  2585   then show ?case
  2586     by (simp add: insert_Diff_if)
  2587 qed auto
  2588 
  2589 lemma Lcm_in_lcm_closed_set_nat:
  2590   fixes M :: "nat set" 
  2591   assumes "finite M" "M \<noteq> {}" "\<And>m n. \<lbrakk>m \<in> M; n \<in> M\<rbrakk> \<Longrightarrow> lcm m n \<in> M"
  2592   shows "Lcm M \<in> M"
  2593   using assms
  2594 proof (induction M rule: finite_linorder_min_induct)
  2595   case (insert x M)
  2596   then have "\<And>m n. m \<in> M \<Longrightarrow> n \<in> M \<Longrightarrow> lcm m n \<in> M"
  2597     by (metis dvd_lcm1 gr0I insert_iff lcm_pos_nat nat_dvd_not_less)
  2598   with insert show ?case
  2599     by simp (metis Lcm_nat_empty One_nat_def dvd_1_left dvd_lcm2)
  2600 qed auto
  2601 
  2602 lemma Lcm_eq_Max_nat:
  2603   fixes M :: "nat set" 
  2604   assumes M: "finite M" "M \<noteq> {}" "0 \<notin> M" and lcm: "\<And>m n. \<lbrakk>m \<in> M; n \<in> M\<rbrakk> \<Longrightarrow> lcm m n \<in> M"
  2605   shows "Lcm M = Max M"
  2606 proof (rule antisym)
  2607   show "Lcm M \<le> Max M"
  2608     by (simp add: Lcm_in_lcm_closed_set_nat \<open>finite M\<close> \<open>M \<noteq> {}\<close> lcm)
  2609   show "Max M \<le> Lcm M"
  2610     by (meson Lcm_0_iff Max_in M dvd_Lcm dvd_imp_le le_0_eq not_le)
  2611 qed
  2612 
  2613 lemma mult_inj_if_coprime_nat:
  2614   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> (\<And>a b. \<lbrakk>a\<in>A; b\<in>B\<rbrakk> \<Longrightarrow> coprime (f a) (g b)) \<Longrightarrow>
  2615     inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)"
  2616   for f :: "'a \<Rightarrow> nat" and g :: "'b \<Rightarrow> nat"
  2617   by (auto simp: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
  2618 
  2619 
  2620 subsubsection \<open>Setwise GCD and LCM for integers\<close>
  2621 
  2622 instantiation int :: Gcd
  2623 begin
  2624 
  2625 definition Gcd_int :: "int set \<Rightarrow> int"
  2626   where "Gcd K = int (GCD k\<in>K. (nat \<circ> abs) k)"
  2627 
  2628 definition Lcm_int :: "int set \<Rightarrow> int"
  2629   where "Lcm K = int (LCM k\<in>K. (nat \<circ> abs) k)"
  2630 
  2631 instance ..
  2632 
  2633 end
  2634 
  2635 lemma Gcd_int_eq [simp]:
  2636   "(GCD n\<in>N. int n) = int (Gcd N)"
  2637   by (simp add: Gcd_int_def image_image)
  2638 
  2639 lemma Gcd_nat_abs_eq [simp]:
  2640   "(GCD k\<in>K. nat \<bar>k\<bar>) = nat (Gcd K)"
  2641   by (simp add: Gcd_int_def)
  2642 
  2643 lemma abs_Gcd_eq [simp]:
  2644   "\<bar>Gcd K\<bar> = Gcd K" for K :: "int set"
  2645   by (simp only: Gcd_int_def)
  2646 
  2647 lemma Gcd_int_greater_eq_0 [simp]:
  2648   "Gcd K \<ge> 0"
  2649   for K :: "int set"
  2650   using abs_ge_zero [of "Gcd K"] by simp
  2651 
  2652 lemma Gcd_abs_eq [simp]:
  2653   "(GCD k\<in>K. \<bar>k\<bar>) = Gcd K"
  2654   for K :: "int set"
  2655   by (simp only: Gcd_int_def image_image) simp
  2656 
  2657 lemma Lcm_int_eq [simp]:
  2658   "(LCM n\<in>N. int n) = int (Lcm N)"
  2659   by (simp add: Lcm_int_def image_image)
  2660 
  2661 lemma Lcm_nat_abs_eq [simp]:
  2662   "(LCM k\<in>K. nat \<bar>k\<bar>) = nat (Lcm K)"
  2663   by (simp add: Lcm_int_def)
  2664 
  2665 lemma abs_Lcm_eq [simp]:
  2666   "\<bar>Lcm K\<bar> = Lcm K" for K :: "int set"
  2667   by (simp only: Lcm_int_def)
  2668 
  2669 lemma Lcm_int_greater_eq_0 [simp]:
  2670   "Lcm K \<ge> 0"
  2671   for K :: "int set"
  2672   using abs_ge_zero [of "Lcm K"] by simp
  2673 
  2674 lemma Lcm_abs_eq [simp]:
  2675   "(LCM k\<in>K. \<bar>k\<bar>) = Lcm K"
  2676   for K :: "int set"
  2677   by (simp only: Lcm_int_def image_image) simp
  2678 
  2679 instance int :: semiring_Gcd
  2680 proof
  2681   fix K :: "int set" and k :: int
  2682   show "Gcd K dvd k" and "k dvd Lcm K" if "k \<in> K"
  2683     using that Gcd_dvd [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"]
  2684       dvd_Lcm [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"]
  2685     by (simp_all add: comp_def)
  2686   show "k dvd Gcd K" if "\<And>l. l \<in> K \<Longrightarrow> k dvd l"
  2687   proof -
  2688     have "nat \<bar>k\<bar> dvd (GCD k\<in>K. nat \<bar>k\<bar>)"
  2689       by (rule Gcd_greatest) (use that in auto)
  2690     then show ?thesis by simp
  2691   qed
  2692   show "Lcm K dvd k" if "\<And>l. l \<in> K \<Longrightarrow> l dvd k"
  2693   proof -
  2694     have "(LCM k\<in>K. nat \<bar>k\<bar>) dvd nat \<bar>k\<bar>"
  2695       by (rule Lcm_least) (use that in auto)
  2696     then show ?thesis by simp
  2697   qed
  2698 qed simp_all
  2699 
  2700 
  2701 subsection \<open>GCD and LCM on \<^typ>\<open>integer\<close>\<close>
  2702 
  2703 instantiation integer :: gcd
  2704 begin
  2705 
  2706 context
  2707   includes integer.lifting
  2708 begin
  2709 
  2710 lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
  2711 
  2712 lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
  2713 
  2714 end
  2715 
  2716 instance ..
  2717 
  2718 end
  2719 
  2720 lifting_update integer.lifting
  2721 lifting_forget integer.lifting
  2722 
  2723 context
  2724   includes integer.lifting
  2725 begin
  2726 
  2727 lemma gcd_code_integer [code]: "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  2728   by transfer (fact gcd_code_int)
  2729 
  2730 lemma lcm_code_integer [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  2731   for a b :: integer
  2732   by transfer (fact lcm_altdef_int)
  2733 
  2734 end
  2735 
  2736 code_printing
  2737   constant "gcd :: integer \<Rightarrow> _" \<rightharpoonup>
  2738     (OCaml) "!(fun k l -> if Z.equal k Z.zero then/ Z.abs l else if Z.equal/ l Z.zero then Z.abs k else Z.gcd k l)"
  2739   and (Haskell) "Prelude.gcd"
  2740   and (Scala) "_.gcd'((_)')"
  2741   \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
  2742 
  2743 text \<open>Some code equations\<close>
  2744 
  2745 lemmas Gcd_nat_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = nat]
  2746 lemmas Lcm_nat_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = nat]
  2747 lemmas Gcd_int_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = int]
  2748 lemmas Lcm_int_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = int]
  2749 
  2750 text \<open>Fact aliases.\<close>
  2751 
  2752 lemma lcm_0_iff_nat [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
  2753   for m n :: nat
  2754   by (fact lcm_eq_0_iff)
  2755 
  2756 lemma lcm_0_iff_int [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
  2757   for m n :: int
  2758   by (fact lcm_eq_0_iff)
  2759 
  2760 lemma dvd_lcm_I1_nat [simp]: "k dvd m \<Longrightarrow> k dvd lcm m n"
  2761   for k m n :: nat
  2762   by (fact dvd_lcmI1)
  2763 
  2764 lemma dvd_lcm_I2_nat [simp]: "k dvd n \<Longrightarrow> k dvd lcm m n"
  2765   for k m n :: nat
  2766   by (fact dvd_lcmI2)
  2767 
  2768 lemma dvd_lcm_I1_int [simp]: "i dvd m \<Longrightarrow> i dvd lcm m n"
  2769   for i m n :: int
  2770   by (fact dvd_lcmI1)
  2771 
  2772 lemma dvd_lcm_I2_int [simp]: "i dvd n \<Longrightarrow> i dvd lcm m n"
  2773   for i m n :: int
  2774   by (fact dvd_lcmI2)
  2775 
  2776 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
  2777 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
  2778 lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
  2779 lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int]
  2780 
  2781 lemma dvd_Lcm_int [simp]: "m \<in> M \<Longrightarrow> m dvd Lcm M"
  2782   for M :: "int set"
  2783   by (fact dvd_Lcm)
  2784 
  2785 lemma gcd_neg_numeral_1_int [simp]: "gcd (- numeral n :: int) x = gcd (numeral n) x"
  2786   by (fact gcd_neg1_int)
  2787 
  2788 lemma gcd_neg_numeral_2_int [simp]: "gcd x (- numeral n :: int) = gcd x (numeral n)"
  2789   by (fact gcd_neg2_int)
  2790 
  2791 lemma gcd_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> gcd x y = x"
  2792   for x y :: nat
  2793   by (fact gcd_nat.absorb1)
  2794 
  2795 lemma gcd_proj2_if_dvd_nat [simp]: "y dvd x \<Longrightarrow> gcd x y = y"
  2796   for x y :: nat
  2797   by (fact gcd_nat.absorb2)
  2798 
  2799 lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]
  2800 lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat]
  2801 lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int]
  2802 
  2803 end