src/HOL/GCD.thy
author avigad
Fri Jul 10 10:45:30 2009 -0400 (2009-07-10)
changeset 32036 8a9228872fbd
parent 31952 40501bb2d57c
child 32040 830141c9e528
permissions -rw-r--r--
Moved factorial lemmas from Binomial.thy to Fact.thy and 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 = one +
    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:
   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:
   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 gcd_is_Max_divisors_nat:
   561   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
   562 apply(rule Max_eqI[THEN sym])
   563   apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat)
   564  apply simp
   565  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
   566 apply simp
   567 done
   568 
   569 lemma gcd_is_Max_divisors_int:
   570   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
   571 apply(rule Max_eqI[THEN sym])
   572   apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int)
   573  apply simp
   574  apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
   575 apply simp
   576 done
   577 
   578 
   579 subsection {* Coprimality *}
   580 
   581 lemma div_gcd_coprime_nat:
   582   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   583   shows "coprime (a div gcd a b) (b div gcd a b)"
   584 proof -
   585   let ?g = "gcd a b"
   586   let ?a' = "a div ?g"
   587   let ?b' = "b div ?g"
   588   let ?g' = "gcd ?a' ?b'"
   589   have dvdg: "?g dvd a" "?g dvd b" by simp_all
   590   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   591   from dvdg dvdg' obtain ka kb ka' kb' where
   592       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   593     unfolding dvd_def by blast
   594   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   595     by simp_all
   596   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   597     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   598       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   599   have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat)
   600   then have gp: "?g > 0" by arith
   601   from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
   602   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   603 qed
   604 
   605 lemma div_gcd_coprime_int:
   606   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   607   shows "coprime (a div gcd a b) (b div gcd a b)"
   608 apply (subst (1 2 3) gcd_abs_int)
   609 apply (subst (1 2) abs_div)
   610   apply simp
   611  apply simp
   612 apply(subst (1 2) abs_gcd_int)
   613 apply (rule div_gcd_coprime_nat [transferred])
   614 using nz apply (auto simp add: gcd_abs_int [symmetric])
   615 done
   616 
   617 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   618   using gcd_unique_nat[of 1 a b, simplified] by auto
   619 
   620 lemma coprime_Suc_0_nat:
   621     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   622   using coprime_nat by (simp add: One_nat_def)
   623 
   624 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
   625     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   626   using gcd_unique_int [of 1 a b]
   627   apply clarsimp
   628   apply (erule subst)
   629   apply (rule iffI)
   630   apply force
   631   apply (drule_tac x = "abs e" in exI)
   632   apply (case_tac "e >= 0")
   633   apply force
   634   apply force
   635 done
   636 
   637 lemma gcd_coprime_nat:
   638   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   639     b: "b = b' * gcd a b"
   640   shows    "coprime a' b'"
   641 
   642   apply (subgoal_tac "a' = a div gcd a b")
   643   apply (erule ssubst)
   644   apply (subgoal_tac "b' = b div gcd a b")
   645   apply (erule ssubst)
   646   apply (rule div_gcd_coprime_nat)
   647   using prems
   648   apply force
   649   apply (subst (1) b)
   650   using z apply force
   651   apply (subst (1) a)
   652   using z apply force
   653 done
   654 
   655 lemma gcd_coprime_int:
   656   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   657     b: "b = b' * gcd a b"
   658   shows    "coprime a' b'"
   659 
   660   apply (subgoal_tac "a' = a div gcd a b")
   661   apply (erule ssubst)
   662   apply (subgoal_tac "b' = b div gcd a b")
   663   apply (erule ssubst)
   664   apply (rule div_gcd_coprime_int)
   665   using prems
   666   apply force
   667   apply (subst (1) b)
   668   using z apply force
   669   apply (subst (1) a)
   670   using z apply force
   671 done
   672 
   673 lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   674     shows "coprime d (a * b)"
   675   apply (subst gcd_commute_nat)
   676   using da apply (subst gcd_mult_cancel_nat)
   677   apply (subst gcd_commute_nat, assumption)
   678   apply (subst gcd_commute_nat, rule db)
   679 done
   680 
   681 lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
   682     shows "coprime d (a * b)"
   683   apply (subst gcd_commute_int)
   684   using da apply (subst gcd_mult_cancel_int)
   685   apply (subst gcd_commute_int, assumption)
   686   apply (subst gcd_commute_int, rule db)
   687 done
   688 
   689 lemma coprime_lmult_nat:
   690   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   691 proof -
   692   have "gcd d a dvd gcd d (a * b)"
   693     by (rule gcd_greatest_nat, auto)
   694   with dab show ?thesis
   695     by auto
   696 qed
   697 
   698 lemma coprime_lmult_int:
   699   assumes "coprime (d::int) (a * b)" shows "coprime d a"
   700 proof -
   701   have "gcd d a dvd gcd d (a * b)"
   702     by (rule gcd_greatest_int, auto)
   703   with assms show ?thesis
   704     by auto
   705 qed
   706 
   707 lemma coprime_rmult_nat:
   708   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   709 proof -
   710   have "gcd d b dvd gcd d (a * b)"
   711     by (rule gcd_greatest_nat, auto intro: dvd_mult)
   712   with assms show ?thesis
   713     by auto
   714 qed
   715 
   716 lemma coprime_rmult_int:
   717   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   718 proof -
   719   have "gcd d b dvd gcd d (a * b)"
   720     by (rule gcd_greatest_int, auto intro: dvd_mult)
   721   with dab show ?thesis
   722     by auto
   723 qed
   724 
   725 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   726     coprime d a \<and>  coprime d b"
   727   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   728     coprime_mult_nat[of d a b]
   729   by blast
   730 
   731 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   732     coprime d a \<and>  coprime d b"
   733   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   734     coprime_mult_int[of d a b]
   735   by blast
   736 
   737 lemma gcd_coprime_exists_nat:
   738     assumes nz: "gcd (a::nat) b \<noteq> 0"
   739     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   740   apply (rule_tac x = "a div gcd a b" in exI)
   741   apply (rule_tac x = "b div gcd a b" in exI)
   742   using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)
   743 done
   744 
   745 lemma gcd_coprime_exists_int:
   746     assumes nz: "gcd (a::int) b \<noteq> 0"
   747     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   748   apply (rule_tac x = "a div gcd a b" in exI)
   749   apply (rule_tac x = "b div gcd a b" in exI)
   750   using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self)
   751 done
   752 
   753 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   754   by (induct n, simp_all add: coprime_mult_nat)
   755 
   756 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   757   by (induct n, simp_all add: coprime_mult_int)
   758 
   759 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   760   apply (rule coprime_exp_nat)
   761   apply (subst gcd_commute_nat)
   762   apply (rule coprime_exp_nat)
   763   apply (subst gcd_commute_nat, assumption)
   764 done
   765 
   766 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   767   apply (rule coprime_exp_int)
   768   apply (subst gcd_commute_int)
   769   apply (rule coprime_exp_int)
   770   apply (subst gcd_commute_int, assumption)
   771 done
   772 
   773 lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   774 proof (cases)
   775   assume "a = 0 & b = 0"
   776   thus ?thesis by simp
   777   next assume "~(a = 0 & b = 0)"
   778   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   779     by (auto simp:div_gcd_coprime_nat)
   780   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   781       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   782     apply (subst (1 2) mult_commute)
   783     apply (subst gcd_mult_distrib_nat [symmetric])
   784     apply simp
   785     done
   786   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   787     apply (subst div_power)
   788     apply auto
   789     apply (rule dvd_div_mult_self)
   790     apply (rule dvd_power_same)
   791     apply auto
   792     done
   793   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
   794     apply (subst div_power)
   795     apply auto
   796     apply (rule dvd_div_mult_self)
   797     apply (rule dvd_power_same)
   798     apply auto
   799     done
   800   finally show ?thesis .
   801 qed
   802 
   803 lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   804   apply (subst (1 2) gcd_abs_int)
   805   apply (subst (1 2) power_abs)
   806   apply (rule gcd_exp_nat [where n = n, transferred])
   807   apply auto
   808 done
   809 
   810 lemma coprime_divprod_nat: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   811   using coprime_dvd_mult_iff_nat[of d a b]
   812   by (auto simp add: mult_commute)
   813 
   814 lemma coprime_divprod_int: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   815   using coprime_dvd_mult_iff_int[of d a b]
   816   by (auto simp add: mult_commute)
   817 
   818 lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
   819   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   820 proof-
   821   let ?g = "gcd a b"
   822   {assume "?g = 0" with dc have ?thesis by auto}
   823   moreover
   824   {assume z: "?g \<noteq> 0"
   825     from gcd_coprime_exists_nat[OF z]
   826     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   827       by blast
   828     have thb: "?g dvd b" by auto
   829     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   830     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   831     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   832     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   833     with z have th_1: "a' dvd b' * c" by auto
   834     from coprime_dvd_mult_nat[OF ab'(3)] th_1
   835     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   836     from ab' have "a = ?g*a'" by algebra
   837     with thb thc have ?thesis by blast }
   838   ultimately show ?thesis by blast
   839 qed
   840 
   841 lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
   842   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   843 proof-
   844   let ?g = "gcd a b"
   845   {assume "?g = 0" with dc have ?thesis by auto}
   846   moreover
   847   {assume z: "?g \<noteq> 0"
   848     from gcd_coprime_exists_int[OF z]
   849     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   850       by blast
   851     have thb: "?g dvd b" by auto
   852     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   853     with dc have th0: "a' dvd b*c"
   854       using dvd_trans[of a' a "b*c"] by simp
   855     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   856     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   857     with z have th_1: "a' dvd b' * c" by auto
   858     from coprime_dvd_mult_int[OF ab'(3)] th_1
   859     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   860     from ab' have "a = ?g*a'" by algebra
   861     with thb thc have ?thesis by blast }
   862   ultimately show ?thesis by blast
   863 qed
   864 
   865 lemma pow_divides_pow_nat:
   866   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   867   shows "a dvd b"
   868 proof-
   869   let ?g = "gcd a b"
   870   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   871   {assume "?g = 0" with ab n have ?thesis by auto }
   872   moreover
   873   {assume z: "?g \<noteq> 0"
   874     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   875     from gcd_coprime_exists_nat[OF z]
   876     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   877       by blast
   878     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   879       by (simp add: ab'(1,2)[symmetric])
   880     hence "?g^n*a'^n dvd ?g^n *b'^n"
   881       by (simp only: power_mult_distrib mult_commute)
   882     with zn z n have th0:"a'^n dvd b'^n" by auto
   883     have "a' dvd a'^n" by (simp add: m)
   884     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   885     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   886     from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
   887     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   888     hence "a'*?g dvd b'*?g" by simp
   889     with ab'(1,2)  have ?thesis by simp }
   890   ultimately show ?thesis by blast
   891 qed
   892 
   893 lemma pow_divides_pow_int:
   894   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
   895   shows "a dvd b"
   896 proof-
   897   let ?g = "gcd a b"
   898   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   899   {assume "?g = 0" with ab n have ?thesis by auto }
   900   moreover
   901   {assume z: "?g \<noteq> 0"
   902     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   903     from gcd_coprime_exists_int[OF z]
   904     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   905       by blast
   906     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   907       by (simp add: ab'(1,2)[symmetric])
   908     hence "?g^n*a'^n dvd ?g^n *b'^n"
   909       by (simp only: power_mult_distrib mult_commute)
   910     with zn z n have th0:"a'^n dvd b'^n" by auto
   911     have "a' dvd a'^n" by (simp add: m)
   912     with th0 have "a' dvd b'^n"
   913       using dvd_trans[of a' "a'^n" "b'^n"] by simp
   914     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   915     from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
   916     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   917     hence "a'*?g dvd b'*?g" by simp
   918     with ab'(1,2)  have ?thesis by simp }
   919   ultimately show ?thesis by blast
   920 qed
   921 
   922 (* FIXME move to Divides(?) *)
   923 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   924   by (auto intro: pow_divides_pow_nat dvd_power_same)
   925 
   926 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   927   by (auto intro: pow_divides_pow_int dvd_power_same)
   928 
   929 lemma divides_mult_nat:
   930   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   931   shows "m * n dvd r"
   932 proof-
   933   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   934     unfolding dvd_def by blast
   935   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   936   hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
   937   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   938   from n' k show ?thesis unfolding dvd_def by auto
   939 qed
   940 
   941 lemma divides_mult_int:
   942   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   943   shows "m * n dvd r"
   944 proof-
   945   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   946     unfolding dvd_def by blast
   947   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   948   hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
   949   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   950   from n' k show ?thesis unfolding dvd_def by auto
   951 qed
   952 
   953 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   954   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   955   apply force
   956   apply (rule dvd_diff_nat)
   957   apply auto
   958 done
   959 
   960 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
   961   using coprime_plus_one_nat by (simp add: One_nat_def)
   962 
   963 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
   964   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   965   apply force
   966   apply (rule dvd_diff)
   967   apply auto
   968 done
   969 
   970 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   971   using coprime_plus_one_nat [of "n - 1"]
   972     gcd_commute_nat [of "n - 1" n] by auto
   973 
   974 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
   975   using coprime_plus_one_int [of "n - 1"]
   976     gcd_commute_int [of "n - 1" n] by auto
   977 
   978 lemma setprod_coprime_nat [rule_format]:
   979     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
   980   apply (case_tac "finite A")
   981   apply (induct set: finite)
   982   apply (auto simp add: gcd_mult_cancel_nat)
   983 done
   984 
   985 lemma setprod_coprime_int [rule_format]:
   986     "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
   987   apply (case_tac "finite A")
   988   apply (induct set: finite)
   989   apply (auto simp add: gcd_mult_cancel_int)
   990 done
   991 
   992 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   993   unfolding prime_nat_def
   994   apply (subst even_mult_two_ex)
   995   apply clarify
   996   apply (drule_tac x = 2 in spec)
   997   apply auto
   998 done
   999 
  1000 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  1001   unfolding prime_int_def
  1002   apply (frule prime_odd_nat)
  1003   apply (auto simp add: even_nat_def)
  1004 done
  1005 
  1006 lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1007     x dvd b \<Longrightarrow> x = 1"
  1008   apply (subgoal_tac "x dvd gcd a b")
  1009   apply simp
  1010   apply (erule (1) gcd_greatest_nat)
  1011 done
  1012 
  1013 lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1014     x dvd b \<Longrightarrow> abs x = 1"
  1015   apply (subgoal_tac "x dvd gcd a b")
  1016   apply simp
  1017   apply (erule (1) gcd_greatest_int)
  1018 done
  1019 
  1020 lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
  1021     coprime d e"
  1022   apply (auto simp add: dvd_def)
  1023   apply (frule coprime_lmult_int)
  1024   apply (subst gcd_commute_int)
  1025   apply (subst (asm) (2) gcd_commute_int)
  1026   apply (erule coprime_lmult_int)
  1027 done
  1028 
  1029 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1030 apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
  1031 done
  1032 
  1033 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1034 apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
  1035 done
  1036 
  1037 
  1038 subsection {* Bezout's theorem *}
  1039 
  1040 (* Function bezw returns a pair of witnesses to Bezout's theorem --
  1041    see the theorems that follow the definition. *)
  1042 fun
  1043   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1044 where
  1045   "bezw x y =
  1046   (if y = 0 then (1, 0) else
  1047       (snd (bezw y (x mod y)),
  1048        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1049 
  1050 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1051 
  1052 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1053        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1054   by simp
  1055 
  1056 declare bezw.simps [simp del]
  1057 
  1058 lemma bezw_aux [rule_format]:
  1059     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1060 proof (induct x y rule: gcd_nat_induct)
  1061   fix m :: nat
  1062   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1063     by auto
  1064   next fix m :: nat and n
  1065     assume ngt0: "n > 0" and
  1066       ih: "fst (bezw n (m mod n)) * int n +
  1067         snd (bezw n (m mod n)) * int (m mod n) =
  1068         int (gcd n (m mod n))"
  1069     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1070       apply (simp add: bezw_non_0 gcd_non_0_nat)
  1071       apply (erule subst)
  1072       apply (simp add: ring_simps)
  1073       apply (subst mod_div_equality [of m n, symmetric])
  1074       (* applying simp here undoes the last substitution!
  1075          what is procedure cancel_div_mod? *)
  1076       apply (simp only: ring_simps zadd_int [symmetric]
  1077         zmult_int [symmetric])
  1078       done
  1079 qed
  1080 
  1081 lemma bezout_int:
  1082   fixes x y
  1083   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1084 proof -
  1085   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1086       EX u v. u * x + v * y = gcd x y"
  1087     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1088     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1089     apply (unfold gcd_int_def)
  1090     apply simp
  1091     apply (subst bezw_aux [symmetric])
  1092     apply auto
  1093     done
  1094   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1095       (x \<le> 0 \<and> y \<le> 0)"
  1096     by auto
  1097   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1098     by (erule (1) bezout_aux)
  1099   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1100     apply (insert bezout_aux [of x "-y"])
  1101     apply auto
  1102     apply (rule_tac x = u in exI)
  1103     apply (rule_tac x = "-v" in exI)
  1104     apply (subst gcd_neg2_int [symmetric])
  1105     apply auto
  1106     done
  1107   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1108     apply (insert bezout_aux [of "-x" y])
  1109     apply auto
  1110     apply (rule_tac x = "-u" in exI)
  1111     apply (rule_tac x = v in exI)
  1112     apply (subst gcd_neg1_int [symmetric])
  1113     apply auto
  1114     done
  1115   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1116     apply (insert bezout_aux [of "-x" "-y"])
  1117     apply auto
  1118     apply (rule_tac x = "-u" in exI)
  1119     apply (rule_tac x = "-v" in exI)
  1120     apply (subst gcd_neg1_int [symmetric])
  1121     apply (subst gcd_neg2_int [symmetric])
  1122     apply auto
  1123     done
  1124   ultimately show ?thesis by blast
  1125 qed
  1126 
  1127 text {* versions of Bezout for nat, by Amine Chaieb *}
  1128 
  1129 lemma ind_euclid:
  1130   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1131   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1132   shows "P a b"
  1133 proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
  1134   fix n a b
  1135   assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
  1136   have "a = b \<or> a < b \<or> b < a" by arith
  1137   moreover {assume eq: "a= b"
  1138     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1139     by simp}
  1140   moreover
  1141   {assume lt: "a < b"
  1142     hence "a + b - a < n \<or> a = 0"  using H(2) by arith
  1143     moreover
  1144     {assume "a =0" with z c have "P a b" by blast }
  1145     moreover
  1146     {assume ab: "a + b - a < n"
  1147       have th0: "a + b - a = a + (b - a)" using lt by arith
  1148       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1149       have "P a b" by (simp add: th0[symmetric])}
  1150     ultimately have "P a b" by blast}
  1151   moreover
  1152   {assume lt: "a > b"
  1153     hence "b + a - b < n \<or> b = 0"  using H(2) by arith
  1154     moreover
  1155     {assume "b =0" with z c have "P a b" by blast }
  1156     moreover
  1157     {assume ab: "b + a - b < n"
  1158       have th0: "b + a - b = b + (a - b)" using lt by arith
  1159       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1160       have "P b a" by (simp add: th0[symmetric])
  1161       hence "P a b" using c by blast }
  1162     ultimately have "P a b" by blast}
  1163 ultimately  show "P a b" by blast
  1164 qed
  1165 
  1166 lemma bezout_lemma_nat:
  1167   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1168     (a * x = b * y + d \<or> b * x = a * y + d)"
  1169   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1170     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1171   using ex
  1172   apply clarsimp
  1173   apply (rule_tac x="d" in exI, simp add: dvd_add)
  1174   apply (case_tac "a * x = b * y + d" , simp_all)
  1175   apply (rule_tac x="x + y" in exI)
  1176   apply (rule_tac x="y" in exI)
  1177   apply algebra
  1178   apply (rule_tac x="x" in exI)
  1179   apply (rule_tac x="x + y" in exI)
  1180   apply algebra
  1181 done
  1182 
  1183 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1184     (a * x = b * y + d \<or> b * x = a * y + d)"
  1185   apply(induct a b rule: ind_euclid)
  1186   apply blast
  1187   apply clarify
  1188   apply (rule_tac x="a" in exI, simp add: dvd_add)
  1189   apply clarsimp
  1190   apply (rule_tac x="d" in exI)
  1191   apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  1192   apply (rule_tac x="x+y" in exI)
  1193   apply (rule_tac x="y" in exI)
  1194   apply algebra
  1195   apply (rule_tac x="x" in exI)
  1196   apply (rule_tac x="x+y" in exI)
  1197   apply algebra
  1198 done
  1199 
  1200 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1201     (a * x - b * y = d \<or> b * x - a * y = d)"
  1202   using bezout_add_nat[of a b]
  1203   apply clarsimp
  1204   apply (rule_tac x="d" in exI, simp)
  1205   apply (rule_tac x="x" in exI)
  1206   apply (rule_tac x="y" in exI)
  1207   apply auto
  1208 done
  1209 
  1210 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1211   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1212 proof-
  1213  from nz have ap: "a > 0" by simp
  1214  from bezout_add_nat[of a b]
  1215  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1216    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1217  moreover
  1218     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1219      from H have ?thesis by blast }
  1220  moreover
  1221  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1222    {assume b0: "b = 0" with H  have ?thesis by simp}
  1223    moreover
  1224    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1225      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1226        by auto
  1227      moreover
  1228      {assume db: "d=b"
  1229        from prems have ?thesis apply simp
  1230 	 apply (rule exI[where x = b], simp)
  1231 	 apply (rule exI[where x = b])
  1232 	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1233     moreover
  1234     {assume db: "d < b"
  1235 	{assume "x=0" hence ?thesis  using prems by simp }
  1236 	moreover
  1237 	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1238 	  from db have "d \<le> b - 1" by simp
  1239 	  hence "d*b \<le> b*(b - 1)" by simp
  1240 	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1241 	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1242 	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1243             by simp
  1244 	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1245 	    by (simp only: mult_assoc right_distrib)
  1246 	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1247             by algebra
  1248 	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1249 	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1250 	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1251 	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1252 	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
  1253 	  hence ?thesis using H(1,2)
  1254 	    apply -
  1255 	    apply (rule exI[where x=d], simp)
  1256 	    apply (rule exI[where x="(b - 1) * y"])
  1257 	    by (rule exI[where x="x*(b - 1) - d"], simp)}
  1258 	ultimately have ?thesis by blast}
  1259     ultimately have ?thesis by blast}
  1260   ultimately have ?thesis by blast}
  1261  ultimately show ?thesis by blast
  1262 qed
  1263 
  1264 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1265   shows "\<exists>x y. a * x = b * y + gcd a b"
  1266 proof-
  1267   let ?g = "gcd a b"
  1268   from bezout_add_strong_nat[OF a, of b]
  1269   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1270   from d(1,2) have "d dvd ?g" by simp
  1271   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1272   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1273   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1274   thus ?thesis by blast
  1275 qed
  1276 
  1277 
  1278 subsection {* LCM *}
  1279 
  1280 lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1281   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1282     zmult_int [symmetric] gcd_int_def)
  1283 
  1284 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1285   unfolding lcm_nat_def
  1286   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1287 
  1288 lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
  1289   unfolding lcm_int_def gcd_int_def
  1290   apply (subst int_mult [symmetric])
  1291   apply (subst prod_gcd_lcm_nat [symmetric])
  1292   apply (subst nat_abs_mult_distrib [symmetric])
  1293   apply (simp, simp add: abs_mult)
  1294 done
  1295 
  1296 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1297   unfolding lcm_nat_def by simp
  1298 
  1299 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1300   unfolding lcm_int_def by simp
  1301 
  1302 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1303   unfolding lcm_nat_def by simp
  1304 
  1305 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1306   unfolding lcm_int_def by simp
  1307 
  1308 lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
  1309   unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
  1310 
  1311 lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
  1312   unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
  1313 
  1314 
  1315 lemma lcm_pos_nat:
  1316   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1317 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1318 
  1319 lemma lcm_pos_int:
  1320   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1321   apply (subst lcm_abs_int)
  1322   apply (rule lcm_pos_nat [transferred])
  1323   apply auto
  1324 done
  1325 
  1326 lemma dvd_pos_nat:
  1327   fixes n m :: nat
  1328   assumes "n > 0" and "m dvd n"
  1329   shows "m > 0"
  1330 using assms by (cases m) auto
  1331 
  1332 lemma lcm_least_nat:
  1333   assumes "(m::nat) dvd k" and "n dvd k"
  1334   shows "lcm m n dvd k"
  1335 proof (cases k)
  1336   case 0 then show ?thesis by auto
  1337 next
  1338   case (Suc _) then have pos_k: "k > 0" by auto
  1339   from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1340   with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
  1341   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1342   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1343   from pos_k k_m have pos_p: "p > 0" by auto
  1344   from pos_k k_n have pos_q: "q > 0" by auto
  1345   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1346     by (simp add: mult_ac gcd_mult_distrib_nat)
  1347   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1348     by (simp add: k_m [symmetric] k_n [symmetric])
  1349   also have "\<dots> = k * p * q * gcd m n"
  1350     by (simp add: mult_ac gcd_mult_distrib_nat)
  1351   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1352     by (simp only: k_m [symmetric] k_n [symmetric])
  1353   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1354     by (simp add: mult_ac)
  1355   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1356     by simp
  1357   with prod_gcd_lcm_nat [of m n]
  1358   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1359     by (simp add: mult_ac)
  1360   with pos_gcd have "lcm m n * gcd q p = k" by auto
  1361   then show ?thesis using dvd_def by auto
  1362 qed
  1363 
  1364 lemma lcm_least_int:
  1365   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1366 apply (subst lcm_abs_int)
  1367 apply (rule dvd_trans)
  1368 apply (rule lcm_least_nat [transferred, of _ "abs k" _])
  1369 apply auto
  1370 done
  1371 
  1372 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
  1373 proof (cases m)
  1374   case 0 then show ?thesis by simp
  1375 next
  1376   case (Suc _)
  1377   then have mpos: "m > 0" by simp
  1378   show ?thesis
  1379   proof (cases n)
  1380     case 0 then show ?thesis by simp
  1381   next
  1382     case (Suc _)
  1383     then have npos: "n > 0" by simp
  1384     have "gcd m n dvd n" by simp
  1385     then obtain k where "n = gcd m n * k" using dvd_def by auto
  1386     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1387       by (simp add: mult_ac)
  1388     also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
  1389     finally show ?thesis by (simp add: lcm_nat_def)
  1390   qed
  1391 qed
  1392 
  1393 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1394   apply (subst lcm_abs_int)
  1395   apply (rule dvd_trans)
  1396   prefer 2
  1397   apply (rule lcm_dvd1_nat [transferred])
  1398   apply auto
  1399 done
  1400 
  1401 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1402   by (subst lcm_commute_nat, rule lcm_dvd1_nat)
  1403 
  1404 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1405   by (subst lcm_commute_int, rule lcm_dvd1_int)
  1406 
  1407 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1408 by(metis lcm_dvd1_nat dvd_trans)
  1409 
  1410 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1411 by(metis lcm_dvd2_nat dvd_trans)
  1412 
  1413 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1414 by(metis lcm_dvd1_int dvd_trans)
  1415 
  1416 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1417 by(metis lcm_dvd2_int dvd_trans)
  1418 
  1419 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1420     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1421   by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1422 
  1423 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1424     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1425   by (auto intro: dvd_anti_sym [transferred] lcm_least_int)
  1426 
  1427 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1428   apply (rule sym)
  1429   apply (subst lcm_unique_nat [symmetric])
  1430   apply auto
  1431 done
  1432 
  1433 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1434   apply (rule sym)
  1435   apply (subst lcm_unique_int [symmetric])
  1436   apply auto
  1437 done
  1438 
  1439 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1440 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
  1441 
  1442 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1443 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1444 
  1445 
  1446 lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
  1447 apply(rule lcm_unique_nat[THEN iffD1])
  1448 apply (metis dvd.order_trans lcm_unique_nat)
  1449 done
  1450 
  1451 lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
  1452 apply(rule lcm_unique_int[THEN iffD1])
  1453 apply (metis dvd_trans lcm_unique_int)
  1454 done
  1455 
  1456 lemmas lcm_left_commute_nat =
  1457   mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
  1458 
  1459 lemmas lcm_left_commute_int =
  1460   mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
  1461 
  1462 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1463 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1464 
  1465 
  1466 subsection {* Primes *}
  1467 
  1468 (* Is there a better way to handle these, rather than making them
  1469    elim rules? *)
  1470 
  1471 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
  1472   by (unfold prime_nat_def, auto)
  1473 
  1474 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
  1475   by (unfold prime_nat_def, auto)
  1476 
  1477 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
  1478   by (unfold prime_nat_def, auto)
  1479 
  1480 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
  1481   by (unfold prime_nat_def, auto)
  1482 
  1483 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
  1484   by (unfold prime_nat_def, auto)
  1485 
  1486 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
  1487   by (unfold prime_nat_def, auto)
  1488 
  1489 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
  1490   by (unfold prime_nat_def, auto)
  1491 
  1492 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
  1493   by (unfold prime_int_def prime_nat_def, auto)
  1494 
  1495 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
  1496   by (unfold prime_int_def prime_nat_def, auto)
  1497 
  1498 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
  1499   by (unfold prime_int_def prime_nat_def, auto)
  1500 
  1501 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
  1502   by (unfold prime_int_def prime_nat_def, auto)
  1503 
  1504 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
  1505   by (unfold prime_int_def prime_nat_def, auto)
  1506 
  1507 thm prime_nat_def;
  1508 thm prime_nat_def [transferred];
  1509 
  1510 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
  1511     m = 1 \<or> m = p))"
  1512   using prime_nat_def [transferred]
  1513     apply (case_tac "p >= 0")
  1514     by (blast, auto simp add: prime_ge_0_int)
  1515 
  1516 (* To do: determine primality of any numeral *)
  1517 
  1518 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
  1519   by (simp add: prime_nat_def)
  1520 
  1521 lemma zero_not_prime_int [simp]: "~prime (0::int)"
  1522   by (simp add: prime_int_def)
  1523 
  1524 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
  1525   by (simp add: prime_nat_def)
  1526 
  1527 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
  1528   by (simp add: prime_nat_def One_nat_def)
  1529 
  1530 lemma one_not_prime_int [simp]: "~prime (1::int)"
  1531   by (simp add: prime_int_def)
  1532 
  1533 lemma two_is_prime_nat [simp]: "prime (2::nat)"
  1534   apply (auto simp add: prime_nat_def)
  1535   apply (case_tac m)
  1536   apply (auto dest!: dvd_imp_le)
  1537   done
  1538 
  1539 lemma two_is_prime_int [simp]: "prime (2::int)"
  1540   by (rule two_is_prime_nat [transferred direction: nat "op <= (0::int)"])
  1541 
  1542 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1543   apply (unfold prime_nat_def)
  1544   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
  1545   done
  1546 
  1547 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1548   apply (unfold prime_int_altdef)
  1549   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
  1550   done
  1551 
  1552 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1553   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
  1554 
  1555 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1556   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
  1557 
  1558 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
  1559     p dvd m * n = (p dvd m \<or> p dvd n)"
  1560   by (rule iffI, rule prime_dvd_mult_nat, auto)
  1561 
  1562 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
  1563     p dvd m * n = (p dvd m \<or> p dvd n)"
  1564   by (rule iffI, rule prime_dvd_mult_int, auto)
  1565 
  1566 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1567     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1568   unfolding prime_nat_def dvd_def apply auto
  1569   apply (subgoal_tac "k > 1")
  1570   apply force
  1571   apply (subgoal_tac "k ~= 0")
  1572   apply force
  1573   apply (rule notI)
  1574   apply force
  1575 done
  1576 
  1577 (* there's a lot of messing around with signs of products here --
  1578    could this be made more automatic? *)
  1579 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1580     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1581   unfolding prime_int_altdef dvd_def
  1582   apply auto
  1583   apply (rule_tac x = m in exI)
  1584   apply (rule_tac x = k in exI)
  1585   apply (auto simp add: mult_compare_simps)
  1586   apply (subgoal_tac "k > 0")
  1587   apply arith
  1588   apply (case_tac "k <= 0")
  1589   apply (subgoal_tac "m * k <= 0")
  1590   apply force
  1591   apply (subst zero_compare_simps(8))
  1592   apply auto
  1593   apply (subgoal_tac "m * k <= 0")
  1594   apply force
  1595   apply (subst zero_compare_simps(8))
  1596   apply auto
  1597 done
  1598 
  1599 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
  1600     n > 0 --> (p dvd x^n --> p dvd x)"
  1601   by (induct n rule: nat_induct, auto)
  1602 
  1603 lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
  1604     n > 0 --> (p dvd x^n --> p dvd x)"
  1605   apply (induct n rule: nat_induct, auto)
  1606   apply (frule prime_ge_0_int)
  1607   apply auto
  1608 done
  1609 
  1610 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1611     coprime a (p^m)"
  1612   apply (rule coprime_exp_nat)
  1613   apply (subst gcd_commute_nat)
  1614   apply (erule (1) prime_imp_coprime_nat)
  1615 done
  1616 
  1617 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1618     coprime a (p^m)"
  1619   apply (rule coprime_exp_int)
  1620   apply (subst gcd_commute_int)
  1621   apply (erule (1) prime_imp_coprime_int)
  1622 done
  1623 
  1624 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1625   apply (rule prime_imp_coprime_nat, assumption)
  1626   apply (unfold prime_nat_def, auto)
  1627 done
  1628 
  1629 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1630   apply (rule prime_imp_coprime_int, assumption)
  1631   apply (unfold prime_int_altdef, clarify)
  1632   apply (drule_tac x = q in spec)
  1633   apply (drule_tac x = p in spec)
  1634   apply auto
  1635 done
  1636 
  1637 lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1638     coprime (p^m) (q^n)"
  1639   by (rule coprime_exp2_nat, rule primes_coprime_nat)
  1640 
  1641 lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1642     coprime (p^m) (q^n)"
  1643   by (rule coprime_exp2_int, rule primes_coprime_int)
  1644 
  1645 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
  1646   apply (induct n rule: nat_less_induct)
  1647   apply (case_tac "n = 0")
  1648   using two_is_prime_nat apply blast
  1649   apply (case_tac "prime n")
  1650   apply blast
  1651   apply (subgoal_tac "n > 1")
  1652   apply (frule (1) not_prime_eq_prod_nat)
  1653   apply (auto intro: dvd_mult dvd_mult2)
  1654 done
  1655 
  1656 (* An Isar version:
  1657 
  1658 lemma prime_factor_b_nat:
  1659   fixes n :: nat
  1660   assumes "n \<noteq> 1"
  1661   shows "\<exists>p. prime p \<and> p dvd n"
  1662 
  1663 using `n ~= 1`
  1664 proof (induct n rule: less_induct_nat)
  1665   fix n :: nat
  1666   assume "n ~= 1" and
  1667     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
  1668   thus "\<exists>p. prime p \<and> p dvd n"
  1669   proof -
  1670   {
  1671     assume "n = 0"
  1672     moreover note two_is_prime_nat
  1673     ultimately have ?thesis
  1674       by (auto simp del: two_is_prime_nat)
  1675   }
  1676   moreover
  1677   {
  1678     assume "prime n"
  1679     hence ?thesis by auto
  1680   }
  1681   moreover
  1682   {
  1683     assume "n ~= 0" and "~ prime n"
  1684     with `n ~= 1` have "n > 1" by auto
  1685     with `~ prime n` and not_prime_eq_prod_nat obtain m k where
  1686       "n = m * k" and "1 < m" and "m < n" by blast
  1687     with ih obtain p where "prime p" and "p dvd m" by blast
  1688     with `n = m * k` have ?thesis by auto
  1689   }
  1690   ultimately show ?thesis by blast
  1691   qed
  1692 qed
  1693 
  1694 *)
  1695 
  1696 text {* One property of coprimality is easier to prove via prime factors. *}
  1697 
  1698 lemma prime_divprod_pow_nat:
  1699   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
  1700   shows "p^n dvd a \<or> p^n dvd b"
  1701 proof-
  1702   {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
  1703       apply (cases "n=0", simp_all)
  1704       apply (cases "a=1", simp_all) done}
  1705   moreover
  1706   {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
  1707     then obtain m where m: "n = Suc m" by (cases n, auto)
  1708     from n have "p dvd p^n" by (intro dvd_power, auto)
  1709     also note pab
  1710     finally have pab': "p dvd a * b".
  1711     from prime_dvd_mult_nat[OF p pab']
  1712     have "p dvd a \<or> p dvd b" .
  1713     moreover
  1714     {assume pa: "p dvd a"
  1715       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1716       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
  1717       with p have "coprime b p"
  1718         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
  1719       hence pnb: "coprime (p^n) b"
  1720         by (subst gcd_commute_nat, rule coprime_exp_nat)
  1721       from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
  1722     moreover
  1723     {assume pb: "p dvd b"
  1724       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1725       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
  1726         by auto
  1727       with p have "coprime a p"
  1728         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
  1729       hence pna: "coprime (p^n) a"
  1730         by (subst gcd_commute_nat, rule coprime_exp_nat)
  1731       from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
  1732     ultimately have ?thesis by blast}
  1733   ultimately show ?thesis by blast
  1734 qed
  1735 
  1736 subsection {* Infinitely many primes *}
  1737 
  1738 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
  1739 proof-
  1740   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
  1741   from prime_factor_nat [OF f1]
  1742       obtain p where "prime p" and "p dvd fact n + 1" by auto
  1743   hence "p \<le> fact n + 1" 
  1744     by (intro dvd_imp_le, auto)
  1745   {assume "p \<le> n"
  1746     from `prime p` have "p \<ge> 1" 
  1747       by (cases p, simp_all)
  1748     with `p <= n` have "p dvd fact n" 
  1749       by (intro dvd_fact_nat)
  1750     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
  1751       by (rule dvd_diff_nat)
  1752     hence "p dvd 1" by simp
  1753     hence "p <= 1" by auto
  1754     moreover from `prime p` have "p > 1" by auto
  1755     ultimately have False by auto}
  1756   hence "n < p" by arith
  1757   with `prime p` and `p <= fact n + 1` show ?thesis by auto
  1758 qed
  1759 
  1760 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
  1761 using next_prime_bound by auto
  1762 
  1763 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
  1764 proof
  1765   assume "finite {(p::nat). prime p}"
  1766   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
  1767     by auto
  1768   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
  1769     by auto
  1770   with bigger_prime [of b] show False by auto
  1771 qed
  1772 
  1773 
  1774 end