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