src/HOL/GCD.thy
author nipkow
Sun Jul 12 10:14:51 2009 +0200 (2009-07-12)
changeset 31992 f8aed98faae7
parent 31952 40501bb2d57c
child 31995 8f37cf60b885
permissions -rw-r--r--
More about gcd/lcm, and some cleaning up
     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 = zero + one + dvd +
    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 gcd_nat_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 gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
   179   by (simp add: gcd_int_def)
   180 
   181 lemma gcd_neg2_int [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 gcd_abs_int: "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 gcd_abs_int)
   192 
   193 lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
   194 by (metis abs_idempotent gcd_abs_int)
   195 
   196 lemma gcd_cases_int:
   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: gcd_neg1_int gcd_neg2_int, arith)
   204 
   205 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   206   by (simp add: gcd_int_def)
   207 
   208 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
   209   by (simp add: lcm_int_def)
   210 
   211 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
   212   by (simp add: lcm_int_def)
   213 
   214 lemma lcm_abs_int: "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 lcm_cases_int:
   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: lcm_neg1_int lcm_neg2_int, arith)
   234 
   235 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   236   by (simp add: lcm_int_def)
   237 
   238 (* was gcd_0, etc. *)
   239 lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
   240   by simp
   241 
   242 (* was igcd_0, etc. *)
   243 lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
   244   by (unfold gcd_int_def, auto)
   245 
   246 lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
   247   by simp
   248 
   249 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
   250   by (unfold gcd_int_def, auto)
   251 
   252 lemma gcd_red_nat: "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 gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   258   by simp
   259 
   260 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   261   by simp
   262 
   263 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   264   by (simp add: One_nat_def)
   265 
   266 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   267   by (simp add: gcd_int_def)
   268 
   269 lemma gcd_idem_nat: "gcd (x::nat) x = x"
   270 by simp
   271 
   272 lemma gcd_idem_int: "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 gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
   283   and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
   284   apply (induct m n rule: gcd_nat_induct)
   285   apply (simp_all add: gcd_non_0_nat)
   286   apply (blast dest: dvd_mod_imp_dvd)
   287 done
   288 
   289 lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"
   290 by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)
   291 
   292 lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"
   293 by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)
   294 
   295 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   296 by(metis gcd_dvd1_nat dvd_trans)
   297 
   298 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   299 by(metis gcd_dvd2_nat dvd_trans)
   300 
   301 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   302 by(metis gcd_dvd1_int dvd_trans)
   303 
   304 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   305 by(metis gcd_dvd2_int dvd_trans)
   306 
   307 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   308   by (rule dvd_imp_le, auto)
   309 
   310 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   311   by (rule dvd_imp_le, auto)
   312 
   313 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   314   by (rule zdvd_imp_le, auto)
   315 
   316 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   317   by (rule zdvd_imp_le, auto)
   318 
   319 lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   320 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
   321 
   322 lemma gcd_greatest_int:
   323   "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   324   apply (subst gcd_abs_int)
   325   apply (subst abs_dvd_iff [symmetric])
   326   apply (rule gcd_greatest_nat [transferred])
   327   apply auto
   328 done
   329 
   330 lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
   331     (k dvd m & k dvd n)"
   332   by (blast intro!: gcd_greatest_nat intro: dvd_trans)
   333 
   334 lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   335   by (blast intro!: gcd_greatest_int intro: dvd_trans)
   336 
   337 lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   338   by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
   339 
   340 lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   341   by (auto simp add: gcd_int_def)
   342 
   343 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   344   by (insert gcd_zero_nat [of m n], arith)
   345 
   346 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   347   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
   348 
   349 lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
   350   by (rule dvd_anti_sym, auto)
   351 
   352 lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
   353   by (auto simp add: gcd_int_def gcd_commute_nat)
   354 
   355 lemma gcd_assoc_nat: "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 gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
   361   by (auto simp add: gcd_int_def gcd_assoc_nat)
   362 
   363 lemmas gcd_left_commute_nat =
   364   mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat]
   365 
   366 lemmas gcd_left_commute_int =
   367   mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int]
   368 
   369 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
   370   -- {* gcd is an AC-operator *}
   371 
   372 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
   373 
   374 lemma gcd_unique_nat: "(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) gcd_greatest_nat)
   379   apply auto
   380 done
   381 
   382 lemma gcd_unique_int: "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 gcd_pos_int)
   390   apply clarsimp
   391   apply (drule_tac x = "d + 1" in spec)
   392   apply (frule zdvd_imp_le)
   393   apply (auto intro: gcd_greatest_int)
   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 gcd_unique_nat)
   398 
   399 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   400 by (metis dvd.eq_iff gcd_unique_nat)
   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 gcd_0_left_int gcd_abs_int gcd_unique_int)
   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 gcd_commute_int)
   407 
   408 
   409 text {*
   410   \medskip Multiplication laws
   411 *}
   412 
   413 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   414     -- {* \cite[page 27]{davenport92} *}
   415   apply (induct m n rule: gcd_nat_induct)
   416   apply simp
   417   apply (case_tac "k = 0")
   418   apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
   419 done
   420 
   421 lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   422   apply (subst (1 2) gcd_abs_int)
   423   apply (subst (1 2) abs_mult)
   424   apply (rule gcd_mult_distrib_nat [transferred])
   425   apply auto
   426 done
   427 
   428 lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   429   apply (insert gcd_mult_distrib_nat [of m k n])
   430   apply simp
   431   apply (erule_tac t = m in ssubst)
   432   apply simp
   433   done
   434 
   435 lemma coprime_dvd_mult_int:
   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) gcd_abs_int)
   440 apply (rule coprime_dvd_mult_nat [transferred])
   441     prefer 4 apply assumption
   442    apply auto
   443 apply (subst abs_mult [symmetric], auto)
   444 done
   445 
   446 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   447     (k dvd m * n) = (k dvd m)"
   448   by (auto intro: coprime_dvd_mult_nat)
   449 
   450 lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   451     (k dvd m * n) = (k dvd m)"
   452   by (auto intro: coprime_dvd_mult_int)
   453 
   454 lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   455   apply (rule dvd_anti_sym)
   456   apply (rule gcd_greatest_nat)
   457   apply (rule_tac n = k in coprime_dvd_mult_nat)
   458   apply (simp add: gcd_assoc_nat)
   459   apply (simp add: gcd_commute_nat)
   460   apply (simp_all add: mult_commute)
   461 done
   462 
   463 lemma gcd_mult_cancel_int:
   464   "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
   465 apply (subst (1 2) gcd_abs_int)
   466 apply (subst abs_mult)
   467 apply (rule gcd_mult_cancel_nat [transferred], auto)
   468 done
   469 
   470 text {* \medskip Addition laws *}
   471 
   472 lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   473   apply (case_tac "n = 0")
   474   apply (simp_all add: gcd_non_0_nat)
   475 done
   476 
   477 lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   478   apply (subst (1 2) gcd_commute_nat)
   479   apply (subst add_commute)
   480   apply simp
   481 done
   482 
   483 (* to do: add the other variations? *)
   484 
   485 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   486   by (subst gcd_add1_nat [symmetric], auto)
   487 
   488 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   489   apply (subst gcd_commute_nat)
   490   apply (subst gcd_diff1_nat [symmetric])
   491   apply auto
   492   apply (subst gcd_commute_nat)
   493   apply (subst gcd_diff1_nat)
   494   apply assumption
   495   apply (rule gcd_commute_nat)
   496 done
   497 
   498 lemma gcd_non_0_int: "(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: gcd_non_0_nat nat_mod_distrib [symmetric]
   502     zmod_zminus1_eq_if)
   503   apply (frule_tac a = x in pos_mod_bound)
   504   apply (subst (1 2) gcd_commute_nat)
   505   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   506     nat_le_eq_zle)
   507 done
   508 
   509 lemma gcd_red_int: "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 gcd_non_0_int, auto)
   514   apply (insert gcd_non_0_int [of "-y" "-x"])
   515   apply (auto simp add: gcd_neg1_int gcd_neg2_int)
   516 done
   517 
   518 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
   519 by (metis gcd_red_int mod_add_self1 zadd_commute)
   520 
   521 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   522 by (metis gcd_add1_int gcd_commute_int zadd_commute)
   523 
   524 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   525 by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
   526 
   527 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   528 by (metis gcd_commute_int gcd_red_int 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 gcd_dvd_prod_nat [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[simp]:
   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 gcd_greatest_iff_nat gcd_pos_nat)
   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 gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
   572 apply simp
   573 done
   574 
   575 
   576 subsection {* Coprimality *}
   577 
   578 lemma div_gcd_coprime_nat:
   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: gcd_zero_nat)
   597   then have gp: "?g > 0" by arith
   598   from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
   599   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   600 qed
   601 
   602 lemma div_gcd_coprime_int:
   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) gcd_abs_int)
   606 apply (subst (1 2) abs_div)
   607   apply simp
   608  apply simp
   609 apply(subst (1 2) abs_gcd_int)
   610 apply (rule div_gcd_coprime_nat [transferred])
   611 using nz apply (auto simp add: gcd_abs_int [symmetric])
   612 done
   613 
   614 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   615   using gcd_unique_nat[of 1 a b, simplified] by auto
   616 
   617 lemma coprime_Suc_0_nat:
   618     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   619   using coprime_nat by (simp add: One_nat_def)
   620 
   621 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
   622     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   623   using gcd_unique_int [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 gcd_coprime_nat:
   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 div_gcd_coprime_nat)
   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 gcd_coprime_int:
   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 div_gcd_coprime_int)
   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 coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   671     shows "coprime d (a * b)"
   672   apply (subst gcd_commute_nat)
   673   using da apply (subst gcd_mult_cancel_nat)
   674   apply (subst gcd_commute_nat, assumption)
   675   apply (subst gcd_commute_nat, rule db)
   676 done
   677 
   678 lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
   679     shows "coprime d (a * b)"
   680   apply (subst gcd_commute_int)
   681   using da apply (subst gcd_mult_cancel_int)
   682   apply (subst gcd_commute_int, assumption)
   683   apply (subst gcd_commute_int, rule db)
   684 done
   685 
   686 lemma coprime_lmult_nat:
   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 gcd_greatest_nat, auto)
   691   with dab show ?thesis
   692     by auto
   693 qed
   694 
   695 lemma coprime_lmult_int:
   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 gcd_greatest_int, auto)
   700   with assms show ?thesis
   701     by auto
   702 qed
   703 
   704 lemma coprime_rmult_nat:
   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 gcd_greatest_nat, auto intro: dvd_mult)
   709   with assms show ?thesis
   710     by auto
   711 qed
   712 
   713 lemma coprime_rmult_int:
   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 gcd_greatest_int, auto intro: dvd_mult)
   718   with dab show ?thesis
   719     by auto
   720 qed
   721 
   722 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   723     coprime d a \<and>  coprime d b"
   724   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   725     coprime_mult_nat[of d a b]
   726   by blast
   727 
   728 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   729     coprime d a \<and>  coprime d b"
   730   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   731     coprime_mult_int[of d a b]
   732   by blast
   733 
   734 lemma gcd_coprime_exists_nat:
   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: div_gcd_coprime_nat dvd_div_mult)
   740 done
   741 
   742 lemma gcd_coprime_exists_int:
   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: div_gcd_coprime_int dvd_div_mult_self)
   748 done
   749 
   750 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   751   by (induct n, simp_all add: coprime_mult_nat)
   752 
   753 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   754   by (induct n, simp_all add: coprime_mult_int)
   755 
   756 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   757   apply (rule coprime_exp_nat)
   758   apply (subst gcd_commute_nat)
   759   apply (rule coprime_exp_nat)
   760   apply (subst gcd_commute_nat, assumption)
   761 done
   762 
   763 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   764   apply (rule coprime_exp_int)
   765   apply (subst gcd_commute_int)
   766   apply (rule coprime_exp_int)
   767   apply (subst gcd_commute_int, assumption)
   768 done
   769 
   770 lemma gcd_exp_nat: "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:div_gcd_coprime_nat)
   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 gcd_mult_distrib_nat [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 gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   801   apply (subst (1 2) gcd_abs_int)
   802   apply (subst (1 2) power_abs)
   803   apply (rule gcd_exp_nat [where n = n, transferred])
   804   apply auto
   805 done
   806 
   807 lemma coprime_divprod_nat: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   808   using coprime_dvd_mult_iff_nat[of d a b]
   809   by (auto simp add: mult_commute)
   810 
   811 lemma coprime_divprod_int: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   812   using coprime_dvd_mult_iff_int[of d a b]
   813   by (auto simp add: mult_commute)
   814 
   815 lemma division_decomp_nat: 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 gcd_coprime_exists_nat[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 coprime_dvd_mult_nat[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 division_decomp_int: 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 gcd_coprime_exists_int[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 coprime_dvd_mult_int[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 pow_divides_pow_nat:
   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 gcd_coprime_exists_nat[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 coprime_dvd_mult_nat[OF coprime_exp_nat [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 pow_divides_pow_int:
   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 gcd_coprime_exists_int[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 coprime_dvd_mult_int[OF coprime_exp_int [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 pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   921   by (auto intro: pow_divides_pow_nat dvd_power_same)
   922 
   923 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   924   by (auto intro: pow_divides_pow_int dvd_power_same)
   925 
   926 lemma divides_mult_nat:
   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 coprime_dvd_mult_iff_nat[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 divides_mult_int:
   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 coprime_dvd_mult_iff_int[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 coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   951   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   952   apply force
   953   apply (rule dvd_diff_nat)
   954   apply auto
   955 done
   956 
   957 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
   958   using coprime_plus_one_nat by (simp add: One_nat_def)
   959 
   960 lemma coprime_plus_one_int [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 coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   968   using coprime_plus_one_nat [of "n - 1"]
   969     gcd_commute_nat [of "n - 1" n] by auto
   970 
   971 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
   972   using coprime_plus_one_int [of "n - 1"]
   973     gcd_commute_int [of "n - 1" n] by auto
   974 
   975 lemma setprod_coprime_nat [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: gcd_mult_cancel_nat)
   980 done
   981 
   982 lemma setprod_coprime_int [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: gcd_mult_cancel_int)
   987 done
   988 
   989 lemma prime_odd_nat: "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 prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   998   unfolding prime_int_def
   999   apply (frule prime_odd_nat)
  1000   apply (auto simp add: even_nat_def)
  1001 done
  1002 
  1003 lemma coprime_common_divisor_nat: "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) gcd_greatest_nat)
  1008 done
  1009 
  1010 lemma coprime_common_divisor_int: "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) gcd_greatest_int)
  1015 done
  1016 
  1017 lemma coprime_divisors_nat: "(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 coprime_lmult_int)
  1021   apply (subst gcd_commute_int)
  1022   apply (subst (asm) (2) gcd_commute_int)
  1023   apply (erule coprime_lmult_int)
  1024 done
  1025 
  1026 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1027 apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
  1028 done
  1029 
  1030 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1031 apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
  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: gcd_nat_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 gcd_non_0_nat)
  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 bezout_int:
  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 gcd_neg2_int [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 gcd_neg1_int [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 gcd_neg1_int [symmetric])
  1118     apply (subst gcd_neg2_int [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 bezout_lemma_nat:
  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 bezout_add_nat: "\<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 bezout1_nat: "\<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 bezout_add_nat[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 bezout_add_strong_nat: 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 bezout_add_nat[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 bezout_nat: 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 bezout_add_strong_nat[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 lcm_altdef_int: "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 prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1282   unfolding lcm_nat_def
  1283   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1284 
  1285 lemma prod_gcd_lcm_int: "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 prod_gcd_lcm_nat [symmetric])
  1289   apply (subst nat_abs_mult_distrib [symmetric])
  1290   apply (simp, simp add: abs_mult)
  1291 done
  1292 
  1293 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1294   unfolding lcm_nat_def by simp
  1295 
  1296 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1297   unfolding lcm_int_def by simp
  1298 
  1299 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1300   unfolding lcm_nat_def by simp
  1301 
  1302 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1303   unfolding lcm_int_def by simp
  1304 
  1305 lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
  1306   unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
  1307 
  1308 lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
  1309   unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
  1310 
  1311 
  1312 lemma lcm_pos_nat:
  1313   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1314 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1315 
  1316 lemma lcm_pos_int:
  1317   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1318   apply (subst lcm_abs_int)
  1319   apply (rule lcm_pos_nat [transferred])
  1320   apply auto
  1321 done
  1322 
  1323 lemma dvd_pos_nat:
  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 lcm_least_nat:
  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 dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1337   with gcd_zero_nat [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 gcd_mult_distrib_nat)
  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 gcd_mult_distrib_nat)
  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 prod_gcd_lcm_nat [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 lcm_least_int:
  1362   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1363 apply (subst lcm_abs_int)
  1364 apply (rule dvd_trans)
  1365 apply (rule lcm_least_nat [transferred, of _ "abs k" _])
  1366 apply auto
  1367 done
  1368 
  1369 lemma lcm_dvd1_nat: "(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 gcd_zero_nat by simp
  1386     finally show ?thesis by (simp add: lcm_nat_def)
  1387   qed
  1388 qed
  1389 
  1390 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1391   apply (subst lcm_abs_int)
  1392   apply (rule dvd_trans)
  1393   prefer 2
  1394   apply (rule lcm_dvd1_nat [transferred])
  1395   apply auto
  1396 done
  1397 
  1398 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1399   by (subst lcm_commute_nat, rule lcm_dvd1_nat)
  1400 
  1401 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1402   by (subst lcm_commute_int, rule lcm_dvd1_int)
  1403 
  1404 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1405 by(metis lcm_dvd1_nat dvd_trans)
  1406 
  1407 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1408 by(metis lcm_dvd2_nat dvd_trans)
  1409 
  1410 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1411 by(metis lcm_dvd1_int dvd_trans)
  1412 
  1413 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1414 by(metis lcm_dvd2_int dvd_trans)
  1415 
  1416 lemma lcm_unique_nat: "(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 lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1419 
  1420 lemma lcm_unique_int: "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] lcm_least_int)
  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 lcm_unique_nat [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 lcm_unique_int [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 lcm_commute_nat, 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 lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1441 
  1442 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1443 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1444 
  1445 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1446 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1447 
  1448 lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
  1449 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1450 
  1451 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
  1452 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1453 
  1454 lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
  1455 by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
  1456 
  1457 lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
  1458 by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
  1459 
  1460 lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
  1461 lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
  1462 
  1463 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1464 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1465 
  1466 lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1467 proof qed (auto simp add: gcd_ac_nat)
  1468 
  1469 lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  1470 proof qed (auto simp add: gcd_ac_int)
  1471 
  1472 lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1473 proof qed (auto simp add: lcm_ac_nat)
  1474 
  1475 lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  1476 proof qed (auto simp add: lcm_ac_int)
  1477 
  1478 
  1479 subsection {* Primes *}
  1480 
  1481 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
  1482 
  1483 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
  1484   by (unfold prime_nat_def, auto)
  1485 
  1486 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
  1487   by (unfold prime_nat_def, auto)
  1488 
  1489 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
  1490   by (unfold prime_nat_def, auto)
  1491 
  1492 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
  1493   by (unfold prime_nat_def, auto)
  1494 
  1495 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
  1496   by (unfold prime_nat_def, auto)
  1497 
  1498 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
  1499   by (unfold prime_nat_def, auto)
  1500 
  1501 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
  1502   by (unfold prime_nat_def, auto)
  1503 
  1504 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
  1505   by (unfold prime_int_def prime_nat_def) auto
  1506 
  1507 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
  1508   by (unfold prime_int_def prime_nat_def, auto)
  1509 
  1510 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
  1511   by (unfold prime_int_def prime_nat_def, auto)
  1512 
  1513 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
  1514   by (unfold prime_int_def prime_nat_def, auto)
  1515 
  1516 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
  1517   by (unfold prime_int_def prime_nat_def, auto)
  1518 
  1519 
  1520 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
  1521     m = 1 \<or> m = p))"
  1522   using prime_nat_def [transferred]
  1523     apply (case_tac "p >= 0")
  1524     by (blast, auto simp add: prime_ge_0_int)
  1525 
  1526 (* To do: determine primality of any numeral *)
  1527 
  1528 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
  1529   by (simp add: prime_nat_def)
  1530 
  1531 lemma zero_not_prime_int [simp]: "~prime (0::int)"
  1532   by (simp add: prime_int_def)
  1533 
  1534 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
  1535   by (simp add: prime_nat_def)
  1536 
  1537 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
  1538   by (simp add: prime_nat_def One_nat_def)
  1539 
  1540 lemma one_not_prime_int [simp]: "~prime (1::int)"
  1541   by (simp add: prime_int_def)
  1542 
  1543 lemma two_is_prime_nat [simp]: "prime (2::nat)"
  1544   apply (auto simp add: prime_nat_def)
  1545   apply (case_tac m)
  1546   apply (auto dest!: dvd_imp_le)
  1547   done
  1548 
  1549 lemma two_is_prime_int [simp]: "prime (2::int)"
  1550   by (rule two_is_prime_nat [transferred direction: nat "op <= (0::int)"])
  1551 
  1552 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1553   apply (unfold prime_nat_def)
  1554   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
  1555   done
  1556 
  1557 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1558   apply (unfold prime_int_altdef)
  1559   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
  1560   done
  1561 
  1562 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1563   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
  1564 
  1565 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1566   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
  1567 
  1568 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
  1569     p dvd m * n = (p dvd m \<or> p dvd n)"
  1570   by (rule iffI, rule prime_dvd_mult_nat, auto)
  1571 
  1572 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
  1573     p dvd m * n = (p dvd m \<or> p dvd n)"
  1574   by (rule iffI, rule prime_dvd_mult_int, auto)
  1575 
  1576 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1577     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1578   unfolding prime_nat_def dvd_def apply auto
  1579   by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
  1580 
  1581 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1582     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1583   unfolding prime_int_altdef dvd_def
  1584   apply auto
  1585   by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
  1586 
  1587 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
  1588     n > 0 --> (p dvd x^n --> p dvd x)"
  1589   by (induct n rule: nat_induct, auto)
  1590 
  1591 lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
  1592     n > 0 --> (p dvd x^n --> p dvd x)"
  1593   apply (induct n rule: nat_induct, auto)
  1594   apply (frule prime_ge_0_int)
  1595   apply auto
  1596 done
  1597 
  1598 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1599     coprime a (p^m)"
  1600   apply (rule coprime_exp_nat)
  1601   apply (subst gcd_commute_nat)
  1602   apply (erule (1) prime_imp_coprime_nat)
  1603 done
  1604 
  1605 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1606     coprime a (p^m)"
  1607   apply (rule coprime_exp_int)
  1608   apply (subst gcd_commute_int)
  1609   apply (erule (1) prime_imp_coprime_int)
  1610 done
  1611 
  1612 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1613   apply (rule prime_imp_coprime_nat, assumption)
  1614   apply (unfold prime_nat_def, auto)
  1615 done
  1616 
  1617 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1618   apply (rule prime_imp_coprime_int, assumption)
  1619   apply (unfold prime_int_altdef, clarify)
  1620   apply (drule_tac x = q in spec)
  1621   apply (drule_tac x = p in spec)
  1622   apply auto
  1623 done
  1624 
  1625 lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1626     coprime (p^m) (q^n)"
  1627   by (rule coprime_exp2_nat, rule primes_coprime_nat)
  1628 
  1629 lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1630     coprime (p^m) (q^n)"
  1631   by (rule coprime_exp2_int, rule primes_coprime_int)
  1632 
  1633 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
  1634   apply (induct n rule: nat_less_induct)
  1635   apply (case_tac "n = 0")
  1636   using two_is_prime_nat apply blast
  1637   apply (case_tac "prime n")
  1638   apply blast
  1639   apply (subgoal_tac "n > 1")
  1640   apply (frule (1) not_prime_eq_prod_nat)
  1641   apply (auto intro: dvd_mult dvd_mult2)
  1642 done
  1643 
  1644 (* An Isar version:
  1645 
  1646 lemma prime_factor_b_nat:
  1647   fixes n :: nat
  1648   assumes "n \<noteq> 1"
  1649   shows "\<exists>p. prime p \<and> p dvd n"
  1650 
  1651 using `n ~= 1`
  1652 proof (induct n rule: less_induct_nat)
  1653   fix n :: nat
  1654   assume "n ~= 1" and
  1655     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
  1656   thus "\<exists>p. prime p \<and> p dvd n"
  1657   proof -
  1658   {
  1659     assume "n = 0"
  1660     moreover note two_is_prime_nat
  1661     ultimately have ?thesis
  1662       by (auto simp del: two_is_prime_nat)
  1663   }
  1664   moreover
  1665   {
  1666     assume "prime n"
  1667     hence ?thesis by auto
  1668   }
  1669   moreover
  1670   {
  1671     assume "n ~= 0" and "~ prime n"
  1672     with `n ~= 1` have "n > 1" by auto
  1673     with `~ prime n` and not_prime_eq_prod_nat obtain m k where
  1674       "n = m * k" and "1 < m" and "m < n" by blast
  1675     with ih obtain p where "prime p" and "p dvd m" by blast
  1676     with `n = m * k` have ?thesis by auto
  1677   }
  1678   ultimately show ?thesis by blast
  1679   qed
  1680 qed
  1681 
  1682 *)
  1683 
  1684 text {* One property of coprimality is easier to prove via prime factors. *}
  1685 
  1686 lemma prime_divprod_pow_nat:
  1687   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
  1688   shows "p^n dvd a \<or> p^n dvd b"
  1689 proof-
  1690   {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
  1691       apply (cases "n=0", simp_all)
  1692       apply (cases "a=1", simp_all) done}
  1693   moreover
  1694   {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
  1695     then obtain m where m: "n = Suc m" by (cases n, auto)
  1696     from n have "p dvd p^n" by (intro dvd_power, auto)
  1697     also note pab
  1698     finally have pab': "p dvd a * b".
  1699     from prime_dvd_mult_nat[OF p pab']
  1700     have "p dvd a \<or> p dvd b" .
  1701     moreover
  1702     {assume pa: "p dvd a"
  1703       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1704       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
  1705       with p have "coprime b p"
  1706         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
  1707       hence pnb: "coprime (p^n) b"
  1708         by (subst gcd_commute_nat, rule coprime_exp_nat)
  1709       from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
  1710     moreover
  1711     {assume pb: "p dvd b"
  1712       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1713       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
  1714         by auto
  1715       with p have "coprime a p"
  1716         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
  1717       hence pna: "coprime (p^n) a"
  1718         by (subst gcd_commute_nat, rule coprime_exp_nat)
  1719       from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
  1720     ultimately have ?thesis by blast}
  1721   ultimately show ?thesis by blast
  1722 qed
  1723 
  1724 end