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