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