src/HOL/GCD.thy
author nipkow
Fri Jun 26 19:44:39 2009 +0200 (2009-06-26)
changeset 31814 7c122634da81
parent 31813 4df828bbc411
child 31952 40501bb2d57c
permissions -rw-r--r--
lcm abs lemmas
     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 Tobias Nipkow cleaned up a lot.
    24 *)
    25 
    26 
    27 header {* GCD *}
    28 
    29 theory GCD
    30 imports NatTransfer
    31 begin
    32 
    33 declare One_nat_def [simp del]
    34 
    35 subsection {* gcd *}
    36 
    37 class gcd = one +
    38 
    39 fixes
    40   gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
    41   lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    42 
    43 begin
    44 
    45 abbreviation
    46   coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    47 where
    48   "coprime x y == (gcd x y = 1)"
    49 
    50 end
    51 
    52 class prime = one +
    53 
    54 fixes
    55   prime :: "'a \<Rightarrow> bool"
    56 
    57 
    58 (* definitions for the natural numbers *)
    59 
    60 instantiation nat :: gcd
    61 
    62 begin
    63 
    64 fun
    65   gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    66 where
    67   "gcd_nat x y =
    68    (if y = 0 then x else gcd y (x mod y))"
    69 
    70 definition
    71   lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    72 where
    73   "lcm_nat x y = x * y div (gcd x y)"
    74 
    75 instance proof qed
    76 
    77 end
    78 
    79 
    80 instantiation nat :: prime
    81 
    82 begin
    83 
    84 definition
    85   prime_nat :: "nat \<Rightarrow> bool"
    86 where
    87   [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    88 
    89 instance proof qed
    90 
    91 end
    92 
    93 
    94 (* definitions for the integers *)
    95 
    96 instantiation int :: gcd
    97 
    98 begin
    99 
   100 definition
   101   gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
   102 where
   103   "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
   104 
   105 definition
   106   lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
   107 where
   108   "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
   109 
   110 instance proof qed
   111 
   112 end
   113 
   114 
   115 instantiation int :: prime
   116 
   117 begin
   118 
   119 definition
   120   prime_int :: "int \<Rightarrow> bool"
   121 where
   122   [code del]: "prime_int p = prime (nat p)"
   123 
   124 instance proof qed
   125 
   126 end
   127 
   128 
   129 subsection {* Set up Transfer *}
   130 
   131 
   132 lemma transfer_nat_int_gcd:
   133   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   134   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   135   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
   136   unfolding gcd_int_def lcm_int_def prime_int_def
   137   by auto
   138 
   139 lemma transfer_nat_int_gcd_closures:
   140   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
   141   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   142   by (auto simp add: gcd_int_def lcm_int_def)
   143 
   144 declare TransferMorphism_nat_int[transfer add return:
   145     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   146 
   147 lemma transfer_int_nat_gcd:
   148   "gcd (int x) (int y) = int (gcd x y)"
   149   "lcm (int x) (int y) = int (lcm x y)"
   150   "prime (int x) = prime x"
   151   by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
   152 
   153 lemma transfer_int_nat_gcd_closures:
   154   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   155   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   156   by (auto simp add: gcd_int_def lcm_int_def)
   157 
   158 declare TransferMorphism_int_nat[transfer add return:
   159     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   160 
   161 
   162 
   163 subsection {* GCD *}
   164 
   165 (* was gcd_induct *)
   166 lemma nat_gcd_induct:
   167   fixes m n :: nat
   168   assumes "\<And>m. P m 0"
   169     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   170   shows "P m n"
   171   apply (rule gcd_nat.induct)
   172   apply (case_tac "y = 0")
   173   using assms apply simp_all
   174 done
   175 
   176 (* specific to int *)
   177 
   178 lemma int_gcd_neg1 [simp]: "gcd (-x::int) y = gcd x y"
   179   by (simp add: gcd_int_def)
   180 
   181 lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y"
   182   by (simp add: gcd_int_def)
   183 
   184 lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
   185 by(simp add: gcd_int_def)
   186 
   187 lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)"
   188 by (simp add: gcd_int_def)
   189 
   190 lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
   191 by (metis abs_idempotent int_gcd_abs)
   192 
   193 lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
   194 by (metis abs_idempotent int_gcd_abs)
   195 
   196 lemma int_gcd_cases:
   197   fixes x :: int and y
   198   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   199       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   200       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   201       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   202   shows "P (gcd x y)"
   203 by (insert prems, auto simp add: int_gcd_neg1 int_gcd_neg2, arith)
   204 
   205 lemma int_gcd_ge_0 [simp]: "gcd (x::int) y >= 0"
   206   by (simp add: gcd_int_def)
   207 
   208 lemma int_lcm_neg1: "lcm (-x::int) y = lcm x y"
   209   by (simp add: lcm_int_def)
   210 
   211 lemma int_lcm_neg2: "lcm (x::int) (-y) = lcm x y"
   212   by (simp add: lcm_int_def)
   213 
   214 lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)"
   215   by (simp add: lcm_int_def)
   216 
   217 lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
   218 by(simp add:lcm_int_def)
   219 
   220 lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
   221 by (metis abs_idempotent lcm_int_def)
   222 
   223 lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
   224 by (metis abs_idempotent lcm_int_def)
   225 
   226 lemma int_lcm_cases:
   227   fixes x :: int and y
   228   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   229       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   230       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   231       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   232   shows "P (lcm x y)"
   233 by (insert prems, auto simp add: int_lcm_neg1 int_lcm_neg2, arith)
   234 
   235 lemma int_lcm_ge_0 [simp]: "lcm (x::int) y >= 0"
   236   by (simp add: lcm_int_def)
   237 
   238 (* was gcd_0, etc. *)
   239 lemma nat_gcd_0 [simp]: "gcd (x::nat) 0 = x"
   240   by simp
   241 
   242 (* was igcd_0, etc. *)
   243 lemma int_gcd_0 [simp]: "gcd (x::int) 0 = abs x"
   244   by (unfold gcd_int_def, auto)
   245 
   246 lemma nat_gcd_0_left [simp]: "gcd 0 (x::nat) = x"
   247   by simp
   248 
   249 lemma int_gcd_0_left [simp]: "gcd 0 (x::int) = abs x"
   250   by (unfold gcd_int_def, auto)
   251 
   252 lemma nat_gcd_red: "gcd (x::nat) y = gcd y (x mod y)"
   253   by (case_tac "y = 0", auto)
   254 
   255 (* weaker, but useful for the simplifier *)
   256 
   257 lemma nat_gcd_non_0: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   258   by simp
   259 
   260 lemma nat_gcd_1 [simp]: "gcd (m::nat) 1 = 1"
   261   by simp
   262 
   263 lemma nat_gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   264   by (simp add: One_nat_def)
   265 
   266 lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1"
   267   by (simp add: gcd_int_def)
   268 
   269 lemma nat_gcd_idem: "gcd (x::nat) x = x"
   270 by simp
   271 
   272 lemma int_gcd_idem: "gcd (x::int) x = abs x"
   273 by (auto simp add: gcd_int_def)
   274 
   275 declare gcd_nat.simps [simp del]
   276 
   277 text {*
   278   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   279   conjunctions don't seem provable separately.
   280 *}
   281 
   282 lemma nat_gcd_dvd1 [iff]: "(gcd (m::nat)) n dvd m"
   283   and nat_gcd_dvd2 [iff]: "(gcd m n) dvd n"
   284   apply (induct m n rule: nat_gcd_induct)
   285   apply (simp_all add: nat_gcd_non_0)
   286   apply (blast dest: dvd_mod_imp_dvd)
   287 done
   288 
   289 lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
   290 by (metis gcd_int_def int_dvd_iff nat_gcd_dvd1)
   291 
   292 lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y"
   293 by (metis gcd_int_def int_dvd_iff nat_gcd_dvd2)
   294 
   295 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   296 by(metis nat_gcd_dvd1 dvd_trans)
   297 
   298 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   299 by(metis nat_gcd_dvd2 dvd_trans)
   300 
   301 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   302 by(metis int_gcd_dvd1 dvd_trans)
   303 
   304 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   305 by(metis int_gcd_dvd2 dvd_trans)
   306 
   307 lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   308   by (rule dvd_imp_le, auto)
   309 
   310 lemma nat_gcd_le2 [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   311   by (rule dvd_imp_le, auto)
   312 
   313 lemma int_gcd_le1 [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   314   by (rule zdvd_imp_le, auto)
   315 
   316 lemma int_gcd_le2 [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   317   by (rule zdvd_imp_le, auto)
   318 
   319 lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   320 by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
   321 
   322 lemma int_gcd_greatest:
   323   "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   324   apply (subst int_gcd_abs)
   325   apply (subst abs_dvd_iff [symmetric])
   326   apply (rule nat_gcd_greatest [transferred])
   327   apply auto
   328 done
   329 
   330 lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) =
   331     (k dvd m & k dvd n)"
   332   by (blast intro!: nat_gcd_greatest intro: dvd_trans)
   333 
   334 lemma int_gcd_greatest_iff: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   335   by (blast intro!: int_gcd_greatest intro: dvd_trans)
   336 
   337 lemma nat_gcd_zero [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   338   by (simp only: dvd_0_left_iff [symmetric] nat_gcd_greatest_iff)
   339 
   340 lemma int_gcd_zero [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   341   by (auto simp add: gcd_int_def)
   342 
   343 lemma nat_gcd_pos [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   344   by (insert nat_gcd_zero [of m n], arith)
   345 
   346 lemma int_gcd_pos [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   347   by (insert int_gcd_zero [of m n], insert int_gcd_ge_0 [of m n], arith)
   348 
   349 lemma nat_gcd_commute: "gcd (m::nat) n = gcd n m"
   350   by (rule dvd_anti_sym, auto)
   351 
   352 lemma int_gcd_commute: "gcd (m::int) n = gcd n m"
   353   by (auto simp add: gcd_int_def nat_gcd_commute)
   354 
   355 lemma nat_gcd_assoc: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
   356   apply (rule dvd_anti_sym)
   357   apply (blast intro: dvd_trans)+
   358 done
   359 
   360 lemma int_gcd_assoc: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
   361   by (auto simp add: gcd_int_def nat_gcd_assoc)
   362 
   363 lemmas nat_gcd_left_commute =
   364   mk_left_commute[of gcd, OF nat_gcd_assoc nat_gcd_commute]
   365 
   366 lemmas int_gcd_left_commute =
   367   mk_left_commute[of gcd, OF int_gcd_assoc int_gcd_commute]
   368 
   369 lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute
   370   -- {* gcd is an AC-operator *}
   371 
   372 lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute
   373 
   374 lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and>
   375     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   376   apply auto
   377   apply (rule dvd_anti_sym)
   378   apply (erule (1) nat_gcd_greatest)
   379   apply auto
   380 done
   381 
   382 lemma int_gcd_unique: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   383     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   384   apply (case_tac "d = 0")
   385   apply force
   386   apply (rule iffI)
   387   apply (rule zdvd_anti_sym)
   388   apply arith
   389   apply (subst int_gcd_pos)
   390   apply clarsimp
   391   apply (drule_tac x = "d + 1" in spec)
   392   apply (frule zdvd_imp_le)
   393   apply (auto intro: int_gcd_greatest)
   394 done
   395 
   396 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   397 by (metis dvd.eq_iff nat_gcd_unique)
   398 
   399 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   400 by (metis dvd.eq_iff nat_gcd_unique)
   401 
   402 lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   403 by (metis abs_dvd_iff abs_eq_0 int_gcd_0_left int_gcd_abs int_gcd_unique)
   404 
   405 lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   406 by (metis gcd_proj1_if_dvd_int int_gcd_commute)
   407 
   408 
   409 text {*
   410   \medskip Multiplication laws
   411 *}
   412 
   413 lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   414     -- {* \cite[page 27]{davenport92} *}
   415   apply (induct m n rule: nat_gcd_induct)
   416   apply simp
   417   apply (case_tac "k = 0")
   418   apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2)
   419 done
   420 
   421 lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   422   apply (subst (1 2) int_gcd_abs)
   423   apply (subst (1 2) abs_mult)
   424   apply (rule nat_gcd_mult_distrib [transferred])
   425   apply auto
   426 done
   427 
   428 lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   429   apply (insert nat_gcd_mult_distrib [of m k n])
   430   apply simp
   431   apply (erule_tac t = m in ssubst)
   432   apply simp
   433   done
   434 
   435 lemma int_coprime_dvd_mult:
   436   "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   437 apply (subst abs_dvd_iff [symmetric])
   438 apply (subst dvd_abs_iff [symmetric])
   439 apply (subst (asm) int_gcd_abs)
   440 apply (rule nat_coprime_dvd_mult [transferred])
   441     prefer 4 apply assumption
   442    apply auto
   443 apply (subst abs_mult [symmetric], auto)
   444 done
   445 
   446 lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow>
   447     (k dvd m * n) = (k dvd m)"
   448   by (auto intro: nat_coprime_dvd_mult)
   449 
   450 lemma int_coprime_dvd_mult_iff: "coprime (k::int) n \<Longrightarrow>
   451     (k dvd m * n) = (k dvd m)"
   452   by (auto intro: int_coprime_dvd_mult)
   453 
   454 lemma nat_gcd_mult_cancel: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   455   apply (rule dvd_anti_sym)
   456   apply (rule nat_gcd_greatest)
   457   apply (rule_tac n = k in nat_coprime_dvd_mult)
   458   apply (simp add: nat_gcd_assoc)
   459   apply (simp add: nat_gcd_commute)
   460   apply (simp_all add: mult_commute)
   461 done
   462 
   463 lemma int_gcd_mult_cancel:
   464   "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
   465 apply (subst (1 2) int_gcd_abs)
   466 apply (subst abs_mult)
   467 apply (rule nat_gcd_mult_cancel [transferred], auto)
   468 done
   469 
   470 text {* \medskip Addition laws *}
   471 
   472 lemma nat_gcd_add1 [simp]: "gcd ((m::nat) + n) n = gcd m n"
   473   apply (case_tac "n = 0")
   474   apply (simp_all add: nat_gcd_non_0)
   475 done
   476 
   477 lemma nat_gcd_add2 [simp]: "gcd (m::nat) (m + n) = gcd m n"
   478   apply (subst (1 2) nat_gcd_commute)
   479   apply (subst add_commute)
   480   apply simp
   481 done
   482 
   483 (* to do: add the other variations? *)
   484 
   485 lemma nat_gcd_diff1: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   486   by (subst nat_gcd_add1 [symmetric], auto)
   487 
   488 lemma nat_gcd_diff2: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   489   apply (subst nat_gcd_commute)
   490   apply (subst nat_gcd_diff1 [symmetric])
   491   apply auto
   492   apply (subst nat_gcd_commute)
   493   apply (subst nat_gcd_diff1)
   494   apply assumption
   495   apply (rule nat_gcd_commute)
   496 done
   497 
   498 lemma int_gcd_non_0: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   499   apply (frule_tac b = y and a = x in pos_mod_sign)
   500   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   501   apply (auto simp add: nat_gcd_non_0 nat_mod_distrib [symmetric]
   502     zmod_zminus1_eq_if)
   503   apply (frule_tac a = x in pos_mod_bound)
   504   apply (subst (1 2) nat_gcd_commute)
   505   apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2
   506     nat_le_eq_zle)
   507 done
   508 
   509 lemma int_gcd_red: "gcd (x::int) y = gcd y (x mod y)"
   510   apply (case_tac "y = 0")
   511   apply force
   512   apply (case_tac "y > 0")
   513   apply (subst int_gcd_non_0, auto)
   514   apply (insert int_gcd_non_0 [of "-y" "-x"])
   515   apply (auto simp add: int_gcd_neg1 int_gcd_neg2)
   516 done
   517 
   518 lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n"
   519 by (metis int_gcd_red mod_add_self1 zadd_commute)
   520 
   521 lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n"
   522 by (metis int_gcd_add1 int_gcd_commute zadd_commute)
   523 
   524 lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n"
   525 by (metis mod_mult_self3 nat_gcd_commute nat_gcd_red)
   526 
   527 lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n"
   528 by (metis int_gcd_commute int_gcd_red mod_mult_self1 zadd_commute)
   529 
   530 
   531 (* to do: differences, and all variations of addition rules
   532     as simplification rules for nat and int *)
   533 
   534 (* FIXME remove iff *)
   535 lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n"
   536   using mult_dvd_mono [of 1] by auto
   537 
   538 (* to do: add the three variations of these, and for ints? *)
   539 
   540 lemma finite_divisors_nat:
   541   assumes "(m::nat)~= 0" shows "finite{d. d dvd m}"
   542 proof-
   543   have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
   544   from finite_subset[OF _ this] show ?thesis using assms
   545     by(bestsimp intro!:dvd_imp_le)
   546 qed
   547 
   548 lemma finite_divisors_int:
   549   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
   550 proof-
   551   have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
   552   hence "finite{d. abs d <= abs i}" by simp
   553   from finite_subset[OF _ this] show ?thesis using assms
   554     by(bestsimp intro!:dvd_imp_le_int)
   555 qed
   556 
   557 lemma gcd_is_Max_divisors_nat:
   558   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
   559 apply(rule Max_eqI[THEN sym])
   560   apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat)
   561  apply simp
   562  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le nat_gcd_greatest_iff nat_gcd_pos)
   563 apply simp
   564 done
   565 
   566 lemma gcd_is_Max_divisors_int:
   567   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
   568 apply(rule Max_eqI[THEN sym])
   569   apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int)
   570  apply simp
   571  apply (metis int_gcd_greatest_iff int_gcd_pos zdvd_imp_le)
   572 apply simp
   573 done
   574 
   575 
   576 subsection {* Coprimality *}
   577 
   578 lemma nat_div_gcd_coprime:
   579   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   580   shows "coprime (a div gcd a b) (b div gcd a b)"
   581 proof -
   582   let ?g = "gcd a b"
   583   let ?a' = "a div ?g"
   584   let ?b' = "b div ?g"
   585   let ?g' = "gcd ?a' ?b'"
   586   have dvdg: "?g dvd a" "?g dvd b" by simp_all
   587   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   588   from dvdg dvdg' obtain ka kb ka' kb' where
   589       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   590     unfolding dvd_def by blast
   591   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   592     by simp_all
   593   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   594     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   595       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   596   have "?g \<noteq> 0" using nz by (simp add: nat_gcd_zero)
   597   then have gp: "?g > 0" by arith
   598   from nat_gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   599   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   600 qed
   601 
   602 lemma int_div_gcd_coprime:
   603   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   604   shows "coprime (a div gcd a b) (b div gcd a b)"
   605 apply (subst (1 2 3) int_gcd_abs)
   606 apply (subst (1 2) abs_div)
   607   apply simp
   608  apply simp
   609 apply(subst (1 2) abs_gcd_int)
   610 apply (rule nat_div_gcd_coprime [transferred])
   611 using nz apply (auto simp add: int_gcd_abs [symmetric])
   612 done
   613 
   614 lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   615   using nat_gcd_unique[of 1 a b, simplified] by auto
   616 
   617 lemma nat_coprime_Suc_0:
   618     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   619   using nat_coprime by (simp add: One_nat_def)
   620 
   621 lemma int_coprime: "coprime (a::int) b \<longleftrightarrow>
   622     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   623   using int_gcd_unique [of 1 a b]
   624   apply clarsimp
   625   apply (erule subst)
   626   apply (rule iffI)
   627   apply force
   628   apply (drule_tac x = "abs e" in exI)
   629   apply (case_tac "e >= 0")
   630   apply force
   631   apply force
   632 done
   633 
   634 lemma nat_gcd_coprime:
   635   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   636     b: "b = b' * gcd a b"
   637   shows    "coprime a' b'"
   638 
   639   apply (subgoal_tac "a' = a div gcd a b")
   640   apply (erule ssubst)
   641   apply (subgoal_tac "b' = b div gcd a b")
   642   apply (erule ssubst)
   643   apply (rule nat_div_gcd_coprime)
   644   using prems
   645   apply force
   646   apply (subst (1) b)
   647   using z apply force
   648   apply (subst (1) a)
   649   using z apply force
   650 done
   651 
   652 lemma int_gcd_coprime:
   653   assumes z: "gcd (a::int) 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 int_div_gcd_coprime)
   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 nat_coprime_mult: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   671     shows "coprime d (a * b)"
   672   apply (subst nat_gcd_commute)
   673   using da apply (subst nat_gcd_mult_cancel)
   674   apply (subst nat_gcd_commute, assumption)
   675   apply (subst nat_gcd_commute, rule db)
   676 done
   677 
   678 lemma int_coprime_mult: assumes da: "coprime (d::int) a" and db: "coprime d b"
   679     shows "coprime d (a * b)"
   680   apply (subst int_gcd_commute)
   681   using da apply (subst int_gcd_mult_cancel)
   682   apply (subst int_gcd_commute, assumption)
   683   apply (subst int_gcd_commute, rule db)
   684 done
   685 
   686 lemma nat_coprime_lmult:
   687   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   688 proof -
   689   have "gcd d a dvd gcd d (a * b)"
   690     by (rule nat_gcd_greatest, auto)
   691   with dab show ?thesis
   692     by auto
   693 qed
   694 
   695 lemma int_coprime_lmult:
   696   assumes "coprime (d::int) (a * b)" shows "coprime d a"
   697 proof -
   698   have "gcd d a dvd gcd d (a * b)"
   699     by (rule int_gcd_greatest, auto)
   700   with assms show ?thesis
   701     by auto
   702 qed
   703 
   704 lemma nat_coprime_rmult:
   705   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   706 proof -
   707   have "gcd d b dvd gcd d (a * b)"
   708     by (rule nat_gcd_greatest, auto intro: dvd_mult)
   709   with assms show ?thesis
   710     by auto
   711 qed
   712 
   713 lemma int_coprime_rmult:
   714   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   715 proof -
   716   have "gcd d b dvd gcd d (a * b)"
   717     by (rule int_gcd_greatest, auto intro: dvd_mult)
   718   with dab show ?thesis
   719     by auto
   720 qed
   721 
   722 lemma nat_coprime_mul_eq: "coprime (d::nat) (a * b) \<longleftrightarrow>
   723     coprime d a \<and>  coprime d b"
   724   using nat_coprime_rmult[of d a b] nat_coprime_lmult[of d a b]
   725     nat_coprime_mult[of d a b]
   726   by blast
   727 
   728 lemma int_coprime_mul_eq: "coprime (d::int) (a * b) \<longleftrightarrow>
   729     coprime d a \<and>  coprime d b"
   730   using int_coprime_rmult[of d a b] int_coprime_lmult[of d a b]
   731     int_coprime_mult[of d a b]
   732   by blast
   733 
   734 lemma nat_gcd_coprime_exists:
   735     assumes nz: "gcd (a::nat) b \<noteq> 0"
   736     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   737   apply (rule_tac x = "a div gcd a b" in exI)
   738   apply (rule_tac x = "b div gcd a b" in exI)
   739   using nz apply (auto simp add: nat_div_gcd_coprime dvd_div_mult)
   740 done
   741 
   742 lemma int_gcd_coprime_exists:
   743     assumes nz: "gcd (a::int) b \<noteq> 0"
   744     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   745   apply (rule_tac x = "a div gcd a b" in exI)
   746   apply (rule_tac x = "b div gcd a b" in exI)
   747   using nz apply (auto simp add: int_div_gcd_coprime dvd_div_mult_self)
   748 done
   749 
   750 lemma nat_coprime_exp: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   751   by (induct n, simp_all add: nat_coprime_mult)
   752 
   753 lemma int_coprime_exp: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   754   by (induct n, simp_all add: int_coprime_mult)
   755 
   756 lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   757   apply (rule nat_coprime_exp)
   758   apply (subst nat_gcd_commute)
   759   apply (rule nat_coprime_exp)
   760   apply (subst nat_gcd_commute, assumption)
   761 done
   762 
   763 lemma int_coprime_exp2 [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   764   apply (rule int_coprime_exp)
   765   apply (subst int_gcd_commute)
   766   apply (rule int_coprime_exp)
   767   apply (subst int_gcd_commute, assumption)
   768 done
   769 
   770 lemma nat_gcd_exp: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   771 proof (cases)
   772   assume "a = 0 & b = 0"
   773   thus ?thesis by simp
   774   next assume "~(a = 0 & b = 0)"
   775   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   776     by (auto simp:nat_div_gcd_coprime)
   777   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   778       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   779     apply (subst (1 2) mult_commute)
   780     apply (subst nat_gcd_mult_distrib [symmetric])
   781     apply simp
   782     done
   783   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   784     apply (subst div_power)
   785     apply auto
   786     apply (rule dvd_div_mult_self)
   787     apply (rule dvd_power_same)
   788     apply auto
   789     done
   790   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
   791     apply (subst div_power)
   792     apply auto
   793     apply (rule dvd_div_mult_self)
   794     apply (rule dvd_power_same)
   795     apply auto
   796     done
   797   finally show ?thesis .
   798 qed
   799 
   800 lemma int_gcd_exp: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   801   apply (subst (1 2) int_gcd_abs)
   802   apply (subst (1 2) power_abs)
   803   apply (rule nat_gcd_exp [where n = n, transferred])
   804   apply auto
   805 done
   806 
   807 lemma nat_coprime_divprod: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   808   using nat_coprime_dvd_mult_iff[of d a b]
   809   by (auto simp add: mult_commute)
   810 
   811 lemma int_coprime_divprod: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   812   using int_coprime_dvd_mult_iff[of d a b]
   813   by (auto simp add: mult_commute)
   814 
   815 lemma nat_division_decomp: assumes dc: "(a::nat) dvd b * c"
   816   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   817 proof-
   818   let ?g = "gcd a b"
   819   {assume "?g = 0" with dc have ?thesis by auto}
   820   moreover
   821   {assume z: "?g \<noteq> 0"
   822     from nat_gcd_coprime_exists[OF z]
   823     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   824       by blast
   825     have thb: "?g dvd b" by auto
   826     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   827     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   828     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   829     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   830     with z have th_1: "a' dvd b' * c" by auto
   831     from nat_coprime_dvd_mult[OF ab'(3)] th_1
   832     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   833     from ab' have "a = ?g*a'" by algebra
   834     with thb thc have ?thesis by blast }
   835   ultimately show ?thesis by blast
   836 qed
   837 
   838 lemma int_division_decomp: assumes dc: "(a::int) dvd b * c"
   839   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   840 proof-
   841   let ?g = "gcd a b"
   842   {assume "?g = 0" with dc have ?thesis by auto}
   843   moreover
   844   {assume z: "?g \<noteq> 0"
   845     from int_gcd_coprime_exists[OF z]
   846     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   847       by blast
   848     have thb: "?g dvd b" by auto
   849     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   850     with dc have th0: "a' dvd b*c"
   851       using dvd_trans[of a' a "b*c"] by simp
   852     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   853     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   854     with z have th_1: "a' dvd b' * c" by auto
   855     from int_coprime_dvd_mult[OF ab'(3)] th_1
   856     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   857     from ab' have "a = ?g*a'" by algebra
   858     with thb thc have ?thesis by blast }
   859   ultimately show ?thesis by blast
   860 qed
   861 
   862 lemma nat_pow_divides_pow:
   863   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   864   shows "a dvd b"
   865 proof-
   866   let ?g = "gcd a b"
   867   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   868   {assume "?g = 0" with ab n have ?thesis by auto }
   869   moreover
   870   {assume z: "?g \<noteq> 0"
   871     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   872     from nat_gcd_coprime_exists[OF z]
   873     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   874       by blast
   875     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   876       by (simp add: ab'(1,2)[symmetric])
   877     hence "?g^n*a'^n dvd ?g^n *b'^n"
   878       by (simp only: power_mult_distrib mult_commute)
   879     with zn z n have th0:"a'^n dvd b'^n" by auto
   880     have "a' dvd a'^n" by (simp add: m)
   881     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   882     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   883     from nat_coprime_dvd_mult[OF nat_coprime_exp [OF ab'(3), of m]] th1
   884     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   885     hence "a'*?g dvd b'*?g" by simp
   886     with ab'(1,2)  have ?thesis by simp }
   887   ultimately show ?thesis by blast
   888 qed
   889 
   890 lemma int_pow_divides_pow:
   891   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
   892   shows "a dvd b"
   893 proof-
   894   let ?g = "gcd a b"
   895   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   896   {assume "?g = 0" with ab n have ?thesis by auto }
   897   moreover
   898   {assume z: "?g \<noteq> 0"
   899     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   900     from int_gcd_coprime_exists[OF z]
   901     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   902       by blast
   903     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   904       by (simp add: ab'(1,2)[symmetric])
   905     hence "?g^n*a'^n dvd ?g^n *b'^n"
   906       by (simp only: power_mult_distrib mult_commute)
   907     with zn z n have th0:"a'^n dvd b'^n" by auto
   908     have "a' dvd a'^n" by (simp add: m)
   909     with th0 have "a' dvd b'^n"
   910       using dvd_trans[of a' "a'^n" "b'^n"] by simp
   911     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   912     from int_coprime_dvd_mult[OF int_coprime_exp [OF ab'(3), of m]] th1
   913     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   914     hence "a'*?g dvd b'*?g" by simp
   915     with ab'(1,2)  have ?thesis by simp }
   916   ultimately show ?thesis by blast
   917 qed
   918 
   919 (* FIXME move to Divides(?) *)
   920 lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   921   by (auto intro: nat_pow_divides_pow dvd_power_same)
   922 
   923 lemma int_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   924   by (auto intro: int_pow_divides_pow dvd_power_same)
   925 
   926 lemma nat_divides_mult:
   927   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   928   shows "m * n dvd r"
   929 proof-
   930   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   931     unfolding dvd_def by blast
   932   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   933   hence "m dvd n'" using nat_coprime_dvd_mult_iff[OF mn] by simp
   934   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   935   from n' k show ?thesis unfolding dvd_def by auto
   936 qed
   937 
   938 lemma int_divides_mult:
   939   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   940   shows "m * n dvd r"
   941 proof-
   942   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   943     unfolding dvd_def by blast
   944   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   945   hence "m dvd n'" using int_coprime_dvd_mult_iff[OF mn] by simp
   946   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   947   from n' k show ?thesis unfolding dvd_def by auto
   948 qed
   949 
   950 lemma nat_coprime_plus_one [simp]: "coprime ((n::nat) + 1) n"
   951   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   952   apply force
   953   apply (rule nat_dvd_diff)
   954   apply auto
   955 done
   956 
   957 lemma nat_coprime_Suc [simp]: "coprime (Suc n) n"
   958   using nat_coprime_plus_one by (simp add: One_nat_def)
   959 
   960 lemma int_coprime_plus_one [simp]: "coprime ((n::int) + 1) n"
   961   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   962   apply force
   963   apply (rule dvd_diff)
   964   apply auto
   965 done
   966 
   967 lemma nat_coprime_minus_one: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   968   using nat_coprime_plus_one [of "n - 1"]
   969     nat_gcd_commute [of "n - 1" n] by auto
   970 
   971 lemma int_coprime_minus_one: "coprime ((n::int) - 1) n"
   972   using int_coprime_plus_one [of "n - 1"]
   973     int_gcd_commute [of "n - 1" n] by auto
   974 
   975 lemma nat_setprod_coprime [rule_format]:
   976     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
   977   apply (case_tac "finite A")
   978   apply (induct set: finite)
   979   apply (auto simp add: nat_gcd_mult_cancel)
   980 done
   981 
   982 lemma int_setprod_coprime [rule_format]:
   983     "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
   984   apply (case_tac "finite A")
   985   apply (induct set: finite)
   986   apply (auto simp add: int_gcd_mult_cancel)
   987 done
   988 
   989 lemma nat_prime_odd: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   990   unfolding prime_nat_def
   991   apply (subst even_mult_two_ex)
   992   apply clarify
   993   apply (drule_tac x = 2 in spec)
   994   apply auto
   995 done
   996 
   997 lemma int_prime_odd: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   998   unfolding prime_int_def
   999   apply (frule nat_prime_odd)
  1000   apply (auto simp add: even_nat_def)
  1001 done
  1002 
  1003 lemma nat_coprime_common_divisor: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1004     x dvd b \<Longrightarrow> x = 1"
  1005   apply (subgoal_tac "x dvd gcd a b")
  1006   apply simp
  1007   apply (erule (1) nat_gcd_greatest)
  1008 done
  1009 
  1010 lemma int_coprime_common_divisor: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1011     x dvd b \<Longrightarrow> abs x = 1"
  1012   apply (subgoal_tac "x dvd gcd a b")
  1013   apply simp
  1014   apply (erule (1) int_gcd_greatest)
  1015 done
  1016 
  1017 lemma nat_coprime_divisors: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
  1018     coprime d e"
  1019   apply (auto simp add: dvd_def)
  1020   apply (frule int_coprime_lmult)
  1021   apply (subst int_gcd_commute)
  1022   apply (subst (asm) (2) int_gcd_commute)
  1023   apply (erule int_coprime_lmult)
  1024 done
  1025 
  1026 lemma nat_invertible_coprime: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1027 apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red)
  1028 done
  1029 
  1030 lemma int_invertible_coprime: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1031 apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red)
  1032 done
  1033 
  1034 
  1035 subsection {* Bezout's theorem *}
  1036 
  1037 (* Function bezw returns a pair of witnesses to Bezout's theorem --
  1038    see the theorems that follow the definition. *)
  1039 fun
  1040   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1041 where
  1042   "bezw x y =
  1043   (if y = 0 then (1, 0) else
  1044       (snd (bezw y (x mod y)),
  1045        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1046 
  1047 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1048 
  1049 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1050        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1051   by simp
  1052 
  1053 declare bezw.simps [simp del]
  1054 
  1055 lemma bezw_aux [rule_format]:
  1056     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1057 proof (induct x y rule: nat_gcd_induct)
  1058   fix m :: nat
  1059   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1060     by auto
  1061   next fix m :: nat and n
  1062     assume ngt0: "n > 0" and
  1063       ih: "fst (bezw n (m mod n)) * int n +
  1064         snd (bezw n (m mod n)) * int (m mod n) =
  1065         int (gcd n (m mod n))"
  1066     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1067       apply (simp add: bezw_non_0 nat_gcd_non_0)
  1068       apply (erule subst)
  1069       apply (simp add: ring_simps)
  1070       apply (subst mod_div_equality [of m n, symmetric])
  1071       (* applying simp here undoes the last substitution!
  1072          what is procedure cancel_div_mod? *)
  1073       apply (simp only: ring_simps zadd_int [symmetric]
  1074         zmult_int [symmetric])
  1075       done
  1076 qed
  1077 
  1078 lemma int_bezout:
  1079   fixes x y
  1080   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1081 proof -
  1082   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1083       EX u v. u * x + v * y = gcd x y"
  1084     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1085     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1086     apply (unfold gcd_int_def)
  1087     apply simp
  1088     apply (subst bezw_aux [symmetric])
  1089     apply auto
  1090     done
  1091   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1092       (x \<le> 0 \<and> y \<le> 0)"
  1093     by auto
  1094   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1095     by (erule (1) bezout_aux)
  1096   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1097     apply (insert bezout_aux [of x "-y"])
  1098     apply auto
  1099     apply (rule_tac x = u in exI)
  1100     apply (rule_tac x = "-v" in exI)
  1101     apply (subst int_gcd_neg2 [symmetric])
  1102     apply auto
  1103     done
  1104   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1105     apply (insert bezout_aux [of "-x" y])
  1106     apply auto
  1107     apply (rule_tac x = "-u" in exI)
  1108     apply (rule_tac x = v in exI)
  1109     apply (subst int_gcd_neg1 [symmetric])
  1110     apply auto
  1111     done
  1112   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1113     apply (insert bezout_aux [of "-x" "-y"])
  1114     apply auto
  1115     apply (rule_tac x = "-u" in exI)
  1116     apply (rule_tac x = "-v" in exI)
  1117     apply (subst int_gcd_neg1 [symmetric])
  1118     apply (subst int_gcd_neg2 [symmetric])
  1119     apply auto
  1120     done
  1121   ultimately show ?thesis by blast
  1122 qed
  1123 
  1124 text {* versions of Bezout for nat, by Amine Chaieb *}
  1125 
  1126 lemma ind_euclid:
  1127   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1128   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1129   shows "P a b"
  1130 proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
  1131   fix n a b
  1132   assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
  1133   have "a = b \<or> a < b \<or> b < a" by arith
  1134   moreover {assume eq: "a= b"
  1135     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1136     by simp}
  1137   moreover
  1138   {assume lt: "a < b"
  1139     hence "a + b - a < n \<or> a = 0"  using H(2) by arith
  1140     moreover
  1141     {assume "a =0" with z c have "P a b" by blast }
  1142     moreover
  1143     {assume ab: "a + b - a < n"
  1144       have th0: "a + b - a = a + (b - a)" using lt by arith
  1145       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1146       have "P a b" by (simp add: th0[symmetric])}
  1147     ultimately have "P a b" by blast}
  1148   moreover
  1149   {assume lt: "a > b"
  1150     hence "b + a - b < n \<or> b = 0"  using H(2) by arith
  1151     moreover
  1152     {assume "b =0" with z c have "P a b" by blast }
  1153     moreover
  1154     {assume ab: "b + a - b < n"
  1155       have th0: "b + a - b = b + (a - b)" using lt by arith
  1156       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1157       have "P b a" by (simp add: th0[symmetric])
  1158       hence "P a b" using c by blast }
  1159     ultimately have "P a b" by blast}
  1160 ultimately  show "P a b" by blast
  1161 qed
  1162 
  1163 lemma nat_bezout_lemma:
  1164   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1165     (a * x = b * y + d \<or> b * x = a * y + d)"
  1166   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1167     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1168   using ex
  1169   apply clarsimp
  1170   apply (rule_tac x="d" in exI, simp add: dvd_add)
  1171   apply (case_tac "a * x = b * y + d" , simp_all)
  1172   apply (rule_tac x="x + y" in exI)
  1173   apply (rule_tac x="y" in exI)
  1174   apply algebra
  1175   apply (rule_tac x="x" in exI)
  1176   apply (rule_tac x="x + y" in exI)
  1177   apply algebra
  1178 done
  1179 
  1180 lemma nat_bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1181     (a * x = b * y + d \<or> b * x = a * y + d)"
  1182   apply(induct a b rule: ind_euclid)
  1183   apply blast
  1184   apply clarify
  1185   apply (rule_tac x="a" in exI, simp add: dvd_add)
  1186   apply clarsimp
  1187   apply (rule_tac x="d" in exI)
  1188   apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  1189   apply (rule_tac x="x+y" in exI)
  1190   apply (rule_tac x="y" in exI)
  1191   apply algebra
  1192   apply (rule_tac x="x" in exI)
  1193   apply (rule_tac x="x+y" in exI)
  1194   apply algebra
  1195 done
  1196 
  1197 lemma nat_bezout1: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1198     (a * x - b * y = d \<or> b * x - a * y = d)"
  1199   using nat_bezout_add[of a b]
  1200   apply clarsimp
  1201   apply (rule_tac x="d" in exI, simp)
  1202   apply (rule_tac x="x" in exI)
  1203   apply (rule_tac x="y" in exI)
  1204   apply auto
  1205 done
  1206 
  1207 lemma nat_bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
  1208   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1209 proof-
  1210  from nz have ap: "a > 0" by simp
  1211  from nat_bezout_add[of a b]
  1212  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1213    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1214  moreover
  1215     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1216      from H have ?thesis by blast }
  1217  moreover
  1218  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1219    {assume b0: "b = 0" with H  have ?thesis by simp}
  1220    moreover
  1221    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1222      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1223        by auto
  1224      moreover
  1225      {assume db: "d=b"
  1226        from prems have ?thesis apply simp
  1227 	 apply (rule exI[where x = b], simp)
  1228 	 apply (rule exI[where x = b])
  1229 	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1230     moreover
  1231     {assume db: "d < b"
  1232 	{assume "x=0" hence ?thesis  using prems by simp }
  1233 	moreover
  1234 	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1235 	  from db have "d \<le> b - 1" by simp
  1236 	  hence "d*b \<le> b*(b - 1)" by simp
  1237 	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1238 	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1239 	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1240             by simp
  1241 	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1242 	    by (simp only: mult_assoc right_distrib)
  1243 	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1244             by algebra
  1245 	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1246 	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1247 	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1248 	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1249 	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
  1250 	  hence ?thesis using H(1,2)
  1251 	    apply -
  1252 	    apply (rule exI[where x=d], simp)
  1253 	    apply (rule exI[where x="(b - 1) * y"])
  1254 	    by (rule exI[where x="x*(b - 1) - d"], simp)}
  1255 	ultimately have ?thesis by blast}
  1256     ultimately have ?thesis by blast}
  1257   ultimately have ?thesis by blast}
  1258  ultimately show ?thesis by blast
  1259 qed
  1260 
  1261 lemma nat_bezout: assumes a: "(a::nat) \<noteq> 0"
  1262   shows "\<exists>x y. a * x = b * y + gcd a b"
  1263 proof-
  1264   let ?g = "gcd a b"
  1265   from nat_bezout_add_strong[OF a, of b]
  1266   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1267   from d(1,2) have "d dvd ?g" by simp
  1268   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1269   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1270   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1271   thus ?thesis by blast
  1272 qed
  1273 
  1274 
  1275 subsection {* LCM *}
  1276 
  1277 lemma int_lcm_altdef: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1278   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1279     zmult_int [symmetric] gcd_int_def)
  1280 
  1281 lemma nat_prod_gcd_lcm: "(m::nat) * n = gcd m n * lcm m n"
  1282   unfolding lcm_nat_def
  1283   by (simp add: dvd_mult_div_cancel [OF nat_gcd_dvd_prod])
  1284 
  1285 lemma int_prod_gcd_lcm: "abs(m::int) * abs n = gcd m n * lcm m n"
  1286   unfolding lcm_int_def gcd_int_def
  1287   apply (subst int_mult [symmetric])
  1288   apply (subst nat_prod_gcd_lcm [symmetric])
  1289   apply (subst nat_abs_mult_distrib [symmetric])
  1290   apply (simp, simp add: abs_mult)
  1291 done
  1292 
  1293 lemma nat_lcm_0 [simp]: "lcm (m::nat) 0 = 0"
  1294   unfolding lcm_nat_def by simp
  1295 
  1296 lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0"
  1297   unfolding lcm_int_def by simp
  1298 
  1299 lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0"
  1300   unfolding lcm_nat_def by simp
  1301 
  1302 lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0"
  1303   unfolding lcm_int_def by simp
  1304 
  1305 lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m"
  1306   unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps)
  1307 
  1308 lemma int_lcm_commute: "lcm (m::int) n = lcm n m"
  1309   unfolding lcm_int_def by (subst nat_lcm_commute, rule refl)
  1310 
  1311 
  1312 lemma nat_lcm_pos:
  1313   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1314 by (metis gr0I mult_is_0 nat_prod_gcd_lcm)
  1315 
  1316 lemma int_lcm_pos:
  1317   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1318   apply (subst int_lcm_abs)
  1319   apply (rule nat_lcm_pos [transferred])
  1320   apply auto
  1321 done
  1322 
  1323 lemma nat_dvd_pos:
  1324   fixes n m :: nat
  1325   assumes "n > 0" and "m dvd n"
  1326   shows "m > 0"
  1327 using assms by (cases m) auto
  1328 
  1329 lemma nat_lcm_least:
  1330   assumes "(m::nat) dvd k" and "n dvd k"
  1331   shows "lcm m n dvd k"
  1332 proof (cases k)
  1333   case 0 then show ?thesis by auto
  1334 next
  1335   case (Suc _) then have pos_k: "k > 0" by auto
  1336   from assms nat_dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1337   with nat_gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
  1338   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1339   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1340   from pos_k k_m have pos_p: "p > 0" by auto
  1341   from pos_k k_n have pos_q: "q > 0" by auto
  1342   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1343     by (simp add: mult_ac nat_gcd_mult_distrib)
  1344   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1345     by (simp add: k_m [symmetric] k_n [symmetric])
  1346   also have "\<dots> = k * p * q * gcd m n"
  1347     by (simp add: mult_ac nat_gcd_mult_distrib)
  1348   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1349     by (simp only: k_m [symmetric] k_n [symmetric])
  1350   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1351     by (simp add: mult_ac)
  1352   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1353     by simp
  1354   with nat_prod_gcd_lcm [of m n]
  1355   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1356     by (simp add: mult_ac)
  1357   with pos_gcd have "lcm m n * gcd q p = k" by auto
  1358   then show ?thesis using dvd_def by auto
  1359 qed
  1360 
  1361 lemma int_lcm_least:
  1362   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1363 apply (subst int_lcm_abs)
  1364 apply (rule dvd_trans)
  1365 apply (rule nat_lcm_least [transferred, of _ "abs k" _])
  1366 apply auto
  1367 done
  1368 
  1369 lemma nat_lcm_dvd1: "(m::nat) dvd lcm m n"
  1370 proof (cases m)
  1371   case 0 then show ?thesis by simp
  1372 next
  1373   case (Suc _)
  1374   then have mpos: "m > 0" by simp
  1375   show ?thesis
  1376   proof (cases n)
  1377     case 0 then show ?thesis by simp
  1378   next
  1379     case (Suc _)
  1380     then have npos: "n > 0" by simp
  1381     have "gcd m n dvd n" by simp
  1382     then obtain k where "n = gcd m n * k" using dvd_def by auto
  1383     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1384       by (simp add: mult_ac)
  1385     also have "\<dots> = m * k" using mpos npos nat_gcd_zero by simp
  1386     finally show ?thesis by (simp add: lcm_nat_def)
  1387   qed
  1388 qed
  1389 
  1390 lemma int_lcm_dvd1: "(m::int) dvd lcm m n"
  1391   apply (subst int_lcm_abs)
  1392   apply (rule dvd_trans)
  1393   prefer 2
  1394   apply (rule nat_lcm_dvd1 [transferred])
  1395   apply auto
  1396 done
  1397 
  1398 lemma nat_lcm_dvd2: "(n::nat) dvd lcm m n"
  1399   by (subst nat_lcm_commute, rule nat_lcm_dvd1)
  1400 
  1401 lemma int_lcm_dvd2: "(n::int) dvd lcm m n"
  1402   by (subst int_lcm_commute, rule int_lcm_dvd1)
  1403 
  1404 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1405 by(metis nat_lcm_dvd1 dvd_trans)
  1406 
  1407 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1408 by(metis nat_lcm_dvd2 dvd_trans)
  1409 
  1410 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1411 by(metis int_lcm_dvd1 dvd_trans)
  1412 
  1413 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1414 by(metis int_lcm_dvd2 dvd_trans)
  1415 
  1416 lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and>
  1417     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1418   by (auto intro: dvd_anti_sym nat_lcm_least nat_lcm_dvd1 nat_lcm_dvd2)
  1419 
  1420 lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1421     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1422   by (auto intro: dvd_anti_sym [transferred] int_lcm_least)
  1423 
  1424 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1425   apply (rule sym)
  1426   apply (subst nat_lcm_unique [symmetric])
  1427   apply auto
  1428 done
  1429 
  1430 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1431   apply (rule sym)
  1432   apply (subst int_lcm_unique [symmetric])
  1433   apply auto
  1434 done
  1435 
  1436 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1437 by (subst nat_lcm_commute, erule lcm_proj2_if_dvd_nat)
  1438 
  1439 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1440 by (subst int_lcm_commute, erule lcm_proj2_if_dvd_int)
  1441 
  1442 
  1443 lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
  1444 apply(rule nat_lcm_unique[THEN iffD1])
  1445 apply (metis dvd.order_trans nat_lcm_unique)
  1446 done
  1447 
  1448 lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
  1449 apply(rule int_lcm_unique[THEN iffD1])
  1450 apply (metis dvd_trans int_lcm_unique)
  1451 done
  1452 
  1453 lemmas lcm_left_commute_nat =
  1454   mk_left_commute[of lcm, OF lcm_assoc_nat nat_lcm_commute]
  1455 
  1456 lemmas lcm_left_commute_int =
  1457   mk_left_commute[of lcm, OF lcm_assoc_int int_lcm_commute]
  1458 
  1459 lemmas lcm_ac_nat = lcm_assoc_nat nat_lcm_commute lcm_left_commute_nat
  1460 lemmas lcm_ac_int = lcm_assoc_int int_lcm_commute lcm_left_commute_int
  1461 
  1462 
  1463 subsection {* Primes *}
  1464 
  1465 (* Is there a better way to handle these, rather than making them
  1466    elim rules? *)
  1467 
  1468 lemma nat_prime_ge_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
  1469   by (unfold prime_nat_def, auto)
  1470 
  1471 lemma nat_prime_gt_0 [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
  1472   by (unfold prime_nat_def, auto)
  1473 
  1474 lemma nat_prime_ge_1 [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
  1475   by (unfold prime_nat_def, auto)
  1476 
  1477 lemma nat_prime_gt_1 [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
  1478   by (unfold prime_nat_def, auto)
  1479 
  1480 lemma nat_prime_ge_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
  1481   by (unfold prime_nat_def, auto)
  1482 
  1483 lemma nat_prime_gt_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
  1484   by (unfold prime_nat_def, auto)
  1485 
  1486 lemma nat_prime_ge_2 [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
  1487   by (unfold prime_nat_def, auto)
  1488 
  1489 lemma int_prime_ge_0 [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
  1490   by (unfold prime_int_def prime_nat_def, auto)
  1491 
  1492 lemma int_prime_gt_0 [elim]: "prime (p::int) \<Longrightarrow> p > 0"
  1493   by (unfold prime_int_def prime_nat_def, auto)
  1494 
  1495 lemma int_prime_ge_1 [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
  1496   by (unfold prime_int_def prime_nat_def, auto)
  1497 
  1498 lemma int_prime_gt_1 [elim]: "prime (p::int) \<Longrightarrow> p > 1"
  1499   by (unfold prime_int_def prime_nat_def, auto)
  1500 
  1501 lemma int_prime_ge_2 [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
  1502   by (unfold prime_int_def prime_nat_def, auto)
  1503 
  1504 thm prime_nat_def;
  1505 thm prime_nat_def [transferred];
  1506 
  1507 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
  1508     m = 1 \<or> m = p))"
  1509   using prime_nat_def [transferred]
  1510     apply (case_tac "p >= 0")
  1511     by (blast, auto simp add: int_prime_ge_0)
  1512 
  1513 (* To do: determine primality of any numeral *)
  1514 
  1515 lemma nat_zero_not_prime [simp]: "~prime (0::nat)"
  1516   by (simp add: prime_nat_def)
  1517 
  1518 lemma int_zero_not_prime [simp]: "~prime (0::int)"
  1519   by (simp add: prime_int_def)
  1520 
  1521 lemma nat_one_not_prime [simp]: "~prime (1::nat)"
  1522   by (simp add: prime_nat_def)
  1523 
  1524 lemma nat_Suc_0_not_prime [simp]: "~prime (Suc 0)"
  1525   by (simp add: prime_nat_def One_nat_def)
  1526 
  1527 lemma int_one_not_prime [simp]: "~prime (1::int)"
  1528   by (simp add: prime_int_def)
  1529 
  1530 lemma nat_two_is_prime [simp]: "prime (2::nat)"
  1531   apply (auto simp add: prime_nat_def)
  1532   apply (case_tac m)
  1533   apply (auto dest!: dvd_imp_le)
  1534   done
  1535 
  1536 lemma int_two_is_prime [simp]: "prime (2::int)"
  1537   by (rule nat_two_is_prime [transferred direction: nat "op <= (0::int)"])
  1538 
  1539 lemma nat_prime_imp_coprime: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1540   apply (unfold prime_nat_def)
  1541   apply (metis nat_gcd_dvd1 nat_gcd_dvd2)
  1542   done
  1543 
  1544 lemma int_prime_imp_coprime: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1545   apply (unfold prime_int_altdef)
  1546   apply (metis int_gcd_dvd1 int_gcd_dvd2 int_gcd_ge_0)
  1547   done
  1548 
  1549 lemma nat_prime_dvd_mult: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1550   by (blast intro: nat_coprime_dvd_mult nat_prime_imp_coprime)
  1551 
  1552 lemma int_prime_dvd_mult: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1553   by (blast intro: int_coprime_dvd_mult int_prime_imp_coprime)
  1554 
  1555 lemma nat_prime_dvd_mult_eq [simp]: "prime (p::nat) \<Longrightarrow>
  1556     p dvd m * n = (p dvd m \<or> p dvd n)"
  1557   by (rule iffI, rule nat_prime_dvd_mult, auto)
  1558 
  1559 lemma int_prime_dvd_mult_eq [simp]: "prime (p::int) \<Longrightarrow>
  1560     p dvd m * n = (p dvd m \<or> p dvd n)"
  1561   by (rule iffI, rule int_prime_dvd_mult, auto)
  1562 
  1563 lemma nat_not_prime_eq_prod: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1564     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1565   unfolding prime_nat_def dvd_def apply auto
  1566   apply (subgoal_tac "k > 1")
  1567   apply force
  1568   apply (subgoal_tac "k ~= 0")
  1569   apply force
  1570   apply (rule notI)
  1571   apply force
  1572 done
  1573 
  1574 (* there's a lot of messing around with signs of products here --
  1575    could this be made more automatic? *)
  1576 lemma int_not_prime_eq_prod: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1577     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1578   unfolding prime_int_altdef dvd_def
  1579   apply auto
  1580   apply (rule_tac x = m in exI)
  1581   apply (rule_tac x = k in exI)
  1582   apply (auto simp add: mult_compare_simps)
  1583   apply (subgoal_tac "k > 0")
  1584   apply arith
  1585   apply (case_tac "k <= 0")
  1586   apply (subgoal_tac "m * k <= 0")
  1587   apply force
  1588   apply (subst zero_compare_simps(8))
  1589   apply auto
  1590   apply (subgoal_tac "m * k <= 0")
  1591   apply force
  1592   apply (subst zero_compare_simps(8))
  1593   apply auto
  1594 done
  1595 
  1596 lemma nat_prime_dvd_power [rule_format]: "prime (p::nat) -->
  1597     n > 0 --> (p dvd x^n --> p dvd x)"
  1598   by (induct n rule: nat_induct, auto)
  1599 
  1600 lemma int_prime_dvd_power [rule_format]: "prime (p::int) -->
  1601     n > 0 --> (p dvd x^n --> p dvd x)"
  1602   apply (induct n rule: nat_induct, auto)
  1603   apply (frule int_prime_ge_0)
  1604   apply auto
  1605 done
  1606 
  1607 lemma nat_prime_imp_power_coprime: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1608     coprime a (p^m)"
  1609   apply (rule nat_coprime_exp)
  1610   apply (subst nat_gcd_commute)
  1611   apply (erule (1) nat_prime_imp_coprime)
  1612 done
  1613 
  1614 lemma int_prime_imp_power_coprime: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1615     coprime a (p^m)"
  1616   apply (rule int_coprime_exp)
  1617   apply (subst int_gcd_commute)
  1618   apply (erule (1) int_prime_imp_coprime)
  1619 done
  1620 
  1621 lemma nat_primes_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1622   apply (rule nat_prime_imp_coprime, assumption)
  1623   apply (unfold prime_nat_def, auto)
  1624 done
  1625 
  1626 lemma int_primes_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1627   apply (rule int_prime_imp_coprime, assumption)
  1628   apply (unfold prime_int_altdef, clarify)
  1629   apply (drule_tac x = q in spec)
  1630   apply (drule_tac x = p in spec)
  1631   apply auto
  1632 done
  1633 
  1634 lemma nat_primes_imp_powers_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1635     coprime (p^m) (q^n)"
  1636   by (rule nat_coprime_exp2, rule nat_primes_coprime)
  1637 
  1638 lemma int_primes_imp_powers_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1639     coprime (p^m) (q^n)"
  1640   by (rule int_coprime_exp2, rule int_primes_coprime)
  1641 
  1642 lemma nat_prime_factor: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
  1643   apply (induct n rule: nat_less_induct)
  1644   apply (case_tac "n = 0")
  1645   using nat_two_is_prime apply blast
  1646   apply (case_tac "prime n")
  1647   apply blast
  1648   apply (subgoal_tac "n > 1")
  1649   apply (frule (1) nat_not_prime_eq_prod)
  1650   apply (auto intro: dvd_mult dvd_mult2)
  1651 done
  1652 
  1653 (* An Isar version:
  1654 
  1655 lemma nat_prime_factor_b:
  1656   fixes n :: nat
  1657   assumes "n \<noteq> 1"
  1658   shows "\<exists>p. prime p \<and> p dvd n"
  1659 
  1660 using `n ~= 1`
  1661 proof (induct n rule: nat_less_induct)
  1662   fix n :: nat
  1663   assume "n ~= 1" and
  1664     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
  1665   thus "\<exists>p. prime p \<and> p dvd n"
  1666   proof -
  1667   {
  1668     assume "n = 0"
  1669     moreover note nat_two_is_prime
  1670     ultimately have ?thesis
  1671       by (auto simp del: nat_two_is_prime)
  1672   }
  1673   moreover
  1674   {
  1675     assume "prime n"
  1676     hence ?thesis by auto
  1677   }
  1678   moreover
  1679   {
  1680     assume "n ~= 0" and "~ prime n"
  1681     with `n ~= 1` have "n > 1" by auto
  1682     with `~ prime n` and nat_not_prime_eq_prod obtain m k where
  1683       "n = m * k" and "1 < m" and "m < n" by blast
  1684     with ih obtain p where "prime p" and "p dvd m" by blast
  1685     with `n = m * k` have ?thesis by auto
  1686   }
  1687   ultimately show ?thesis by blast
  1688   qed
  1689 qed
  1690 
  1691 *)
  1692 
  1693 text {* One property of coprimality is easier to prove via prime factors. *}
  1694 
  1695 lemma nat_prime_divprod_pow:
  1696   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
  1697   shows "p^n dvd a \<or> p^n dvd b"
  1698 proof-
  1699   {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
  1700       apply (cases "n=0", simp_all)
  1701       apply (cases "a=1", simp_all) done}
  1702   moreover
  1703   {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
  1704     then obtain m where m: "n = Suc m" by (cases n, auto)
  1705     from n have "p dvd p^n" by (intro dvd_power, auto)
  1706     also note pab
  1707     finally have pab': "p dvd a * b".
  1708     from nat_prime_dvd_mult[OF p pab']
  1709     have "p dvd a \<or> p dvd b" .
  1710     moreover
  1711     {assume pa: "p dvd a"
  1712       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1713       from nat_coprime_common_divisor [OF ab, OF pa] p have "\<not> p dvd b" by auto
  1714       with p have "coprime b p"
  1715         by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
  1716       hence pnb: "coprime (p^n) b"
  1717         by (subst nat_gcd_commute, rule nat_coprime_exp)
  1718       from nat_coprime_divprod[OF pnba pnb] have ?thesis by blast }
  1719     moreover
  1720     {assume pb: "p dvd b"
  1721       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1722       from nat_coprime_common_divisor [OF ab, of p] pb p have "\<not> p dvd a"
  1723         by auto
  1724       with p have "coprime a p"
  1725         by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
  1726       hence pna: "coprime (p^n) a"
  1727         by (subst nat_gcd_commute, rule nat_coprime_exp)
  1728       from nat_coprime_divprod[OF pab pna] have ?thesis by blast }
  1729     ultimately have ?thesis by blast}
  1730   ultimately show ?thesis by blast
  1731 qed
  1732 
  1733 end