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