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