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