src/HOL/GCD.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 37770 cddb3106adb8
child 41550 efa734d9b221
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     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 
    40 fixes
    41   gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
    42   lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    43 
    44 begin
    45 
    46 abbreviation
    47   coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    48 where
    49   "coprime x y == (gcd x y = 1)"
    50 
    51 end
    52 
    53 instantiation nat :: gcd
    54 begin
    55 
    56 fun
    57   gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    58 where
    59   "gcd_nat x y =
    60    (if y = 0 then x else gcd y (x mod y))"
    61 
    62 definition
    63   lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    64 where
    65   "lcm_nat x y = x * y div (gcd x y)"
    66 
    67 instance proof qed
    68 
    69 end
    70 
    71 instantiation int :: gcd
    72 begin
    73 
    74 definition
    75   gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
    76 where
    77   "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
    78 
    79 definition
    80   lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
    81 where
    82   "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
    83 
    84 instance proof qed
    85 
    86 end
    87 
    88 
    89 subsection {* Transfer setup *}
    90 
    91 lemma transfer_nat_int_gcd:
    92   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
    93   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
    94   unfolding gcd_int_def lcm_int_def
    95   by auto
    96 
    97 lemma transfer_nat_int_gcd_closures:
    98   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
    99   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   100   by (auto simp add: gcd_int_def lcm_int_def)
   101 
   102 declare transfer_morphism_nat_int[transfer add return:
   103     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   104 
   105 lemma transfer_int_nat_gcd:
   106   "gcd (int x) (int y) = int (gcd x y)"
   107   "lcm (int x) (int y) = int (lcm x y)"
   108   by (unfold gcd_int_def lcm_int_def, auto)
   109 
   110 lemma transfer_int_nat_gcd_closures:
   111   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   112   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   113   by (auto simp add: gcd_int_def lcm_int_def)
   114 
   115 declare transfer_morphism_int_nat[transfer add return:
   116     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   117 
   118 
   119 subsection {* GCD properties *}
   120 
   121 (* was gcd_induct *)
   122 lemma gcd_nat_induct:
   123   fixes m n :: nat
   124   assumes "\<And>m. P m 0"
   125     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   126   shows "P m n"
   127   apply (rule gcd_nat.induct)
   128   apply (case_tac "y = 0")
   129   using assms apply simp_all
   130 done
   131 
   132 (* specific to int *)
   133 
   134 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
   135   by (simp add: gcd_int_def)
   136 
   137 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
   138   by (simp add: gcd_int_def)
   139 
   140 lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
   141 by(simp add: gcd_int_def)
   142 
   143 lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"
   144 by (simp add: gcd_int_def)
   145 
   146 lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
   147 by (metis abs_idempotent gcd_abs_int)
   148 
   149 lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
   150 by (metis abs_idempotent gcd_abs_int)
   151 
   152 lemma gcd_cases_int:
   153   fixes x :: int and y
   154   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   155       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   156       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   157       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   158   shows "P (gcd x y)"
   159 by (insert assms, auto, arith)
   160 
   161 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   162   by (simp add: gcd_int_def)
   163 
   164 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
   165   by (simp add: lcm_int_def)
   166 
   167 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
   168   by (simp add: lcm_int_def)
   169 
   170 lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"
   171   by (simp add: lcm_int_def)
   172 
   173 lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
   174 by(simp add:lcm_int_def)
   175 
   176 lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
   177 by (metis abs_idempotent lcm_int_def)
   178 
   179 lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
   180 by (metis abs_idempotent lcm_int_def)
   181 
   182 lemma lcm_cases_int:
   183   fixes x :: int and y
   184   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   185       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   186       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   187       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   188   shows "P (lcm x y)"
   189 by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith)
   190 
   191 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   192   by (simp add: lcm_int_def)
   193 
   194 (* was gcd_0, etc. *)
   195 lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
   196   by simp
   197 
   198 (* was igcd_0, etc. *)
   199 lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
   200   by (unfold gcd_int_def, auto)
   201 
   202 lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
   203   by simp
   204 
   205 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
   206   by (unfold gcd_int_def, auto)
   207 
   208 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
   209   by (case_tac "y = 0", auto)
   210 
   211 (* weaker, but useful for the simplifier *)
   212 
   213 lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   214   by simp
   215 
   216 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   217   by simp
   218 
   219 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   220   by (simp add: One_nat_def)
   221 
   222 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   223   by (simp add: gcd_int_def)
   224 
   225 lemma gcd_idem_nat: "gcd (x::nat) x = x"
   226 by simp
   227 
   228 lemma gcd_idem_int: "gcd (x::int) x = abs x"
   229 by (auto simp add: gcd_int_def)
   230 
   231 declare gcd_nat.simps [simp del]
   232 
   233 text {*
   234   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   235   conjunctions don't seem provable separately.
   236 *}
   237 
   238 lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
   239   and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
   240   apply (induct m n rule: gcd_nat_induct)
   241   apply (simp_all add: gcd_non_0_nat)
   242   apply (blast dest: dvd_mod_imp_dvd)
   243 done
   244 
   245 lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"
   246 by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)
   247 
   248 lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"
   249 by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)
   250 
   251 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   252 by(metis gcd_dvd1_nat dvd_trans)
   253 
   254 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   255 by(metis gcd_dvd2_nat dvd_trans)
   256 
   257 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   258 by(metis gcd_dvd1_int dvd_trans)
   259 
   260 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   261 by(metis gcd_dvd2_int dvd_trans)
   262 
   263 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   264   by (rule dvd_imp_le, auto)
   265 
   266 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   267   by (rule dvd_imp_le, auto)
   268 
   269 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   270   by (rule zdvd_imp_le, auto)
   271 
   272 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   273   by (rule zdvd_imp_le, auto)
   274 
   275 lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   276 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
   277 
   278 lemma gcd_greatest_int:
   279   "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   280   apply (subst gcd_abs_int)
   281   apply (subst abs_dvd_iff [symmetric])
   282   apply (rule gcd_greatest_nat [transferred])
   283   apply auto
   284 done
   285 
   286 lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
   287     (k dvd m & k dvd n)"
   288   by (blast intro!: gcd_greatest_nat intro: dvd_trans)
   289 
   290 lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   291   by (blast intro!: gcd_greatest_int intro: dvd_trans)
   292 
   293 lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   294   by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
   295 
   296 lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   297   by (auto simp add: gcd_int_def)
   298 
   299 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   300   by (insert gcd_zero_nat [of m n], arith)
   301 
   302 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   303   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
   304 
   305 interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
   306 proof
   307 qed (auto intro: dvd_antisym dvd_trans)
   308 
   309 interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
   310 proof
   311 qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
   312 
   313 lemmas gcd_assoc_nat = gcd_nat.assoc
   314 lemmas gcd_commute_nat = gcd_nat.commute
   315 lemmas gcd_left_commute_nat = gcd_nat.left_commute
   316 lemmas gcd_assoc_int = gcd_int.assoc
   317 lemmas gcd_commute_int = gcd_int.commute
   318 lemmas gcd_left_commute_int = gcd_int.left_commute
   319 
   320 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
   321 
   322 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
   323 
   324 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
   325     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   326   apply auto
   327   apply (rule dvd_antisym)
   328   apply (erule (1) gcd_greatest_nat)
   329   apply auto
   330 done
   331 
   332 lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   333     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   334 apply (case_tac "d = 0")
   335  apply simp
   336 apply (rule iffI)
   337  apply (rule zdvd_antisym_nonneg)
   338  apply (auto intro: gcd_greatest_int)
   339 done
   340 
   341 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   342 by (metis dvd.eq_iff gcd_unique_nat)
   343 
   344 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   345 by (metis dvd.eq_iff gcd_unique_nat)
   346 
   347 lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   348 by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
   349 
   350 lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   351 by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   352 
   353 
   354 text {*
   355   \medskip Multiplication laws
   356 *}
   357 
   358 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   359     -- {* \cite[page 27]{davenport92} *}
   360   apply (induct m n rule: gcd_nat_induct)
   361   apply simp
   362   apply (case_tac "k = 0")
   363   apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
   364 done
   365 
   366 lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   367   apply (subst (1 2) gcd_abs_int)
   368   apply (subst (1 2) abs_mult)
   369   apply (rule gcd_mult_distrib_nat [transferred])
   370   apply auto
   371 done
   372 
   373 lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   374   apply (insert gcd_mult_distrib_nat [of m k n])
   375   apply simp
   376   apply (erule_tac t = m in ssubst)
   377   apply simp
   378   done
   379 
   380 lemma coprime_dvd_mult_int:
   381   "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   382 apply (subst abs_dvd_iff [symmetric])
   383 apply (subst dvd_abs_iff [symmetric])
   384 apply (subst (asm) gcd_abs_int)
   385 apply (rule coprime_dvd_mult_nat [transferred])
   386     prefer 4 apply assumption
   387    apply auto
   388 apply (subst abs_mult [symmetric], auto)
   389 done
   390 
   391 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   392     (k dvd m * n) = (k dvd m)"
   393   by (auto intro: coprime_dvd_mult_nat)
   394 
   395 lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   396     (k dvd m * n) = (k dvd m)"
   397   by (auto intro: coprime_dvd_mult_int)
   398 
   399 lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   400   apply (rule dvd_antisym)
   401   apply (rule gcd_greatest_nat)
   402   apply (rule_tac n = k in coprime_dvd_mult_nat)
   403   apply (simp add: gcd_assoc_nat)
   404   apply (simp add: gcd_commute_nat)
   405   apply (simp_all add: mult_commute)
   406 done
   407 
   408 lemma gcd_mult_cancel_int:
   409   "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
   410 apply (subst (1 2) gcd_abs_int)
   411 apply (subst abs_mult)
   412 apply (rule gcd_mult_cancel_nat [transferred], auto)
   413 done
   414 
   415 lemma coprime_crossproduct_nat:
   416   fixes a b c d :: nat
   417   assumes "coprime a d" and "coprime b c"
   418   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" (is "?lhs \<longleftrightarrow> ?rhs")
   419 proof
   420   assume ?rhs then show ?lhs by simp
   421 next
   422   assume ?lhs
   423   from `?lhs` have "a dvd b * d" by (auto intro: dvdI dest: sym)
   424   with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
   425   from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym)
   426   with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
   427   from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult_commute)
   428   with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
   429   from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult_commute)
   430   with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
   431   from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym)
   432   moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym)
   433   ultimately show ?rhs ..
   434 qed
   435 
   436 lemma coprime_crossproduct_int:
   437   fixes a b c d :: int
   438   assumes "coprime a d" and "coprime b c"
   439   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>"
   440   using assms by (intro coprime_crossproduct_nat [transferred]) auto
   441 
   442 text {* \medskip Addition laws *}
   443 
   444 lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   445   apply (case_tac "n = 0")
   446   apply (simp_all add: gcd_non_0_nat)
   447 done
   448 
   449 lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   450   apply (subst (1 2) gcd_commute_nat)
   451   apply (subst add_commute)
   452   apply simp
   453 done
   454 
   455 (* to do: add the other variations? *)
   456 
   457 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   458   by (subst gcd_add1_nat [symmetric], auto)
   459 
   460 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   461   apply (subst gcd_commute_nat)
   462   apply (subst gcd_diff1_nat [symmetric])
   463   apply auto
   464   apply (subst gcd_commute_nat)
   465   apply (subst gcd_diff1_nat)
   466   apply assumption
   467   apply (rule gcd_commute_nat)
   468 done
   469 
   470 lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   471   apply (frule_tac b = y and a = x in pos_mod_sign)
   472   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   473   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
   474     zmod_zminus1_eq_if)
   475   apply (frule_tac a = x in pos_mod_bound)
   476   apply (subst (1 2) gcd_commute_nat)
   477   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   478     nat_le_eq_zle)
   479 done
   480 
   481 lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
   482   apply (case_tac "y = 0")
   483   apply force
   484   apply (case_tac "y > 0")
   485   apply (subst gcd_non_0_int, auto)
   486   apply (insert gcd_non_0_int [of "-y" "-x"])
   487   apply auto
   488 done
   489 
   490 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
   491 by (metis gcd_red_int mod_add_self1 zadd_commute)
   492 
   493 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   494 by (metis gcd_add1_int gcd_commute_int zadd_commute)
   495 
   496 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   497 by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
   498 
   499 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   500 by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
   501 
   502 
   503 (* to do: differences, and all variations of addition rules
   504     as simplification rules for nat and int *)
   505 
   506 (* FIXME remove iff *)
   507 lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n"
   508   using mult_dvd_mono [of 1] by auto
   509 
   510 (* to do: add the three variations of these, and for ints? *)
   511 
   512 lemma finite_divisors_nat[simp]:
   513   assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
   514 proof-
   515   have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
   516   from finite_subset[OF _ this] show ?thesis using assms
   517     by(bestsimp intro!:dvd_imp_le)
   518 qed
   519 
   520 lemma finite_divisors_int[simp]:
   521   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
   522 proof-
   523   have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
   524   hence "finite{d. abs d <= abs i}" by simp
   525   from finite_subset[OF _ this] show ?thesis using assms
   526     by(bestsimp intro!:dvd_imp_le_int)
   527 qed
   528 
   529 lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
   530 apply(rule antisym)
   531  apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
   532 apply simp
   533 done
   534 
   535 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
   536 apply(rule antisym)
   537  apply(rule Max_le_iff[THEN iffD2])
   538    apply simp
   539   apply fastsimp
   540  apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
   541 apply simp
   542 done
   543 
   544 lemma gcd_is_Max_divisors_nat:
   545   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
   546 apply(rule Max_eqI[THEN sym])
   547   apply (metis finite_Collect_conjI finite_divisors_nat)
   548  apply simp
   549  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
   550 apply simp
   551 done
   552 
   553 lemma gcd_is_Max_divisors_int:
   554   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
   555 apply(rule Max_eqI[THEN sym])
   556   apply (metis finite_Collect_conjI finite_divisors_int)
   557  apply simp
   558  apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
   559 apply simp
   560 done
   561 
   562 lemma gcd_code_int [code]:
   563   "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   564   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
   565 
   566 
   567 subsection {* Coprimality *}
   568 
   569 lemma div_gcd_coprime_nat:
   570   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   571   shows "coprime (a div gcd a b) (b div gcd a b)"
   572 proof -
   573   let ?g = "gcd a b"
   574   let ?a' = "a div ?g"
   575   let ?b' = "b div ?g"
   576   let ?g' = "gcd ?a' ?b'"
   577   have dvdg: "?g dvd a" "?g dvd b" by simp_all
   578   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   579   from dvdg dvdg' obtain ka kb ka' kb' where
   580       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   581     unfolding dvd_def by blast
   582   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   583     by simp_all
   584   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   585     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   586       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   587   have "?g \<noteq> 0" using nz by simp
   588   then have gp: "?g > 0" by arith
   589   from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
   590   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   591 qed
   592 
   593 lemma div_gcd_coprime_int:
   594   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   595   shows "coprime (a div gcd a b) (b div gcd a b)"
   596 apply (subst (1 2 3) gcd_abs_int)
   597 apply (subst (1 2) abs_div)
   598   apply simp
   599  apply simp
   600 apply(subst (1 2) abs_gcd_int)
   601 apply (rule div_gcd_coprime_nat [transferred])
   602 using nz apply (auto simp add: gcd_abs_int [symmetric])
   603 done
   604 
   605 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   606   using gcd_unique_nat[of 1 a b, simplified] by auto
   607 
   608 lemma coprime_Suc_0_nat:
   609     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   610   using coprime_nat by (simp add: One_nat_def)
   611 
   612 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
   613     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   614   using gcd_unique_int [of 1 a b]
   615   apply clarsimp
   616   apply (erule subst)
   617   apply (rule iffI)
   618   apply force
   619   apply (drule_tac x = "abs e" in exI)
   620   apply (case_tac "e >= 0")
   621   apply force
   622   apply force
   623 done
   624 
   625 lemma gcd_coprime_nat:
   626   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   627     b: "b = b' * gcd a b"
   628   shows    "coprime a' b'"
   629 
   630   apply (subgoal_tac "a' = a div gcd a b")
   631   apply (erule ssubst)
   632   apply (subgoal_tac "b' = b div gcd a b")
   633   apply (erule ssubst)
   634   apply (rule div_gcd_coprime_nat)
   635   using prems
   636   apply force
   637   apply (subst (1) b)
   638   using z apply force
   639   apply (subst (1) a)
   640   using z apply force
   641 done
   642 
   643 lemma gcd_coprime_int:
   644   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   645     b: "b = b' * gcd a b"
   646   shows    "coprime a' b'"
   647 
   648   apply (subgoal_tac "a' = a div gcd a b")
   649   apply (erule ssubst)
   650   apply (subgoal_tac "b' = b div gcd a b")
   651   apply (erule ssubst)
   652   apply (rule div_gcd_coprime_int)
   653   using prems
   654   apply force
   655   apply (subst (1) b)
   656   using z apply force
   657   apply (subst (1) a)
   658   using z apply force
   659 done
   660 
   661 lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   662     shows "coprime d (a * b)"
   663   apply (subst gcd_commute_nat)
   664   using da apply (subst gcd_mult_cancel_nat)
   665   apply (subst gcd_commute_nat, assumption)
   666   apply (subst gcd_commute_nat, rule db)
   667 done
   668 
   669 lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
   670     shows "coprime d (a * b)"
   671   apply (subst gcd_commute_int)
   672   using da apply (subst gcd_mult_cancel_int)
   673   apply (subst gcd_commute_int, assumption)
   674   apply (subst gcd_commute_int, rule db)
   675 done
   676 
   677 lemma coprime_lmult_nat:
   678   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   679 proof -
   680   have "gcd d a dvd gcd d (a * b)"
   681     by (rule gcd_greatest_nat, auto)
   682   with dab show ?thesis
   683     by auto
   684 qed
   685 
   686 lemma coprime_lmult_int:
   687   assumes "coprime (d::int) (a * b)" shows "coprime d a"
   688 proof -
   689   have "gcd d a dvd gcd d (a * b)"
   690     by (rule gcd_greatest_int, auto)
   691   with assms show ?thesis
   692     by auto
   693 qed
   694 
   695 lemma coprime_rmult_nat:
   696   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   697 proof -
   698   have "gcd d b dvd gcd d (a * b)"
   699     by (rule gcd_greatest_nat, auto intro: dvd_mult)
   700   with assms show ?thesis
   701     by auto
   702 qed
   703 
   704 lemma coprime_rmult_int:
   705   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   706 proof -
   707   have "gcd d b dvd gcd d (a * b)"
   708     by (rule gcd_greatest_int, auto intro: dvd_mult)
   709   with dab show ?thesis
   710     by auto
   711 qed
   712 
   713 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   714     coprime d a \<and>  coprime d b"
   715   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   716     coprime_mult_nat[of d a b]
   717   by blast
   718 
   719 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   720     coprime d a \<and>  coprime d b"
   721   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   722     coprime_mult_int[of d a b]
   723   by blast
   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 zadd_int [symmetric]
  1042         zmult_int [symmetric])
  1043       done
  1044 qed
  1045 
  1046 lemma bezout_int:
  1047   fixes x y
  1048   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1049 proof -
  1050   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1051       EX u v. u * x + v * y = gcd x y"
  1052     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1053     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1054     apply (unfold gcd_int_def)
  1055     apply simp
  1056     apply (subst bezw_aux [symmetric])
  1057     apply auto
  1058     done
  1059   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1060       (x \<le> 0 \<and> y \<le> 0)"
  1061     by auto
  1062   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1063     by (erule (1) bezout_aux)
  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_neg2_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 auto
  1079     done
  1080   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1081     apply (insert bezout_aux [of "-x" "-y"])
  1082     apply auto
  1083     apply (rule_tac x = "-u" in exI)
  1084     apply (rule_tac x = "-v" in exI)
  1085     apply (subst gcd_neg1_int [symmetric])
  1086     apply (subst gcd_neg2_int [symmetric])
  1087     apply auto
  1088     done
  1089   ultimately show ?thesis by blast
  1090 qed
  1091 
  1092 text {* versions of Bezout for nat, by Amine Chaieb *}
  1093 
  1094 lemma ind_euclid:
  1095   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1096   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1097   shows "P a b"
  1098 proof(induct "a + b" arbitrary: a b rule: less_induct)
  1099   case less
  1100   have "a = b \<or> a < b \<or> b < a" by arith
  1101   moreover {assume eq: "a= b"
  1102     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1103     by simp}
  1104   moreover
  1105   {assume lt: "a < b"
  1106     hence "a + b - a < a + b \<or> a = 0" by arith
  1107     moreover
  1108     {assume "a =0" with z c have "P a b" by blast }
  1109     moreover
  1110     {assume "a + b - a < a + b"
  1111       also have th0: "a + b - a = a + (b - a)" using lt by arith
  1112       finally have "a + (b - a) < a + b" .
  1113       then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
  1114       then have "P a b" by (simp add: th0[symmetric])}
  1115     ultimately have "P a b" by blast}
  1116   moreover
  1117   {assume lt: "a > b"
  1118     hence "b + a - b < a + b \<or> b = 0" by arith
  1119     moreover
  1120     {assume "b =0" with z c have "P a b" by blast }
  1121     moreover
  1122     {assume "b + a - b < a + b"
  1123       also have th0: "b + a - b = b + (a - b)" using lt by arith
  1124       finally have "b + (a - b) < a + b" .
  1125       then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
  1126       then have "P b a" by (simp add: th0[symmetric])
  1127       hence "P a b" using c by blast }
  1128     ultimately have "P a b" by blast}
  1129 ultimately  show "P a b" by blast
  1130 qed
  1131 
  1132 lemma bezout_lemma_nat:
  1133   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1134     (a * x = b * y + d \<or> b * x = a * y + d)"
  1135   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1136     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1137   using ex
  1138   apply clarsimp
  1139   apply (rule_tac x="d" in exI, simp)
  1140   apply (case_tac "a * x = b * y + d" , simp_all)
  1141   apply (rule_tac x="x + y" in exI)
  1142   apply (rule_tac x="y" in exI)
  1143   apply algebra
  1144   apply (rule_tac x="x" in exI)
  1145   apply (rule_tac x="x + y" in exI)
  1146   apply algebra
  1147 done
  1148 
  1149 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1150     (a * x = b * y + d \<or> b * x = a * y + d)"
  1151   apply(induct a b rule: ind_euclid)
  1152   apply blast
  1153   apply clarify
  1154   apply (rule_tac x="a" in exI, simp)
  1155   apply clarsimp
  1156   apply (rule_tac x="d" in exI)
  1157   apply (case_tac "a * x = b * y + d", simp_all)
  1158   apply (rule_tac x="x+y" in exI)
  1159   apply (rule_tac x="y" in exI)
  1160   apply algebra
  1161   apply (rule_tac x="x" in exI)
  1162   apply (rule_tac x="x+y" in exI)
  1163   apply algebra
  1164 done
  1165 
  1166 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1167     (a * x - b * y = d \<or> b * x - a * y = d)"
  1168   using bezout_add_nat[of a b]
  1169   apply clarsimp
  1170   apply (rule_tac x="d" in exI, simp)
  1171   apply (rule_tac x="x" in exI)
  1172   apply (rule_tac x="y" in exI)
  1173   apply auto
  1174 done
  1175 
  1176 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1177   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1178 proof-
  1179  from nz have ap: "a > 0" by simp
  1180  from bezout_add_nat[of a b]
  1181  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1182    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1183  moreover
  1184     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1185      from H have ?thesis by blast }
  1186  moreover
  1187  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1188    {assume b0: "b = 0" with H  have ?thesis by simp}
  1189    moreover
  1190    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1191      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1192        by auto
  1193      moreover
  1194      {assume db: "d=b"
  1195        from prems have ?thesis apply simp
  1196          apply (rule exI[where x = b], simp)
  1197          apply (rule exI[where x = b])
  1198         by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1199     moreover
  1200     {assume db: "d < b"
  1201         {assume "x=0" hence ?thesis  using prems by simp }
  1202         moreover
  1203         {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1204           from db have "d \<le> b - 1" by simp
  1205           hence "d*b \<le> b*(b - 1)" by simp
  1206           with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1207           have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1208           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1209             by simp
  1210           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1211             by (simp only: mult_assoc right_distrib)
  1212           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1213             by algebra
  1214           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1215           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1216             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1217           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1218             by (simp only: diff_mult_distrib2 add_commute mult_ac)
  1219           hence ?thesis using H(1,2)
  1220             apply -
  1221             apply (rule exI[where x=d], simp)
  1222             apply (rule exI[where x="(b - 1) * y"])
  1223             by (rule exI[where x="x*(b - 1) - d"], simp)}
  1224         ultimately have ?thesis by blast}
  1225     ultimately have ?thesis by blast}
  1226   ultimately have ?thesis by blast}
  1227  ultimately show ?thesis by blast
  1228 qed
  1229 
  1230 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1231   shows "\<exists>x y. a * x = b * y + gcd a b"
  1232 proof-
  1233   let ?g = "gcd a b"
  1234   from bezout_add_strong_nat[OF a, of b]
  1235   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1236   from d(1,2) have "d dvd ?g" by simp
  1237   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1238   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1239   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1240   thus ?thesis by blast
  1241 qed
  1242 
  1243 
  1244 subsection {* LCM properties *}
  1245 
  1246 lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1247   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1248     zmult_int [symmetric] gcd_int_def)
  1249 
  1250 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1251   unfolding lcm_nat_def
  1252   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1253 
  1254 lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
  1255   unfolding lcm_int_def gcd_int_def
  1256   apply (subst int_mult [symmetric])
  1257   apply (subst prod_gcd_lcm_nat [symmetric])
  1258   apply (subst nat_abs_mult_distrib [symmetric])
  1259   apply (simp, simp add: abs_mult)
  1260 done
  1261 
  1262 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1263   unfolding lcm_nat_def by simp
  1264 
  1265 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1266   unfolding lcm_int_def by simp
  1267 
  1268 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1269   unfolding lcm_nat_def by simp
  1270 
  1271 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1272   unfolding lcm_int_def by simp
  1273 
  1274 lemma lcm_pos_nat:
  1275   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1276 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1277 
  1278 lemma lcm_pos_int:
  1279   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1280   apply (subst lcm_abs_int)
  1281   apply (rule lcm_pos_nat [transferred])
  1282   apply auto
  1283 done
  1284 
  1285 lemma dvd_pos_nat:
  1286   fixes n m :: nat
  1287   assumes "n > 0" and "m dvd n"
  1288   shows "m > 0"
  1289 using assms by (cases m) auto
  1290 
  1291 lemma lcm_least_nat:
  1292   assumes "(m::nat) dvd k" and "n dvd k"
  1293   shows "lcm m n dvd k"
  1294 proof (cases k)
  1295   case 0 then show ?thesis by auto
  1296 next
  1297   case (Suc _) then have pos_k: "k > 0" by auto
  1298   from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1299   with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
  1300   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1301   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1302   from pos_k k_m have pos_p: "p > 0" by auto
  1303   from pos_k k_n have pos_q: "q > 0" by auto
  1304   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1305     by (simp add: mult_ac gcd_mult_distrib_nat)
  1306   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1307     by (simp add: k_m [symmetric] k_n [symmetric])
  1308   also have "\<dots> = k * p * q * gcd m n"
  1309     by (simp add: mult_ac gcd_mult_distrib_nat)
  1310   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1311     by (simp only: k_m [symmetric] k_n [symmetric])
  1312   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1313     by (simp add: mult_ac)
  1314   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1315     by simp
  1316   with prod_gcd_lcm_nat [of m n]
  1317   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1318     by (simp add: mult_ac)
  1319   with pos_gcd have "lcm m n * gcd q p = k" by auto
  1320   then show ?thesis using dvd_def by auto
  1321 qed
  1322 
  1323 lemma lcm_least_int:
  1324   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1325 apply (subst lcm_abs_int)
  1326 apply (rule dvd_trans)
  1327 apply (rule lcm_least_nat [transferred, of _ "abs k" _])
  1328 apply auto
  1329 done
  1330 
  1331 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
  1332 proof (cases m)
  1333   case 0 then show ?thesis by simp
  1334 next
  1335   case (Suc _)
  1336   then have mpos: "m > 0" by simp
  1337   show ?thesis
  1338   proof (cases n)
  1339     case 0 then show ?thesis by simp
  1340   next
  1341     case (Suc _)
  1342     then have npos: "n > 0" by simp
  1343     have "gcd m n dvd n" by simp
  1344     then obtain k where "n = gcd m n * k" using dvd_def by auto
  1345     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1346       by (simp add: mult_ac)
  1347     also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
  1348     finally show ?thesis by (simp add: lcm_nat_def)
  1349   qed
  1350 qed
  1351 
  1352 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1353   apply (subst lcm_abs_int)
  1354   apply (rule dvd_trans)
  1355   prefer 2
  1356   apply (rule lcm_dvd1_nat [transferred])
  1357   apply auto
  1358 done
  1359 
  1360 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1361   using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def mult.commute gcd_nat.commute)
  1362 
  1363 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1364   using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def mult.commute gcd_nat.commute)
  1365 
  1366 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1367 by(metis lcm_dvd1_nat dvd_trans)
  1368 
  1369 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1370 by(metis lcm_dvd2_nat dvd_trans)
  1371 
  1372 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1373 by(metis lcm_dvd1_int dvd_trans)
  1374 
  1375 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1376 by(metis lcm_dvd2_int dvd_trans)
  1377 
  1378 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1379     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1380   by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1381 
  1382 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1383     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1384   by (auto intro: dvd_antisym [transferred] lcm_least_int)
  1385 
  1386 interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
  1387 proof
  1388   fix n m p :: nat
  1389   show "lcm (lcm n m) p = lcm n (lcm m p)"
  1390     by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
  1391   show "lcm m n = lcm n m"
  1392     by (simp add: lcm_nat_def gcd_commute_nat field_simps)
  1393 qed
  1394 
  1395 interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
  1396 proof
  1397   fix n m p :: int
  1398   show "lcm (lcm n m) p = lcm n (lcm m p)"
  1399     by (rule lcm_unique_int [THEN iffD1]) (metis dvd_trans lcm_unique_int)
  1400   show "lcm m n = lcm n m"
  1401     by (simp add: lcm_int_def lcm_nat.commute)
  1402 qed
  1403 
  1404 lemmas lcm_assoc_nat = lcm_nat.assoc
  1405 lemmas lcm_commute_nat = lcm_nat.commute
  1406 lemmas lcm_left_commute_nat = lcm_nat.left_commute
  1407 lemmas lcm_assoc_int = lcm_int.assoc
  1408 lemmas lcm_commute_int = lcm_int.commute
  1409 lemmas lcm_left_commute_int = lcm_int.left_commute
  1410 
  1411 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1412 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1413 
  1414 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1415   apply (rule sym)
  1416   apply (subst lcm_unique_nat [symmetric])
  1417   apply auto
  1418 done
  1419 
  1420 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1421   apply (rule sym)
  1422   apply (subst lcm_unique_int [symmetric])
  1423   apply auto
  1424 done
  1425 
  1426 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1427 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
  1428 
  1429 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1430 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1431 
  1432 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1433 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1434 
  1435 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1436 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1437 
  1438 lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
  1439 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1440 
  1441 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
  1442 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1443 
  1444 lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1445 proof qed (auto simp add: gcd_ac_nat)
  1446 
  1447 lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  1448 proof qed (auto simp add: gcd_ac_int)
  1449 
  1450 lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1451 proof qed (auto simp add: lcm_ac_nat)
  1452 
  1453 lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  1454 proof qed (auto simp add: lcm_ac_int)
  1455 
  1456 
  1457 (* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
  1458 
  1459 lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1460 by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
  1461 
  1462 lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1463 by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
  1464 
  1465 lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
  1466 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
  1467 
  1468 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  1469 by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
  1470 
  1471 
  1472 subsubsection {* The complete divisibility lattice *}
  1473 
  1474 
  1475 interpretation gcd_semilattice_nat: semilattice_inf "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
  1476 proof
  1477   case goal3 thus ?case by(metis gcd_unique_nat)
  1478 qed auto
  1479 
  1480 interpretation lcm_semilattice_nat: semilattice_sup "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
  1481 proof
  1482   case goal3 thus ?case by(metis lcm_unique_nat)
  1483 qed auto
  1484 
  1485 interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
  1486 
  1487 text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
  1488 GCD is defined via LCM to facilitate the proof that we have a complete lattice.
  1489 Later on we show that GCD and Gcd coincide on finite sets.
  1490 *}
  1491 context gcd
  1492 begin
  1493 
  1494 definition Gcd :: "'a set \<Rightarrow> 'a"
  1495 where "Gcd = fold gcd 0"
  1496 
  1497 definition Lcm :: "'a set \<Rightarrow> 'a"
  1498 where "Lcm = fold lcm 1"
  1499 
  1500 definition LCM :: "'a set \<Rightarrow> 'a" where
  1501 "LCM M = (if finite M then Lcm M else 0)"
  1502 
  1503 definition GCD :: "'a set \<Rightarrow> 'a" where
  1504 "GCD M = LCM(INT m:M. {d. d dvd m})"
  1505 
  1506 end
  1507 
  1508 lemma Gcd_empty[simp]: "Gcd {} = 0"
  1509 by(simp add:Gcd_def)
  1510 
  1511 lemma Lcm_empty[simp]: "Lcm {} = 1"
  1512 by(simp add:Lcm_def)
  1513 
  1514 lemma GCD_empty_nat[simp]: "GCD {} = (0::nat)"
  1515 by(simp add:GCD_def LCM_def)
  1516 
  1517 lemma LCM_eq_Lcm[simp]: "finite M \<Longrightarrow> LCM M = Lcm M"
  1518 by(simp add:LCM_def)
  1519 
  1520 lemma Lcm_insert_nat [simp]:
  1521   assumes "finite N"
  1522   shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
  1523 proof -
  1524   interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
  1525     by (rule fun_left_comm_idem_lcm_nat)
  1526   from assms show ?thesis by(simp add: Lcm_def)
  1527 qed
  1528 
  1529 lemma Lcm_insert_int [simp]:
  1530   assumes "finite N"
  1531   shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
  1532 proof -
  1533   interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
  1534     by (rule fun_left_comm_idem_lcm_int)
  1535   from assms show ?thesis by(simp add: Lcm_def)
  1536 qed
  1537 
  1538 lemma Gcd_insert_nat [simp]:
  1539   assumes "finite N"
  1540   shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
  1541 proof -
  1542   interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
  1543     by (rule fun_left_comm_idem_gcd_nat)
  1544   from assms show ?thesis by(simp add: Gcd_def)
  1545 qed
  1546 
  1547 lemma Gcd_insert_int [simp]:
  1548   assumes "finite N"
  1549   shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
  1550 proof -
  1551   interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
  1552     by (rule fun_left_comm_idem_gcd_int)
  1553   from assms show ?thesis by(simp add: Gcd_def)
  1554 qed
  1555 
  1556 lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
  1557 by(induct rule:finite_ne_induct) auto
  1558 
  1559 lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
  1560 by (metis Lcm0_iff empty_iff)
  1561 
  1562 lemma Gcd_dvd_nat [simp]:
  1563   assumes "finite M" and "(m::nat) \<in> M"
  1564   shows "Gcd M dvd m"
  1565 proof -
  1566   show ?thesis using gcd_semilattice_nat.fold_inf_le_inf[OF assms, of 0] by (simp add: Gcd_def)
  1567 qed
  1568 
  1569 lemma dvd_Gcd_nat[simp]:
  1570   assumes "finite M" and "ALL (m::nat) : M. n dvd m"
  1571   shows "n dvd Gcd M"
  1572 proof -
  1573   show ?thesis using gcd_semilattice_nat.inf_le_fold_inf[OF assms, of 0] by (simp add: Gcd_def)
  1574 qed
  1575 
  1576 lemma dvd_Lcm_nat [simp]:
  1577   assumes "finite M" and "(m::nat) \<in> M"
  1578   shows "m dvd Lcm M"
  1579 proof -
  1580   show ?thesis using lcm_semilattice_nat.sup_le_fold_sup[OF assms, of 1] by (simp add: Lcm_def)
  1581 qed
  1582 
  1583 lemma Lcm_dvd_nat[simp]:
  1584   assumes "finite M" and "ALL (m::nat) : M. m dvd n"
  1585   shows "Lcm M dvd n"
  1586 proof -
  1587   show ?thesis using lcm_semilattice_nat.fold_sup_le_sup[OF assms, of 1] by (simp add: Lcm_def)
  1588 qed
  1589 
  1590 interpretation gcd_lcm_complete_lattice_nat:
  1591   complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
  1592 proof
  1593   case goal1 show ?case by simp
  1594 next
  1595   case goal2 show ?case by simp
  1596 next
  1597   case goal5 thus ?case by (auto simp: LCM_def)
  1598 next
  1599   case goal6 thus ?case
  1600     by(auto simp: LCM_def)(metis finite_nat_set_iff_bounded_le gcd_proj2_if_dvd_nat gcd_le1_nat)
  1601 next
  1602   case goal3 thus ?case by (auto simp: GCD_def LCM_def)(metis finite_INT finite_divisors_nat)
  1603 next
  1604   case goal4 thus ?case by(auto simp: LCM_def GCD_def)
  1605 qed
  1606 
  1607 text{* Alternative characterizations of Gcd and GCD: *}
  1608 
  1609 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})"
  1610 apply(rule antisym)
  1611  apply(rule Max_ge)
  1612   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1613  apply simp
  1614 apply (rule Max_le_iff[THEN iffD2])
  1615   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1616  apply fastsimp
  1617 apply clarsimp
  1618 apply (metis Gcd_dvd_nat Max_in dvd_0_left dvd_Gcd_nat dvd_imp_le linorder_antisym_conv3 not_less0)
  1619 done
  1620 
  1621 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
  1622 apply(induct pred:finite)
  1623  apply simp
  1624 apply(case_tac "x=0")
  1625  apply simp
  1626 apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
  1627  apply simp
  1628 apply blast
  1629 done
  1630 
  1631 lemma Lcm_in_lcm_closed_set_nat:
  1632   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
  1633 apply(induct rule:finite_linorder_min_induct)
  1634  apply simp
  1635 apply simp
  1636 apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
  1637  apply simp
  1638  apply(case_tac "A={}")
  1639   apply simp
  1640  apply simp
  1641 apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  1642 done
  1643 
  1644 lemma Lcm_eq_Max_nat:
  1645   "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"
  1646 apply(rule antisym)
  1647  apply(rule Max_ge, assumption)
  1648  apply(erule (2) Lcm_in_lcm_closed_set_nat)
  1649 apply clarsimp
  1650 apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
  1651 done
  1652 
  1653 text{* Finally GCD is Gcd: *}
  1654 
  1655 lemma GCD_eq_Gcd[simp]: assumes "finite(M::nat set)" shows "GCD M = Gcd M"
  1656 proof-
  1657   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
  1658   show ?thesis
  1659   proof cases
  1660     assume "M={}" thus ?thesis by simp
  1661   next
  1662     assume "M\<noteq>{}"
  1663     show ?thesis
  1664     proof cases
  1665       assume "M={0}" thus ?thesis by(simp add:GCD_def LCM_def)
  1666     next
  1667       assume "M\<noteq>{0}"
  1668       with `M\<noteq>{}` assms show ?thesis
  1669         apply(subst Gcd_remove0_nat[OF assms])
  1670         apply(simp add:GCD_def)
  1671         apply(subst divisors_remove0_nat)
  1672         apply(simp add:LCM_def)
  1673         apply rule
  1674          apply rule
  1675          apply(subst Gcd_eq_Max)
  1676             apply simp
  1677            apply blast
  1678           apply blast
  1679          apply(rule Lcm_eq_Max_nat)
  1680             apply simp
  1681            apply blast
  1682           apply fastsimp
  1683          apply clarsimp
  1684         apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
  1685         done
  1686     qed
  1687   qed
  1688 qed
  1689 
  1690 lemma Lcm_set_nat [code_unfold]:
  1691   "Lcm (set ns) = foldl lcm (1::nat) ns"
  1692 proof -
  1693   interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
  1694   show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
  1695 qed
  1696 
  1697 lemma Lcm_set_int [code_unfold]:
  1698   "Lcm (set is) = foldl lcm (1::int) is"
  1699 proof -
  1700   interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
  1701   show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
  1702 qed
  1703 
  1704 lemma Gcd_set_nat [code_unfold]:
  1705   "Gcd (set ns) = foldl gcd (0::nat) ns"
  1706 proof -
  1707   interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
  1708   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
  1709 qed
  1710 
  1711 lemma Gcd_set_int [code_unfold]:
  1712   "Gcd (set ns) = foldl gcd (0::int) ns"
  1713 proof -
  1714   interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
  1715   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
  1716 qed
  1717 
  1718 
  1719 lemma mult_inj_if_coprime_nat:
  1720   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
  1721    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
  1722 apply(auto simp add:inj_on_def)
  1723 apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
  1724 apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
  1725              dvd.neq_le_trans dvd_triv_right mult_commute)
  1726 done
  1727 
  1728 text{* Nitpick: *}
  1729 
  1730 lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
  1731 apply (rule eq_reflection)
  1732 apply (induct x y rule: nat_gcd.induct)
  1733 by (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  1734 
  1735 lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \<equiv> Nitpick.nat_lcm x y"
  1736 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  1737 
  1738 end