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