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