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