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