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