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