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