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