src/HOL/GCD.thy
author wenzelm
Fri Jan 14 15:44:47 2011 +0100 (2011-01-14)
changeset 41550 efa734d9b221
parent 37770 cddb3106adb8
child 41792 ff3cb0c418b7
permissions -rw-r--r--
eliminated global prems;
tuned proofs;
     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 header {* Greatest common divisor and least common multiple *}
    29 
    30 theory GCD
    31 imports Fact Parity
    32 begin
    33 
    34 declare One_nat_def [simp del]
    35 
    36 subsection {* GCD and LCM definitions *}
    37 
    38 class gcd = zero + one + dvd +
    39   fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    40     and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    41 begin
    42 
    43 abbreviation
    44   coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    45 where
    46   "coprime x y == (gcd x y = 1)"
    47 
    48 end
    49 
    50 instantiation nat :: gcd
    51 begin
    52 
    53 fun
    54   gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    55 where
    56   "gcd_nat x y =
    57    (if y = 0 then x else gcd y (x mod y))"
    58 
    59 definition
    60   lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    61 where
    62   "lcm_nat x y = x * y div (gcd x y)"
    63 
    64 instance proof qed
    65 
    66 end
    67 
    68 instantiation int :: gcd
    69 begin
    70 
    71 definition
    72   gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
    73 where
    74   "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
    75 
    76 definition
    77   lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
    78 where
    79   "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
    80 
    81 instance proof qed
    82 
    83 end
    84 
    85 
    86 subsection {* Transfer setup *}
    87 
    88 lemma transfer_nat_int_gcd:
    89   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
    90   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
    91   unfolding gcd_int_def lcm_int_def
    92   by auto
    93 
    94 lemma transfer_nat_int_gcd_closures:
    95   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
    96   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
    97   by (auto simp add: gcd_int_def lcm_int_def)
    98 
    99 declare transfer_morphism_nat_int[transfer add return:
   100     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   101 
   102 lemma transfer_int_nat_gcd:
   103   "gcd (int x) (int y) = int (gcd x y)"
   104   "lcm (int x) (int y) = int (lcm x y)"
   105   by (unfold gcd_int_def lcm_int_def, auto)
   106 
   107 lemma transfer_int_nat_gcd_closures:
   108   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   109   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   110   by (auto simp add: gcd_int_def lcm_int_def)
   111 
   112 declare transfer_morphism_int_nat[transfer add return:
   113     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   114 
   115 
   116 subsection {* GCD properties *}
   117 
   118 (* was gcd_induct *)
   119 lemma gcd_nat_induct:
   120   fixes m n :: nat
   121   assumes "\<And>m. P m 0"
   122     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   123   shows "P m n"
   124   apply (rule gcd_nat.induct)
   125   apply (case_tac "y = 0")
   126   using assms apply simp_all
   127 done
   128 
   129 (* specific to int *)
   130 
   131 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
   132   by (simp add: gcd_int_def)
   133 
   134 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
   135   by (simp add: gcd_int_def)
   136 
   137 lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
   138 by(simp add: gcd_int_def)
   139 
   140 lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"
   141 by (simp add: gcd_int_def)
   142 
   143 lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
   144 by (metis abs_idempotent gcd_abs_int)
   145 
   146 lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
   147 by (metis abs_idempotent gcd_abs_int)
   148 
   149 lemma gcd_cases_int:
   150   fixes x :: int and y
   151   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   152       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   153       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   154       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   155   shows "P (gcd x y)"
   156 by (insert assms, auto, arith)
   157 
   158 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   159   by (simp add: gcd_int_def)
   160 
   161 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
   162   by (simp add: lcm_int_def)
   163 
   164 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
   165   by (simp add: lcm_int_def)
   166 
   167 lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"
   168   by (simp add: lcm_int_def)
   169 
   170 lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
   171 by(simp add:lcm_int_def)
   172 
   173 lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
   174 by (metis abs_idempotent lcm_int_def)
   175 
   176 lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
   177 by (metis abs_idempotent lcm_int_def)
   178 
   179 lemma lcm_cases_int:
   180   fixes x :: int and y
   181   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   182       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   183       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   184       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   185   shows "P (lcm x y)"
   186   using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
   187 
   188 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   189   by (simp add: lcm_int_def)
   190 
   191 (* was gcd_0, etc. *)
   192 lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
   193   by simp
   194 
   195 (* was igcd_0, etc. *)
   196 lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
   197   by (unfold gcd_int_def, auto)
   198 
   199 lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
   200   by simp
   201 
   202 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
   203   by (unfold gcd_int_def, auto)
   204 
   205 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
   206   by (case_tac "y = 0", auto)
   207 
   208 (* weaker, but useful for the simplifier *)
   209 
   210 lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   211   by simp
   212 
   213 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   214   by simp
   215 
   216 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   217   by (simp add: One_nat_def)
   218 
   219 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   220   by (simp add: gcd_int_def)
   221 
   222 lemma gcd_idem_nat: "gcd (x::nat) x = x"
   223 by simp
   224 
   225 lemma gcd_idem_int: "gcd (x::int) x = abs x"
   226 by (auto simp add: gcd_int_def)
   227 
   228 declare gcd_nat.simps [simp del]
   229 
   230 text {*
   231   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   232   conjunctions don't seem provable separately.
   233 *}
   234 
   235 lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
   236   and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
   237   apply (induct m n rule: gcd_nat_induct)
   238   apply (simp_all add: gcd_non_0_nat)
   239   apply (blast dest: dvd_mod_imp_dvd)
   240 done
   241 
   242 lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"
   243 by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)
   244 
   245 lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"
   246 by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)
   247 
   248 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   249 by(metis gcd_dvd1_nat dvd_trans)
   250 
   251 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   252 by(metis gcd_dvd2_nat dvd_trans)
   253 
   254 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   255 by(metis gcd_dvd1_int dvd_trans)
   256 
   257 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   258 by(metis gcd_dvd2_int dvd_trans)
   259 
   260 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   261   by (rule dvd_imp_le, auto)
   262 
   263 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   264   by (rule dvd_imp_le, auto)
   265 
   266 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   267   by (rule zdvd_imp_le, auto)
   268 
   269 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   270   by (rule zdvd_imp_le, auto)
   271 
   272 lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   273 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
   274 
   275 lemma gcd_greatest_int:
   276   "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   277   apply (subst gcd_abs_int)
   278   apply (subst abs_dvd_iff [symmetric])
   279   apply (rule gcd_greatest_nat [transferred])
   280   apply auto
   281 done
   282 
   283 lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
   284     (k dvd m & k dvd n)"
   285   by (blast intro!: gcd_greatest_nat intro: dvd_trans)
   286 
   287 lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   288   by (blast intro!: gcd_greatest_int intro: dvd_trans)
   289 
   290 lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   291   by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
   292 
   293 lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   294   by (auto simp add: gcd_int_def)
   295 
   296 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   297   by (insert gcd_zero_nat [of m n], arith)
   298 
   299 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   300   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
   301 
   302 interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
   303 proof
   304 qed (auto intro: dvd_antisym dvd_trans)
   305 
   306 interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
   307 proof
   308 qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
   309 
   310 lemmas gcd_assoc_nat = gcd_nat.assoc
   311 lemmas gcd_commute_nat = gcd_nat.commute
   312 lemmas gcd_left_commute_nat = gcd_nat.left_commute
   313 lemmas gcd_assoc_int = gcd_int.assoc
   314 lemmas gcd_commute_int = gcd_int.commute
   315 lemmas gcd_left_commute_int = gcd_int.left_commute
   316 
   317 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
   318 
   319 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
   320 
   321 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
   322     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   323   apply auto
   324   apply (rule dvd_antisym)
   325   apply (erule (1) gcd_greatest_nat)
   326   apply auto
   327 done
   328 
   329 lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   330     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   331 apply (case_tac "d = 0")
   332  apply simp
   333 apply (rule iffI)
   334  apply (rule zdvd_antisym_nonneg)
   335  apply (auto intro: gcd_greatest_int)
   336 done
   337 
   338 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   339 by (metis dvd.eq_iff gcd_unique_nat)
   340 
   341 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   342 by (metis dvd.eq_iff gcd_unique_nat)
   343 
   344 lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   345 by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
   346 
   347 lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   348 by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   349 
   350 
   351 text {*
   352   \medskip Multiplication laws
   353 *}
   354 
   355 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   356     -- {* \cite[page 27]{davenport92} *}
   357   apply (induct m n rule: gcd_nat_induct)
   358   apply simp
   359   apply (case_tac "k = 0")
   360   apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
   361 done
   362 
   363 lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   364   apply (subst (1 2) gcd_abs_int)
   365   apply (subst (1 2) abs_mult)
   366   apply (rule gcd_mult_distrib_nat [transferred])
   367   apply auto
   368 done
   369 
   370 lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   371   apply (insert gcd_mult_distrib_nat [of m k n])
   372   apply simp
   373   apply (erule_tac t = m in ssubst)
   374   apply simp
   375   done
   376 
   377 lemma coprime_dvd_mult_int:
   378   "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   379 apply (subst abs_dvd_iff [symmetric])
   380 apply (subst dvd_abs_iff [symmetric])
   381 apply (subst (asm) gcd_abs_int)
   382 apply (rule coprime_dvd_mult_nat [transferred])
   383     prefer 4 apply assumption
   384    apply auto
   385 apply (subst abs_mult [symmetric], auto)
   386 done
   387 
   388 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   389     (k dvd m * n) = (k dvd m)"
   390   by (auto intro: coprime_dvd_mult_nat)
   391 
   392 lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   393     (k dvd m * n) = (k dvd m)"
   394   by (auto intro: coprime_dvd_mult_int)
   395 
   396 lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   397   apply (rule dvd_antisym)
   398   apply (rule gcd_greatest_nat)
   399   apply (rule_tac n = k in coprime_dvd_mult_nat)
   400   apply (simp add: gcd_assoc_nat)
   401   apply (simp add: gcd_commute_nat)
   402   apply (simp_all add: mult_commute)
   403 done
   404 
   405 lemma gcd_mult_cancel_int:
   406   "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
   407 apply (subst (1 2) gcd_abs_int)
   408 apply (subst abs_mult)
   409 apply (rule gcd_mult_cancel_nat [transferred], auto)
   410 done
   411 
   412 lemma coprime_crossproduct_nat:
   413   fixes a b c d :: nat
   414   assumes "coprime a d" and "coprime b c"
   415   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" (is "?lhs \<longleftrightarrow> ?rhs")
   416 proof
   417   assume ?rhs then show ?lhs by simp
   418 next
   419   assume ?lhs
   420   from `?lhs` have "a dvd b * d" by (auto intro: dvdI dest: sym)
   421   with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
   422   from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym)
   423   with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
   424   from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult_commute)
   425   with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
   426   from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult_commute)
   427   with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
   428   from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym)
   429   moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym)
   430   ultimately show ?rhs ..
   431 qed
   432 
   433 lemma coprime_crossproduct_int:
   434   fixes a b c d :: int
   435   assumes "coprime a d" and "coprime b c"
   436   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>"
   437   using assms by (intro coprime_crossproduct_nat [transferred]) auto
   438 
   439 text {* \medskip Addition laws *}
   440 
   441 lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   442   apply (case_tac "n = 0")
   443   apply (simp_all add: gcd_non_0_nat)
   444 done
   445 
   446 lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   447   apply (subst (1 2) gcd_commute_nat)
   448   apply (subst add_commute)
   449   apply simp
   450 done
   451 
   452 (* to do: add the other variations? *)
   453 
   454 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   455   by (subst gcd_add1_nat [symmetric], auto)
   456 
   457 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   458   apply (subst gcd_commute_nat)
   459   apply (subst gcd_diff1_nat [symmetric])
   460   apply auto
   461   apply (subst gcd_commute_nat)
   462   apply (subst gcd_diff1_nat)
   463   apply assumption
   464   apply (rule gcd_commute_nat)
   465 done
   466 
   467 lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   468   apply (frule_tac b = y and a = x in pos_mod_sign)
   469   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   470   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
   471     zmod_zminus1_eq_if)
   472   apply (frule_tac a = x in pos_mod_bound)
   473   apply (subst (1 2) gcd_commute_nat)
   474   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   475     nat_le_eq_zle)
   476 done
   477 
   478 lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
   479   apply (case_tac "y = 0")
   480   apply force
   481   apply (case_tac "y > 0")
   482   apply (subst gcd_non_0_int, auto)
   483   apply (insert gcd_non_0_int [of "-y" "-x"])
   484   apply auto
   485 done
   486 
   487 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
   488 by (metis gcd_red_int mod_add_self1 zadd_commute)
   489 
   490 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   491 by (metis gcd_add1_int gcd_commute_int zadd_commute)
   492 
   493 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   494 by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
   495 
   496 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   497 by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
   498 
   499 
   500 (* to do: differences, and all variations of addition rules
   501     as simplification rules for nat and int *)
   502 
   503 (* FIXME remove iff *)
   504 lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n"
   505   using mult_dvd_mono [of 1] by auto
   506 
   507 (* to do: add the three variations of these, and for ints? *)
   508 
   509 lemma finite_divisors_nat[simp]:
   510   assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
   511 proof-
   512   have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
   513   from finite_subset[OF _ this] show ?thesis using assms
   514     by(bestsimp intro!:dvd_imp_le)
   515 qed
   516 
   517 lemma finite_divisors_int[simp]:
   518   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
   519 proof-
   520   have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
   521   hence "finite{d. abs d <= abs i}" by simp
   522   from finite_subset[OF _ this] show ?thesis using assms
   523     by(bestsimp intro!:dvd_imp_le_int)
   524 qed
   525 
   526 lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
   527 apply(rule antisym)
   528  apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
   529 apply simp
   530 done
   531 
   532 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
   533 apply(rule antisym)
   534  apply(rule Max_le_iff[THEN iffD2])
   535    apply simp
   536   apply fastsimp
   537  apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
   538 apply simp
   539 done
   540 
   541 lemma gcd_is_Max_divisors_nat:
   542   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
   543 apply(rule Max_eqI[THEN sym])
   544   apply (metis finite_Collect_conjI finite_divisors_nat)
   545  apply simp
   546  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
   547 apply simp
   548 done
   549 
   550 lemma gcd_is_Max_divisors_int:
   551   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
   552 apply(rule Max_eqI[THEN sym])
   553   apply (metis finite_Collect_conjI finite_divisors_int)
   554  apply simp
   555  apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
   556 apply simp
   557 done
   558 
   559 lemma gcd_code_int [code]:
   560   "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   561   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
   562 
   563 
   564 subsection {* Coprimality *}
   565 
   566 lemma div_gcd_coprime_nat:
   567   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   568   shows "coprime (a div gcd a b) (b div gcd a b)"
   569 proof -
   570   let ?g = "gcd a b"
   571   let ?a' = "a div ?g"
   572   let ?b' = "b div ?g"
   573   let ?g' = "gcd ?a' ?b'"
   574   have dvdg: "?g dvd a" "?g dvd b" by simp_all
   575   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   576   from dvdg dvdg' obtain ka kb ka' kb' where
   577       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   578     unfolding dvd_def by blast
   579   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   580     by simp_all
   581   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   582     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   583       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   584   have "?g \<noteq> 0" using nz by simp
   585   then have gp: "?g > 0" by arith
   586   from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
   587   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   588 qed
   589 
   590 lemma div_gcd_coprime_int:
   591   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   592   shows "coprime (a div gcd a b) (b div gcd a b)"
   593 apply (subst (1 2 3) gcd_abs_int)
   594 apply (subst (1 2) abs_div)
   595   apply simp
   596  apply simp
   597 apply(subst (1 2) abs_gcd_int)
   598 apply (rule div_gcd_coprime_nat [transferred])
   599 using nz apply (auto simp add: gcd_abs_int [symmetric])
   600 done
   601 
   602 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   603   using gcd_unique_nat[of 1 a b, simplified] by auto
   604 
   605 lemma coprime_Suc_0_nat:
   606     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   607   using coprime_nat by (simp add: One_nat_def)
   608 
   609 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
   610     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   611   using gcd_unique_int [of 1 a b]
   612   apply clarsimp
   613   apply (erule subst)
   614   apply (rule iffI)
   615   apply force
   616   apply (drule_tac x = "abs e" in exI)
   617   apply (case_tac "e >= 0")
   618   apply force
   619   apply force
   620 done
   621 
   622 lemma gcd_coprime_nat:
   623   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   624     b: "b = b' * gcd a b"
   625   shows    "coprime a' b'"
   626 
   627   apply (subgoal_tac "a' = a div gcd a b")
   628   apply (erule ssubst)
   629   apply (subgoal_tac "b' = b div gcd a b")
   630   apply (erule ssubst)
   631   apply (rule div_gcd_coprime_nat)
   632   using z apply force
   633   apply (subst (1) b)
   634   using z apply force
   635   apply (subst (1) a)
   636   using z apply force
   637   done
   638 
   639 lemma gcd_coprime_int:
   640   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   641     b: "b = b' * gcd a b"
   642   shows    "coprime a' b'"
   643 
   644   apply (subgoal_tac "a' = a div gcd a b")
   645   apply (erule ssubst)
   646   apply (subgoal_tac "b' = b div gcd a b")
   647   apply (erule ssubst)
   648   apply (rule div_gcd_coprime_int)
   649   using z apply force
   650   apply (subst (1) b)
   651   using z apply force
   652   apply (subst (1) a)
   653   using z apply force
   654   done
   655 
   656 lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   657     shows "coprime d (a * b)"
   658   apply (subst gcd_commute_nat)
   659   using da apply (subst gcd_mult_cancel_nat)
   660   apply (subst gcd_commute_nat, assumption)
   661   apply (subst gcd_commute_nat, rule db)
   662 done
   663 
   664 lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
   665     shows "coprime d (a * b)"
   666   apply (subst gcd_commute_int)
   667   using da apply (subst gcd_mult_cancel_int)
   668   apply (subst gcd_commute_int, assumption)
   669   apply (subst gcd_commute_int, rule db)
   670 done
   671 
   672 lemma coprime_lmult_nat:
   673   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   674 proof -
   675   have "gcd d a dvd gcd d (a * b)"
   676     by (rule gcd_greatest_nat, auto)
   677   with dab show ?thesis
   678     by auto
   679 qed
   680 
   681 lemma coprime_lmult_int:
   682   assumes "coprime (d::int) (a * b)" shows "coprime d a"
   683 proof -
   684   have "gcd d a dvd gcd d (a * b)"
   685     by (rule gcd_greatest_int, auto)
   686   with assms show ?thesis
   687     by auto
   688 qed
   689 
   690 lemma coprime_rmult_nat:
   691   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   692 proof -
   693   have "gcd d b dvd gcd d (a * b)"
   694     by (rule gcd_greatest_nat, auto intro: dvd_mult)
   695   with assms show ?thesis
   696     by auto
   697 qed
   698 
   699 lemma coprime_rmult_int:
   700   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   701 proof -
   702   have "gcd d b dvd gcd d (a * b)"
   703     by (rule gcd_greatest_int, auto intro: dvd_mult)
   704   with dab show ?thesis
   705     by auto
   706 qed
   707 
   708 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   709     coprime d a \<and>  coprime d b"
   710   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   711     coprime_mult_nat[of d a b]
   712   by blast
   713 
   714 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   715     coprime d a \<and>  coprime d b"
   716   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   717     coprime_mult_int[of d a b]
   718   by blast
   719 
   720 lemma gcd_coprime_exists_nat:
   721     assumes nz: "gcd (a::nat) b \<noteq> 0"
   722     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   723   apply (rule_tac x = "a div gcd a b" in exI)
   724   apply (rule_tac x = "b div gcd a b" in exI)
   725   using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)
   726 done
   727 
   728 lemma gcd_coprime_exists_int:
   729     assumes nz: "gcd (a::int) b \<noteq> 0"
   730     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   731   apply (rule_tac x = "a div gcd a b" in exI)
   732   apply (rule_tac x = "b div gcd a b" in exI)
   733   using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self)
   734 done
   735 
   736 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   737   by (induct n, simp_all add: coprime_mult_nat)
   738 
   739 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   740   by (induct n, simp_all add: coprime_mult_int)
   741 
   742 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   743   apply (rule coprime_exp_nat)
   744   apply (subst gcd_commute_nat)
   745   apply (rule coprime_exp_nat)
   746   apply (subst gcd_commute_nat, assumption)
   747 done
   748 
   749 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   750   apply (rule coprime_exp_int)
   751   apply (subst gcd_commute_int)
   752   apply (rule coprime_exp_int)
   753   apply (subst gcd_commute_int, assumption)
   754 done
   755 
   756 lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   757 proof (cases)
   758   assume "a = 0 & b = 0"
   759   thus ?thesis by simp
   760   next assume "~(a = 0 & b = 0)"
   761   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   762     by (auto simp:div_gcd_coprime_nat)
   763   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   764       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   765     apply (subst (1 2) mult_commute)
   766     apply (subst gcd_mult_distrib_nat [symmetric])
   767     apply simp
   768     done
   769   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   770     apply (subst div_power)
   771     apply auto
   772     apply (rule dvd_div_mult_self)
   773     apply (rule dvd_power_same)
   774     apply auto
   775     done
   776   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
   777     apply (subst div_power)
   778     apply auto
   779     apply (rule dvd_div_mult_self)
   780     apply (rule dvd_power_same)
   781     apply auto
   782     done
   783   finally show ?thesis .
   784 qed
   785 
   786 lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   787   apply (subst (1 2) gcd_abs_int)
   788   apply (subst (1 2) power_abs)
   789   apply (rule gcd_exp_nat [where n = n, transferred])
   790   apply auto
   791 done
   792 
   793 lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
   794   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   795 proof-
   796   let ?g = "gcd a b"
   797   {assume "?g = 0" with dc have ?thesis by auto}
   798   moreover
   799   {assume z: "?g \<noteq> 0"
   800     from gcd_coprime_exists_nat[OF z]
   801     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   802       by blast
   803     have thb: "?g dvd b" by auto
   804     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   805     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   806     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   807     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   808     with z have th_1: "a' dvd b' * c" by auto
   809     from coprime_dvd_mult_nat[OF ab'(3)] th_1
   810     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   811     from ab' have "a = ?g*a'" by algebra
   812     with thb thc have ?thesis by blast }
   813   ultimately show ?thesis by blast
   814 qed
   815 
   816 lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
   817   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   818 proof-
   819   let ?g = "gcd a b"
   820   {assume "?g = 0" with dc have ?thesis by auto}
   821   moreover
   822   {assume z: "?g \<noteq> 0"
   823     from gcd_coprime_exists_int[OF z]
   824     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   825       by blast
   826     have thb: "?g dvd b" by auto
   827     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   828     with dc have th0: "a' dvd b*c"
   829       using dvd_trans[of a' a "b*c"] by simp
   830     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   831     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   832     with z have th_1: "a' dvd b' * c" by auto
   833     from coprime_dvd_mult_int[OF ab'(3)] th_1
   834     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   835     from ab' have "a = ?g*a'" by algebra
   836     with thb thc have ?thesis by blast }
   837   ultimately show ?thesis by blast
   838 qed
   839 
   840 lemma pow_divides_pow_nat:
   841   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   842   shows "a dvd b"
   843 proof-
   844   let ?g = "gcd a b"
   845   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   846   {assume "?g = 0" with ab n have ?thesis by auto }
   847   moreover
   848   {assume z: "?g \<noteq> 0"
   849     hence zn: "?g ^ n \<noteq> 0" using n by simp
   850     from gcd_coprime_exists_nat[OF z]
   851     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   852       by blast
   853     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   854       by (simp add: ab'(1,2)[symmetric])
   855     hence "?g^n*a'^n dvd ?g^n *b'^n"
   856       by (simp only: power_mult_distrib mult_commute)
   857     with zn z n have th0:"a'^n dvd b'^n" by auto
   858     have "a' dvd a'^n" by (simp add: m)
   859     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   860     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   861     from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
   862     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   863     hence "a'*?g dvd b'*?g" by simp
   864     with ab'(1,2)  have ?thesis by simp }
   865   ultimately show ?thesis by blast
   866 qed
   867 
   868 lemma pow_divides_pow_int:
   869   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
   870   shows "a dvd b"
   871 proof-
   872   let ?g = "gcd a b"
   873   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   874   {assume "?g = 0" with ab n have ?thesis by auto }
   875   moreover
   876   {assume z: "?g \<noteq> 0"
   877     hence zn: "?g ^ n \<noteq> 0" using n by simp
   878     from gcd_coprime_exists_int[OF z]
   879     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   880       by blast
   881     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   882       by (simp add: ab'(1,2)[symmetric])
   883     hence "?g^n*a'^n dvd ?g^n *b'^n"
   884       by (simp only: power_mult_distrib mult_commute)
   885     with zn z n have th0:"a'^n dvd b'^n" by auto
   886     have "a' dvd a'^n" by (simp add: m)
   887     with th0 have "a' dvd b'^n"
   888       using dvd_trans[of a' "a'^n" "b'^n"] by simp
   889     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   890     from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
   891     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   892     hence "a'*?g dvd b'*?g" by simp
   893     with ab'(1,2)  have ?thesis by simp }
   894   ultimately show ?thesis by blast
   895 qed
   896 
   897 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   898   by (auto intro: pow_divides_pow_nat dvd_power_same)
   899 
   900 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   901   by (auto intro: pow_divides_pow_int dvd_power_same)
   902 
   903 lemma divides_mult_nat:
   904   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   905   shows "m * n dvd r"
   906 proof-
   907   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   908     unfolding dvd_def by blast
   909   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   910   hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
   911   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   912   from n' k show ?thesis unfolding dvd_def by auto
   913 qed
   914 
   915 lemma divides_mult_int:
   916   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   917   shows "m * n dvd r"
   918 proof-
   919   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   920     unfolding dvd_def by blast
   921   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   922   hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
   923   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   924   from n' k show ?thesis unfolding dvd_def by auto
   925 qed
   926 
   927 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   928   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   929   apply force
   930   apply (rule dvd_diff_nat)
   931   apply auto
   932 done
   933 
   934 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
   935   using coprime_plus_one_nat by (simp add: One_nat_def)
   936 
   937 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
   938   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   939   apply force
   940   apply (rule dvd_diff)
   941   apply auto
   942 done
   943 
   944 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   945   using coprime_plus_one_nat [of "n - 1"]
   946     gcd_commute_nat [of "n - 1" n] by auto
   947 
   948 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
   949   using coprime_plus_one_int [of "n - 1"]
   950     gcd_commute_int [of "n - 1" n] by auto
   951 
   952 lemma setprod_coprime_nat [rule_format]:
   953     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
   954   apply (case_tac "finite A")
   955   apply (induct set: finite)
   956   apply (auto simp add: gcd_mult_cancel_nat)
   957 done
   958 
   959 lemma setprod_coprime_int [rule_format]:
   960     "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
   961   apply (case_tac "finite A")
   962   apply (induct set: finite)
   963   apply (auto simp add: gcd_mult_cancel_int)
   964 done
   965 
   966 lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
   967     x dvd b \<Longrightarrow> x = 1"
   968   apply (subgoal_tac "x dvd gcd a b")
   969   apply simp
   970   apply (erule (1) gcd_greatest_nat)
   971 done
   972 
   973 lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
   974     x dvd b \<Longrightarrow> abs x = 1"
   975   apply (subgoal_tac "x dvd gcd a b")
   976   apply simp
   977   apply (erule (1) gcd_greatest_int)
   978 done
   979 
   980 lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
   981     coprime d e"
   982   apply (auto simp add: dvd_def)
   983   apply (frule coprime_lmult_int)
   984   apply (subst gcd_commute_int)
   985   apply (subst (asm) (2) gcd_commute_int)
   986   apply (erule coprime_lmult_int)
   987 done
   988 
   989 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
   990 apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
   991 done
   992 
   993 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
   994 apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
   995 done
   996 
   997 
   998 subsection {* Bezout's theorem *}
   999 
  1000 (* Function bezw returns a pair of witnesses to Bezout's theorem --
  1001    see the theorems that follow the definition. *)
  1002 fun
  1003   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1004 where
  1005   "bezw x y =
  1006   (if y = 0 then (1, 0) else
  1007       (snd (bezw y (x mod y)),
  1008        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1009 
  1010 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1011 
  1012 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1013        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1014   by simp
  1015 
  1016 declare bezw.simps [simp del]
  1017 
  1018 lemma bezw_aux [rule_format]:
  1019     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1020 proof (induct x y rule: gcd_nat_induct)
  1021   fix m :: nat
  1022   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1023     by auto
  1024   next fix m :: nat and n
  1025     assume ngt0: "n > 0" and
  1026       ih: "fst (bezw n (m mod n)) * int n +
  1027         snd (bezw n (m mod n)) * int (m mod n) =
  1028         int (gcd n (m mod n))"
  1029     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1030       apply (simp add: bezw_non_0 gcd_non_0_nat)
  1031       apply (erule subst)
  1032       apply (simp add: field_simps)
  1033       apply (subst mod_div_equality [of m n, symmetric])
  1034       (* applying simp here undoes the last substitution!
  1035          what is procedure cancel_div_mod? *)
  1036       apply (simp only: field_simps zadd_int [symmetric]
  1037         zmult_int [symmetric])
  1038       done
  1039 qed
  1040 
  1041 lemma bezout_int:
  1042   fixes x y
  1043   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1044 proof -
  1045   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1046       EX u v. u * x + v * y = gcd x y"
  1047     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1048     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1049     apply (unfold gcd_int_def)
  1050     apply simp
  1051     apply (subst bezw_aux [symmetric])
  1052     apply auto
  1053     done
  1054   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1055       (x \<le> 0 \<and> y \<le> 0)"
  1056     by auto
  1057   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1058     by (erule (1) bezout_aux)
  1059   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1060     apply (insert bezout_aux [of x "-y"])
  1061     apply auto
  1062     apply (rule_tac x = u in exI)
  1063     apply (rule_tac x = "-v" in exI)
  1064     apply (subst gcd_neg2_int [symmetric])
  1065     apply auto
  1066     done
  1067   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1068     apply (insert bezout_aux [of "-x" y])
  1069     apply auto
  1070     apply (rule_tac x = "-u" in exI)
  1071     apply (rule_tac x = v in exI)
  1072     apply (subst gcd_neg1_int [symmetric])
  1073     apply auto
  1074     done
  1075   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1076     apply (insert bezout_aux [of "-x" "-y"])
  1077     apply auto
  1078     apply (rule_tac x = "-u" in exI)
  1079     apply (rule_tac x = "-v" in exI)
  1080     apply (subst gcd_neg1_int [symmetric])
  1081     apply (subst gcd_neg2_int [symmetric])
  1082     apply auto
  1083     done
  1084   ultimately show ?thesis by blast
  1085 qed
  1086 
  1087 text {* versions of Bezout for nat, by Amine Chaieb *}
  1088 
  1089 lemma ind_euclid:
  1090   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1091   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1092   shows "P a b"
  1093 proof(induct "a + b" arbitrary: a b rule: less_induct)
  1094   case less
  1095   have "a = b \<or> a < b \<or> b < a" by arith
  1096   moreover {assume eq: "a= b"
  1097     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1098     by simp}
  1099   moreover
  1100   {assume lt: "a < b"
  1101     hence "a + b - a < a + b \<or> a = 0" by arith
  1102     moreover
  1103     {assume "a =0" with z c have "P a b" by blast }
  1104     moreover
  1105     {assume "a + b - a < a + b"
  1106       also have th0: "a + b - a = a + (b - a)" using lt by arith
  1107       finally have "a + (b - a) < a + b" .
  1108       then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
  1109       then have "P a b" by (simp add: th0[symmetric])}
  1110     ultimately have "P a b" by blast}
  1111   moreover
  1112   {assume lt: "a > b"
  1113     hence "b + a - b < a + b \<or> b = 0" by arith
  1114     moreover
  1115     {assume "b =0" with z c have "P a b" by blast }
  1116     moreover
  1117     {assume "b + a - b < a + b"
  1118       also have th0: "b + a - b = b + (a - b)" using lt by arith
  1119       finally have "b + (a - b) < a + b" .
  1120       then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
  1121       then have "P b a" by (simp add: th0[symmetric])
  1122       hence "P a b" using c by blast }
  1123     ultimately have "P a b" by blast}
  1124 ultimately  show "P a b" by blast
  1125 qed
  1126 
  1127 lemma bezout_lemma_nat:
  1128   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1129     (a * x = b * y + d \<or> b * x = a * y + d)"
  1130   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1131     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1132   using ex
  1133   apply clarsimp
  1134   apply (rule_tac x="d" in exI, simp)
  1135   apply (case_tac "a * x = b * y + d" , simp_all)
  1136   apply (rule_tac x="x + y" in exI)
  1137   apply (rule_tac x="y" in exI)
  1138   apply algebra
  1139   apply (rule_tac x="x" in exI)
  1140   apply (rule_tac x="x + y" in exI)
  1141   apply algebra
  1142 done
  1143 
  1144 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1145     (a * x = b * y + d \<or> b * x = a * y + d)"
  1146   apply(induct a b rule: ind_euclid)
  1147   apply blast
  1148   apply clarify
  1149   apply (rule_tac x="a" in exI, simp)
  1150   apply clarsimp
  1151   apply (rule_tac x="d" in exI)
  1152   apply (case_tac "a * x = b * y + d", simp_all)
  1153   apply (rule_tac x="x+y" in exI)
  1154   apply (rule_tac x="y" in exI)
  1155   apply algebra
  1156   apply (rule_tac x="x" in exI)
  1157   apply (rule_tac x="x+y" in exI)
  1158   apply algebra
  1159 done
  1160 
  1161 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1162     (a * x - b * y = d \<or> b * x - a * y = d)"
  1163   using bezout_add_nat[of a b]
  1164   apply clarsimp
  1165   apply (rule_tac x="d" in exI, simp)
  1166   apply (rule_tac x="x" in exI)
  1167   apply (rule_tac x="y" in exI)
  1168   apply auto
  1169 done
  1170 
  1171 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1172   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1173 proof-
  1174  from nz have ap: "a > 0" by simp
  1175  from bezout_add_nat[of a b]
  1176  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1177    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1178  moreover
  1179     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1180      from H have ?thesis by blast }
  1181  moreover
  1182  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1183    {assume b0: "b = 0" with H  have ?thesis by simp}
  1184    moreover
  1185    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1186      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1187        by auto
  1188      moreover
  1189      {assume db: "d=b"
  1190        with nz H have ?thesis apply simp
  1191          apply (rule exI[where x = b], simp)
  1192          apply (rule exI[where x = b])
  1193         by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1194     moreover
  1195     {assume db: "d < b"
  1196         {assume "x=0" hence ?thesis using nz H by simp }
  1197         moreover
  1198         {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1199           from db have "d \<le> b - 1" by simp
  1200           hence "d*b \<le> b*(b - 1)" by simp
  1201           with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1202           have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1203           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1204             by simp
  1205           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1206             by (simp only: mult_assoc right_distrib)
  1207           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1208             by algebra
  1209           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1210           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1211             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1212           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1213             by (simp only: diff_mult_distrib2 add_commute mult_ac)
  1214           hence ?thesis using H(1,2)
  1215             apply -
  1216             apply (rule exI[where x=d], simp)
  1217             apply (rule exI[where x="(b - 1) * y"])
  1218             by (rule exI[where x="x*(b - 1) - d"], simp)}
  1219         ultimately have ?thesis by blast}
  1220     ultimately have ?thesis by blast}
  1221   ultimately have ?thesis by blast}
  1222  ultimately show ?thesis by blast
  1223 qed
  1224 
  1225 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1226   shows "\<exists>x y. a * x = b * y + gcd a b"
  1227 proof-
  1228   let ?g = "gcd a b"
  1229   from bezout_add_strong_nat[OF a, of b]
  1230   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1231   from d(1,2) have "d dvd ?g" by simp
  1232   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1233   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1234   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1235   thus ?thesis by blast
  1236 qed
  1237 
  1238 
  1239 subsection {* LCM properties *}
  1240 
  1241 lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1242   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1243     zmult_int [symmetric] gcd_int_def)
  1244 
  1245 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1246   unfolding lcm_nat_def
  1247   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1248 
  1249 lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
  1250   unfolding lcm_int_def gcd_int_def
  1251   apply (subst int_mult [symmetric])
  1252   apply (subst prod_gcd_lcm_nat [symmetric])
  1253   apply (subst nat_abs_mult_distrib [symmetric])
  1254   apply (simp, simp add: abs_mult)
  1255 done
  1256 
  1257 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1258   unfolding lcm_nat_def by simp
  1259 
  1260 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1261   unfolding lcm_int_def by simp
  1262 
  1263 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1264   unfolding lcm_nat_def by simp
  1265 
  1266 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1267   unfolding lcm_int_def by simp
  1268 
  1269 lemma lcm_pos_nat:
  1270   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1271 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1272 
  1273 lemma lcm_pos_int:
  1274   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1275   apply (subst lcm_abs_int)
  1276   apply (rule lcm_pos_nat [transferred])
  1277   apply auto
  1278 done
  1279 
  1280 lemma dvd_pos_nat:
  1281   fixes n m :: nat
  1282   assumes "n > 0" and "m dvd n"
  1283   shows "m > 0"
  1284 using assms by (cases m) auto
  1285 
  1286 lemma lcm_least_nat:
  1287   assumes "(m::nat) dvd k" and "n dvd k"
  1288   shows "lcm m n dvd k"
  1289 proof (cases k)
  1290   case 0 then show ?thesis by auto
  1291 next
  1292   case (Suc _) then have pos_k: "k > 0" by auto
  1293   from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1294   with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
  1295   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1296   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1297   from pos_k k_m have pos_p: "p > 0" by auto
  1298   from pos_k k_n have pos_q: "q > 0" by auto
  1299   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1300     by (simp add: mult_ac gcd_mult_distrib_nat)
  1301   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1302     by (simp add: k_m [symmetric] k_n [symmetric])
  1303   also have "\<dots> = k * p * q * gcd m n"
  1304     by (simp add: mult_ac gcd_mult_distrib_nat)
  1305   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1306     by (simp only: k_m [symmetric] k_n [symmetric])
  1307   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1308     by (simp add: mult_ac)
  1309   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1310     by simp
  1311   with prod_gcd_lcm_nat [of m n]
  1312   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1313     by (simp add: mult_ac)
  1314   with pos_gcd have "lcm m n * gcd q p = k" by auto
  1315   then show ?thesis using dvd_def by auto
  1316 qed
  1317 
  1318 lemma lcm_least_int:
  1319   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1320 apply (subst lcm_abs_int)
  1321 apply (rule dvd_trans)
  1322 apply (rule lcm_least_nat [transferred, of _ "abs k" _])
  1323 apply auto
  1324 done
  1325 
  1326 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
  1327 proof (cases m)
  1328   case 0 then show ?thesis by simp
  1329 next
  1330   case (Suc _)
  1331   then have mpos: "m > 0" by simp
  1332   show ?thesis
  1333   proof (cases n)
  1334     case 0 then show ?thesis by simp
  1335   next
  1336     case (Suc _)
  1337     then have npos: "n > 0" by simp
  1338     have "gcd m n dvd n" by simp
  1339     then obtain k where "n = gcd m n * k" using dvd_def by auto
  1340     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1341       by (simp add: mult_ac)
  1342     also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
  1343     finally show ?thesis by (simp add: lcm_nat_def)
  1344   qed
  1345 qed
  1346 
  1347 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1348   apply (subst lcm_abs_int)
  1349   apply (rule dvd_trans)
  1350   prefer 2
  1351   apply (rule lcm_dvd1_nat [transferred])
  1352   apply auto
  1353 done
  1354 
  1355 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1356   using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def mult.commute gcd_nat.commute)
  1357 
  1358 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1359   using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def mult.commute gcd_nat.commute)
  1360 
  1361 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1362 by(metis lcm_dvd1_nat dvd_trans)
  1363 
  1364 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1365 by(metis lcm_dvd2_nat dvd_trans)
  1366 
  1367 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1368 by(metis lcm_dvd1_int dvd_trans)
  1369 
  1370 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1371 by(metis lcm_dvd2_int dvd_trans)
  1372 
  1373 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1374     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1375   by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1376 
  1377 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1378     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1379   by (auto intro: dvd_antisym [transferred] lcm_least_int)
  1380 
  1381 interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
  1382 proof
  1383   fix n m p :: nat
  1384   show "lcm (lcm n m) p = lcm n (lcm m p)"
  1385     by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
  1386   show "lcm m n = lcm n m"
  1387     by (simp add: lcm_nat_def gcd_commute_nat field_simps)
  1388 qed
  1389 
  1390 interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
  1391 proof
  1392   fix n m p :: int
  1393   show "lcm (lcm n m) p = lcm n (lcm m p)"
  1394     by (rule lcm_unique_int [THEN iffD1]) (metis dvd_trans lcm_unique_int)
  1395   show "lcm m n = lcm n m"
  1396     by (simp add: lcm_int_def lcm_nat.commute)
  1397 qed
  1398 
  1399 lemmas lcm_assoc_nat = lcm_nat.assoc
  1400 lemmas lcm_commute_nat = lcm_nat.commute
  1401 lemmas lcm_left_commute_nat = lcm_nat.left_commute
  1402 lemmas lcm_assoc_int = lcm_int.assoc
  1403 lemmas lcm_commute_int = lcm_int.commute
  1404 lemmas lcm_left_commute_int = lcm_int.left_commute
  1405 
  1406 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1407 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1408 
  1409 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1410   apply (rule sym)
  1411   apply (subst lcm_unique_nat [symmetric])
  1412   apply auto
  1413 done
  1414 
  1415 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1416   apply (rule sym)
  1417   apply (subst lcm_unique_int [symmetric])
  1418   apply auto
  1419 done
  1420 
  1421 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1422 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
  1423 
  1424 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1425 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1426 
  1427 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1428 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1429 
  1430 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1431 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1432 
  1433 lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
  1434 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1435 
  1436 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
  1437 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1438 
  1439 lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1440 proof qed (auto simp add: gcd_ac_nat)
  1441 
  1442 lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  1443 proof qed (auto simp add: gcd_ac_int)
  1444 
  1445 lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1446 proof qed (auto simp add: lcm_ac_nat)
  1447 
  1448 lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  1449 proof qed (auto simp add: lcm_ac_int)
  1450 
  1451 
  1452 (* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
  1453 
  1454 lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1455 by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
  1456 
  1457 lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1458 by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
  1459 
  1460 lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
  1461 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
  1462 
  1463 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  1464 by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
  1465 
  1466 
  1467 subsubsection {* The complete divisibility lattice *}
  1468 
  1469 
  1470 interpretation gcd_semilattice_nat: semilattice_inf "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
  1471 proof
  1472   case goal3 thus ?case by(metis gcd_unique_nat)
  1473 qed auto
  1474 
  1475 interpretation lcm_semilattice_nat: semilattice_sup "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
  1476 proof
  1477   case goal3 thus ?case by(metis lcm_unique_nat)
  1478 qed auto
  1479 
  1480 interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
  1481 
  1482 text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
  1483 GCD is defined via LCM to facilitate the proof that we have a complete lattice.
  1484 Later on we show that GCD and Gcd coincide on finite sets.
  1485 *}
  1486 context gcd
  1487 begin
  1488 
  1489 definition Gcd :: "'a set \<Rightarrow> 'a"
  1490 where "Gcd = fold gcd 0"
  1491 
  1492 definition Lcm :: "'a set \<Rightarrow> 'a"
  1493 where "Lcm = fold lcm 1"
  1494 
  1495 definition LCM :: "'a set \<Rightarrow> 'a" where
  1496 "LCM M = (if finite M then Lcm M else 0)"
  1497 
  1498 definition GCD :: "'a set \<Rightarrow> 'a" where
  1499 "GCD M = LCM(INT m:M. {d. d dvd m})"
  1500 
  1501 end
  1502 
  1503 lemma Gcd_empty[simp]: "Gcd {} = 0"
  1504 by(simp add:Gcd_def)
  1505 
  1506 lemma Lcm_empty[simp]: "Lcm {} = 1"
  1507 by(simp add:Lcm_def)
  1508 
  1509 lemma GCD_empty_nat[simp]: "GCD {} = (0::nat)"
  1510 by(simp add:GCD_def LCM_def)
  1511 
  1512 lemma LCM_eq_Lcm[simp]: "finite M \<Longrightarrow> LCM M = Lcm M"
  1513 by(simp add:LCM_def)
  1514 
  1515 lemma Lcm_insert_nat [simp]:
  1516   assumes "finite N"
  1517   shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
  1518 proof -
  1519   interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
  1520     by (rule fun_left_comm_idem_lcm_nat)
  1521   from assms show ?thesis by(simp add: Lcm_def)
  1522 qed
  1523 
  1524 lemma Lcm_insert_int [simp]:
  1525   assumes "finite N"
  1526   shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
  1527 proof -
  1528   interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
  1529     by (rule fun_left_comm_idem_lcm_int)
  1530   from assms show ?thesis by(simp add: Lcm_def)
  1531 qed
  1532 
  1533 lemma Gcd_insert_nat [simp]:
  1534   assumes "finite N"
  1535   shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
  1536 proof -
  1537   interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
  1538     by (rule fun_left_comm_idem_gcd_nat)
  1539   from assms show ?thesis by(simp add: Gcd_def)
  1540 qed
  1541 
  1542 lemma Gcd_insert_int [simp]:
  1543   assumes "finite N"
  1544   shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
  1545 proof -
  1546   interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
  1547     by (rule fun_left_comm_idem_gcd_int)
  1548   from assms show ?thesis by(simp add: Gcd_def)
  1549 qed
  1550 
  1551 lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
  1552 by(induct rule:finite_ne_induct) auto
  1553 
  1554 lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
  1555 by (metis Lcm0_iff empty_iff)
  1556 
  1557 lemma Gcd_dvd_nat [simp]:
  1558   assumes "finite M" and "(m::nat) \<in> M"
  1559   shows "Gcd M dvd m"
  1560 proof -
  1561   show ?thesis using gcd_semilattice_nat.fold_inf_le_inf[OF assms, of 0] by (simp add: Gcd_def)
  1562 qed
  1563 
  1564 lemma dvd_Gcd_nat[simp]:
  1565   assumes "finite M" and "ALL (m::nat) : M. n dvd m"
  1566   shows "n dvd Gcd M"
  1567 proof -
  1568   show ?thesis using gcd_semilattice_nat.inf_le_fold_inf[OF assms, of 0] by (simp add: Gcd_def)
  1569 qed
  1570 
  1571 lemma dvd_Lcm_nat [simp]:
  1572   assumes "finite M" and "(m::nat) \<in> M"
  1573   shows "m dvd Lcm M"
  1574 proof -
  1575   show ?thesis using lcm_semilattice_nat.sup_le_fold_sup[OF assms, of 1] by (simp add: Lcm_def)
  1576 qed
  1577 
  1578 lemma Lcm_dvd_nat[simp]:
  1579   assumes "finite M" and "ALL (m::nat) : M. m dvd n"
  1580   shows "Lcm M dvd n"
  1581 proof -
  1582   show ?thesis using lcm_semilattice_nat.fold_sup_le_sup[OF assms, of 1] by (simp add: Lcm_def)
  1583 qed
  1584 
  1585 interpretation gcd_lcm_complete_lattice_nat:
  1586   complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
  1587 proof
  1588   case goal1 show ?case by simp
  1589 next
  1590   case goal2 show ?case by simp
  1591 next
  1592   case goal5 thus ?case by (auto simp: LCM_def)
  1593 next
  1594   case goal6 thus ?case
  1595     by(auto simp: LCM_def)(metis finite_nat_set_iff_bounded_le gcd_proj2_if_dvd_nat gcd_le1_nat)
  1596 next
  1597   case goal3 thus ?case by (auto simp: GCD_def LCM_def)(metis finite_INT finite_divisors_nat)
  1598 next
  1599   case goal4 thus ?case by(auto simp: LCM_def GCD_def)
  1600 qed
  1601 
  1602 text{* Alternative characterizations of Gcd and GCD: *}
  1603 
  1604 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})"
  1605 apply(rule antisym)
  1606  apply(rule Max_ge)
  1607   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1608  apply simp
  1609 apply (rule Max_le_iff[THEN iffD2])
  1610   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1611  apply fastsimp
  1612 apply clarsimp
  1613 apply (metis Gcd_dvd_nat Max_in dvd_0_left dvd_Gcd_nat dvd_imp_le linorder_antisym_conv3 not_less0)
  1614 done
  1615 
  1616 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
  1617 apply(induct pred:finite)
  1618  apply simp
  1619 apply(case_tac "x=0")
  1620  apply simp
  1621 apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
  1622  apply simp
  1623 apply blast
  1624 done
  1625 
  1626 lemma Lcm_in_lcm_closed_set_nat:
  1627   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
  1628 apply(induct rule:finite_linorder_min_induct)
  1629  apply simp
  1630 apply simp
  1631 apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
  1632  apply simp
  1633  apply(case_tac "A={}")
  1634   apply simp
  1635  apply simp
  1636 apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  1637 done
  1638 
  1639 lemma Lcm_eq_Max_nat:
  1640   "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"
  1641 apply(rule antisym)
  1642  apply(rule Max_ge, assumption)
  1643  apply(erule (2) Lcm_in_lcm_closed_set_nat)
  1644 apply clarsimp
  1645 apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
  1646 done
  1647 
  1648 text{* Finally GCD is Gcd: *}
  1649 
  1650 lemma GCD_eq_Gcd[simp]: assumes "finite(M::nat set)" shows "GCD M = Gcd M"
  1651 proof-
  1652   have divisors_remove0_nat: "(\<Inter>m\<in>M. {d::nat. d dvd m}) = (\<Inter>m\<in>M-{0}. {d::nat. d dvd m})" by auto
  1653   show ?thesis
  1654   proof cases
  1655     assume "M={}" thus ?thesis by simp
  1656   next
  1657     assume "M\<noteq>{}"
  1658     show ?thesis
  1659     proof cases
  1660       assume "M={0}" thus ?thesis by(simp add:GCD_def LCM_def)
  1661     next
  1662       assume "M\<noteq>{0}"
  1663       with `M\<noteq>{}` assms show ?thesis
  1664         apply(subst Gcd_remove0_nat[OF assms])
  1665         apply(simp add:GCD_def)
  1666         apply(subst divisors_remove0_nat)
  1667         apply(simp add:LCM_def)
  1668         apply rule
  1669          apply rule
  1670          apply(subst Gcd_eq_Max)
  1671             apply simp
  1672            apply blast
  1673           apply blast
  1674          apply(rule Lcm_eq_Max_nat)
  1675             apply simp
  1676            apply blast
  1677           apply fastsimp
  1678          apply clarsimp
  1679         apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
  1680         done
  1681     qed
  1682   qed
  1683 qed
  1684 
  1685 lemma Lcm_set_nat [code_unfold]:
  1686   "Lcm (set ns) = foldl lcm (1::nat) ns"
  1687 proof -
  1688   interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
  1689   show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
  1690 qed
  1691 
  1692 lemma Lcm_set_int [code_unfold]:
  1693   "Lcm (set is) = foldl lcm (1::int) is"
  1694 proof -
  1695   interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
  1696   show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
  1697 qed
  1698 
  1699 lemma Gcd_set_nat [code_unfold]:
  1700   "Gcd (set ns) = foldl gcd (0::nat) ns"
  1701 proof -
  1702   interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
  1703   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
  1704 qed
  1705 
  1706 lemma Gcd_set_int [code_unfold]:
  1707   "Gcd (set ns) = foldl gcd (0::int) ns"
  1708 proof -
  1709   interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
  1710   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
  1711 qed
  1712 
  1713 
  1714 lemma mult_inj_if_coprime_nat:
  1715   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
  1716    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
  1717 apply(auto simp add:inj_on_def)
  1718 apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
  1719 apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
  1720              dvd.neq_le_trans dvd_triv_right mult_commute)
  1721 done
  1722 
  1723 text{* Nitpick: *}
  1724 
  1725 lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
  1726 apply (rule eq_reflection)
  1727 apply (induct x y rule: nat_gcd.induct)
  1728 by (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  1729 
  1730 lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \<equiv> Nitpick.nat_lcm x y"
  1731 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  1732 
  1733 end