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