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