src/HOL/GCD.thy
author haftmann
Sat Jun 27 20:20:32 2015 +0200 (2015-06-27)
changeset 60596 54168997757f
parent 60580 7e741e22d7fc
child 60597 2da9b632069b
permissions -rw-r--r--
algebraic specification for set gcd
     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}"
   529     by (blast intro: bounded_nat_set_is_finite)
   530   from finite_subset[OF _ this] show ?thesis using assms
   531     by (metis Collect_mono dvd_imp_le neq0_conv)
   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 (simp add: dvd_imp_le_int subset_iff)
   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" for e in exI)
   631   apply (case_tac "e >= 0" for e :: int)
   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   by (simp add: coprime_exp_nat gcd_nat.commute)
   766 
   767 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   768   by (simp add: coprime_exp_int gcd_int.commute)
   769 
   770 lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   771 proof (cases)
   772   assume "a = 0 & b = 0"
   773   thus ?thesis by simp
   774   next assume "~(a = 0 & b = 0)"
   775   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   776     by (auto simp:div_gcd_coprime_nat)
   777   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   778       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   779     by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
   780   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   781     by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
   782   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
   783     by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
   784   finally show ?thesis .
   785 qed
   786 
   787 lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   788   apply (subst (1 2) gcd_abs_int)
   789   apply (subst (1 2) power_abs)
   790   apply (rule gcd_exp_nat [where n = n, transferred])
   791   apply auto
   792 done
   793 
   794 lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
   795   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   796 proof-
   797   let ?g = "gcd a b"
   798   {assume "?g = 0" with dc have ?thesis by auto}
   799   moreover
   800   {assume z: "?g \<noteq> 0"
   801     from gcd_coprime_exists_nat[OF z]
   802     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   803       by blast
   804     have thb: "?g dvd b" by auto
   805     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   806     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   807     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   808     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
   809     with z have th_1: "a' dvd b' * c" by auto
   810     from coprime_dvd_mult_nat[OF ab'(3)] th_1
   811     have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
   812     from ab' have "a = ?g*a'" by algebra
   813     with thb thc have ?thesis by blast }
   814   ultimately show ?thesis by blast
   815 qed
   816 
   817 lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
   818   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   819 proof-
   820   let ?g = "gcd a b"
   821   {assume "?g = 0" with dc have ?thesis by auto}
   822   moreover
   823   {assume z: "?g \<noteq> 0"
   824     from gcd_coprime_exists_int[OF z]
   825     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   826       by blast
   827     have thb: "?g dvd b" by auto
   828     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   829     with dc have th0: "a' dvd b*c"
   830       using dvd_trans[of a' a "b*c"] by simp
   831     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   832     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
   833     with z have th_1: "a' dvd b' * c" by auto
   834     from coprime_dvd_mult_int[OF ab'(3)] th_1
   835     have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
   836     from ab' have "a = ?g*a'" by algebra
   837     with thb thc have ?thesis by blast }
   838   ultimately show ?thesis by blast
   839 qed
   840 
   841 lemma pow_divides_pow_nat:
   842   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   843   shows "a dvd b"
   844 proof-
   845   let ?g = "gcd a b"
   846   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   847   {assume "?g = 0" with ab n have ?thesis by auto }
   848   moreover
   849   {assume z: "?g \<noteq> 0"
   850     hence zn: "?g ^ n \<noteq> 0" using n by simp
   851     from gcd_coprime_exists_nat[OF z]
   852     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   853       by blast
   854     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   855       by (simp add: ab'(1,2)[symmetric])
   856     hence "?g^n*a'^n dvd ?g^n *b'^n"
   857       by (simp only: power_mult_distrib mult.commute)
   858     then have th0: "a'^n dvd b'^n"
   859       using zn by auto
   860     have "a' dvd a'^n" by (simp add: m)
   861     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   862     hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
   863     from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
   864     have "a' dvd b'" by (subst (asm) mult.commute, blast)
   865     hence "a'*?g dvd b'*?g" by simp
   866     with ab'(1,2)  have ?thesis by simp }
   867   ultimately show ?thesis by blast
   868 qed
   869 
   870 lemma pow_divides_pow_int:
   871   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
   872   shows "a dvd b"
   873 proof-
   874   let ?g = "gcd a b"
   875   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   876   {assume "?g = 0" with ab n have ?thesis by auto }
   877   moreover
   878   {assume z: "?g \<noteq> 0"
   879     hence zn: "?g ^ n \<noteq> 0" using n by simp
   880     from gcd_coprime_exists_int[OF z]
   881     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   882       by blast
   883     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   884       by (simp add: ab'(1,2)[symmetric])
   885     hence "?g^n*a'^n dvd ?g^n *b'^n"
   886       by (simp only: power_mult_distrib mult.commute)
   887     with zn z n have th0:"a'^n dvd b'^n" by auto
   888     have "a' dvd a'^n" by (simp add: m)
   889     with th0 have "a' dvd b'^n"
   890       using dvd_trans[of a' "a'^n" "b'^n"] by simp
   891     hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
   892     from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
   893     have "a' dvd b'" by (subst (asm) mult.commute, blast)
   894     hence "a'*?g dvd b'*?g" by simp
   895     with ab'(1,2)  have ?thesis by simp }
   896   ultimately show ?thesis by blast
   897 qed
   898 
   899 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   900   by (auto intro: pow_divides_pow_nat dvd_power_same)
   901 
   902 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   903   by (auto intro: pow_divides_pow_int dvd_power_same)
   904 
   905 lemma divides_mult_nat:
   906   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   907   shows "m * n dvd r"
   908 proof-
   909   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   910     unfolding dvd_def by blast
   911   from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   912   hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
   913   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   914   from n' k show ?thesis unfolding dvd_def by auto
   915 qed
   916 
   917 lemma divides_mult_int:
   918   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   919   shows "m * n dvd r"
   920 proof-
   921   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   922     unfolding dvd_def by blast
   923   from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   924   hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
   925   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   926   from n' k show ?thesis unfolding dvd_def by auto
   927 qed
   928 
   929 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   930   by (simp add: gcd_nat.commute)
   931 
   932 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
   933   using coprime_plus_one_nat by (simp add: One_nat_def)
   934 
   935 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
   936   by (simp add: gcd_int.commute)
   937 
   938 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   939   using coprime_plus_one_nat [of "n - 1"]
   940     gcd_commute_nat [of "n - 1" n] by auto
   941 
   942 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
   943   using coprime_plus_one_int [of "n - 1"]
   944     gcd_commute_int [of "n - 1" n] by auto
   945 
   946 lemma setprod_coprime_nat [rule_format]:
   947     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
   948   apply (case_tac "finite A")
   949   apply (induct set: finite)
   950   apply (auto simp add: gcd_mult_cancel_nat)
   951 done
   952 
   953 lemma setprod_coprime_int [rule_format]:
   954     "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
   955   apply (case_tac "finite A")
   956   apply (induct set: finite)
   957   apply (auto simp add: gcd_mult_cancel_int)
   958 done
   959 
   960 lemma coprime_common_divisor_nat: 
   961     "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
   962   by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
   963 
   964 lemma coprime_common_divisor_int:
   965     "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
   966   using gcd_greatest by fastforce
   967 
   968 lemma coprime_divisors_nat:
   969     "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
   970   by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
   971 
   972 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
   973 by (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
   974 
   975 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
   976 by (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
   977 
   978 
   979 subsection {* Bezout's theorem *}
   980 
   981 (* Function bezw returns a pair of witnesses to Bezout's theorem --
   982    see the theorems that follow the definition. *)
   983 fun
   984   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
   985 where
   986   "bezw x y =
   987   (if y = 0 then (1, 0) else
   988       (snd (bezw y (x mod y)),
   989        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
   990 
   991 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
   992 
   993 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
   994        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
   995   by simp
   996 
   997 declare bezw.simps [simp del]
   998 
   999 lemma bezw_aux [rule_format]:
  1000     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1001 proof (induct x y rule: gcd_nat_induct)
  1002   fix m :: nat
  1003   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1004     by auto
  1005   next fix m :: nat and n
  1006     assume ngt0: "n > 0" and
  1007       ih: "fst (bezw n (m mod n)) * int n +
  1008         snd (bezw n (m mod n)) * int (m mod n) =
  1009         int (gcd n (m mod n))"
  1010     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1011       apply (simp add: bezw_non_0 gcd_non_0_nat)
  1012       apply (erule subst)
  1013       apply (simp add: field_simps)
  1014       apply (subst mod_div_equality [of m n, symmetric])
  1015       (* applying simp here undoes the last substitution!
  1016          what is procedure cancel_div_mod? *)
  1017       apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
  1018       done
  1019 qed
  1020 
  1021 lemma bezout_int:
  1022   fixes x y
  1023   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1024 proof -
  1025   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1026       EX u v. u * x + v * y = gcd x y"
  1027     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1028     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1029     apply (unfold gcd_int_def)
  1030     apply simp
  1031     apply (subst bezw_aux [symmetric])
  1032     apply auto
  1033     done
  1034   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1035       (x \<le> 0 \<and> y \<le> 0)"
  1036     by auto
  1037   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1038     by (erule (1) bezout_aux)
  1039   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1040     apply (insert bezout_aux [of x "-y"])
  1041     apply auto
  1042     apply (rule_tac x = u in exI)
  1043     apply (rule_tac x = "-v" in exI)
  1044     apply (subst gcd_neg2_int [symmetric])
  1045     apply auto
  1046     done
  1047   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1048     apply (insert bezout_aux [of "-x" y])
  1049     apply auto
  1050     apply (rule_tac x = "-u" in exI)
  1051     apply (rule_tac x = v in exI)
  1052     apply (subst gcd_neg1_int [symmetric])
  1053     apply auto
  1054     done
  1055   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1056     apply (insert bezout_aux [of "-x" "-y"])
  1057     apply auto
  1058     apply (rule_tac x = "-u" in exI)
  1059     apply (rule_tac x = "-v" in exI)
  1060     apply (subst gcd_neg1_int [symmetric])
  1061     apply (subst gcd_neg2_int [symmetric])
  1062     apply auto
  1063     done
  1064   ultimately show ?thesis by blast
  1065 qed
  1066 
  1067 text {* versions of Bezout for nat, by Amine Chaieb *}
  1068 
  1069 lemma ind_euclid:
  1070   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1071   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1072   shows "P a b"
  1073 proof(induct "a + b" arbitrary: a b rule: less_induct)
  1074   case less
  1075   have "a = b \<or> a < b \<or> b < a" by arith
  1076   moreover {assume eq: "a= b"
  1077     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1078     by simp}
  1079   moreover
  1080   {assume lt: "a < b"
  1081     hence "a + b - a < a + b \<or> a = 0" by arith
  1082     moreover
  1083     {assume "a =0" with z c have "P a b" by blast }
  1084     moreover
  1085     {assume "a + b - a < a + b"
  1086       also have th0: "a + b - a = a + (b - a)" using lt by arith
  1087       finally have "a + (b - a) < a + b" .
  1088       then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
  1089       then have "P a b" by (simp add: th0[symmetric])}
  1090     ultimately have "P a b" by blast}
  1091   moreover
  1092   {assume lt: "a > b"
  1093     hence "b + a - b < a + b \<or> b = 0" by arith
  1094     moreover
  1095     {assume "b =0" with z c have "P a b" by blast }
  1096     moreover
  1097     {assume "b + a - b < a + b"
  1098       also have th0: "b + a - b = b + (a - b)" using lt by arith
  1099       finally have "b + (a - b) < a + b" .
  1100       then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
  1101       then have "P b a" by (simp add: th0[symmetric])
  1102       hence "P a b" using c by blast }
  1103     ultimately have "P a b" by blast}
  1104 ultimately  show "P a b" by blast
  1105 qed
  1106 
  1107 lemma bezout_lemma_nat:
  1108   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1109     (a * x = b * y + d \<or> b * x = a * y + d)"
  1110   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1111     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1112   using ex
  1113   apply clarsimp
  1114   apply (rule_tac x="d" in exI, simp)
  1115   apply (case_tac "a * x = b * y + d" , simp_all)
  1116   apply (rule_tac x="x + y" in exI)
  1117   apply (rule_tac x="y" in exI)
  1118   apply algebra
  1119   apply (rule_tac x="x" in exI)
  1120   apply (rule_tac x="x + y" in exI)
  1121   apply algebra
  1122 done
  1123 
  1124 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1125     (a * x = b * y + d \<or> b * x = a * y + d)"
  1126   apply(induct a b rule: ind_euclid)
  1127   apply blast
  1128   apply clarify
  1129   apply (rule_tac x="a" in exI, simp)
  1130   apply clarsimp
  1131   apply (rule_tac x="d" in exI)
  1132   apply (case_tac "a * x = b * y + d", simp_all)
  1133   apply (rule_tac x="x+y" in exI)
  1134   apply (rule_tac x="y" in exI)
  1135   apply algebra
  1136   apply (rule_tac x="x" in exI)
  1137   apply (rule_tac x="x+y" in exI)
  1138   apply algebra
  1139 done
  1140 
  1141 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1142     (a * x - b * y = d \<or> b * x - a * y = d)"
  1143   using bezout_add_nat[of a b]
  1144   apply clarsimp
  1145   apply (rule_tac x="d" in exI, simp)
  1146   apply (rule_tac x="x" in exI)
  1147   apply (rule_tac x="y" in exI)
  1148   apply auto
  1149 done
  1150 
  1151 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1152   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1153 proof-
  1154  from nz have ap: "a > 0" by simp
  1155  from bezout_add_nat[of a b]
  1156  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1157    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1158  moreover
  1159     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1160      from H have ?thesis by blast }
  1161  moreover
  1162  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1163    {assume b0: "b = 0" with H  have ?thesis by simp}
  1164    moreover
  1165    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1166      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1167        by auto
  1168      moreover
  1169      {assume db: "d=b"
  1170        with nz H have ?thesis apply simp
  1171          apply (rule exI[where x = b], simp)
  1172          apply (rule exI[where x = b])
  1173         by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1174     moreover
  1175     {assume db: "d < b"
  1176         {assume "x=0" hence ?thesis using nz H by simp }
  1177         moreover
  1178         {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1179           from db have "d \<le> b - 1" by simp
  1180           hence "d*b \<le> b*(b - 1)" by simp
  1181           with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1182           have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1183           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1184             by simp
  1185           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1186             by (simp only: mult.assoc distrib_left)
  1187           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1188             by algebra
  1189           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1190           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1191             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1192           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1193             by (simp only: diff_mult_distrib2 ac_simps)
  1194           hence ?thesis using H(1,2)
  1195             apply -
  1196             apply (rule exI[where x=d], simp)
  1197             apply (rule exI[where x="(b - 1) * y"])
  1198             by (rule exI[where x="x*(b - 1) - d"], simp)}
  1199         ultimately have ?thesis by blast}
  1200     ultimately have ?thesis by blast}
  1201   ultimately have ?thesis by blast}
  1202  ultimately show ?thesis by blast
  1203 qed
  1204 
  1205 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1206   shows "\<exists>x y. a * x = b * y + gcd a b"
  1207 proof-
  1208   let ?g = "gcd a b"
  1209   from bezout_add_strong_nat[OF a, of b]
  1210   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1211   from d(1,2) have "d dvd ?g" by simp
  1212   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1213   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1214   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1215   thus ?thesis by blast
  1216 qed
  1217 
  1218 
  1219 subsection {* LCM properties *}
  1220 
  1221 lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1222   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1223     of_nat_mult gcd_int_def)
  1224 
  1225 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1226   unfolding lcm_nat_def
  1227   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1228 
  1229 lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
  1230   unfolding lcm_int_def gcd_int_def
  1231   apply (subst int_mult [symmetric])
  1232   apply (subst prod_gcd_lcm_nat [symmetric])
  1233   apply (subst nat_abs_mult_distrib [symmetric])
  1234   apply (simp, simp add: abs_mult)
  1235 done
  1236 
  1237 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1238   unfolding lcm_nat_def by simp
  1239 
  1240 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1241   unfolding lcm_int_def by simp
  1242 
  1243 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1244   unfolding lcm_nat_def by simp
  1245 
  1246 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1247   unfolding lcm_int_def by simp
  1248 
  1249 lemma lcm_pos_nat:
  1250   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1251 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1252 
  1253 lemma lcm_pos_int:
  1254   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1255   apply (subst lcm_abs_int)
  1256   apply (rule lcm_pos_nat [transferred])
  1257   apply auto
  1258 done
  1259 
  1260 lemma dvd_pos_nat:
  1261   fixes n m :: nat
  1262   assumes "n > 0" and "m dvd n"
  1263   shows "m > 0"
  1264 using assms by (cases m) auto
  1265 
  1266 lemma lcm_least_nat:
  1267   assumes "(m::nat) dvd k" and "n dvd k"
  1268   shows "lcm m n dvd k"
  1269 proof (cases k)
  1270   case 0 then show ?thesis by auto
  1271 next
  1272   case (Suc _) then have pos_k: "k > 0" by auto
  1273   from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1274   with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
  1275   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1276   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1277   from pos_k k_m have pos_p: "p > 0" by auto
  1278   from pos_k k_n have pos_q: "q > 0" by auto
  1279   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1280     by (simp add: ac_simps gcd_mult_distrib_nat)
  1281   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1282     by (simp add: k_m [symmetric] k_n [symmetric])
  1283   also have "\<dots> = k * p * q * gcd m n"
  1284     by (simp add: ac_simps gcd_mult_distrib_nat)
  1285   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1286     by (simp only: k_m [symmetric] k_n [symmetric])
  1287   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1288     by (simp add: ac_simps)
  1289   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1290     by simp
  1291   with prod_gcd_lcm_nat [of m n]
  1292   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1293     by (simp add: ac_simps)
  1294   with pos_gcd have "lcm m n * gcd q p = k" by auto
  1295   then show ?thesis using dvd_def by auto
  1296 qed
  1297 
  1298 lemma lcm_least_int:
  1299   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1300 apply (subst lcm_abs_int)
  1301 apply (rule dvd_trans)
  1302 apply (rule lcm_least_nat [transferred, of _ "abs k" _])
  1303 apply auto
  1304 done
  1305 
  1306 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
  1307 proof (cases m)
  1308   case 0 then show ?thesis by simp
  1309 next
  1310   case (Suc _)
  1311   then have mpos: "m > 0" by simp
  1312   show ?thesis
  1313   proof (cases n)
  1314     case 0 then show ?thesis by simp
  1315   next
  1316     case (Suc _)
  1317     then have npos: "n > 0" by simp
  1318     have "gcd m n dvd n" by simp
  1319     then obtain k where "n = gcd m n * k" using dvd_def by auto
  1320     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1321       by (simp add: ac_simps)
  1322     also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
  1323     finally show ?thesis by (simp add: lcm_nat_def)
  1324   qed
  1325 qed
  1326 
  1327 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1328   apply (subst lcm_abs_int)
  1329   apply (rule dvd_trans)
  1330   prefer 2
  1331   apply (rule lcm_dvd1_nat [transferred])
  1332   apply auto
  1333 done
  1334 
  1335 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1336   using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def mult.commute gcd_nat.commute)
  1337 
  1338 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1339   using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def mult.commute gcd_nat.commute)
  1340 
  1341 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1342 by(metis lcm_dvd1_nat dvd_trans)
  1343 
  1344 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1345 by(metis lcm_dvd2_nat dvd_trans)
  1346 
  1347 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1348 by(metis lcm_dvd1_int dvd_trans)
  1349 
  1350 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1351 by(metis lcm_dvd2_int dvd_trans)
  1352 
  1353 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1354     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1355   by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1356 
  1357 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1358     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1359   using lcm_least_int zdvd_antisym_nonneg by auto
  1360 
  1361 interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
  1362   + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
  1363 proof
  1364   fix n m p :: nat
  1365   show "lcm (lcm n m) p = lcm n (lcm m p)"
  1366     by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
  1367   show "lcm m n = lcm n m"
  1368     by (simp add: lcm_nat_def gcd_commute_nat field_simps)
  1369   show "lcm m m = m"
  1370     by (metis dvd.order_refl lcm_unique_nat)
  1371   show "lcm m 1 = m"
  1372     by (metis dvd.dual_order.refl lcm_unique_nat one_dvd)
  1373 qed
  1374 
  1375 interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
  1376 proof
  1377   fix n m p :: int
  1378   show "lcm (lcm n m) p = lcm n (lcm m p)"
  1379     by (rule lcm_unique_int [THEN iffD1]) (metis dvd_trans lcm_unique_int)
  1380   show "lcm m n = lcm n m"
  1381     by (simp add: lcm_int_def lcm_nat.commute)
  1382 qed
  1383 
  1384 lemmas lcm_assoc_nat = lcm_nat.assoc
  1385 lemmas lcm_commute_nat = lcm_nat.commute
  1386 lemmas lcm_left_commute_nat = lcm_nat.left_commute
  1387 lemmas lcm_assoc_int = lcm_int.assoc
  1388 lemmas lcm_commute_int = lcm_int.commute
  1389 lemmas lcm_left_commute_int = lcm_int.left_commute
  1390 
  1391 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1392 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1393 
  1394 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1395   apply (rule sym)
  1396   apply (subst lcm_unique_nat [symmetric])
  1397   apply auto
  1398 done
  1399 
  1400 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1401   apply (rule sym)
  1402   apply (subst lcm_unique_int [symmetric])
  1403   apply auto
  1404 done
  1405 
  1406 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1407 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
  1408 
  1409 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1410 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1411 
  1412 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1413 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1414 
  1415 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1416 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1417 
  1418 lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
  1419 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1420 
  1421 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
  1422 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1423 
  1424 lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1425 proof qed (auto simp add: gcd_ac_nat)
  1426 
  1427 lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  1428 proof qed (auto simp add: gcd_ac_int)
  1429 
  1430 lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1431 proof qed (auto simp add: lcm_ac_nat)
  1432 
  1433 lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  1434 proof qed (auto simp add: lcm_ac_int)
  1435 
  1436 
  1437 (* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
  1438 
  1439 lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1440 by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
  1441 
  1442 lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1443 by (metis lcm_0_int lcm_0_left_int lcm_pos_int less_le)
  1444 
  1445 lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
  1446 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
  1447 
  1448 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  1449 by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
  1450 
  1451 
  1452 subsection {* The complete divisibility lattice *}
  1453 
  1454 interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
  1455 proof (default, goals)
  1456   case 3
  1457   thus ?case by(metis gcd_unique_nat)
  1458 qed auto
  1459 
  1460 interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
  1461 proof (default, goals)
  1462   case 3
  1463   thus ?case by(metis lcm_unique_nat)
  1464 qed auto
  1465 
  1466 interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
  1467 
  1468 text{* Lifting gcd and lcm to sets (Gcd/Lcm).
  1469 Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
  1470 *}
  1471 
  1472 class Gcd = gcd +
  1473   fixes Gcd :: "'a set \<Rightarrow> 'a"
  1474   fixes Lcm :: "'a set \<Rightarrow> 'a"
  1475 
  1476 instantiation nat :: Gcd
  1477 begin
  1478 
  1479 definition
  1480   "Lcm (M::nat set) = (if finite M then semilattice_neutr_set.F lcm 1 M else 0)"
  1481 
  1482 interpretation semilattice_neutr_set lcm "1::nat" ..
  1483 
  1484 lemma Lcm_nat_infinite:
  1485   "\<not> finite M \<Longrightarrow> Lcm M = (0::nat)"
  1486   by (simp add: Lcm_nat_def)
  1487 
  1488 lemma Lcm_nat_empty:
  1489   "Lcm {} = (1::nat)"
  1490   by (simp add: Lcm_nat_def)
  1491 
  1492 lemma Lcm_nat_insert:
  1493   "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
  1494   by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite)
  1495 
  1496 definition
  1497   "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
  1498 
  1499 instance ..
  1500 
  1501 end
  1502 
  1503 class semiring_Gcd = semiring_gcd + Gcd +
  1504   assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
  1505     and dvd_Gcd: "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
  1506     and Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)"
  1507 begin
  1508 
  1509 lemma Gcd_empty [simp]:
  1510   "Gcd {} = 0"
  1511   by (rule dvd_0_left, rule dvd_Gcd) simp
  1512 
  1513 end
  1514 
  1515 lemma dvd_Lcm_nat [simp]:
  1516   fixes M :: "nat set"
  1517   assumes "m \<in> M"
  1518   shows "m dvd Lcm M"
  1519 proof (cases "finite M")
  1520   case False then show ?thesis by (simp add: Lcm_nat_infinite)
  1521 next
  1522   case True then show ?thesis using assms by (induct M) (auto simp add: Lcm_nat_insert)
  1523 qed
  1524 
  1525 lemma Lcm_dvd_nat [simp]:
  1526   fixes M :: "nat set"
  1527   assumes "\<forall>m\<in>M. m dvd n"
  1528   shows "Lcm M dvd n"
  1529 proof (cases "n = 0")
  1530   assume "n \<noteq> 0"
  1531   hence "finite {d. d dvd n}" by (rule finite_divisors_nat)
  1532   moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
  1533   ultimately have "finite M" by (rule rev_finite_subset)
  1534   then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
  1535 qed simp
  1536 
  1537 interpretation gcd_lcm_complete_lattice_nat:
  1538   complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
  1539 where "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
  1540   and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
  1541 proof -
  1542   show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
  1543   proof (default, goals)
  1544     case 1
  1545     thus ?case by (simp add: Gcd_nat_def)
  1546   next
  1547     case 2
  1548     thus ?case by (simp add: Gcd_nat_def)
  1549   next
  1550     case 5
  1551     show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
  1552   next
  1553     case 6
  1554     show ?case by (simp add: Lcm_nat_empty)
  1555   next
  1556     case 3
  1557     thus ?case by simp
  1558   next
  1559     case 4
  1560     thus ?case by simp
  1561   qed
  1562   then interpret gcd_lcm_complete_lattice_nat:
  1563     complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
  1564   from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
  1565   from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" .
  1566 qed
  1567 
  1568 declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
  1569 declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
  1570 
  1571 lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
  1572   by (fact Lcm_nat_empty)
  1573 
  1574 lemma Lcm_insert_nat [simp]:
  1575   shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
  1576   by (fact gcd_lcm_complete_lattice_nat.Sup_insert)
  1577 
  1578 lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
  1579 by(induct rule:finite_ne_induct) auto
  1580 
  1581 lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
  1582 by (metis Lcm0_iff empty_iff)
  1583 
  1584 instance nat :: semiring_Gcd
  1585 proof
  1586   show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
  1587     using that by (fact gcd_lcm_complete_lattice_nat.Inf_lower)
  1588 next
  1589   show "n dvd Gcd N" if "\<forall>m\<in>N. n dvd m" for N and n :: nat
  1590     using that by (simp only: gcd_lcm_complete_lattice_nat.Inf_greatest)
  1591 next
  1592   show "Gcd (insert n N) = gcd n (Gcd N)" for N and n :: nat
  1593     by simp
  1594 qed
  1595 
  1596 text{* Alternative characterizations of Gcd: *}
  1597 
  1598 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})"
  1599 apply(rule antisym)
  1600  apply(rule Max_ge)
  1601   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1602  apply (simp add: Gcd_dvd)
  1603 apply (rule Max_le_iff[THEN iffD2])
  1604   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1605  apply fastforce
  1606 apply clarsimp
  1607 apply (metis Gcd_dvd Max_in dvd_0_left dvd_Gcd dvd_imp_le linorder_antisym_conv3 not_less0)
  1608 done
  1609 
  1610 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
  1611 apply(induct pred:finite)
  1612  apply simp
  1613 apply(case_tac "x=0")
  1614  apply simp
  1615 apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
  1616  apply simp
  1617 apply blast
  1618 done
  1619 
  1620 lemma Lcm_in_lcm_closed_set_nat:
  1621   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
  1622 apply(induct rule:finite_linorder_min_induct)
  1623  apply simp
  1624 apply simp
  1625 apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
  1626  apply simp
  1627  apply(case_tac "A={}")
  1628   apply simp
  1629  apply simp
  1630 apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  1631 done
  1632 
  1633 lemma Lcm_eq_Max_nat:
  1634   "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"
  1635 apply(rule antisym)
  1636  apply(rule Max_ge, assumption)
  1637  apply(erule (2) Lcm_in_lcm_closed_set_nat)
  1638 apply clarsimp
  1639 apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
  1640 done
  1641 
  1642 lemma Lcm_set_nat [code, code_unfold]:
  1643   "Lcm (set ns) = fold lcm ns (1::nat)"
  1644   by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
  1645 
  1646 lemma Gcd_set_nat [code, code_unfold]:
  1647   "Gcd (set ns) = fold gcd ns (0::nat)"
  1648   by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
  1649 
  1650 lemma mult_inj_if_coprime_nat:
  1651   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
  1652    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
  1653 apply(auto simp add:inj_on_def)
  1654 apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
  1655 apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
  1656              dvd.neq_le_trans dvd_triv_right mult.commute)
  1657 done
  1658 
  1659 text{* Nitpick: *}
  1660 
  1661 lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
  1662 by (induct x y rule: nat_gcd.induct)
  1663    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  1664 
  1665 lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
  1666 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  1667 
  1668 
  1669 subsubsection {* Setwise gcd and lcm for integers *}
  1670 
  1671 instantiation int :: Gcd
  1672 begin
  1673 
  1674 definition
  1675   "Lcm M = int (Lcm (nat ` abs ` M))"
  1676 
  1677 definition
  1678   "Gcd M = int (Gcd (nat ` abs ` M))"
  1679 
  1680 instance ..
  1681 end
  1682 
  1683 lemma Lcm_empty_int [simp]: "Lcm {} = (1::int)"
  1684   by (simp add: Lcm_int_def)
  1685 
  1686 lemma Lcm_insert_int [simp]:
  1687   shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
  1688   by (simp add: Lcm_int_def lcm_int_def)
  1689 
  1690 lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat (abs x) dvd nat (abs y)"
  1691   by (simp add: zdvd_int)
  1692 
  1693 lemma dvd_Lcm_int [simp]:
  1694   fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
  1695   using assms by (simp add: Lcm_int_def dvd_int_iff)
  1696 
  1697 lemma Lcm_dvd_int [simp]:
  1698   fixes M :: "int set"
  1699   assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
  1700   using assms by (simp add: Lcm_int_def dvd_int_iff)
  1701 
  1702 instance int :: semiring_Gcd
  1703   by intro_classes (simp_all add: Gcd_int_def gcd_int_def dvd_int_iff Gcd_dvd dvd_Gcd)
  1704   
  1705 lemma Lcm_set_int [code, code_unfold]:
  1706   "Lcm (set xs) = fold lcm xs (1::int)"
  1707   by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
  1708 
  1709 lemma Gcd_set_int [code, code_unfold]:
  1710   "Gcd (set xs) = fold gcd xs (0::int)"
  1711   by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
  1712 
  1713 
  1714 text \<open>Fact aliasses\<close>
  1715 
  1716 lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
  1717   and gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
  1718   and gcd_greatest_nat = gcd_greatest [where ?'a = nat]
  1719 
  1720 lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
  1721   and gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
  1722   and gcd_greatest_int = gcd_greatest [where ?'a = int]
  1723 
  1724 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
  1725   and dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
  1726 
  1727 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
  1728   and dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
  1729 
  1730 lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
  1731   and Gcd_insert_nat = Gcd_insert [where ?'a = nat]
  1732 
  1733 lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
  1734   and Gcd_insert_int = Gcd_insert [where ?'a = int]
  1735 
  1736 end