src/HOL/GCD.thy
 author haftmann Sun Apr 23 14:53:33 2017 +0200 (2017-04-23) changeset 65555 85ed070017b7 parent 65552 f533820e7248 child 65811 2653f1cd8775 permissions -rw-r--r--
include GCD as integral part of computational algebra in session HOL
```     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
```
```  1514 definition pairwise_coprime
```
```  1515   where "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
```
```  1516
```
```  1517 lemma pairwise_coprimeI [intro?]:
```
```  1518   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
```
```  1519   by (simp add: pairwise_coprime_def)
```
```  1520
```
```  1521 lemma pairwise_coprimeD:
```
```  1522   "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
```
```  1523   by (simp add: pairwise_coprime_def)
```
```  1524
```
```  1525 lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
```
```  1526   by (force simp: pairwise_coprime_def)
```
```  1527
```
```  1528 end
```
```  1529
```
```  1530
```
```  1531 subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close>
```
```  1532
```
```  1533 context semiring_gcd
```
```  1534 begin
```
```  1535
```
```  1536 sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
```
```  1537 defines
```
```  1538   Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n _"  900) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
```
```  1539
```
```  1540 abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
```
```  1541   where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
```
```  1542
```
```  1543 sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
```
```  1544 defines
```
```  1545   Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n _"  900) = Lcm_fin.F ..
```
```  1546
```
```  1547 abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
```
```  1548   where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
```
```  1549
```
```  1550 lemma Gcd_fin_dvd:
```
```  1551   "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a"
```
```  1552   by (induct A rule: infinite_finite_induct)
```
```  1553     (auto intro: dvd_trans)
```
```  1554
```
```  1555 lemma dvd_Lcm_fin:
```
```  1556   "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A"
```
```  1557   by (induct A rule: infinite_finite_induct)
```
```  1558     (auto intro: dvd_trans)
```
```  1559
```
```  1560 lemma Gcd_fin_greatest:
```
```  1561   "a dvd Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
```
```  1562   using that by (induct A) simp_all
```
```  1563
```
```  1564 lemma Lcm_fin_least:
```
```  1565   "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd a" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
```
```  1566   using that by (induct A) simp_all
```
```  1567
```
```  1568 lemma gcd_list_greatest:
```
```  1569   "a dvd gcd_list bs" if "\<And>b. b \<in> set bs \<Longrightarrow> a dvd b"
```
```  1570   by (rule Gcd_fin_greatest) (simp_all add: that)
```
```  1571
```
```  1572 lemma lcm_list_least:
```
```  1573   "lcm_list bs dvd a" if "\<And>b. b \<in> set bs \<Longrightarrow> b dvd a"
```
```  1574   by (rule Lcm_fin_least) (simp_all add: that)
```
```  1575
```
```  1576 lemma dvd_Gcd_fin_iff:
```
```  1577   "b dvd Gcd\<^sub>f\<^sub>i\<^sub>n A \<longleftrightarrow> (\<forall>a\<in>A. b dvd a)" if "finite A"
```
```  1578   using that by (auto intro: Gcd_fin_greatest Gcd_fin_dvd dvd_trans [of b "Gcd\<^sub>f\<^sub>i\<^sub>n A"])
```
```  1579
```
```  1580 lemma dvd_gcd_list_iff:
```
```  1581   "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)"
```
```  1582   by (simp add: dvd_Gcd_fin_iff)
```
```  1583
```
```  1584 lemma Lcm_fin_dvd_iff:
```
```  1585   "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b  \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A"
```
```  1586   using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b])
```
```  1587
```
```  1588 lemma lcm_list_dvd_iff:
```
```  1589   "lcm_list xs dvd b  \<longleftrightarrow> (\<forall>a\<in>set xs. a dvd b)"
```
```  1590   by (simp add: Lcm_fin_dvd_iff)
```
```  1591
```
```  1592 lemma Gcd_fin_mult:
```
```  1593   "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A"
```
```  1594 using that proof induct
```
```  1595   case empty
```
```  1596   then show ?case
```
```  1597     by simp
```
```  1598 next
```
```  1599   case (insert a A)
```
```  1600   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))"
```
```  1601     by simp
```
```  1602   also have "\<dots> = gcd (b * a) (normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A)"
```
```  1603     by (simp add: normalize_mult)
```
```  1604   finally show ?case
```
```  1605     using insert by (simp add: gcd_mult_distrib')
```
```  1606 qed
```
```  1607
```
```  1608 lemma Lcm_fin_mult:
```
```  1609   "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A" if "A \<noteq> {}"
```
```  1610 proof (cases "b = 0")
```
```  1611   case True
```
```  1612   moreover from that have "times 0 ` A = {0}"
```
```  1613     by auto
```
```  1614   ultimately show ?thesis
```
```  1615     by simp
```
```  1616 next
```
```  1617   case False
```
```  1618   then have "inj (times b)"
```
```  1619     by (rule inj_times)
```
```  1620   show ?thesis proof (cases "finite A")
```
```  1621     case False
```
```  1622     moreover from \<open>inj (times b)\<close>
```
```  1623     have "inj_on (times b) A"
```
```  1624       by (rule inj_on_subset) simp
```
```  1625     ultimately have "infinite (times b ` A)"
```
```  1626       by (simp add: finite_image_iff)
```
```  1627     with False show ?thesis
```
```  1628       by simp
```
```  1629   next
```
```  1630     case True
```
```  1631     then show ?thesis using that proof (induct A rule: finite_ne_induct)
```
```  1632       case (singleton a)
```
```  1633       then show ?case
```
```  1634         by (simp add: normalize_mult)
```
```  1635     next
```
```  1636       case (insert a A)
```
```  1637       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))"
```
```  1638         by simp
```
```  1639       also have "\<dots> = lcm (b * a) (normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A)"
```
```  1640         by (simp add: normalize_mult)
```
```  1641       finally show ?case
```
```  1642         using insert by (simp add: lcm_mult_distrib')
```
```  1643     qed
```
```  1644   qed
```
```  1645 qed
```
```  1646
```
```  1647 end
```
```  1648
```
```  1649 context semiring_Gcd
```
```  1650 begin
```
```  1651
```
```  1652 lemma Gcd_fin_eq_Gcd [simp]:
```
```  1653   "Gcd\<^sub>f\<^sub>i\<^sub>n A = Gcd A" if "finite A" for A :: "'a set"
```
```  1654   using that by induct simp_all
```
```  1655
```
```  1656 lemma Gcd_set_eq_fold [code_unfold]:
```
```  1657   "Gcd (set xs) = fold gcd xs 0"
```
```  1658   by (simp add: Gcd_fin.set_eq_fold [symmetric])
```
```  1659
```
```  1660 lemma Lcm_fin_eq_Lcm [simp]:
```
```  1661   "Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A" if "finite A" for A :: "'a set"
```
```  1662   using that by induct simp_all
```
```  1663
```
```  1664 lemma Lcm_set_eq_fold [code_unfold]:
```
```  1665   "Lcm (set xs) = fold lcm xs 1"
```
```  1666   by (simp add: Lcm_fin.set_eq_fold [symmetric])
```
```  1667
```
```  1668 end
```
```  1669
```
```  1670 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
```
```  1671
```
```  1672 instantiation nat :: gcd
```
```  1673 begin
```
```  1674
```
```  1675 fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
```
```  1676   where "gcd_nat x y = (if y = 0 then x else gcd y (x mod y))"
```
```  1677
```
```  1678 definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
```
```  1679   where "lcm_nat x y = x * y div (gcd x y)"
```
```  1680
```
```  1681 instance ..
```
```  1682
```
```  1683 end
```
```  1684
```
```  1685 instantiation int :: gcd
```
```  1686 begin
```
```  1687
```
```  1688 definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
```
```  1689   where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
```
```  1690
```
```  1691 definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
```
```  1692   where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
```
```  1693
```
```  1694 instance ..
```
```  1695
```
```  1696 end
```
```  1697
```
```  1698 text \<open>Transfer setup\<close>
```
```  1699
```
```  1700 lemma transfer_nat_int_gcd:
```
```  1701   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
```
```  1702   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
```
```  1703   for x y :: int
```
```  1704   unfolding gcd_int_def lcm_int_def by auto
```
```  1705
```
```  1706 lemma transfer_nat_int_gcd_closures:
```
```  1707   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
```
```  1708   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
```
```  1709   for x y :: int
```
```  1710   by (auto simp add: gcd_int_def lcm_int_def)
```
```  1711
```
```  1712 declare transfer_morphism_nat_int
```
```  1713   [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
```
```  1714
```
```  1715 lemma transfer_int_nat_gcd:
```
```  1716   "gcd (int x) (int y) = int (gcd x y)"
```
```  1717   "lcm (int x) (int y) = int (lcm x y)"
```
```  1718   by (auto simp: gcd_int_def lcm_int_def)
```
```  1719
```
```  1720 lemma transfer_int_nat_gcd_closures:
```
```  1721   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
```
```  1722   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
```
```  1723   by (auto simp: gcd_int_def lcm_int_def)
```
```  1724
```
```  1725 declare transfer_morphism_int_nat
```
```  1726   [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
```
```  1727
```
```  1728 lemma gcd_nat_induct:
```
```  1729   fixes m n :: nat
```
```  1730   assumes "\<And>m. P m 0"
```
```  1731     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
```
```  1732   shows "P m n"
```
```  1733   apply (rule gcd_nat.induct)
```
```  1734   apply (case_tac "y = 0")
```
```  1735   using assms
```
```  1736    apply simp_all
```
```  1737   done
```
```  1738
```
```  1739
```
```  1740 text \<open>Specific to \<open>int\<close>.\<close>
```
```  1741
```
```  1742 lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
```
```  1743   by (simp add: gcd_int_def)
```
```  1744
```
```  1745 lemma lcm_eq_int_iff: "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
```
```  1746   by (simp add: lcm_int_def)
```
```  1747
```
```  1748 lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
```
```  1749   for x y :: int
```
```  1750   by (simp add: gcd_int_def)
```
```  1751
```
```  1752 lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y"
```
```  1753   for x y :: int
```
```  1754   by (simp add: gcd_int_def)
```
```  1755
```
```  1756 lemma abs_gcd_int [simp]: "\<bar>gcd x y\<bar> = gcd x y"
```
```  1757   for x y :: int
```
```  1758   by (simp add: gcd_int_def)
```
```  1759
```
```  1760 lemma gcd_abs_int: "gcd x y = gcd \<bar>x\<bar> \<bar>y\<bar>"
```
```  1761   for x y :: int
```
```  1762   by (simp add: gcd_int_def)
```
```  1763
```
```  1764 lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> y = gcd x y"
```
```  1765   for x y :: int
```
```  1766   by (metis abs_idempotent gcd_abs_int)
```
```  1767
```
```  1768 lemma gcd_abs2_int [simp]: "gcd x \<bar>y\<bar> = gcd x y"
```
```  1769   for x y :: int
```
```  1770   by (metis abs_idempotent gcd_abs_int)
```
```  1771
```
```  1772 lemma gcd_cases_int:
```
```  1773   fixes x y :: int
```
```  1774   assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd x y)"
```
```  1775     and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd x (- y))"
```
```  1776     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd (- x) y)"
```
```  1777     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd (- x) (- y))"
```
```  1778   shows "P (gcd x y)"
```
```  1779   using assms by auto arith
```
```  1780
```
```  1781 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
```
```  1782   for x y :: int
```
```  1783   by (simp add: gcd_int_def)
```
```  1784
```
```  1785 lemma lcm_neg1_int: "lcm (- x) y = lcm x y"
```
```  1786   for x y :: int
```
```  1787   by (simp add: lcm_int_def)
```
```  1788
```
```  1789 lemma lcm_neg2_int: "lcm x (- y) = lcm x y"
```
```  1790   for x y :: int
```
```  1791   by (simp add: lcm_int_def)
```
```  1792
```
```  1793 lemma lcm_abs_int: "lcm x y = lcm \<bar>x\<bar> \<bar>y\<bar>"
```
```  1794   for x y :: int
```
```  1795   by (simp add: lcm_int_def)
```
```  1796
```
```  1797 lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
```
```  1798   for i j :: int
```
```  1799   by (simp add:lcm_int_def)
```
```  1800
```
```  1801 lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> y = lcm x y"
```
```  1802   for x y :: int
```
```  1803   by (metis abs_idempotent lcm_int_def)
```
```  1804
```
```  1805 lemma lcm_abs2_int [simp]: "lcm x \<bar>y\<bar> = lcm x y"
```
```  1806   for x y :: int
```
```  1807   by (metis abs_idempotent lcm_int_def)
```
```  1808
```
```  1809 lemma lcm_cases_int:
```
```  1810   fixes x y :: int
```
```  1811   assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm x y)"
```
```  1812     and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm x (- y))"
```
```  1813     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm (- x) y)"
```
```  1814     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm (- x) (- y))"
```
```  1815   shows "P (lcm x y)"
```
```  1816   using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
```
```  1817
```
```  1818 lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
```
```  1819   for x y :: int
```
```  1820   by (simp add: lcm_int_def)
```
```  1821
```
```  1822 lemma gcd_0_nat: "gcd x 0 = x"
```
```  1823   for x :: nat
```
```  1824   by simp
```
```  1825
```
```  1826 lemma gcd_0_int [simp]: "gcd x 0 = \<bar>x\<bar>"
```
```  1827   for x :: int
```
```  1828   by (auto simp: gcd_int_def)
```
```  1829
```
```  1830 lemma gcd_0_left_nat: "gcd 0 x = x"
```
```  1831   for x :: nat
```
```  1832   by simp
```
```  1833
```
```  1834 lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>"
```
```  1835   for x :: int
```
```  1836   by (auto simp:gcd_int_def)
```
```  1837
```
```  1838 lemma gcd_red_nat: "gcd x y = gcd y (x mod y)"
```
```  1839   for x y :: nat
```
```  1840   by (cases "y = 0") auto
```
```  1841
```
```  1842
```
```  1843 text \<open>Weaker, but useful for the simplifier.\<close>
```
```  1844
```
```  1845 lemma gcd_non_0_nat: "y \<noteq> 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
```
```  1846   for x y :: nat
```
```  1847   by simp
```
```  1848
```
```  1849 lemma gcd_1_nat [simp]: "gcd m 1 = 1"
```
```  1850   for m :: nat
```
```  1851   by simp
```
```  1852
```
```  1853 lemma gcd_Suc_0 [simp]: "gcd m (Suc 0) = Suc 0"
```
```  1854   for m :: nat
```
```  1855   by simp
```
```  1856
```
```  1857 lemma gcd_1_int [simp]: "gcd m 1 = 1"
```
```  1858   for m :: int
```
```  1859   by (simp add: gcd_int_def)
```
```  1860
```
```  1861 lemma gcd_idem_nat: "gcd x x = x"
```
```  1862   for x :: nat
```
```  1863   by simp
```
```  1864
```
```  1865 lemma gcd_idem_int: "gcd x x = \<bar>x\<bar>"
```
```  1866   for x :: int
```
```  1867   by (auto simp add: gcd_int_def)
```
```  1868
```
```  1869 declare gcd_nat.simps [simp del]
```
```  1870
```
```  1871 text \<open>
```
```  1872   \<^medskip> @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.
```
```  1873   The conjunctions don't seem provable separately.
```
```  1874 \<close>
```
```  1875
```
```  1876 instance nat :: semiring_gcd
```
```  1877 proof
```
```  1878   fix m n :: nat
```
```  1879   show "gcd m n dvd m" and "gcd m n dvd n"
```
```  1880   proof (induct m n rule: gcd_nat_induct)
```
```  1881     fix m n :: nat
```
```  1882     assume "gcd n (m mod n) dvd m mod n"
```
```  1883       and "gcd n (m mod n) dvd n"
```
```  1884     then have "gcd n (m mod n) dvd m"
```
```  1885       by (rule dvd_mod_imp_dvd)
```
```  1886     moreover assume "0 < n"
```
```  1887     ultimately show "gcd m n dvd m"
```
```  1888       by (simp add: gcd_non_0_nat)
```
```  1889   qed (simp_all add: gcd_0_nat gcd_non_0_nat)
```
```  1890 next
```
```  1891   fix m n k :: nat
```
```  1892   assume "k dvd m" and "k dvd n"
```
```  1893   then show "k dvd gcd m n"
```
```  1894     by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
```
```  1895 qed (simp_all add: lcm_nat_def)
```
```  1896
```
```  1897 instance int :: ring_gcd
```
```  1898   by standard
```
```  1899     (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def
```
```  1900       zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
```
```  1901
```
```  1902 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a"
```
```  1903   for a b :: nat
```
```  1904   by (rule dvd_imp_le) auto
```
```  1905
```
```  1906 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd a b \<le> b"
```
```  1907   for a b :: nat
```
```  1908   by (rule dvd_imp_le) auto
```
```  1909
```
```  1910 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd a b \<le> a"
```
```  1911   for a b :: int
```
```  1912   by (rule zdvd_imp_le) auto
```
```  1913
```
```  1914 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd a b \<le> b"
```
```  1915   for a b :: int
```
```  1916   by (rule zdvd_imp_le) auto
```
```  1917
```
```  1918 lemma gcd_pos_nat [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
```
```  1919   for m n :: nat
```
```  1920   using gcd_eq_0_iff [of m n] by arith
```
```  1921
```
```  1922 lemma gcd_pos_int [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
```
```  1923   for m n :: int
```
```  1924   using gcd_eq_0_iff [of m n] gcd_ge_0_int [of m n] by arith
```
```  1925
```
```  1926 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"
```
```  1927   for d a :: nat
```
```  1928   apply auto
```
```  1929   apply (rule dvd_antisym)
```
```  1930    apply (erule (1) gcd_greatest)
```
```  1931   apply auto
```
```  1932   done
```
```  1933
```
```  1934 lemma gcd_unique_int:
```
```  1935   "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"
```
```  1936   for d a :: int
```
```  1937   apply (cases "d = 0")
```
```  1938    apply simp
```
```  1939   apply (rule iffI)
```
```  1940    apply (rule zdvd_antisym_nonneg)
```
```  1941       apply (auto intro: gcd_greatest)
```
```  1942   done
```
```  1943
```
```  1944 interpretation gcd_nat:
```
```  1945   semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
```
```  1946   by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
```
```  1947
```
```  1948 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
```
```  1949   for x y :: int
```
```  1950   by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
```
```  1951
```
```  1952 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>"
```
```  1953   for x y :: int
```
```  1954   by (metis gcd_proj1_if_dvd_int gcd.commute)
```
```  1955
```
```  1956
```
```  1957 text \<open>\<^medskip> Multiplication laws.\<close>
```
```  1958
```
```  1959 lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
```
```  1960   for k m n :: nat
```
```  1961   \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
```
```  1962   apply (induct m n rule: gcd_nat_induct)
```
```  1963    apply simp
```
```  1964   apply (cases "k = 0")
```
```  1965    apply (simp_all add: gcd_non_0_nat)
```
```  1966   done
```
```  1967
```
```  1968 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
```
```  1969   for k m n :: int
```
```  1970   apply (subst (1 2) gcd_abs_int)
```
```  1971   apply (subst (1 2) abs_mult)
```
```  1972   apply (rule gcd_mult_distrib_nat [transferred])
```
```  1973     apply auto
```
```  1974   done
```
```  1975
```
```  1976 lemma coprime_crossproduct_nat:
```
```  1977   fixes a b c d :: nat
```
```  1978   assumes "coprime a d" and "coprime b c"
```
```  1979   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
```
```  1980   using assms coprime_crossproduct [of a d b c] by simp
```
```  1981
```
```  1982 lemma coprime_crossproduct_int:
```
```  1983   fixes a b c d :: int
```
```  1984   assumes "coprime a d" and "coprime b c"
```
```  1985   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>"
```
```  1986   using assms coprime_crossproduct [of a d b c] by simp
```
```  1987
```
```  1988
```
```  1989 text \<open>\medskip Addition laws.\<close>
```
```  1990
```
```  1991 (* TODO: add the other variations? *)
```
```  1992
```
```  1993 lemma gcd_diff1_nat: "m \<ge> n \<Longrightarrow> gcd (m - n) n = gcd m n"
```
```  1994   for m n :: nat
```
```  1995   by (subst gcd_add1 [symmetric]) auto
```
```  1996
```
```  1997 lemma gcd_diff2_nat: "n \<ge> m \<Longrightarrow> gcd (n - m) n = gcd m n"
```
```  1998   for m n :: nat
```
```  1999   apply (subst gcd.commute)
```
```  2000   apply (subst gcd_diff1_nat [symmetric])
```
```  2001    apply auto
```
```  2002   apply (subst gcd.commute)
```
```  2003   apply (subst gcd_diff1_nat)
```
```  2004    apply assumption
```
```  2005   apply (rule gcd.commute)
```
```  2006   done
```
```  2007
```
```  2008 lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
```
```  2009   for x y :: int
```
```  2010   apply (frule_tac b = y and a = x in pos_mod_sign)
```
```  2011   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
```
```  2012   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
```
```  2013   apply (frule_tac a = x in pos_mod_bound)
```
```  2014   apply (subst (1 2) gcd.commute)
```
```  2015   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
```
```  2016   done
```
```  2017
```
```  2018 lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
```
```  2019   for x y :: int
```
```  2020   apply (cases "y = 0")
```
```  2021    apply force
```
```  2022   apply (cases "y > 0")
```
```  2023    apply (subst gcd_non_0_int, auto)
```
```  2024   apply (insert gcd_non_0_int [of "- y" "- x"])
```
```  2025   apply auto
```
```  2026   done
```
```  2027
```
```  2028 (* TODO: differences, and all variations of addition rules
```
```  2029     as simplification rules for nat and int *)
```
```  2030
```
```  2031 (* TODO: add the three variations of these, and for ints? *)
```
```  2032
```
```  2033 lemma finite_divisors_nat [simp]: (* FIXME move *)
```
```  2034   fixes m :: nat
```
```  2035   assumes "m > 0"
```
```  2036   shows "finite {d. d dvd m}"
```
```  2037 proof-
```
```  2038   from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}"
```
```  2039     by (auto dest: dvd_imp_le)
```
```  2040   then show ?thesis
```
```  2041     using finite_Collect_le_nat by (rule finite_subset)
```
```  2042 qed
```
```  2043
```
```  2044 lemma finite_divisors_int [simp]:
```
```  2045   fixes i :: int
```
```  2046   assumes "i \<noteq> 0"
```
```  2047   shows "finite {d. d dvd i}"
```
```  2048 proof -
```
```  2049   have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}"
```
```  2050     by (auto simp: abs_if)
```
```  2051   then have "finite {d. \<bar>d\<bar> \<le> \<bar>i\<bar>}"
```
```  2052     by simp
```
```  2053   from finite_subset [OF _ this] show ?thesis
```
```  2054     using assms by (simp add: dvd_imp_le_int subset_iff)
```
```  2055 qed
```
```  2056
```
```  2057 lemma Max_divisors_self_nat [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::nat. d dvd n} = n"
```
```  2058   apply (rule antisym)
```
```  2059    apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
```
```  2060   apply simp
```
```  2061   done
```
```  2062
```
```  2063 lemma Max_divisors_self_int [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::int. d dvd n} = \<bar>n\<bar>"
```
```  2064   apply (rule antisym)
```
```  2065    apply (rule Max_le_iff [THEN iffD2])
```
```  2066      apply (auto intro: abs_le_D1 dvd_imp_le_int)
```
```  2067   done
```
```  2068
```
```  2069 lemma gcd_is_Max_divisors_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
```
```  2070   for m n :: nat
```
```  2071   apply (rule Max_eqI[THEN sym])
```
```  2072     apply (metis finite_Collect_conjI finite_divisors_nat)
```
```  2073    apply simp
```
```  2074    apply (metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
```
```  2075   apply simp
```
```  2076   done
```
```  2077
```
```  2078 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}"
```
```  2079   for m n :: int
```
```  2080   apply (rule Max_eqI[THEN sym])
```
```  2081     apply (metis finite_Collect_conjI finite_divisors_int)
```
```  2082    apply simp
```
```  2083    apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
```
```  2084   apply simp
```
```  2085   done
```
```  2086
```
```  2087 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>"
```
```  2088   for k l :: int
```
```  2089   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
```
```  2090
```
```  2091
```
```  2092 subsection \<open>Coprimality\<close>
```
```  2093
```
```  2094 lemma coprime_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
```
```  2095   for a b :: nat
```
```  2096   using coprime [of a b] by simp
```
```  2097
```
```  2098 lemma coprime_Suc_0_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
```
```  2099   for a b :: nat
```
```  2100   using coprime_nat by simp
```
```  2101
```
```  2102 lemma coprime_int: "coprime a b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
```
```  2103   for a b :: int
```
```  2104   using gcd_unique_int [of 1 a b]
```
```  2105   apply clarsimp
```
```  2106   apply (erule subst)
```
```  2107   apply (rule iffI)
```
```  2108    apply force
```
```  2109   using abs_dvd_iff abs_ge_zero apply blast
```
```  2110   done
```
```  2111
```
```  2112 lemma pow_divides_eq_nat [simp]: "n > 0 \<Longrightarrow> a^n dvd b^n \<longleftrightarrow> a dvd b"
```
```  2113   for a b n :: nat
```
```  2114   using pow_divs_eq[of n] by simp
```
```  2115
```
```  2116 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
```
```  2117   using coprime_plus_one[of n] by simp
```
```  2118
```
```  2119 lemma coprime_minus_one_nat: "n \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
```
```  2120   for n :: nat
```
```  2121   using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
```
```  2122
```
```  2123 lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
```
```  2124   for a b :: nat
```
```  2125   by (metis gcd_greatest_iff nat_dvd_1_iff_1)
```
```  2126
```
```  2127 lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
```
```  2128   for a b :: int
```
```  2129   using gcd_greatest_iff [of x a b] by auto
```
```  2130
```
```  2131 lemma invertible_coprime_nat: "x * y mod m = 1 \<Longrightarrow> coprime x m"
```
```  2132   for m x y :: nat
```
```  2133   by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
```
```  2134
```
```  2135 lemma invertible_coprime_int: "x * y mod m = 1 \<Longrightarrow> coprime x m"
```
```  2136   for m x y :: int
```
```  2137   by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
```
```  2138
```
```  2139
```
```  2140 subsection \<open>Bezout's theorem\<close>
```
```  2141
```
```  2142 text \<open>
```
```  2143   Function \<open>bezw\<close> returns a pair of witnesses to Bezout's theorem --
```
```  2144   see the theorems that follow the definition.
```
```  2145 \<close>
```
```  2146
```
```  2147 fun bezw :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
```
```  2148   where "bezw x y =
```
```  2149     (if y = 0 then (1, 0)
```
```  2150      else
```
```  2151       (snd (bezw y (x mod y)),
```
```  2152        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
```
```  2153
```
```  2154 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)"
```
```  2155   by simp
```
```  2156
```
```  2157 lemma bezw_non_0:
```
```  2158   "y > 0 \<Longrightarrow> bezw x y =
```
```  2159     (snd (bezw y (x mod y)), fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
```
```  2160   by simp
```
```  2161
```
```  2162 declare bezw.simps [simp del]
```
```  2163
```
```  2164 lemma bezw_aux: "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
```
```  2165 proof (induct x y rule: gcd_nat_induct)
```
```  2166   fix m :: nat
```
```  2167   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
```
```  2168     by auto
```
```  2169 next
```
```  2170   fix m n :: nat
```
```  2171   assume ngt0: "n > 0"
```
```  2172     and ih: "fst (bezw n (m mod n)) * int n + snd (bezw n (m mod n)) * int (m mod n) =
```
```  2173       int (gcd n (m mod n))"
```
```  2174   then show "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
```
```  2175     apply (simp add: bezw_non_0 gcd_non_0_nat)
```
```  2176     apply (erule subst)
```
```  2177     apply (simp add: field_simps)
```
```  2178     apply (subst div_mult_mod_eq [of m n, symmetric])
```
```  2179       (* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *)
```
```  2180     apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
```
```  2181     done
```
```  2182 qed
```
```  2183
```
```  2184 lemma bezout_int: "\<exists>u v. u * x + v * y = gcd x y"
```
```  2185   for x y :: int
```
```  2186 proof -
```
```  2187   have aux: "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> \<exists>u v. u * x + v * y = gcd x y" for x y :: int
```
```  2188     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
```
```  2189     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
```
```  2190     apply (unfold gcd_int_def)
```
```  2191     apply simp
```
```  2192     apply (subst bezw_aux [symmetric])
```
```  2193     apply auto
```
```  2194     done
```
```  2195   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"
```
```  2196     by atomize_elim auto
```
```  2197   then show ?thesis
```
```  2198   proof cases
```
```  2199     case 1
```
```  2200     then show ?thesis by (rule aux)
```
```  2201   next
```
```  2202     case 2
```
```  2203     then show ?thesis
```
```  2204       apply -
```
```  2205       apply (insert aux [of x "-y"])
```
```  2206       apply auto
```
```  2207       apply (rule_tac x = u in exI)
```
```  2208       apply (rule_tac x = "-v" in exI)
```
```  2209       apply (subst gcd_neg2_int [symmetric])
```
```  2210       apply auto
```
```  2211       done
```
```  2212   next
```
```  2213     case 3
```
```  2214     then show ?thesis
```
```  2215       apply -
```
```  2216       apply (insert aux [of "-x" y])
```
```  2217       apply auto
```
```  2218       apply (rule_tac x = "-u" in exI)
```
```  2219       apply (rule_tac x = v in exI)
```
```  2220       apply (subst gcd_neg1_int [symmetric])
```
```  2221       apply auto
```
```  2222       done
```
```  2223   next
```
```  2224     case 4
```
```  2225     then show ?thesis
```
```  2226       apply -
```
```  2227       apply (insert aux [of "-x" "-y"])
```
```  2228       apply auto
```
```  2229       apply (rule_tac x = "-u" in exI)
```
```  2230       apply (rule_tac x = "-v" in exI)
```
```  2231       apply (subst gcd_neg1_int [symmetric])
```
```  2232       apply (subst gcd_neg2_int [symmetric])
```
```  2233       apply auto
```
```  2234       done
```
```  2235   qed
```
```  2236 qed
```
```  2237
```
```  2238
```
```  2239 text \<open>Versions of Bezout for \<open>nat\<close>, by Amine Chaieb.\<close>
```
```  2240
```
```  2241 lemma ind_euclid:
```
```  2242   fixes P :: "nat \<Rightarrow> nat \<Rightarrow> bool"
```
```  2243   assumes c: " \<forall>a b. P a b \<longleftrightarrow> P b a"
```
```  2244     and z: "\<forall>a. P a 0"
```
```  2245     and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
```
```  2246   shows "P a b"
```
```  2247 proof (induct "a + b" arbitrary: a b rule: less_induct)
```
```  2248   case less
```
```  2249   consider (eq) "a = b" | (lt) "a < b" "a + b - a < a + b" | "b = 0" | "b + a - b < a + b"
```
```  2250     by arith
```
```  2251   show ?case
```
```  2252   proof (cases a b rule: linorder_cases)
```
```  2253     case equal
```
```  2254     with add [rule_format, OF z [rule_format, of a]] show ?thesis by simp
```
```  2255   next
```
```  2256     case lt: less
```
```  2257     then consider "a = 0" | "a + b - a < a + b" by arith
```
```  2258     then show ?thesis
```
```  2259     proof cases
```
```  2260       case 1
```
```  2261       with z c show ?thesis by blast
```
```  2262     next
```
```  2263       case 2
```
```  2264       also have *: "a + b - a = a + (b - a)" using lt by arith
```
```  2265       finally have "a + (b - a) < a + b" .
```
```  2266       then have "P a (a + (b - a))" by (rule add [rule_format, OF less])
```
```  2267       then show ?thesis by (simp add: *[symmetric])
```
```  2268     qed
```
```  2269   next
```
```  2270     case gt: greater
```
```  2271     then consider "b = 0" | "b + a - b < a + b" by arith
```
```  2272     then show ?thesis
```
```  2273     proof cases
```
```  2274       case 1
```
```  2275       with z c show ?thesis by blast
```
```  2276     next
```
```  2277       case 2
```
```  2278       also have *: "b + a - b = b + (a - b)" using gt by arith
```
```  2279       finally have "b + (a - b) < a + b" .
```
```  2280       then have "P b (b + (a - b))" by (rule add [rule_format, OF less])
```
```  2281       then have "P b a" by (simp add: *[symmetric])
```
```  2282       with c show ?thesis by blast
```
```  2283     qed
```
```  2284   qed
```
```  2285 qed
```
```  2286
```
```  2287 lemma bezout_lemma_nat:
```
```  2288   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
```
```  2289     (a * x = b * y + d \<or> b * x = a * y + d)"
```
```  2290   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
```
```  2291     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
```
```  2292   using ex
```
```  2293   apply clarsimp
```
```  2294   apply (rule_tac x="d" in exI)
```
```  2295   apply simp
```
```  2296   apply (case_tac "a * x = b * y + d")
```
```  2297    apply simp_all
```
```  2298    apply (rule_tac x="x + y" in exI)
```
```  2299    apply (rule_tac x="y" in exI)
```
```  2300    apply algebra
```
```  2301   apply (rule_tac x="x" in exI)
```
```  2302   apply (rule_tac x="x + y" in exI)
```
```  2303   apply algebra
```
```  2304   done
```
```  2305
```
```  2306 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
```
```  2307     (a * x = b * y + d \<or> b * x = a * y + d)"
```
```  2308   apply (induct a b rule: ind_euclid)
```
```  2309     apply blast
```
```  2310    apply clarify
```
```  2311    apply (rule_tac x="a" in exI)
```
```  2312    apply simp
```
```  2313   apply clarsimp
```
```  2314   apply (rule_tac x="d" in exI)
```
```  2315   apply (case_tac "a * x = b * y + d")
```
```  2316    apply simp_all
```
```  2317    apply (rule_tac x="x+y" in exI)
```
```  2318    apply (rule_tac x="y" in exI)
```
```  2319    apply algebra
```
```  2320   apply (rule_tac x="x" in exI)
```
```  2321   apply (rule_tac x="x+y" in exI)
```
```  2322   apply algebra
```
```  2323   done
```
```  2324
```
```  2325 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
```
```  2326     (a * x - b * y = d \<or> b * x - a * y = d)"
```
```  2327   using bezout_add_nat[of a b]
```
```  2328   apply clarsimp
```
```  2329   apply (rule_tac x="d" in exI)
```
```  2330   apply simp
```
```  2331   apply (rule_tac x="x" in exI)
```
```  2332   apply (rule_tac x="y" in exI)
```
```  2333   apply auto
```
```  2334   done
```
```  2335
```
```  2336 lemma bezout_add_strong_nat:
```
```  2337   fixes a b :: nat
```
```  2338   assumes a: "a \<noteq> 0"
```
```  2339   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
```
```  2340 proof -
```
```  2341   consider d x y where "d dvd a" "d dvd b" "a * x = b * y + d"
```
```  2342     | d x y where "d dvd a" "d dvd b" "b * x = a * y + d"
```
```  2343     using bezout_add_nat [of a b] by blast
```
```  2344   then show ?thesis
```
```  2345   proof cases
```
```  2346     case 1
```
```  2347     then show ?thesis by blast
```
```  2348   next
```
```  2349     case H: 2
```
```  2350     show ?thesis
```
```  2351     proof (cases "b = 0")
```
```  2352       case True
```
```  2353       with H show ?thesis by simp
```
```  2354     next
```
```  2355       case False
```
```  2356       then have bp: "b > 0" by simp
```
```  2357       with dvd_imp_le [OF H(2)] consider "d = b" | "d < b"
```
```  2358         by atomize_elim auto
```
```  2359       then show ?thesis
```
```  2360       proof cases
```
```  2361         case 1
```
```  2362         with a H show ?thesis
```
```  2363           apply simp
```
```  2364           apply (rule exI[where x = b])
```
```  2365           apply simp
```
```  2366           apply (rule exI[where x = b])
```
```  2367           apply (rule exI[where x = "a - 1"])
```
```  2368           apply (simp add: diff_mult_distrib2)
```
```  2369           done
```
```  2370       next
```
```  2371         case 2
```
```  2372         show ?thesis
```
```  2373         proof (cases "x = 0")
```
```  2374           case True
```
```  2375           with a H show ?thesis by simp
```
```  2376         next
```
```  2377           case x0: False
```
```  2378           then have xp: "x > 0" by simp
```
```  2379           from \<open>d < b\<close> have "d \<le> b - 1" by simp
```
```  2380           then have "d * b \<le> b * (b - 1)" by simp
```
```  2381           with xp mult_mono[of "1" "x" "d * b" "b * (b - 1)"]
```
```  2382           have dble: "d * b \<le> x * b * (b - 1)" using bp by simp
```
```  2383           from H(3) have "d + (b - 1) * (b * x) = d + (b - 1) * (a * y + d)"
```
```  2384             by simp
```
```  2385           then have "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
```
```  2386             by (simp only: mult.assoc distrib_left)
```
```  2387           then have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x * b * (b - 1)"
```
```  2388             by algebra
```
```  2389           then have "a * ((b - 1) * y) = d + x * b * (b - 1) - d * b"
```
```  2390             using bp by simp
```
```  2391           then have "a * ((b - 1) * y) = d + (x * b * (b - 1) - d * b)"
```
```  2392             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
```
```  2393           then have "a * ((b - 1) * y) = b * (x * (b - 1) - d) + d"
```
```  2394             by (simp only: diff_mult_distrib2 ac_simps)
```
```  2395           with H(1,2) show ?thesis
```
```  2396             apply -
```
```  2397             apply (rule exI [where x = d])
```
```  2398             apply simp
```
```  2399             apply (rule exI [where x = "(b - 1) * y"])
```
```  2400             apply (rule exI [where x = "x * (b - 1) - d"])
```
```  2401             apply simp
```
```  2402             done
```
```  2403         qed
```
```  2404       qed
```
```  2405     qed
```
```  2406   qed
```
```  2407 qed
```
```  2408
```
```  2409 lemma bezout_nat:
```
```  2410   fixes a :: nat
```
```  2411   assumes a: "a \<noteq> 0"
```
```  2412   shows "\<exists>x y. a * x = b * y + gcd a b"
```
```  2413 proof -
```
```  2414   obtain d x y where d: "d dvd a" "d dvd b" and eq: "a * x = b * y + d"
```
```  2415     using bezout_add_strong_nat [OF a, of b] by blast
```
```  2416   from d have "d dvd gcd a b"
```
```  2417     by simp
```
```  2418   then obtain k where k: "gcd a b = d * k"
```
```  2419     unfolding dvd_def by blast
```
```  2420   from eq have "a * x * k = (b * y + d) * k"
```
```  2421     by auto
```
```  2422   then have "a * (x * k) = b * (y * k) + gcd a b"
```
```  2423     by (algebra add: k)
```
```  2424   then show ?thesis
```
```  2425     by blast
```
```  2426 qed
```
```  2427
```
```  2428
```
```  2429 subsection \<open>LCM properties on @{typ nat} and @{typ int}\<close>
```
```  2430
```
```  2431 lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
```
```  2432   for a b :: int
```
```  2433   by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
```
```  2434
```
```  2435 lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
```
```  2436   for m n :: nat
```
```  2437   unfolding lcm_nat_def
```
```  2438   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
```
```  2439
```
```  2440 lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
```
```  2441   for m n :: int
```
```  2442   unfolding lcm_int_def gcd_int_def
```
```  2443   apply (subst of_nat_mult [symmetric])
```
```  2444   apply (subst prod_gcd_lcm_nat [symmetric])
```
```  2445   apply (subst nat_abs_mult_distrib [symmetric])
```
```  2446   apply (simp add: abs_mult)
```
```  2447   done
```
```  2448
```
```  2449 lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
```
```  2450   for m n :: nat
```
```  2451   by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
```
```  2452
```
```  2453 lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
```
```  2454   for m n :: int
```
```  2455   apply (subst lcm_abs_int)
```
```  2456   apply (rule lcm_pos_nat [transferred])
```
```  2457      apply auto
```
```  2458   done
```
```  2459
```
```  2460 lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
```
```  2461   for m n :: nat
```
```  2462   by (cases m) auto
```
```  2463
```
```  2464 lemma lcm_unique_nat:
```
```  2465   "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"
```
```  2466   for a b d :: nat
```
```  2467   by (auto intro: dvd_antisym lcm_least)
```
```  2468
```
```  2469 lemma lcm_unique_int:
```
```  2470   "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"
```
```  2471   for a b d :: int
```
```  2472   using lcm_least zdvd_antisym_nonneg by auto
```
```  2473
```
```  2474 lemma lcm_proj2_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm x y = y"
```
```  2475   for x y :: nat
```
```  2476   apply (rule sym)
```
```  2477   apply (subst lcm_unique_nat [symmetric])
```
```  2478   apply auto
```
```  2479   done
```
```  2480
```
```  2481 lemma lcm_proj2_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
```
```  2482   for x y :: int
```
```  2483   apply (rule sym)
```
```  2484   apply (subst lcm_unique_int [symmetric])
```
```  2485   apply auto
```
```  2486   done
```
```  2487
```
```  2488 lemma lcm_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm y x = y"
```
```  2489   for x y :: nat
```
```  2490   by (subst lcm.commute) (erule lcm_proj2_if_dvd_nat)
```
```  2491
```
```  2492 lemma lcm_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
```
```  2493   for x y :: int
```
```  2494   by (subst lcm.commute) (erule lcm_proj2_if_dvd_int)
```
```  2495
```
```  2496 lemma lcm_proj1_iff_nat [simp]: "lcm m n = m \<longleftrightarrow> n dvd m"
```
```  2497   for m n :: nat
```
```  2498   by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
```
```  2499
```
```  2500 lemma lcm_proj2_iff_nat [simp]: "lcm m n = n \<longleftrightarrow> m dvd n"
```
```  2501   for m n :: nat
```
```  2502   by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
```
```  2503
```
```  2504 lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m\<bar> \<longleftrightarrow> n dvd m"
```
```  2505   for m n :: int
```
```  2506   by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
```
```  2507
```
```  2508 lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n\<bar> \<longleftrightarrow> m dvd n"
```
```  2509   for m n :: int
```
```  2510   by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
```
```  2511
```
```  2512 lemma lcm_1_iff_nat [simp]: "lcm m n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
```
```  2513   for m n :: nat
```
```  2514   using lcm_eq_1_iff [of m n] by simp
```
```  2515
```
```  2516 lemma lcm_1_iff_int [simp]: "lcm m n = 1 \<longleftrightarrow> (m = 1 \<or> m = -1) \<and> (n = 1 \<or> n = -1)"
```
```  2517   for m n :: int
```
```  2518   by auto
```
```  2519
```
```  2520
```
```  2521 subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
```
```  2522
```
```  2523 text \<open>
```
```  2524   Lifting \<open>gcd\<close> and \<open>lcm\<close> to sets (\<open>Gcd\<close> / \<open>Lcm\<close>).
```
```  2525   \<open>Gcd\<close> is defined via \<open>Lcm\<close> to facilitate the proof that we have a complete lattice.
```
```  2526 \<close>
```
```  2527
```
```  2528 instantiation nat :: semiring_Gcd
```
```  2529 begin
```
```  2530
```
```  2531 interpretation semilattice_neutr_set lcm "1::nat"
```
```  2532   by standard simp_all
```
```  2533
```
```  2534 definition "Lcm M = (if finite M then F M else 0)" for M :: "nat set"
```
```  2535
```
```  2536 lemma Lcm_nat_empty: "Lcm {} = (1::nat)"
```
```  2537   by (simp add: Lcm_nat_def del: One_nat_def)
```
```  2538
```
```  2539 lemma Lcm_nat_insert: "Lcm (insert n M) = lcm n (Lcm M)" for n :: nat
```
```  2540   by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
```
```  2541
```
```  2542 lemma Lcm_nat_infinite: "infinite M \<Longrightarrow> Lcm M = 0" for M :: "nat set"
```
```  2543   by (simp add: Lcm_nat_def)
```
```  2544
```
```  2545 lemma dvd_Lcm_nat [simp]:
```
```  2546   fixes M :: "nat set"
```
```  2547   assumes "m \<in> M"
```
```  2548   shows "m dvd Lcm M"
```
```  2549 proof -
```
```  2550   from assms have "insert m M = M"
```
```  2551     by auto
```
```  2552   moreover have "m dvd Lcm (insert m M)"
```
```  2553     by (simp add: Lcm_nat_insert)
```
```  2554   ultimately show ?thesis
```
```  2555     by simp
```
```  2556 qed
```
```  2557
```
```  2558 lemma Lcm_dvd_nat [simp]:
```
```  2559   fixes M :: "nat set"
```
```  2560   assumes "\<forall>m\<in>M. m dvd n"
```
```  2561   shows "Lcm M dvd n"
```
```  2562 proof (cases "n > 0")
```
```  2563   case False
```
```  2564   then show ?thesis by simp
```
```  2565 next
```
```  2566   case True
```
```  2567   then have "finite {d. d dvd n}"
```
```  2568     by (rule finite_divisors_nat)
```
```  2569   moreover have "M \<subseteq> {d. d dvd n}"
```
```  2570     using assms by fast
```
```  2571   ultimately have "finite M"
```
```  2572     by (rule rev_finite_subset)
```
```  2573   then show ?thesis
```
```  2574     using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
```
```  2575 qed
```
```  2576
```
```  2577 definition "Gcd M = Lcm {d. \<forall>m\<in>M. d dvd m}" for M :: "nat set"
```
```  2578
```
```  2579 instance
```
```  2580 proof
```
```  2581   fix N :: "nat set"
```
```  2582   fix n :: nat
```
```  2583   show "Gcd N dvd n" if "n \<in> N"
```
```  2584     using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
```
```  2585   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m"
```
```  2586     using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
```
```  2587   show "n dvd Lcm N" if "n \<in> N"
```
```  2588     using that by (induct N rule: infinite_finite_induct) auto
```
```  2589   show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n"
```
```  2590     using that by (induct N rule: infinite_finite_induct) auto
```
```  2591   show "normalize (Gcd N) = Gcd N" and "normalize (Lcm N) = Lcm N"
```
```  2592     by simp_all
```
```  2593 qed
```
```  2594
```
```  2595 end
```
```  2596
```
```  2597 lemma Gcd_nat_eq_one: "1 \<in> N \<Longrightarrow> Gcd N = 1"
```
```  2598   for N :: "nat set"
```
```  2599   by (rule Gcd_eq_1_I) auto
```
```  2600
```
```  2601
```
```  2602 text \<open>Alternative characterizations of Gcd:\<close>
```
```  2603
```
```  2604 lemma Gcd_eq_Max:
```
```  2605   fixes M :: "nat set"
```
```  2606   assumes "finite (M::nat set)" and "M \<noteq> {}" and "0 \<notin> M"
```
```  2607   shows "Gcd M = Max (\<Inter>m\<in>M. {d. d dvd m})"
```
```  2608 proof (rule antisym)
```
```  2609   from assms obtain m where "m \<in> M" and "m > 0"
```
```  2610     by auto
```
```  2611   from \<open>m > 0\<close> have "finite {d. d dvd m}"
```
```  2612     by (blast intro: finite_divisors_nat)
```
```  2613   with \<open>m \<in> M\<close> have fin: "finite (\<Inter>m\<in>M. {d. d dvd m})"
```
```  2614     by blast
```
```  2615   from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
```
```  2616     by (auto intro: Max_ge Gcd_dvd)
```
```  2617   from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
```
```  2618     apply (rule Max.boundedI)
```
```  2619      apply auto
```
```  2620     apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
```
```  2621     done
```
```  2622 qed
```
```  2623
```
```  2624 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0})"
```
```  2625   for M :: "nat set"
```
```  2626   apply (induct pred: finite)
```
```  2627    apply simp
```
```  2628   apply (case_tac "x = 0")
```
```  2629    apply simp
```
```  2630   apply (subgoal_tac "insert x F - {0} = insert x (F - {0})")
```
```  2631    apply simp
```
```  2632   apply blast
```
```  2633   done
```
```  2634
```
```  2635 lemma Lcm_in_lcm_closed_set_nat:
```
```  2636   "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"
```
```  2637   for M :: "nat set"
```
```  2638   apply (induct rule: finite_linorder_min_induct)
```
```  2639    apply simp
```
```  2640   apply simp
```
```  2641   apply (subgoal_tac "\<forall>m n. m \<in> A \<longrightarrow> n \<in> A \<longrightarrow> lcm m n \<in> A")
```
```  2642    apply simp
```
```  2643    apply(case_tac "A = {}")
```
```  2644     apply simp
```
```  2645    apply simp
```
```  2646   apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
```
```  2647   done
```
```  2648
```
```  2649 lemma Lcm_eq_Max_nat:
```
```  2650   "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"
```
```  2651   for M :: "nat set"
```
```  2652   apply (rule antisym)
```
```  2653    apply (rule Max_ge)
```
```  2654     apply assumption
```
```  2655    apply (erule (2) Lcm_in_lcm_closed_set_nat)
```
```  2656   apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
```
```  2657   done
```
```  2658
```
```  2659 lemma mult_inj_if_coprime_nat:
```
```  2660   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>B. coprime (f a) (g b) \<Longrightarrow>
```
```  2661     inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)"
```
```  2662   for f :: "'a \<Rightarrow> nat" and g :: "'b \<Rightarrow> nat"
```
```  2663   by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
```
```  2664
```
```  2665
```
```  2666 subsubsection \<open>Setwise GCD and LCM for integers\<close>
```
```  2667
```
```  2668 instantiation int :: semiring_Gcd
```
```  2669 begin
```
```  2670
```
```  2671 definition "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
```
```  2672
```
```  2673 definition "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
```
```  2674
```
```  2675 instance
```
```  2676   by standard
```
```  2677     (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
```
```  2678       Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
```
```  2679
```
```  2680 end
```
```  2681
```
```  2682 lemma abs_Gcd [simp]: "\<bar>Gcd K\<bar> = Gcd K"
```
```  2683   for K :: "int set"
```
```  2684   using normalize_Gcd [of K] by simp
```
```  2685
```
```  2686 lemma abs_Lcm [simp]: "\<bar>Lcm K\<bar> = Lcm K"
```
```  2687   for K :: "int set"
```
```  2688   using normalize_Lcm [of K] by simp
```
```  2689
```
```  2690 lemma Gcm_eq_int_iff: "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
```
```  2691   by (simp add: Gcd_int_def comp_def image_image)
```
```  2692
```
```  2693 lemma Lcm_eq_int_iff: "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
```
```  2694   by (simp add: Lcm_int_def comp_def image_image)
```
```  2695
```
```  2696
```
```  2697 subsection \<open>GCD and LCM on @{typ integer}\<close>
```
```  2698
```
```  2699 instantiation integer :: gcd
```
```  2700 begin
```
```  2701
```
```  2702 context
```
```  2703   includes integer.lifting
```
```  2704 begin
```
```  2705
```
```  2706 lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
```
```  2707
```
```  2708 lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
```
```  2709
```
```  2710 end
```
```  2711
```
```  2712 instance ..
```
```  2713
```
```  2714 end
```
```  2715
```
```  2716 lifting_update integer.lifting
```
```  2717 lifting_forget integer.lifting
```
```  2718
```
```  2719 context
```
```  2720   includes integer.lifting
```
```  2721 begin
```
```  2722
```
```  2723 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>"
```
```  2724   by transfer (fact gcd_code_int)
```
```  2725
```
```  2726 lemma lcm_code_integer [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
```
```  2727   for a b :: integer
```
```  2728   by transfer (fact lcm_altdef_int)
```
```  2729
```
```  2730 end
```
```  2731
```
```  2732 code_printing
```
```  2733   constant "gcd :: integer \<Rightarrow> _" \<rightharpoonup>
```
```  2734     (OCaml) "Big'_int.gcd'_big'_int"
```
```  2735   and (Haskell) "Prelude.gcd"
```
```  2736   and (Scala) "_.gcd'((_)')"
```
```  2737   \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
```
```  2738
```
```  2739 text \<open>Some code equations\<close>
```
```  2740
```
```  2741 lemmas Gcd_nat_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = nat]
```
```  2742 lemmas Lcm_nat_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = nat]
```
```  2743 lemmas Gcd_int_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = int]
```
```  2744 lemmas Lcm_int_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = int]
```
```  2745
```
```  2746 text \<open>Fact aliases.\<close>
```
```  2747
```
```  2748 lemma lcm_0_iff_nat [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
```
```  2749   for m n :: nat
```
```  2750   by (fact lcm_eq_0_iff)
```
```  2751
```
```  2752 lemma lcm_0_iff_int [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
```
```  2753   for m n :: int
```
```  2754   by (fact lcm_eq_0_iff)
```
```  2755
```
```  2756 lemma dvd_lcm_I1_nat [simp]: "k dvd m \<Longrightarrow> k dvd lcm m n"
```
```  2757   for k m n :: nat
```
```  2758   by (fact dvd_lcmI1)
```
```  2759
```
```  2760 lemma dvd_lcm_I2_nat [simp]: "k dvd n \<Longrightarrow> k dvd lcm m n"
```
```  2761   for k m n :: nat
```
```  2762   by (fact dvd_lcmI2)
```
```  2763
```
```  2764 lemma dvd_lcm_I1_int [simp]: "i dvd m \<Longrightarrow> i dvd lcm m n"
```
```  2765   for i m n :: int
```
```  2766   by (fact dvd_lcmI1)
```
```  2767
```
```  2768 lemma dvd_lcm_I2_int [simp]: "i dvd n \<Longrightarrow> i dvd lcm m n"
```
```  2769   for i m n :: int
```
```  2770   by (fact dvd_lcmI2)
```
```  2771
```
```  2772 lemma coprime_exp2_nat [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
```
```  2773   for a b :: nat
```
```  2774   by (fact coprime_exp2)
```
```  2775
```
```  2776 lemma coprime_exp2_int [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
```
```  2777   for a b :: int
```
```  2778   by (fact coprime_exp2)
```
```  2779
```
```  2780 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
```
```  2781 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
```
```  2782 lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
```
```  2783 lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int]
```
```  2784
```
```  2785 lemma dvd_Lcm_int [simp]: "m \<in> M \<Longrightarrow> m dvd Lcm M"
```
```  2786   for M :: "int set"
```
```  2787   by (fact dvd_Lcm)
```
```  2788
```
```  2789 lemma gcd_neg_numeral_1_int [simp]: "gcd (- numeral n :: int) x = gcd (numeral n) x"
```
```  2790   by (fact gcd_neg1_int)
```
```  2791
```
```  2792 lemma gcd_neg_numeral_2_int [simp]: "gcd x (- numeral n :: int) = gcd x (numeral n)"
```
```  2793   by (fact gcd_neg2_int)
```
```  2794
```
```  2795 lemma gcd_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> gcd x y = x"
```
```  2796   for x y :: nat
```
```  2797   by (fact gcd_nat.absorb1)
```
```  2798
```
```  2799 lemma gcd_proj2_if_dvd_nat [simp]: "y dvd x \<Longrightarrow> gcd x y = y"
```
```  2800   for x y :: nat
```
```  2801   by (fact gcd_nat.absorb2)
```
```  2802
```
```  2803 lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]
```
```  2804 lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat]
```
```  2805 lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int]
```
```  2806
```
```  2807 end
```
{"ft_lang_label":"__label__en","ft_lang_prob":0.51085097,"math_prob":0.9815316,"size":83536,"snap":"2020-34-2020-40","text_gpt3_token_len":28453,"char_repetition_ratio":0.22074175,"word_repetition_ratio":0.17484768,"special_character_ratio":0.4092128,"punctuation_ratio":0.083024025,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99926966,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-09-19T03:58:39Z\",\"WARC-Record-ID\":\"<urn:uuid:5e46713d-1fce-4a62-a1d1-499296cf6fad>\",\"Content-Length\":\"460201\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:ce870112-7400-4b5e-908c-0f446e97df81>\",\"WARC-Concurrent-To\":\"<urn:uuid:aae0d36f-2b2d-48b8-8fa2-012df47a047e>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"http://isabelle.in.tum.de/repos/isabelle/file/85ed070017b7/src/HOL/GCD.thy\",\"WARC-Payload-Digest\":\"sha1:CM6IA4UAXP44CEOKU2CY4EKC34RCDNRM\",\"WARC-Block-Digest\":\"sha1:C6GHPERBQV65HCW2OGWQTOQADLMKAKWU\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-40/CC-MAIN-2020-40_segments_1600400189928.2_warc_CC-MAIN-20200919013135-20200919043135-00459.warc.gz\"}"}