src/HOL/GCD.thy
author nipkow
Wed Jul 15 20:34:58 2009 +0200 (2009-07-15)
changeset 32007 a2a3685f61c3
parent 31996 1d93369079c4
child 32045 efc5f4806cd5
permissions -rw-r--r--
Made "prime" executable
     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 subsection {* GCD *}
   163 
   164 (* was gcd_induct *)
   165 lemma gcd_nat_induct:
   166   fixes m n :: nat
   167   assumes "\<And>m. P m 0"
   168     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   169   shows "P m n"
   170   apply (rule gcd_nat.induct)
   171   apply (case_tac "y = 0")
   172   using assms apply simp_all
   173 done
   174 
   175 (* specific to int *)
   176 
   177 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
   178   by (simp add: gcd_int_def)
   179 
   180 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
   181   by (simp add: gcd_int_def)
   182 
   183 lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
   184 by(simp add: gcd_int_def)
   185 
   186 lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"
   187 by (simp add: gcd_int_def)
   188 
   189 lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
   190 by (metis abs_idempotent gcd_abs_int)
   191 
   192 lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
   193 by (metis abs_idempotent gcd_abs_int)
   194 
   195 lemma gcd_cases_int:
   196   fixes x :: int and y
   197   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   198       and "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   shows "P (gcd x y)"
   202 by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith)
   203 
   204 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   205   by (simp add: gcd_int_def)
   206 
   207 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
   208   by (simp add: lcm_int_def)
   209 
   210 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
   211   by (simp add: lcm_int_def)
   212 
   213 lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"
   214   by (simp add: lcm_int_def)
   215 
   216 lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
   217 by(simp add:lcm_int_def)
   218 
   219 lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
   220 by (metis abs_idempotent lcm_int_def)
   221 
   222 lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
   223 by (metis abs_idempotent lcm_int_def)
   224 
   225 lemma lcm_cases_int:
   226   fixes x :: int and y
   227   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   228       and "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   shows "P (lcm x y)"
   232 by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith)
   233 
   234 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   235   by (simp add: lcm_int_def)
   236 
   237 (* was gcd_0, etc. *)
   238 lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
   239   by simp
   240 
   241 (* was igcd_0, etc. *)
   242 lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
   243   by (unfold gcd_int_def, auto)
   244 
   245 lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
   246   by simp
   247 
   248 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
   249   by (unfold gcd_int_def, auto)
   250 
   251 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
   252   by (case_tac "y = 0", auto)
   253 
   254 (* weaker, but useful for the simplifier *)
   255 
   256 lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   257   by simp
   258 
   259 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   260   by simp
   261 
   262 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   263   by (simp add: One_nat_def)
   264 
   265 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   266   by (simp add: gcd_int_def)
   267 
   268 lemma gcd_idem_nat: "gcd (x::nat) x = x"
   269 by simp
   270 
   271 lemma gcd_idem_int: "gcd (x::int) x = abs x"
   272 by (auto simp add: gcd_int_def)
   273 
   274 declare gcd_nat.simps [simp del]
   275 
   276 text {*
   277   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   278   conjunctions don't seem provable separately.
   279 *}
   280 
   281 lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
   282   and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
   283   apply (induct m n rule: gcd_nat_induct)
   284   apply (simp_all add: gcd_non_0_nat)
   285   apply (blast dest: dvd_mod_imp_dvd)
   286 done
   287 
   288 lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"
   289 by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)
   290 
   291 lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"
   292 by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)
   293 
   294 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   295 by(metis gcd_dvd1_nat dvd_trans)
   296 
   297 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   298 by(metis gcd_dvd2_nat dvd_trans)
   299 
   300 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   301 by(metis gcd_dvd1_int dvd_trans)
   302 
   303 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   304 by(metis gcd_dvd2_int dvd_trans)
   305 
   306 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   307   by (rule dvd_imp_le, auto)
   308 
   309 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   310   by (rule dvd_imp_le, auto)
   311 
   312 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   313   by (rule zdvd_imp_le, auto)
   314 
   315 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   316   by (rule zdvd_imp_le, auto)
   317 
   318 lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   319 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
   320 
   321 lemma gcd_greatest_int:
   322   "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   323   apply (subst gcd_abs_int)
   324   apply (subst abs_dvd_iff [symmetric])
   325   apply (rule gcd_greatest_nat [transferred])
   326   apply auto
   327 done
   328 
   329 lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
   330     (k dvd m & k dvd n)"
   331   by (blast intro!: gcd_greatest_nat intro: dvd_trans)
   332 
   333 lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   334   by (blast intro!: gcd_greatest_int intro: dvd_trans)
   335 
   336 lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   337   by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
   338 
   339 lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   340   by (auto simp add: gcd_int_def)
   341 
   342 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   343   by (insert gcd_zero_nat [of m n], arith)
   344 
   345 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   346   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
   347 
   348 lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
   349   by (rule dvd_anti_sym, auto)
   350 
   351 lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
   352   by (auto simp add: gcd_int_def gcd_commute_nat)
   353 
   354 lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
   355   apply (rule dvd_anti_sym)
   356   apply (blast intro: dvd_trans)+
   357 done
   358 
   359 lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
   360   by (auto simp add: gcd_int_def gcd_assoc_nat)
   361 
   362 lemmas gcd_left_commute_nat =
   363   mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat]
   364 
   365 lemmas gcd_left_commute_int =
   366   mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int]
   367 
   368 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
   369   -- {* gcd is an AC-operator *}
   370 
   371 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
   372 
   373 lemma gcd_unique_nat: "(d::nat) 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 auto
   376   apply (rule dvd_anti_sym)
   377   apply (erule (1) gcd_greatest_nat)
   378   apply auto
   379 done
   380 
   381 lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   382     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   383   apply (case_tac "d = 0")
   384   apply force
   385   apply (rule iffI)
   386   apply (rule zdvd_anti_sym)
   387   apply arith
   388   apply (subst gcd_pos_int)
   389   apply clarsimp
   390   apply (drule_tac x = "d + 1" in spec)
   391   apply (frule zdvd_imp_le)
   392   apply (auto intro: gcd_greatest_int)
   393 done
   394 
   395 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   396 by (metis dvd.eq_iff gcd_unique_nat)
   397 
   398 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   399 by (metis dvd.eq_iff gcd_unique_nat)
   400 
   401 lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   402 by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
   403 
   404 lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   405 by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   406 
   407 
   408 text {*
   409   \medskip Multiplication laws
   410 *}
   411 
   412 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   413     -- {* \cite[page 27]{davenport92} *}
   414   apply (induct m n rule: gcd_nat_induct)
   415   apply simp
   416   apply (case_tac "k = 0")
   417   apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
   418 done
   419 
   420 lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   421   apply (subst (1 2) gcd_abs_int)
   422   apply (subst (1 2) abs_mult)
   423   apply (rule gcd_mult_distrib_nat [transferred])
   424   apply auto
   425 done
   426 
   427 lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   428   apply (insert gcd_mult_distrib_nat [of m k n])
   429   apply simp
   430   apply (erule_tac t = m in ssubst)
   431   apply simp
   432   done
   433 
   434 lemma coprime_dvd_mult_int:
   435   "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   436 apply (subst abs_dvd_iff [symmetric])
   437 apply (subst dvd_abs_iff [symmetric])
   438 apply (subst (asm) gcd_abs_int)
   439 apply (rule coprime_dvd_mult_nat [transferred])
   440     prefer 4 apply assumption
   441    apply auto
   442 apply (subst abs_mult [symmetric], auto)
   443 done
   444 
   445 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   446     (k dvd m * n) = (k dvd m)"
   447   by (auto intro: coprime_dvd_mult_nat)
   448 
   449 lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   450     (k dvd m * n) = (k dvd m)"
   451   by (auto intro: coprime_dvd_mult_int)
   452 
   453 lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   454   apply (rule dvd_anti_sym)
   455   apply (rule gcd_greatest_nat)
   456   apply (rule_tac n = k in coprime_dvd_mult_nat)
   457   apply (simp add: gcd_assoc_nat)
   458   apply (simp add: gcd_commute_nat)
   459   apply (simp_all add: mult_commute)
   460 done
   461 
   462 lemma gcd_mult_cancel_int:
   463   "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
   464 apply (subst (1 2) gcd_abs_int)
   465 apply (subst abs_mult)
   466 apply (rule gcd_mult_cancel_nat [transferred], auto)
   467 done
   468 
   469 text {* \medskip Addition laws *}
   470 
   471 lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   472   apply (case_tac "n = 0")
   473   apply (simp_all add: gcd_non_0_nat)
   474 done
   475 
   476 lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   477   apply (subst (1 2) gcd_commute_nat)
   478   apply (subst add_commute)
   479   apply simp
   480 done
   481 
   482 (* to do: add the other variations? *)
   483 
   484 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   485   by (subst gcd_add1_nat [symmetric], auto)
   486 
   487 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   488   apply (subst gcd_commute_nat)
   489   apply (subst gcd_diff1_nat [symmetric])
   490   apply auto
   491   apply (subst gcd_commute_nat)
   492   apply (subst gcd_diff1_nat)
   493   apply assumption
   494   apply (rule gcd_commute_nat)
   495 done
   496 
   497 lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   498   apply (frule_tac b = y and a = x in pos_mod_sign)
   499   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   500   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
   501     zmod_zminus1_eq_if)
   502   apply (frule_tac a = x in pos_mod_bound)
   503   apply (subst (1 2) gcd_commute_nat)
   504   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   505     nat_le_eq_zle)
   506 done
   507 
   508 lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
   509   apply (case_tac "y = 0")
   510   apply force
   511   apply (case_tac "y > 0")
   512   apply (subst gcd_non_0_int, auto)
   513   apply (insert gcd_non_0_int [of "-y" "-x"])
   514   apply (auto simp add: gcd_neg1_int gcd_neg2_int)
   515 done
   516 
   517 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
   518 by (metis gcd_red_int mod_add_self1 zadd_commute)
   519 
   520 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   521 by (metis gcd_add1_int gcd_commute_int zadd_commute)
   522 
   523 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   524 by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
   525 
   526 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   527 by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
   528 
   529 
   530 (* to do: differences, and all variations of addition rules
   531     as simplification rules for nat and int *)
   532 
   533 (* FIXME remove iff *)
   534 lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n"
   535   using mult_dvd_mono [of 1] by auto
   536 
   537 (* to do: add the three variations of these, and for ints? *)
   538 
   539 lemma finite_divisors_nat[simp]:
   540   assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
   541 proof-
   542   have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
   543   from finite_subset[OF _ this] show ?thesis using assms
   544     by(bestsimp intro!:dvd_imp_le)
   545 qed
   546 
   547 lemma finite_divisors_int[simp]:
   548   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
   549 proof-
   550   have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
   551   hence "finite{d. abs d <= abs i}" by simp
   552   from finite_subset[OF _ this] show ?thesis using assms
   553     by(bestsimp intro!:dvd_imp_le_int)
   554 qed
   555 
   556 lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
   557 apply(rule antisym)
   558  apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
   559 apply simp
   560 done
   561 
   562 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
   563 apply(rule antisym)
   564  apply(rule Max_le_iff[THEN iffD2])
   565    apply simp
   566   apply fastsimp
   567  apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
   568 apply simp
   569 done
   570 
   571 lemma gcd_is_Max_divisors_nat:
   572   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
   573 apply(rule Max_eqI[THEN sym])
   574   apply (metis finite_Collect_conjI finite_divisors_nat)
   575  apply simp
   576  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
   577 apply simp
   578 done
   579 
   580 lemma gcd_is_Max_divisors_int:
   581   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
   582 apply(rule Max_eqI[THEN sym])
   583   apply (metis finite_Collect_conjI finite_divisors_int)
   584  apply simp
   585  apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
   586 apply simp
   587 done
   588 
   589 
   590 subsection {* Coprimality *}
   591 
   592 lemma div_gcd_coprime_nat:
   593   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   594   shows "coprime (a div gcd a b) (b div gcd a b)"
   595 proof -
   596   let ?g = "gcd a b"
   597   let ?a' = "a div ?g"
   598   let ?b' = "b div ?g"
   599   let ?g' = "gcd ?a' ?b'"
   600   have dvdg: "?g dvd a" "?g dvd b" by simp_all
   601   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   602   from dvdg dvdg' obtain ka kb ka' kb' where
   603       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   604     unfolding dvd_def by blast
   605   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   606     by simp_all
   607   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   608     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   609       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   610   have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat)
   611   then have gp: "?g > 0" by arith
   612   from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
   613   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   614 qed
   615 
   616 lemma div_gcd_coprime_int:
   617   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   618   shows "coprime (a div gcd a b) (b div gcd a b)"
   619 apply (subst (1 2 3) gcd_abs_int)
   620 apply (subst (1 2) abs_div)
   621   apply simp
   622  apply simp
   623 apply(subst (1 2) abs_gcd_int)
   624 apply (rule div_gcd_coprime_nat [transferred])
   625 using nz apply (auto simp add: gcd_abs_int [symmetric])
   626 done
   627 
   628 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   629   using gcd_unique_nat[of 1 a b, simplified] by auto
   630 
   631 lemma coprime_Suc_0_nat:
   632     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   633   using coprime_nat by (simp add: One_nat_def)
   634 
   635 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
   636     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   637   using gcd_unique_int [of 1 a b]
   638   apply clarsimp
   639   apply (erule subst)
   640   apply (rule iffI)
   641   apply force
   642   apply (drule_tac x = "abs e" in exI)
   643   apply (case_tac "e >= 0")
   644   apply force
   645   apply force
   646 done
   647 
   648 lemma gcd_coprime_nat:
   649   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   650     b: "b = b' * gcd a b"
   651   shows    "coprime a' b'"
   652 
   653   apply (subgoal_tac "a' = a div gcd a b")
   654   apply (erule ssubst)
   655   apply (subgoal_tac "b' = b div gcd a b")
   656   apply (erule ssubst)
   657   apply (rule div_gcd_coprime_nat)
   658   using prems
   659   apply force
   660   apply (subst (1) b)
   661   using z apply force
   662   apply (subst (1) a)
   663   using z apply force
   664 done
   665 
   666 lemma gcd_coprime_int:
   667   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   668     b: "b = b' * gcd a b"
   669   shows    "coprime a' b'"
   670 
   671   apply (subgoal_tac "a' = a div gcd a b")
   672   apply (erule ssubst)
   673   apply (subgoal_tac "b' = b div gcd a b")
   674   apply (erule ssubst)
   675   apply (rule div_gcd_coprime_int)
   676   using prems
   677   apply force
   678   apply (subst (1) b)
   679   using z apply force
   680   apply (subst (1) a)
   681   using z apply force
   682 done
   683 
   684 lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   685     shows "coprime d (a * b)"
   686   apply (subst gcd_commute_nat)
   687   using da apply (subst gcd_mult_cancel_nat)
   688   apply (subst gcd_commute_nat, assumption)
   689   apply (subst gcd_commute_nat, rule db)
   690 done
   691 
   692 lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
   693     shows "coprime d (a * b)"
   694   apply (subst gcd_commute_int)
   695   using da apply (subst gcd_mult_cancel_int)
   696   apply (subst gcd_commute_int, assumption)
   697   apply (subst gcd_commute_int, rule db)
   698 done
   699 
   700 lemma coprime_lmult_nat:
   701   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   702 proof -
   703   have "gcd d a dvd gcd d (a * b)"
   704     by (rule gcd_greatest_nat, auto)
   705   with dab show ?thesis
   706     by auto
   707 qed
   708 
   709 lemma coprime_lmult_int:
   710   assumes "coprime (d::int) (a * b)" shows "coprime d a"
   711 proof -
   712   have "gcd d a dvd gcd d (a * b)"
   713     by (rule gcd_greatest_int, auto)
   714   with assms show ?thesis
   715     by auto
   716 qed
   717 
   718 lemma coprime_rmult_nat:
   719   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   720 proof -
   721   have "gcd d b dvd gcd d (a * b)"
   722     by (rule gcd_greatest_nat, auto intro: dvd_mult)
   723   with assms show ?thesis
   724     by auto
   725 qed
   726 
   727 lemma coprime_rmult_int:
   728   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   729 proof -
   730   have "gcd d b dvd gcd d (a * b)"
   731     by (rule gcd_greatest_int, auto intro: dvd_mult)
   732   with dab show ?thesis
   733     by auto
   734 qed
   735 
   736 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   737     coprime d a \<and>  coprime d b"
   738   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   739     coprime_mult_nat[of d a b]
   740   by blast
   741 
   742 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   743     coprime d a \<and>  coprime d b"
   744   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   745     coprime_mult_int[of d a b]
   746   by blast
   747 
   748 lemma gcd_coprime_exists_nat:
   749     assumes nz: "gcd (a::nat) b \<noteq> 0"
   750     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   751   apply (rule_tac x = "a div gcd a b" in exI)
   752   apply (rule_tac x = "b div gcd a b" in exI)
   753   using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)
   754 done
   755 
   756 lemma gcd_coprime_exists_int:
   757     assumes nz: "gcd (a::int) b \<noteq> 0"
   758     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   759   apply (rule_tac x = "a div gcd a b" in exI)
   760   apply (rule_tac x = "b div gcd a b" in exI)
   761   using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self)
   762 done
   763 
   764 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   765   by (induct n, simp_all add: coprime_mult_nat)
   766 
   767 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   768   by (induct n, simp_all add: coprime_mult_int)
   769 
   770 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   771   apply (rule coprime_exp_nat)
   772   apply (subst gcd_commute_nat)
   773   apply (rule coprime_exp_nat)
   774   apply (subst gcd_commute_nat, assumption)
   775 done
   776 
   777 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   778   apply (rule coprime_exp_int)
   779   apply (subst gcd_commute_int)
   780   apply (rule coprime_exp_int)
   781   apply (subst gcd_commute_int, assumption)
   782 done
   783 
   784 lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   785 proof (cases)
   786   assume "a = 0 & b = 0"
   787   thus ?thesis by simp
   788   next assume "~(a = 0 & b = 0)"
   789   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   790     by (auto simp:div_gcd_coprime_nat)
   791   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   792       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   793     apply (subst (1 2) mult_commute)
   794     apply (subst gcd_mult_distrib_nat [symmetric])
   795     apply simp
   796     done
   797   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   798     apply (subst div_power)
   799     apply auto
   800     apply (rule dvd_div_mult_self)
   801     apply (rule dvd_power_same)
   802     apply auto
   803     done
   804   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
   805     apply (subst div_power)
   806     apply auto
   807     apply (rule dvd_div_mult_self)
   808     apply (rule dvd_power_same)
   809     apply auto
   810     done
   811   finally show ?thesis .
   812 qed
   813 
   814 lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   815   apply (subst (1 2) gcd_abs_int)
   816   apply (subst (1 2) power_abs)
   817   apply (rule gcd_exp_nat [where n = n, transferred])
   818   apply auto
   819 done
   820 
   821 lemma coprime_divprod_nat: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   822   using coprime_dvd_mult_iff_nat[of d a b]
   823   by (auto simp add: mult_commute)
   824 
   825 lemma coprime_divprod_int: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   826   using coprime_dvd_mult_iff_int[of d a b]
   827   by (auto simp add: mult_commute)
   828 
   829 lemma division_decomp_nat: assumes dc: "(a::nat) 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 gcd_coprime_exists_nat[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" using dvd_trans[of a' a "b*c"] by simp
   842     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   843     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   844     with z have th_1: "a' dvd b' * c" by auto
   845     from coprime_dvd_mult_nat[OF ab'(3)] th_1
   846     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   847     from ab' have "a = ?g*a'" by algebra
   848     with thb thc have ?thesis by blast }
   849   ultimately show ?thesis by blast
   850 qed
   851 
   852 lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
   853   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   854 proof-
   855   let ?g = "gcd a b"
   856   {assume "?g = 0" with dc have ?thesis by auto}
   857   moreover
   858   {assume z: "?g \<noteq> 0"
   859     from gcd_coprime_exists_int[OF z]
   860     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   861       by blast
   862     have thb: "?g dvd b" by auto
   863     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   864     with dc have th0: "a' dvd b*c"
   865       using dvd_trans[of a' a "b*c"] by simp
   866     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   867     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   868     with z have th_1: "a' dvd b' * c" by auto
   869     from coprime_dvd_mult_int[OF ab'(3)] th_1
   870     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   871     from ab' have "a = ?g*a'" by algebra
   872     with thb thc have ?thesis by blast }
   873   ultimately show ?thesis by blast
   874 qed
   875 
   876 lemma pow_divides_pow_nat:
   877   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   878   shows "a dvd b"
   879 proof-
   880   let ?g = "gcd a b"
   881   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   882   {assume "?g = 0" with ab n have ?thesis by auto }
   883   moreover
   884   {assume z: "?g \<noteq> 0"
   885     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   886     from gcd_coprime_exists_nat[OF z]
   887     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   888       by blast
   889     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   890       by (simp add: ab'(1,2)[symmetric])
   891     hence "?g^n*a'^n dvd ?g^n *b'^n"
   892       by (simp only: power_mult_distrib mult_commute)
   893     with zn z n have th0:"a'^n dvd b'^n" by auto
   894     have "a' dvd a'^n" by (simp add: m)
   895     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   896     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   897     from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
   898     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   899     hence "a'*?g dvd b'*?g" by simp
   900     with ab'(1,2)  have ?thesis by simp }
   901   ultimately show ?thesis by blast
   902 qed
   903 
   904 lemma pow_divides_pow_int:
   905   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
   906   shows "a dvd b"
   907 proof-
   908   let ?g = "gcd a b"
   909   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   910   {assume "?g = 0" with ab n have ?thesis by auto }
   911   moreover
   912   {assume z: "?g \<noteq> 0"
   913     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   914     from gcd_coprime_exists_int[OF z]
   915     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   916       by blast
   917     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   918       by (simp add: ab'(1,2)[symmetric])
   919     hence "?g^n*a'^n dvd ?g^n *b'^n"
   920       by (simp only: power_mult_distrib mult_commute)
   921     with zn z n have th0:"a'^n dvd b'^n" by auto
   922     have "a' dvd a'^n" by (simp add: m)
   923     with th0 have "a' dvd b'^n"
   924       using dvd_trans[of a' "a'^n" "b'^n"] by simp
   925     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   926     from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
   927     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   928     hence "a'*?g dvd b'*?g" by simp
   929     with ab'(1,2)  have ?thesis by simp }
   930   ultimately show ?thesis by blast
   931 qed
   932 
   933 (* FIXME move to Divides(?) *)
   934 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   935   by (auto intro: pow_divides_pow_nat dvd_power_same)
   936 
   937 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   938   by (auto intro: pow_divides_pow_int dvd_power_same)
   939 
   940 lemma divides_mult_nat:
   941   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   942   shows "m * n dvd r"
   943 proof-
   944   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   945     unfolding dvd_def by blast
   946   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   947   hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
   948   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   949   from n' k show ?thesis unfolding dvd_def by auto
   950 qed
   951 
   952 lemma divides_mult_int:
   953   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   954   shows "m * n dvd r"
   955 proof-
   956   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   957     unfolding dvd_def by blast
   958   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   959   hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
   960   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   961   from n' k show ?thesis unfolding dvd_def by auto
   962 qed
   963 
   964 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   965   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   966   apply force
   967   apply (rule dvd_diff_nat)
   968   apply auto
   969 done
   970 
   971 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
   972   using coprime_plus_one_nat by (simp add: One_nat_def)
   973 
   974 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
   975   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   976   apply force
   977   apply (rule dvd_diff)
   978   apply auto
   979 done
   980 
   981 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   982   using coprime_plus_one_nat [of "n - 1"]
   983     gcd_commute_nat [of "n - 1" n] by auto
   984 
   985 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
   986   using coprime_plus_one_int [of "n - 1"]
   987     gcd_commute_int [of "n - 1" n] by auto
   988 
   989 lemma setprod_coprime_nat [rule_format]:
   990     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
   991   apply (case_tac "finite A")
   992   apply (induct set: finite)
   993   apply (auto simp add: gcd_mult_cancel_nat)
   994 done
   995 
   996 lemma setprod_coprime_int [rule_format]:
   997     "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
   998   apply (case_tac "finite A")
   999   apply (induct set: finite)
  1000   apply (auto simp add: gcd_mult_cancel_int)
  1001 done
  1002 
  1003 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  1004   unfolding prime_nat_def
  1005   apply (subst even_mult_two_ex)
  1006   apply clarify
  1007   apply (drule_tac x = 2 in spec)
  1008   apply auto
  1009 done
  1010 
  1011 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  1012   unfolding prime_int_def
  1013   apply (frule prime_odd_nat)
  1014   apply (auto simp add: even_nat_def)
  1015 done
  1016 
  1017 lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1018     x dvd b \<Longrightarrow> x = 1"
  1019   apply (subgoal_tac "x dvd gcd a b")
  1020   apply simp
  1021   apply (erule (1) gcd_greatest_nat)
  1022 done
  1023 
  1024 lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1025     x dvd b \<Longrightarrow> abs x = 1"
  1026   apply (subgoal_tac "x dvd gcd a b")
  1027   apply simp
  1028   apply (erule (1) gcd_greatest_int)
  1029 done
  1030 
  1031 lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
  1032     coprime d e"
  1033   apply (auto simp add: dvd_def)
  1034   apply (frule coprime_lmult_int)
  1035   apply (subst gcd_commute_int)
  1036   apply (subst (asm) (2) gcd_commute_int)
  1037   apply (erule coprime_lmult_int)
  1038 done
  1039 
  1040 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1041 apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
  1042 done
  1043 
  1044 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1045 apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
  1046 done
  1047 
  1048 
  1049 subsection {* Bezout's theorem *}
  1050 
  1051 (* Function bezw returns a pair of witnesses to Bezout's theorem --
  1052    see the theorems that follow the definition. *)
  1053 fun
  1054   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1055 where
  1056   "bezw x y =
  1057   (if y = 0 then (1, 0) else
  1058       (snd (bezw y (x mod y)),
  1059        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1060 
  1061 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1062 
  1063 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1064        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1065   by simp
  1066 
  1067 declare bezw.simps [simp del]
  1068 
  1069 lemma bezw_aux [rule_format]:
  1070     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1071 proof (induct x y rule: gcd_nat_induct)
  1072   fix m :: nat
  1073   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1074     by auto
  1075   next fix m :: nat and n
  1076     assume ngt0: "n > 0" and
  1077       ih: "fst (bezw n (m mod n)) * int n +
  1078         snd (bezw n (m mod n)) * int (m mod n) =
  1079         int (gcd n (m mod n))"
  1080     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1081       apply (simp add: bezw_non_0 gcd_non_0_nat)
  1082       apply (erule subst)
  1083       apply (simp add: ring_simps)
  1084       apply (subst mod_div_equality [of m n, symmetric])
  1085       (* applying simp here undoes the last substitution!
  1086          what is procedure cancel_div_mod? *)
  1087       apply (simp only: ring_simps zadd_int [symmetric]
  1088         zmult_int [symmetric])
  1089       done
  1090 qed
  1091 
  1092 lemma bezout_int:
  1093   fixes x y
  1094   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1095 proof -
  1096   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1097       EX u v. u * x + v * y = gcd x y"
  1098     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1099     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1100     apply (unfold gcd_int_def)
  1101     apply simp
  1102     apply (subst bezw_aux [symmetric])
  1103     apply auto
  1104     done
  1105   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1106       (x \<le> 0 \<and> y \<le> 0)"
  1107     by auto
  1108   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1109     by (erule (1) bezout_aux)
  1110   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1111     apply (insert bezout_aux [of x "-y"])
  1112     apply auto
  1113     apply (rule_tac x = u in exI)
  1114     apply (rule_tac x = "-v" in exI)
  1115     apply (subst gcd_neg2_int [symmetric])
  1116     apply auto
  1117     done
  1118   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1119     apply (insert bezout_aux [of "-x" y])
  1120     apply auto
  1121     apply (rule_tac x = "-u" in exI)
  1122     apply (rule_tac x = v in exI)
  1123     apply (subst gcd_neg1_int [symmetric])
  1124     apply auto
  1125     done
  1126   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1127     apply (insert bezout_aux [of "-x" "-y"])
  1128     apply auto
  1129     apply (rule_tac x = "-u" in exI)
  1130     apply (rule_tac x = "-v" in exI)
  1131     apply (subst gcd_neg1_int [symmetric])
  1132     apply (subst gcd_neg2_int [symmetric])
  1133     apply auto
  1134     done
  1135   ultimately show ?thesis by blast
  1136 qed
  1137 
  1138 text {* versions of Bezout for nat, by Amine Chaieb *}
  1139 
  1140 lemma ind_euclid:
  1141   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1142   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1143   shows "P a b"
  1144 proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
  1145   fix n a b
  1146   assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
  1147   have "a = b \<or> a < b \<or> b < a" by arith
  1148   moreover {assume eq: "a= b"
  1149     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1150     by simp}
  1151   moreover
  1152   {assume lt: "a < b"
  1153     hence "a + b - a < n \<or> a = 0"  using H(2) by arith
  1154     moreover
  1155     {assume "a =0" with z c have "P a b" by blast }
  1156     moreover
  1157     {assume ab: "a + b - a < n"
  1158       have th0: "a + b - a = a + (b - a)" using lt by arith
  1159       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1160       have "P a b" by (simp add: th0[symmetric])}
  1161     ultimately have "P a b" by blast}
  1162   moreover
  1163   {assume lt: "a > b"
  1164     hence "b + a - b < n \<or> b = 0"  using H(2) by arith
  1165     moreover
  1166     {assume "b =0" with z c have "P a b" by blast }
  1167     moreover
  1168     {assume ab: "b + a - b < n"
  1169       have th0: "b + a - b = b + (a - b)" using lt by arith
  1170       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1171       have "P b a" by (simp add: th0[symmetric])
  1172       hence "P a b" using c by blast }
  1173     ultimately have "P a b" by blast}
  1174 ultimately  show "P a b" by blast
  1175 qed
  1176 
  1177 lemma bezout_lemma_nat:
  1178   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1179     (a * x = b * y + d \<or> b * x = a * y + d)"
  1180   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1181     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1182   using ex
  1183   apply clarsimp
  1184   apply (rule_tac x="d" in exI, simp add: dvd_add)
  1185   apply (case_tac "a * x = b * y + d" , simp_all)
  1186   apply (rule_tac x="x + y" in exI)
  1187   apply (rule_tac x="y" in exI)
  1188   apply algebra
  1189   apply (rule_tac x="x" in exI)
  1190   apply (rule_tac x="x + y" in exI)
  1191   apply algebra
  1192 done
  1193 
  1194 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1195     (a * x = b * y + d \<or> b * x = a * y + d)"
  1196   apply(induct a b rule: ind_euclid)
  1197   apply blast
  1198   apply clarify
  1199   apply (rule_tac x="a" in exI, simp add: dvd_add)
  1200   apply clarsimp
  1201   apply (rule_tac x="d" in exI)
  1202   apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  1203   apply (rule_tac x="x+y" in exI)
  1204   apply (rule_tac x="y" in exI)
  1205   apply algebra
  1206   apply (rule_tac x="x" in exI)
  1207   apply (rule_tac x="x+y" in exI)
  1208   apply algebra
  1209 done
  1210 
  1211 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1212     (a * x - b * y = d \<or> b * x - a * y = d)"
  1213   using bezout_add_nat[of a b]
  1214   apply clarsimp
  1215   apply (rule_tac x="d" in exI, simp)
  1216   apply (rule_tac x="x" in exI)
  1217   apply (rule_tac x="y" in exI)
  1218   apply auto
  1219 done
  1220 
  1221 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1222   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1223 proof-
  1224  from nz have ap: "a > 0" by simp
  1225  from bezout_add_nat[of a b]
  1226  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1227    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1228  moreover
  1229     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1230      from H have ?thesis by blast }
  1231  moreover
  1232  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1233    {assume b0: "b = 0" with H  have ?thesis by simp}
  1234    moreover
  1235    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1236      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1237        by auto
  1238      moreover
  1239      {assume db: "d=b"
  1240        from prems have ?thesis apply simp
  1241 	 apply (rule exI[where x = b], simp)
  1242 	 apply (rule exI[where x = b])
  1243 	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1244     moreover
  1245     {assume db: "d < b"
  1246 	{assume "x=0" hence ?thesis  using prems by simp }
  1247 	moreover
  1248 	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1249 	  from db have "d \<le> b - 1" by simp
  1250 	  hence "d*b \<le> b*(b - 1)" by simp
  1251 	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1252 	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1253 	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1254             by simp
  1255 	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1256 	    by (simp only: mult_assoc right_distrib)
  1257 	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1258             by algebra
  1259 	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1260 	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1261 	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1262 	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1263 	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
  1264 	  hence ?thesis using H(1,2)
  1265 	    apply -
  1266 	    apply (rule exI[where x=d], simp)
  1267 	    apply (rule exI[where x="(b - 1) * y"])
  1268 	    by (rule exI[where x="x*(b - 1) - d"], simp)}
  1269 	ultimately have ?thesis by blast}
  1270     ultimately have ?thesis by blast}
  1271   ultimately have ?thesis by blast}
  1272  ultimately show ?thesis by blast
  1273 qed
  1274 
  1275 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1276   shows "\<exists>x y. a * x = b * y + gcd a b"
  1277 proof-
  1278   let ?g = "gcd a b"
  1279   from bezout_add_strong_nat[OF a, of b]
  1280   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1281   from d(1,2) have "d dvd ?g" by simp
  1282   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1283   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1284   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1285   thus ?thesis by blast
  1286 qed
  1287 
  1288 
  1289 subsection {* LCM *}
  1290 
  1291 lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1292   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1293     zmult_int [symmetric] gcd_int_def)
  1294 
  1295 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1296   unfolding lcm_nat_def
  1297   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1298 
  1299 lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
  1300   unfolding lcm_int_def gcd_int_def
  1301   apply (subst int_mult [symmetric])
  1302   apply (subst prod_gcd_lcm_nat [symmetric])
  1303   apply (subst nat_abs_mult_distrib [symmetric])
  1304   apply (simp, simp add: abs_mult)
  1305 done
  1306 
  1307 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1308   unfolding lcm_nat_def by simp
  1309 
  1310 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1311   unfolding lcm_int_def by simp
  1312 
  1313 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1314   unfolding lcm_nat_def by simp
  1315 
  1316 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1317   unfolding lcm_int_def by simp
  1318 
  1319 lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
  1320   unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
  1321 
  1322 lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
  1323   unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
  1324 
  1325 
  1326 lemma lcm_pos_nat:
  1327   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1328 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1329 
  1330 lemma lcm_pos_int:
  1331   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1332   apply (subst lcm_abs_int)
  1333   apply (rule lcm_pos_nat [transferred])
  1334   apply auto
  1335 done
  1336 
  1337 lemma dvd_pos_nat:
  1338   fixes n m :: nat
  1339   assumes "n > 0" and "m dvd n"
  1340   shows "m > 0"
  1341 using assms by (cases m) auto
  1342 
  1343 lemma lcm_least_nat:
  1344   assumes "(m::nat) dvd k" and "n dvd k"
  1345   shows "lcm m n dvd k"
  1346 proof (cases k)
  1347   case 0 then show ?thesis by auto
  1348 next
  1349   case (Suc _) then have pos_k: "k > 0" by auto
  1350   from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1351   with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
  1352   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1353   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1354   from pos_k k_m have pos_p: "p > 0" by auto
  1355   from pos_k k_n have pos_q: "q > 0" by auto
  1356   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1357     by (simp add: mult_ac gcd_mult_distrib_nat)
  1358   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1359     by (simp add: k_m [symmetric] k_n [symmetric])
  1360   also have "\<dots> = k * p * q * gcd m n"
  1361     by (simp add: mult_ac gcd_mult_distrib_nat)
  1362   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1363     by (simp only: k_m [symmetric] k_n [symmetric])
  1364   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1365     by (simp add: mult_ac)
  1366   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1367     by simp
  1368   with prod_gcd_lcm_nat [of m n]
  1369   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1370     by (simp add: mult_ac)
  1371   with pos_gcd have "lcm m n * gcd q p = k" by auto
  1372   then show ?thesis using dvd_def by auto
  1373 qed
  1374 
  1375 lemma lcm_least_int:
  1376   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1377 apply (subst lcm_abs_int)
  1378 apply (rule dvd_trans)
  1379 apply (rule lcm_least_nat [transferred, of _ "abs k" _])
  1380 apply auto
  1381 done
  1382 
  1383 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
  1384 proof (cases m)
  1385   case 0 then show ?thesis by simp
  1386 next
  1387   case (Suc _)
  1388   then have mpos: "m > 0" by simp
  1389   show ?thesis
  1390   proof (cases n)
  1391     case 0 then show ?thesis by simp
  1392   next
  1393     case (Suc _)
  1394     then have npos: "n > 0" by simp
  1395     have "gcd m n dvd n" by simp
  1396     then obtain k where "n = gcd m n * k" using dvd_def by auto
  1397     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1398       by (simp add: mult_ac)
  1399     also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
  1400     finally show ?thesis by (simp add: lcm_nat_def)
  1401   qed
  1402 qed
  1403 
  1404 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1405   apply (subst lcm_abs_int)
  1406   apply (rule dvd_trans)
  1407   prefer 2
  1408   apply (rule lcm_dvd1_nat [transferred])
  1409   apply auto
  1410 done
  1411 
  1412 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1413   by (subst lcm_commute_nat, rule lcm_dvd1_nat)
  1414 
  1415 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1416   by (subst lcm_commute_int, rule lcm_dvd1_int)
  1417 
  1418 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1419 by(metis lcm_dvd1_nat dvd_trans)
  1420 
  1421 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1422 by(metis lcm_dvd2_nat dvd_trans)
  1423 
  1424 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1425 by(metis lcm_dvd1_int dvd_trans)
  1426 
  1427 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1428 by(metis lcm_dvd2_int dvd_trans)
  1429 
  1430 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1431     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1432   by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1433 
  1434 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1435     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1436   by (auto intro: dvd_anti_sym [transferred] lcm_least_int)
  1437 
  1438 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1439   apply (rule sym)
  1440   apply (subst lcm_unique_nat [symmetric])
  1441   apply auto
  1442 done
  1443 
  1444 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1445   apply (rule sym)
  1446   apply (subst lcm_unique_int [symmetric])
  1447   apply auto
  1448 done
  1449 
  1450 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1451 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
  1452 
  1453 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1454 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1455 
  1456 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1457 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1458 
  1459 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1460 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1461 
  1462 lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
  1463 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1464 
  1465 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
  1466 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1467 
  1468 lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
  1469 by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
  1470 
  1471 lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
  1472 by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
  1473 
  1474 lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
  1475 lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
  1476 
  1477 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1478 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1479 
  1480 lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1481 proof qed (auto simp add: gcd_ac_nat)
  1482 
  1483 lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  1484 proof qed (auto simp add: gcd_ac_int)
  1485 
  1486 lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1487 proof qed (auto simp add: lcm_ac_nat)
  1488 
  1489 lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  1490 proof qed (auto simp add: lcm_ac_int)
  1491 
  1492 
  1493 (* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
  1494 
  1495 lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1496 by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
  1497 
  1498 lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1499 by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
  1500 
  1501 lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
  1502 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
  1503 
  1504 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  1505 by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
  1506 
  1507 
  1508 subsection {* Primes *}
  1509 
  1510 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
  1511 
  1512 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
  1513   by (unfold prime_nat_def, auto)
  1514 
  1515 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
  1516   by (unfold prime_nat_def, auto)
  1517 
  1518 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
  1519   by (unfold prime_nat_def, auto)
  1520 
  1521 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
  1522   by (unfold prime_nat_def, auto)
  1523 
  1524 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
  1525   by (unfold prime_nat_def, auto)
  1526 
  1527 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
  1528   by (unfold prime_nat_def, auto)
  1529 
  1530 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
  1531   by (unfold prime_nat_def, auto)
  1532 
  1533 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
  1534   by (unfold prime_int_def prime_nat_def) auto
  1535 
  1536 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
  1537   by (unfold prime_int_def prime_nat_def, auto)
  1538 
  1539 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
  1540   by (unfold prime_int_def prime_nat_def, auto)
  1541 
  1542 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
  1543   by (unfold prime_int_def prime_nat_def, auto)
  1544 
  1545 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
  1546   by (unfold prime_int_def prime_nat_def, auto)
  1547 
  1548 
  1549 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
  1550     m = 1 \<or> m = p))"
  1551   using prime_nat_def [transferred]
  1552     apply (case_tac "p >= 0")
  1553     by (blast, auto simp add: prime_ge_0_int)
  1554 
  1555 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1556   apply (unfold prime_nat_def)
  1557   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
  1558   done
  1559 
  1560 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1561   apply (unfold prime_int_altdef)
  1562   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
  1563   done
  1564 
  1565 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1566   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
  1567 
  1568 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1569   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
  1570 
  1571 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
  1572     p dvd m * n = (p dvd m \<or> p dvd n)"
  1573   by (rule iffI, rule prime_dvd_mult_nat, auto)
  1574 
  1575 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
  1576     p dvd m * n = (p dvd m \<or> p dvd n)"
  1577   by (rule iffI, rule prime_dvd_mult_int, auto)
  1578 
  1579 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1580     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1581   unfolding prime_nat_def dvd_def apply auto
  1582   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)
  1583 
  1584 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1585     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1586   unfolding prime_int_altdef dvd_def
  1587   apply auto
  1588   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)
  1589 
  1590 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
  1591     n > 0 --> (p dvd x^n --> p dvd x)"
  1592   by (induct n rule: nat_induct, auto)
  1593 
  1594 lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
  1595     n > 0 --> (p dvd x^n --> p dvd x)"
  1596   apply (induct n rule: nat_induct, auto)
  1597   apply (frule prime_ge_0_int)
  1598   apply auto
  1599 done
  1600 
  1601 subsubsection{* Make prime naively executable *}
  1602 
  1603 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
  1604   by (simp add: prime_nat_def)
  1605 
  1606 lemma zero_not_prime_int [simp]: "~prime (0::int)"
  1607   by (simp add: prime_int_def)
  1608 
  1609 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
  1610   by (simp add: prime_nat_def)
  1611 
  1612 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
  1613   by (simp add: prime_nat_def One_nat_def)
  1614 
  1615 lemma one_not_prime_int [simp]: "~prime (1::int)"
  1616   by (simp add: prime_int_def)
  1617 
  1618 lemma prime_nat_code[code]:
  1619  "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
  1620 apply(simp add: Ball_def)
  1621 apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
  1622 done
  1623 
  1624 lemma prime_nat_simp:
  1625  "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
  1626 apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
  1627 apply(simp add:nat_number One_nat_def)
  1628 done
  1629 
  1630 lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard]
  1631 
  1632 lemma prime_int_code[code]:
  1633   "prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R")
  1634 proof
  1635   assume "?L" thus "?R"
  1636     by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
  1637 next
  1638     assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
  1639 qed
  1640 
  1641 lemma prime_int_simp:
  1642   "prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))"
  1643 apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto)
  1644 apply simp
  1645 done
  1646 
  1647 lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
  1648 
  1649 declare successor_int_def[simp]
  1650 
  1651 lemma two_is_prime_nat [simp]: "prime (2::nat)"
  1652 by simp
  1653 
  1654 lemma two_is_prime_int [simp]: "prime (2::int)"
  1655 by simp
  1656 
  1657 
  1658 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
  1659   apply (rule coprime_exp_nat)
  1660   apply (subst gcd_commute_nat)
  1661   apply (erule (1) prime_imp_coprime_nat)
  1662 done
  1663 
  1664 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
  1665   apply (rule coprime_exp_int)
  1666   apply (subst gcd_commute_int)
  1667   apply (erule (1) prime_imp_coprime_int)
  1668 done
  1669 
  1670 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1671   apply (rule prime_imp_coprime_nat, assumption)
  1672   apply (unfold prime_nat_def, auto)
  1673 done
  1674 
  1675 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1676   apply (rule prime_imp_coprime_int, assumption)
  1677   apply (unfold prime_int_altdef, clarify)
  1678   apply (drule_tac x = q in spec)
  1679   apply (drule_tac x = p in spec)
  1680   apply auto
  1681 done
  1682 
  1683 lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
  1684   by (rule coprime_exp2_nat, rule primes_coprime_nat)
  1685 
  1686 lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
  1687   by (rule coprime_exp2_int, rule primes_coprime_int)
  1688 
  1689 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
  1690   apply (induct n rule: nat_less_induct)
  1691   apply (case_tac "n = 0")
  1692   using two_is_prime_nat apply blast
  1693   apply (case_tac "prime n")
  1694   apply blast
  1695   apply (subgoal_tac "n > 1")
  1696   apply (frule (1) not_prime_eq_prod_nat)
  1697   apply (auto intro: dvd_mult dvd_mult2)
  1698 done
  1699 
  1700 (* An Isar version:
  1701 
  1702 lemma prime_factor_b_nat:
  1703   fixes n :: nat
  1704   assumes "n \<noteq> 1"
  1705   shows "\<exists>p. prime p \<and> p dvd n"
  1706 
  1707 using `n ~= 1`
  1708 proof (induct n rule: less_induct_nat)
  1709   fix n :: nat
  1710   assume "n ~= 1" and
  1711     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
  1712   thus "\<exists>p. prime p \<and> p dvd n"
  1713   proof -
  1714   {
  1715     assume "n = 0"
  1716     moreover note two_is_prime_nat
  1717     ultimately have ?thesis
  1718       by (auto simp del: two_is_prime_nat)
  1719   }
  1720   moreover
  1721   {
  1722     assume "prime n"
  1723     hence ?thesis by auto
  1724   }
  1725   moreover
  1726   {
  1727     assume "n ~= 0" and "~ prime n"
  1728     with `n ~= 1` have "n > 1" by auto
  1729     with `~ prime n` and not_prime_eq_prod_nat obtain m k where
  1730       "n = m * k" and "1 < m" and "m < n" by blast
  1731     with ih obtain p where "prime p" and "p dvd m" by blast
  1732     with `n = m * k` have ?thesis by auto
  1733   }
  1734   ultimately show ?thesis by blast
  1735   qed
  1736 qed
  1737 
  1738 *)
  1739 
  1740 text {* One property of coprimality is easier to prove via prime factors. *}
  1741 
  1742 lemma prime_divprod_pow_nat:
  1743   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
  1744   shows "p^n dvd a \<or> p^n dvd b"
  1745 proof-
  1746   {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
  1747       apply (cases "n=0", simp_all)
  1748       apply (cases "a=1", simp_all) done}
  1749   moreover
  1750   {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
  1751     then obtain m where m: "n = Suc m" by (cases n, auto)
  1752     from n have "p dvd p^n" by (intro dvd_power, auto)
  1753     also note pab
  1754     finally have pab': "p dvd a * b".
  1755     from prime_dvd_mult_nat[OF p pab']
  1756     have "p dvd a \<or> p dvd b" .
  1757     moreover
  1758     {assume pa: "p dvd a"
  1759       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1760       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
  1761       with p have "coprime b p"
  1762         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
  1763       hence pnb: "coprime (p^n) b"
  1764         by (subst gcd_commute_nat, rule coprime_exp_nat)
  1765       from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
  1766     moreover
  1767     {assume pb: "p dvd b"
  1768       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1769       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
  1770         by auto
  1771       with p have "coprime a p"
  1772         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
  1773       hence pna: "coprime (p^n) a"
  1774         by (subst gcd_commute_nat, rule coprime_exp_nat)
  1775       from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
  1776     ultimately have ?thesis by blast}
  1777   ultimately show ?thesis by blast
  1778 qed
  1779 
  1780 end