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