src/HOL/GCD.thy
author nipkow
Wed Aug 26 19:54:01 2009 +0200 (2009-08-26)
changeset 32415 1dddf2f64266
parent 32112 6da9c2a49fed
child 32479 521cc9bf2958
permissions -rw-r--r--
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
     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 Jeremy Avigad combined all of these, made everything uniform for the
    24 natural numbers and the integers, and added a number of new theorems.
    25 
    26 Tobias Nipkow cleaned up a lot.
    27 *)
    28 
    29 
    30 header {* GCD *}
    31 
    32 theory GCD
    33 imports Fact
    34 begin
    35 
    36 declare One_nat_def [simp del]
    37 
    38 subsection {* gcd *}
    39 
    40 class gcd = zero + one + dvd +
    41 
    42 fixes
    43   gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
    44   lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    45 
    46 begin
    47 
    48 abbreviation
    49   coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    50 where
    51   "coprime x y == (gcd x y = 1)"
    52 
    53 end
    54 
    55 class prime = one +
    56 
    57 fixes
    58   prime :: "'a \<Rightarrow> bool"
    59 
    60 
    61 (* definitions for the natural numbers *)
    62 
    63 instantiation nat :: gcd
    64 
    65 begin
    66 
    67 fun
    68   gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    69 where
    70   "gcd_nat x y =
    71    (if y = 0 then x else gcd y (x mod y))"
    72 
    73 definition
    74   lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    75 where
    76   "lcm_nat x y = x * y div (gcd x y)"
    77 
    78 instance proof qed
    79 
    80 end
    81 
    82 
    83 instantiation nat :: prime
    84 
    85 begin
    86 
    87 definition
    88   prime_nat :: "nat \<Rightarrow> bool"
    89 where
    90   [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    91 
    92 instance proof qed
    93 
    94 end
    95 
    96 
    97 (* definitions for the integers *)
    98 
    99 instantiation int :: gcd
   100 
   101 begin
   102 
   103 definition
   104   gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
   105 where
   106   "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
   107 
   108 definition
   109   lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
   110 where
   111   "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
   112 
   113 instance proof qed
   114 
   115 end
   116 
   117 
   118 instantiation int :: prime
   119 
   120 begin
   121 
   122 definition
   123   prime_int :: "int \<Rightarrow> bool"
   124 where
   125   [code del]: "prime_int p = prime (nat p)"
   126 
   127 instance proof qed
   128 
   129 end
   130 
   131 
   132 subsection {* Set up Transfer *}
   133 
   134 
   135 lemma transfer_nat_int_gcd:
   136   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   137   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   138   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
   139   unfolding gcd_int_def lcm_int_def prime_int_def
   140   by auto
   141 
   142 lemma transfer_nat_int_gcd_closures:
   143   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
   144   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   145   by (auto simp add: gcd_int_def lcm_int_def)
   146 
   147 declare TransferMorphism_nat_int[transfer add return:
   148     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   149 
   150 lemma transfer_int_nat_gcd:
   151   "gcd (int x) (int y) = int (gcd x y)"
   152   "lcm (int x) (int y) = int (lcm x y)"
   153   "prime (int x) = prime x"
   154   by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
   155 
   156 lemma transfer_int_nat_gcd_closures:
   157   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   158   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   159   by (auto simp add: gcd_int_def lcm_int_def)
   160 
   161 declare TransferMorphism_int_nat[transfer add return:
   162     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   163 
   164 
   165 subsection {* GCD *}
   166 
   167 (* was gcd_induct *)
   168 lemma gcd_nat_induct:
   169   fixes m n :: nat
   170   assumes "\<And>m. P m 0"
   171     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   172   shows "P m n"
   173   apply (rule gcd_nat.induct)
   174   apply (case_tac "y = 0")
   175   using assms apply simp_all
   176 done
   177 
   178 (* specific to int *)
   179 
   180 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
   181   by (simp add: gcd_int_def)
   182 
   183 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
   184   by (simp add: gcd_int_def)
   185 
   186 lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
   187 by(simp add: gcd_int_def)
   188 
   189 lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"
   190 by (simp add: gcd_int_def)
   191 
   192 lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
   193 by (metis abs_idempotent gcd_abs_int)
   194 
   195 lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
   196 by (metis abs_idempotent gcd_abs_int)
   197 
   198 lemma gcd_cases_int:
   199   fixes x :: int and y
   200   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   201       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   202       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   203       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   204   shows "P (gcd x y)"
   205 by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith)
   206 
   207 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   208   by (simp add: gcd_int_def)
   209 
   210 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
   211   by (simp add: lcm_int_def)
   212 
   213 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
   214   by (simp add: lcm_int_def)
   215 
   216 lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"
   217   by (simp add: lcm_int_def)
   218 
   219 lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
   220 by(simp add:lcm_int_def)
   221 
   222 lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
   223 by (metis abs_idempotent lcm_int_def)
   224 
   225 lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
   226 by (metis abs_idempotent lcm_int_def)
   227 
   228 lemma lcm_cases_int:
   229   fixes x :: int and y
   230   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   231       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   232       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   233       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   234   shows "P (lcm x y)"
   235 by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith)
   236 
   237 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   238   by (simp add: lcm_int_def)
   239 
   240 (* was gcd_0, etc. *)
   241 lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
   242   by simp
   243 
   244 (* was igcd_0, etc. *)
   245 lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
   246   by (unfold gcd_int_def, auto)
   247 
   248 lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
   249   by simp
   250 
   251 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
   252   by (unfold gcd_int_def, auto)
   253 
   254 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
   255   by (case_tac "y = 0", auto)
   256 
   257 (* weaker, but useful for the simplifier *)
   258 
   259 lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   260   by simp
   261 
   262 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   263   by simp
   264 
   265 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   266   by (simp add: One_nat_def)
   267 
   268 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   269   by (simp add: gcd_int_def)
   270 
   271 lemma gcd_idem_nat: "gcd (x::nat) x = x"
   272 by simp
   273 
   274 lemma gcd_idem_int: "gcd (x::int) x = abs x"
   275 by (auto simp add: gcd_int_def)
   276 
   277 declare gcd_nat.simps [simp del]
   278 
   279 text {*
   280   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   281   conjunctions don't seem provable separately.
   282 *}
   283 
   284 lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
   285   and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
   286   apply (induct m n rule: gcd_nat_induct)
   287   apply (simp_all add: gcd_non_0_nat)
   288   apply (blast dest: dvd_mod_imp_dvd)
   289 done
   290 
   291 lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"
   292 by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)
   293 
   294 lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"
   295 by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)
   296 
   297 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   298 by(metis gcd_dvd1_nat dvd_trans)
   299 
   300 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   301 by(metis gcd_dvd2_nat dvd_trans)
   302 
   303 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   304 by(metis gcd_dvd1_int dvd_trans)
   305 
   306 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   307 by(metis gcd_dvd2_int dvd_trans)
   308 
   309 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   310   by (rule dvd_imp_le, auto)
   311 
   312 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   313   by (rule dvd_imp_le, auto)
   314 
   315 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   316   by (rule zdvd_imp_le, auto)
   317 
   318 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   319   by (rule zdvd_imp_le, auto)
   320 
   321 lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   322 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
   323 
   324 lemma gcd_greatest_int:
   325   "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   326   apply (subst gcd_abs_int)
   327   apply (subst abs_dvd_iff [symmetric])
   328   apply (rule gcd_greatest_nat [transferred])
   329   apply auto
   330 done
   331 
   332 lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
   333     (k dvd m & k dvd n)"
   334   by (blast intro!: gcd_greatest_nat intro: dvd_trans)
   335 
   336 lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   337   by (blast intro!: gcd_greatest_int intro: dvd_trans)
   338 
   339 lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   340   by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
   341 
   342 lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   343   by (auto simp add: gcd_int_def)
   344 
   345 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   346   by (insert gcd_zero_nat [of m n], arith)
   347 
   348 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   349   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
   350 
   351 lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
   352   by (rule dvd_anti_sym, auto)
   353 
   354 lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
   355   by (auto simp add: gcd_int_def gcd_commute_nat)
   356 
   357 lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
   358   apply (rule dvd_anti_sym)
   359   apply (blast intro: dvd_trans)+
   360 done
   361 
   362 lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
   363   by (auto simp add: gcd_int_def gcd_assoc_nat)
   364 
   365 lemmas gcd_left_commute_nat =
   366   mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat]
   367 
   368 lemmas gcd_left_commute_int =
   369   mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int]
   370 
   371 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
   372   -- {* gcd is an AC-operator *}
   373 
   374 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
   375 
   376 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
   377     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   378   apply auto
   379   apply (rule dvd_anti_sym)
   380   apply (erule (1) gcd_greatest_nat)
   381   apply auto
   382 done
   383 
   384 lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   385     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   386   apply (case_tac "d = 0")
   387   apply force
   388   apply (rule iffI)
   389   apply (rule zdvd_anti_sym)
   390   apply arith
   391   apply (subst gcd_pos_int)
   392   apply clarsimp
   393   apply (drule_tac x = "d + 1" in spec)
   394   apply (frule zdvd_imp_le)
   395   apply (auto intro: gcd_greatest_int)
   396 done
   397 
   398 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   399 by (metis dvd.eq_iff gcd_unique_nat)
   400 
   401 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   402 by (metis dvd.eq_iff gcd_unique_nat)
   403 
   404 lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   405 by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
   406 
   407 lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   408 by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   409 
   410 
   411 text {*
   412   \medskip Multiplication laws
   413 *}
   414 
   415 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   416     -- {* \cite[page 27]{davenport92} *}
   417   apply (induct m n rule: gcd_nat_induct)
   418   apply simp
   419   apply (case_tac "k = 0")
   420   apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
   421 done
   422 
   423 lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   424   apply (subst (1 2) gcd_abs_int)
   425   apply (subst (1 2) abs_mult)
   426   apply (rule gcd_mult_distrib_nat [transferred])
   427   apply auto
   428 done
   429 
   430 lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   431   apply (insert gcd_mult_distrib_nat [of m k n])
   432   apply simp
   433   apply (erule_tac t = m in ssubst)
   434   apply simp
   435   done
   436 
   437 lemma coprime_dvd_mult_int:
   438   "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   439 apply (subst abs_dvd_iff [symmetric])
   440 apply (subst dvd_abs_iff [symmetric])
   441 apply (subst (asm) gcd_abs_int)
   442 apply (rule coprime_dvd_mult_nat [transferred])
   443     prefer 4 apply assumption
   444    apply auto
   445 apply (subst abs_mult [symmetric], auto)
   446 done
   447 
   448 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   449     (k dvd m * n) = (k dvd m)"
   450   by (auto intro: coprime_dvd_mult_nat)
   451 
   452 lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   453     (k dvd m * n) = (k dvd m)"
   454   by (auto intro: coprime_dvd_mult_int)
   455 
   456 lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   457   apply (rule dvd_anti_sym)
   458   apply (rule gcd_greatest_nat)
   459   apply (rule_tac n = k in coprime_dvd_mult_nat)
   460   apply (simp add: gcd_assoc_nat)
   461   apply (simp add: gcd_commute_nat)
   462   apply (simp_all add: mult_commute)
   463 done
   464 
   465 lemma gcd_mult_cancel_int:
   466   "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
   467 apply (subst (1 2) gcd_abs_int)
   468 apply (subst abs_mult)
   469 apply (rule gcd_mult_cancel_nat [transferred], auto)
   470 done
   471 
   472 text {* \medskip Addition laws *}
   473 
   474 lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   475   apply (case_tac "n = 0")
   476   apply (simp_all add: gcd_non_0_nat)
   477 done
   478 
   479 lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   480   apply (subst (1 2) gcd_commute_nat)
   481   apply (subst add_commute)
   482   apply simp
   483 done
   484 
   485 (* to do: add the other variations? *)
   486 
   487 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   488   by (subst gcd_add1_nat [symmetric], auto)
   489 
   490 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   491   apply (subst gcd_commute_nat)
   492   apply (subst gcd_diff1_nat [symmetric])
   493   apply auto
   494   apply (subst gcd_commute_nat)
   495   apply (subst gcd_diff1_nat)
   496   apply assumption
   497   apply (rule gcd_commute_nat)
   498 done
   499 
   500 lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   501   apply (frule_tac b = y and a = x in pos_mod_sign)
   502   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   503   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
   504     zmod_zminus1_eq_if)
   505   apply (frule_tac a = x in pos_mod_bound)
   506   apply (subst (1 2) gcd_commute_nat)
   507   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   508     nat_le_eq_zle)
   509 done
   510 
   511 lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
   512   apply (case_tac "y = 0")
   513   apply force
   514   apply (case_tac "y > 0")
   515   apply (subst gcd_non_0_int, auto)
   516   apply (insert gcd_non_0_int [of "-y" "-x"])
   517   apply (auto simp add: gcd_neg1_int gcd_neg2_int)
   518 done
   519 
   520 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
   521 by (metis gcd_red_int mod_add_self1 zadd_commute)
   522 
   523 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   524 by (metis gcd_add1_int gcd_commute_int zadd_commute)
   525 
   526 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   527 by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
   528 
   529 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   530 by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
   531 
   532 
   533 (* to do: differences, and all variations of addition rules
   534     as simplification rules for nat and int *)
   535 
   536 (* FIXME remove iff *)
   537 lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n"
   538   using mult_dvd_mono [of 1] by auto
   539 
   540 (* to do: add the three variations of these, and for ints? *)
   541 
   542 lemma finite_divisors_nat[simp]:
   543   assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
   544 proof-
   545   have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
   546   from finite_subset[OF _ this] show ?thesis using assms
   547     by(bestsimp intro!:dvd_imp_le)
   548 qed
   549 
   550 lemma finite_divisors_int[simp]:
   551   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
   552 proof-
   553   have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
   554   hence "finite{d. abs d <= abs i}" by simp
   555   from finite_subset[OF _ this] show ?thesis using assms
   556     by(bestsimp intro!:dvd_imp_le_int)
   557 qed
   558 
   559 lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
   560 apply(rule antisym)
   561  apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
   562 apply simp
   563 done
   564 
   565 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
   566 apply(rule antisym)
   567  apply(rule Max_le_iff[THEN iffD2])
   568    apply simp
   569   apply fastsimp
   570  apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
   571 apply simp
   572 done
   573 
   574 lemma gcd_is_Max_divisors_nat:
   575   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
   576 apply(rule Max_eqI[THEN sym])
   577   apply (metis finite_Collect_conjI finite_divisors_nat)
   578  apply simp
   579  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
   580 apply simp
   581 done
   582 
   583 lemma gcd_is_Max_divisors_int:
   584   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
   585 apply(rule Max_eqI[THEN sym])
   586   apply (metis finite_Collect_conjI finite_divisors_int)
   587  apply simp
   588  apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
   589 apply simp
   590 done
   591 
   592 
   593 subsection {* Coprimality *}
   594 
   595 lemma div_gcd_coprime_nat:
   596   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   597   shows "coprime (a div gcd a b) (b div gcd a b)"
   598 proof -
   599   let ?g = "gcd a b"
   600   let ?a' = "a div ?g"
   601   let ?b' = "b div ?g"
   602   let ?g' = "gcd ?a' ?b'"
   603   have dvdg: "?g dvd a" "?g dvd b" by simp_all
   604   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   605   from dvdg dvdg' obtain ka kb ka' kb' where
   606       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   607     unfolding dvd_def by blast
   608   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   609     by simp_all
   610   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   611     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   612       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   613   have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat)
   614   then have gp: "?g > 0" by arith
   615   from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
   616   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   617 qed
   618 
   619 lemma div_gcd_coprime_int:
   620   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   621   shows "coprime (a div gcd a b) (b div gcd a b)"
   622 apply (subst (1 2 3) gcd_abs_int)
   623 apply (subst (1 2) abs_div)
   624   apply simp
   625  apply simp
   626 apply(subst (1 2) abs_gcd_int)
   627 apply (rule div_gcd_coprime_nat [transferred])
   628 using nz apply (auto simp add: gcd_abs_int [symmetric])
   629 done
   630 
   631 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   632   using gcd_unique_nat[of 1 a b, simplified] by auto
   633 
   634 lemma coprime_Suc_0_nat:
   635     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   636   using coprime_nat by (simp add: One_nat_def)
   637 
   638 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
   639     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   640   using gcd_unique_int [of 1 a b]
   641   apply clarsimp
   642   apply (erule subst)
   643   apply (rule iffI)
   644   apply force
   645   apply (drule_tac x = "abs e" in exI)
   646   apply (case_tac "e >= 0")
   647   apply force
   648   apply force
   649 done
   650 
   651 lemma gcd_coprime_nat:
   652   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   653     b: "b = b' * gcd a b"
   654   shows    "coprime a' b'"
   655 
   656   apply (subgoal_tac "a' = a div gcd a b")
   657   apply (erule ssubst)
   658   apply (subgoal_tac "b' = b div gcd a b")
   659   apply (erule ssubst)
   660   apply (rule div_gcd_coprime_nat)
   661   using prems
   662   apply force
   663   apply (subst (1) b)
   664   using z apply force
   665   apply (subst (1) a)
   666   using z apply force
   667 done
   668 
   669 lemma gcd_coprime_int:
   670   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   671     b: "b = b' * gcd a b"
   672   shows    "coprime a' b'"
   673 
   674   apply (subgoal_tac "a' = a div gcd a b")
   675   apply (erule ssubst)
   676   apply (subgoal_tac "b' = b div gcd a b")
   677   apply (erule ssubst)
   678   apply (rule div_gcd_coprime_int)
   679   using prems
   680   apply force
   681   apply (subst (1) b)
   682   using z apply force
   683   apply (subst (1) a)
   684   using z apply force
   685 done
   686 
   687 lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   688     shows "coprime d (a * b)"
   689   apply (subst gcd_commute_nat)
   690   using da apply (subst gcd_mult_cancel_nat)
   691   apply (subst gcd_commute_nat, assumption)
   692   apply (subst gcd_commute_nat, rule db)
   693 done
   694 
   695 lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
   696     shows "coprime d (a * b)"
   697   apply (subst gcd_commute_int)
   698   using da apply (subst gcd_mult_cancel_int)
   699   apply (subst gcd_commute_int, assumption)
   700   apply (subst gcd_commute_int, rule db)
   701 done
   702 
   703 lemma coprime_lmult_nat:
   704   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   705 proof -
   706   have "gcd d a dvd gcd d (a * b)"
   707     by (rule gcd_greatest_nat, auto)
   708   with dab show ?thesis
   709     by auto
   710 qed
   711 
   712 lemma coprime_lmult_int:
   713   assumes "coprime (d::int) (a * b)" shows "coprime d a"
   714 proof -
   715   have "gcd d a dvd gcd d (a * b)"
   716     by (rule gcd_greatest_int, auto)
   717   with assms show ?thesis
   718     by auto
   719 qed
   720 
   721 lemma coprime_rmult_nat:
   722   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   723 proof -
   724   have "gcd d b dvd gcd d (a * b)"
   725     by (rule gcd_greatest_nat, auto intro: dvd_mult)
   726   with assms show ?thesis
   727     by auto
   728 qed
   729 
   730 lemma coprime_rmult_int:
   731   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   732 proof -
   733   have "gcd d b dvd gcd d (a * b)"
   734     by (rule gcd_greatest_int, auto intro: dvd_mult)
   735   with dab show ?thesis
   736     by auto
   737 qed
   738 
   739 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   740     coprime d a \<and>  coprime d b"
   741   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   742     coprime_mult_nat[of d a b]
   743   by blast
   744 
   745 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   746     coprime d a \<and>  coprime d b"
   747   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   748     coprime_mult_int[of d a b]
   749   by blast
   750 
   751 lemma gcd_coprime_exists_nat:
   752     assumes nz: "gcd (a::nat) b \<noteq> 0"
   753     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   754   apply (rule_tac x = "a div gcd a b" in exI)
   755   apply (rule_tac x = "b div gcd a b" in exI)
   756   using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)
   757 done
   758 
   759 lemma gcd_coprime_exists_int:
   760     assumes nz: "gcd (a::int) b \<noteq> 0"
   761     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   762   apply (rule_tac x = "a div gcd a b" in exI)
   763   apply (rule_tac x = "b div gcd a b" in exI)
   764   using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self)
   765 done
   766 
   767 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   768   by (induct n, simp_all add: coprime_mult_nat)
   769 
   770 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   771   by (induct n, simp_all add: coprime_mult_int)
   772 
   773 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   774   apply (rule coprime_exp_nat)
   775   apply (subst gcd_commute_nat)
   776   apply (rule coprime_exp_nat)
   777   apply (subst gcd_commute_nat, assumption)
   778 done
   779 
   780 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   781   apply (rule coprime_exp_int)
   782   apply (subst gcd_commute_int)
   783   apply (rule coprime_exp_int)
   784   apply (subst gcd_commute_int, assumption)
   785 done
   786 
   787 lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   788 proof (cases)
   789   assume "a = 0 & b = 0"
   790   thus ?thesis by simp
   791   next assume "~(a = 0 & b = 0)"
   792   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   793     by (auto simp:div_gcd_coprime_nat)
   794   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   795       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   796     apply (subst (1 2) mult_commute)
   797     apply (subst gcd_mult_distrib_nat [symmetric])
   798     apply simp
   799     done
   800   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   801     apply (subst div_power)
   802     apply auto
   803     apply (rule dvd_div_mult_self)
   804     apply (rule dvd_power_same)
   805     apply auto
   806     done
   807   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
   808     apply (subst div_power)
   809     apply auto
   810     apply (rule dvd_div_mult_self)
   811     apply (rule dvd_power_same)
   812     apply auto
   813     done
   814   finally show ?thesis .
   815 qed
   816 
   817 lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   818   apply (subst (1 2) gcd_abs_int)
   819   apply (subst (1 2) power_abs)
   820   apply (rule gcd_exp_nat [where n = n, transferred])
   821   apply auto
   822 done
   823 
   824 lemma coprime_divprod_nat: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   825   using coprime_dvd_mult_iff_nat[of d a b]
   826   by (auto simp add: mult_commute)
   827 
   828 lemma coprime_divprod_int: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   829   using coprime_dvd_mult_iff_int[of d a b]
   830   by (auto simp add: mult_commute)
   831 
   832 lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
   833   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   834 proof-
   835   let ?g = "gcd a b"
   836   {assume "?g = 0" with dc have ?thesis by auto}
   837   moreover
   838   {assume z: "?g \<noteq> 0"
   839     from gcd_coprime_exists_nat[OF z]
   840     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   841       by blast
   842     have thb: "?g dvd b" by auto
   843     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   844     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   845     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   846     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   847     with z have th_1: "a' dvd b' * c" by auto
   848     from coprime_dvd_mult_nat[OF ab'(3)] th_1
   849     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   850     from ab' have "a = ?g*a'" by algebra
   851     with thb thc have ?thesis by blast }
   852   ultimately show ?thesis by blast
   853 qed
   854 
   855 lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
   856   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   857 proof-
   858   let ?g = "gcd a b"
   859   {assume "?g = 0" with dc have ?thesis by auto}
   860   moreover
   861   {assume z: "?g \<noteq> 0"
   862     from gcd_coprime_exists_int[OF z]
   863     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   864       by blast
   865     have thb: "?g dvd b" by auto
   866     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   867     with dc have th0: "a' dvd b*c"
   868       using dvd_trans[of a' a "b*c"] by simp
   869     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   870     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   871     with z have th_1: "a' dvd b' * c" by auto
   872     from coprime_dvd_mult_int[OF ab'(3)] th_1
   873     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   874     from ab' have "a = ?g*a'" by algebra
   875     with thb thc have ?thesis by blast }
   876   ultimately show ?thesis by blast
   877 qed
   878 
   879 lemma pow_divides_pow_nat:
   880   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   881   shows "a dvd b"
   882 proof-
   883   let ?g = "gcd a b"
   884   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   885   {assume "?g = 0" with ab n have ?thesis by auto }
   886   moreover
   887   {assume z: "?g \<noteq> 0"
   888     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   889     from gcd_coprime_exists_nat[OF z]
   890     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   891       by blast
   892     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   893       by (simp add: ab'(1,2)[symmetric])
   894     hence "?g^n*a'^n dvd ?g^n *b'^n"
   895       by (simp only: power_mult_distrib mult_commute)
   896     with zn z n have th0:"a'^n dvd b'^n" by auto
   897     have "a' dvd a'^n" by (simp add: m)
   898     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   899     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   900     from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
   901     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   902     hence "a'*?g dvd b'*?g" by simp
   903     with ab'(1,2)  have ?thesis by simp }
   904   ultimately show ?thesis by blast
   905 qed
   906 
   907 lemma pow_divides_pow_int:
   908   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
   909   shows "a dvd b"
   910 proof-
   911   let ?g = "gcd a b"
   912   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   913   {assume "?g = 0" with ab n have ?thesis by auto }
   914   moreover
   915   {assume z: "?g \<noteq> 0"
   916     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   917     from gcd_coprime_exists_int[OF z]
   918     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   919       by blast
   920     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   921       by (simp add: ab'(1,2)[symmetric])
   922     hence "?g^n*a'^n dvd ?g^n *b'^n"
   923       by (simp only: power_mult_distrib mult_commute)
   924     with zn z n have th0:"a'^n dvd b'^n" by auto
   925     have "a' dvd a'^n" by (simp add: m)
   926     with th0 have "a' dvd b'^n"
   927       using dvd_trans[of a' "a'^n" "b'^n"] by simp
   928     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   929     from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
   930     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   931     hence "a'*?g dvd b'*?g" by simp
   932     with ab'(1,2)  have ?thesis by simp }
   933   ultimately show ?thesis by blast
   934 qed
   935 
   936 (* FIXME move to Divides(?) *)
   937 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   938   by (auto intro: pow_divides_pow_nat dvd_power_same)
   939 
   940 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   941   by (auto intro: pow_divides_pow_int dvd_power_same)
   942 
   943 lemma divides_mult_nat:
   944   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   945   shows "m * n dvd r"
   946 proof-
   947   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   948     unfolding dvd_def by blast
   949   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   950   hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
   951   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   952   from n' k show ?thesis unfolding dvd_def by auto
   953 qed
   954 
   955 lemma divides_mult_int:
   956   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   957   shows "m * n dvd r"
   958 proof-
   959   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   960     unfolding dvd_def by blast
   961   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   962   hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
   963   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   964   from n' k show ?thesis unfolding dvd_def by auto
   965 qed
   966 
   967 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   968   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   969   apply force
   970   apply (rule dvd_diff_nat)
   971   apply auto
   972 done
   973 
   974 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
   975   using coprime_plus_one_nat by (simp add: One_nat_def)
   976 
   977 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
   978   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   979   apply force
   980   apply (rule dvd_diff)
   981   apply auto
   982 done
   983 
   984 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   985   using coprime_plus_one_nat [of "n - 1"]
   986     gcd_commute_nat [of "n - 1" n] by auto
   987 
   988 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
   989   using coprime_plus_one_int [of "n - 1"]
   990     gcd_commute_int [of "n - 1" n] by auto
   991 
   992 lemma setprod_coprime_nat [rule_format]:
   993     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
   994   apply (case_tac "finite A")
   995   apply (induct set: finite)
   996   apply (auto simp add: gcd_mult_cancel_nat)
   997 done
   998 
   999 lemma setprod_coprime_int [rule_format]:
  1000     "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
  1001   apply (case_tac "finite A")
  1002   apply (induct set: finite)
  1003   apply (auto simp add: gcd_mult_cancel_int)
  1004 done
  1005 
  1006 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  1007   unfolding prime_nat_def
  1008   apply (subst even_mult_two_ex)
  1009   apply clarify
  1010   apply (drule_tac x = 2 in spec)
  1011   apply auto
  1012 done
  1013 
  1014 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  1015   unfolding prime_int_def
  1016   apply (frule prime_odd_nat)
  1017   apply (auto simp add: even_nat_def)
  1018 done
  1019 
  1020 lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1021     x dvd b \<Longrightarrow> x = 1"
  1022   apply (subgoal_tac "x dvd gcd a b")
  1023   apply simp
  1024   apply (erule (1) gcd_greatest_nat)
  1025 done
  1026 
  1027 lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1028     x dvd b \<Longrightarrow> abs x = 1"
  1029   apply (subgoal_tac "x dvd gcd a b")
  1030   apply simp
  1031   apply (erule (1) gcd_greatest_int)
  1032 done
  1033 
  1034 lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
  1035     coprime d e"
  1036   apply (auto simp add: dvd_def)
  1037   apply (frule coprime_lmult_int)
  1038   apply (subst gcd_commute_int)
  1039   apply (subst (asm) (2) gcd_commute_int)
  1040   apply (erule coprime_lmult_int)
  1041 done
  1042 
  1043 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1044 apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
  1045 done
  1046 
  1047 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1048 apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
  1049 done
  1050 
  1051 
  1052 subsection {* Bezout's theorem *}
  1053 
  1054 (* Function bezw returns a pair of witnesses to Bezout's theorem --
  1055    see the theorems that follow the definition. *)
  1056 fun
  1057   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1058 where
  1059   "bezw x y =
  1060   (if y = 0 then (1, 0) else
  1061       (snd (bezw y (x mod y)),
  1062        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1063 
  1064 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1065 
  1066 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1067        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1068   by simp
  1069 
  1070 declare bezw.simps [simp del]
  1071 
  1072 lemma bezw_aux [rule_format]:
  1073     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1074 proof (induct x y rule: gcd_nat_induct)
  1075   fix m :: nat
  1076   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1077     by auto
  1078   next fix m :: nat and n
  1079     assume ngt0: "n > 0" and
  1080       ih: "fst (bezw n (m mod n)) * int n +
  1081         snd (bezw n (m mod n)) * int (m mod n) =
  1082         int (gcd n (m mod n))"
  1083     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1084       apply (simp add: bezw_non_0 gcd_non_0_nat)
  1085       apply (erule subst)
  1086       apply (simp add: ring_simps)
  1087       apply (subst mod_div_equality [of m n, symmetric])
  1088       (* applying simp here undoes the last substitution!
  1089          what is procedure cancel_div_mod? *)
  1090       apply (simp only: ring_simps zadd_int [symmetric]
  1091         zmult_int [symmetric])
  1092       done
  1093 qed
  1094 
  1095 lemma bezout_int:
  1096   fixes x y
  1097   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1098 proof -
  1099   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1100       EX u v. u * x + v * y = gcd x y"
  1101     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1102     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1103     apply (unfold gcd_int_def)
  1104     apply simp
  1105     apply (subst bezw_aux [symmetric])
  1106     apply auto
  1107     done
  1108   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1109       (x \<le> 0 \<and> y \<le> 0)"
  1110     by auto
  1111   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1112     by (erule (1) bezout_aux)
  1113   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1114     apply (insert bezout_aux [of x "-y"])
  1115     apply auto
  1116     apply (rule_tac x = u in exI)
  1117     apply (rule_tac x = "-v" in exI)
  1118     apply (subst gcd_neg2_int [symmetric])
  1119     apply auto
  1120     done
  1121   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1122     apply (insert bezout_aux [of "-x" y])
  1123     apply auto
  1124     apply (rule_tac x = "-u" in exI)
  1125     apply (rule_tac x = v in exI)
  1126     apply (subst gcd_neg1_int [symmetric])
  1127     apply auto
  1128     done
  1129   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1130     apply (insert bezout_aux [of "-x" "-y"])
  1131     apply auto
  1132     apply (rule_tac x = "-u" in exI)
  1133     apply (rule_tac x = "-v" in exI)
  1134     apply (subst gcd_neg1_int [symmetric])
  1135     apply (subst gcd_neg2_int [symmetric])
  1136     apply auto
  1137     done
  1138   ultimately show ?thesis by blast
  1139 qed
  1140 
  1141 text {* versions of Bezout for nat, by Amine Chaieb *}
  1142 
  1143 lemma ind_euclid:
  1144   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1145   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1146   shows "P a b"
  1147 proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
  1148   fix n a b
  1149   assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
  1150   have "a = b \<or> a < b \<or> b < a" by arith
  1151   moreover {assume eq: "a= b"
  1152     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1153     by simp}
  1154   moreover
  1155   {assume lt: "a < b"
  1156     hence "a + b - a < n \<or> a = 0"  using H(2) by arith
  1157     moreover
  1158     {assume "a =0" with z c have "P a b" by blast }
  1159     moreover
  1160     {assume ab: "a + b - a < n"
  1161       have th0: "a + b - a = a + (b - a)" using lt by arith
  1162       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1163       have "P a b" by (simp add: th0[symmetric])}
  1164     ultimately have "P a b" by blast}
  1165   moreover
  1166   {assume lt: "a > b"
  1167     hence "b + a - b < n \<or> b = 0"  using H(2) by arith
  1168     moreover
  1169     {assume "b =0" with z c have "P a b" by blast }
  1170     moreover
  1171     {assume ab: "b + a - b < n"
  1172       have th0: "b + a - b = b + (a - b)" using lt by arith
  1173       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1174       have "P b a" by (simp add: th0[symmetric])
  1175       hence "P a b" using c by blast }
  1176     ultimately have "P a b" by blast}
  1177 ultimately  show "P a b" by blast
  1178 qed
  1179 
  1180 lemma bezout_lemma_nat:
  1181   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1182     (a * x = b * y + d \<or> b * x = a * y + d)"
  1183   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1184     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1185   using ex
  1186   apply clarsimp
  1187   apply (rule_tac x="d" in exI, simp add: dvd_add)
  1188   apply (case_tac "a * x = b * y + d" , simp_all)
  1189   apply (rule_tac x="x + y" in exI)
  1190   apply (rule_tac x="y" in exI)
  1191   apply algebra
  1192   apply (rule_tac x="x" in exI)
  1193   apply (rule_tac x="x + y" in exI)
  1194   apply algebra
  1195 done
  1196 
  1197 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1198     (a * x = b * y + d \<or> b * x = a * y + d)"
  1199   apply(induct a b rule: ind_euclid)
  1200   apply blast
  1201   apply clarify
  1202   apply (rule_tac x="a" in exI, simp add: dvd_add)
  1203   apply clarsimp
  1204   apply (rule_tac x="d" in exI)
  1205   apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  1206   apply (rule_tac x="x+y" in exI)
  1207   apply (rule_tac x="y" in exI)
  1208   apply algebra
  1209   apply (rule_tac x="x" in exI)
  1210   apply (rule_tac x="x+y" in exI)
  1211   apply algebra
  1212 done
  1213 
  1214 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1215     (a * x - b * y = d \<or> b * x - a * y = d)"
  1216   using bezout_add_nat[of a b]
  1217   apply clarsimp
  1218   apply (rule_tac x="d" in exI, simp)
  1219   apply (rule_tac x="x" in exI)
  1220   apply (rule_tac x="y" in exI)
  1221   apply auto
  1222 done
  1223 
  1224 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1225   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1226 proof-
  1227  from nz have ap: "a > 0" by simp
  1228  from bezout_add_nat[of a b]
  1229  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1230    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1231  moreover
  1232     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1233      from H have ?thesis by blast }
  1234  moreover
  1235  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1236    {assume b0: "b = 0" with H  have ?thesis by simp}
  1237    moreover
  1238    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1239      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1240        by auto
  1241      moreover
  1242      {assume db: "d=b"
  1243        from prems have ?thesis apply simp
  1244 	 apply (rule exI[where x = b], simp)
  1245 	 apply (rule exI[where x = b])
  1246 	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1247     moreover
  1248     {assume db: "d < b"
  1249 	{assume "x=0" hence ?thesis  using prems by simp }
  1250 	moreover
  1251 	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1252 	  from db have "d \<le> b - 1" by simp
  1253 	  hence "d*b \<le> b*(b - 1)" by simp
  1254 	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1255 	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1256 	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1257             by simp
  1258 	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1259 	    by (simp only: mult_assoc right_distrib)
  1260 	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1261             by algebra
  1262 	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1263 	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1264 	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1265 	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1266 	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
  1267 	  hence ?thesis using H(1,2)
  1268 	    apply -
  1269 	    apply (rule exI[where x=d], simp)
  1270 	    apply (rule exI[where x="(b - 1) * y"])
  1271 	    by (rule exI[where x="x*(b - 1) - d"], simp)}
  1272 	ultimately have ?thesis by blast}
  1273     ultimately have ?thesis by blast}
  1274   ultimately have ?thesis by blast}
  1275  ultimately show ?thesis by blast
  1276 qed
  1277 
  1278 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1279   shows "\<exists>x y. a * x = b * y + gcd a b"
  1280 proof-
  1281   let ?g = "gcd a b"
  1282   from bezout_add_strong_nat[OF a, of b]
  1283   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1284   from d(1,2) have "d dvd ?g" by simp
  1285   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1286   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1287   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1288   thus ?thesis by blast
  1289 qed
  1290 
  1291 
  1292 subsection {* LCM *}
  1293 
  1294 lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1295   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1296     zmult_int [symmetric] gcd_int_def)
  1297 
  1298 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1299   unfolding lcm_nat_def
  1300   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1301 
  1302 lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
  1303   unfolding lcm_int_def gcd_int_def
  1304   apply (subst int_mult [symmetric])
  1305   apply (subst prod_gcd_lcm_nat [symmetric])
  1306   apply (subst nat_abs_mult_distrib [symmetric])
  1307   apply (simp, simp add: abs_mult)
  1308 done
  1309 
  1310 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1311   unfolding lcm_nat_def by simp
  1312 
  1313 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1314   unfolding lcm_int_def by simp
  1315 
  1316 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1317   unfolding lcm_nat_def by simp
  1318 
  1319 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1320   unfolding lcm_int_def by simp
  1321 
  1322 lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
  1323   unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
  1324 
  1325 lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
  1326   unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
  1327 
  1328 
  1329 lemma lcm_pos_nat:
  1330   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1331 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1332 
  1333 lemma lcm_pos_int:
  1334   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1335   apply (subst lcm_abs_int)
  1336   apply (rule lcm_pos_nat [transferred])
  1337   apply auto
  1338 done
  1339 
  1340 lemma dvd_pos_nat:
  1341   fixes n m :: nat
  1342   assumes "n > 0" and "m dvd n"
  1343   shows "m > 0"
  1344 using assms by (cases m) auto
  1345 
  1346 lemma lcm_least_nat:
  1347   assumes "(m::nat) dvd k" and "n dvd k"
  1348   shows "lcm m n dvd k"
  1349 proof (cases k)
  1350   case 0 then show ?thesis by auto
  1351 next
  1352   case (Suc _) then have pos_k: "k > 0" by auto
  1353   from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1354   with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
  1355   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1356   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1357   from pos_k k_m have pos_p: "p > 0" by auto
  1358   from pos_k k_n have pos_q: "q > 0" by auto
  1359   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1360     by (simp add: mult_ac gcd_mult_distrib_nat)
  1361   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1362     by (simp add: k_m [symmetric] k_n [symmetric])
  1363   also have "\<dots> = k * p * q * gcd m n"
  1364     by (simp add: mult_ac gcd_mult_distrib_nat)
  1365   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1366     by (simp only: k_m [symmetric] k_n [symmetric])
  1367   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1368     by (simp add: mult_ac)
  1369   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1370     by simp
  1371   with prod_gcd_lcm_nat [of m n]
  1372   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1373     by (simp add: mult_ac)
  1374   with pos_gcd have "lcm m n * gcd q p = k" by auto
  1375   then show ?thesis using dvd_def by auto
  1376 qed
  1377 
  1378 lemma lcm_least_int:
  1379   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1380 apply (subst lcm_abs_int)
  1381 apply (rule dvd_trans)
  1382 apply (rule lcm_least_nat [transferred, of _ "abs k" _])
  1383 apply auto
  1384 done
  1385 
  1386 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
  1387 proof (cases m)
  1388   case 0 then show ?thesis by simp
  1389 next
  1390   case (Suc _)
  1391   then have mpos: "m > 0" by simp
  1392   show ?thesis
  1393   proof (cases n)
  1394     case 0 then show ?thesis by simp
  1395   next
  1396     case (Suc _)
  1397     then have npos: "n > 0" by simp
  1398     have "gcd m n dvd n" by simp
  1399     then obtain k where "n = gcd m n * k" using dvd_def by auto
  1400     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1401       by (simp add: mult_ac)
  1402     also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
  1403     finally show ?thesis by (simp add: lcm_nat_def)
  1404   qed
  1405 qed
  1406 
  1407 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1408   apply (subst lcm_abs_int)
  1409   apply (rule dvd_trans)
  1410   prefer 2
  1411   apply (rule lcm_dvd1_nat [transferred])
  1412   apply auto
  1413 done
  1414 
  1415 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1416   by (subst lcm_commute_nat, rule lcm_dvd1_nat)
  1417 
  1418 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1419   by (subst lcm_commute_int, rule lcm_dvd1_int)
  1420 
  1421 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1422 by(metis lcm_dvd1_nat dvd_trans)
  1423 
  1424 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1425 by(metis lcm_dvd2_nat dvd_trans)
  1426 
  1427 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1428 by(metis lcm_dvd1_int dvd_trans)
  1429 
  1430 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1431 by(metis lcm_dvd2_int dvd_trans)
  1432 
  1433 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1434     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1435   by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1436 
  1437 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1438     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1439   by (auto intro: dvd_anti_sym [transferred] lcm_least_int)
  1440 
  1441 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1442   apply (rule sym)
  1443   apply (subst lcm_unique_nat [symmetric])
  1444   apply auto
  1445 done
  1446 
  1447 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1448   apply (rule sym)
  1449   apply (subst lcm_unique_int [symmetric])
  1450   apply auto
  1451 done
  1452 
  1453 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1454 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
  1455 
  1456 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1457 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1458 
  1459 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1460 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1461 
  1462 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1463 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1464 
  1465 lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
  1466 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1467 
  1468 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
  1469 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1470 
  1471 lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
  1472 by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
  1473 
  1474 lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
  1475 by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
  1476 
  1477 lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
  1478 lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
  1479 
  1480 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1481 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1482 
  1483 lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1484 proof qed (auto simp add: gcd_ac_nat)
  1485 
  1486 lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  1487 proof qed (auto simp add: gcd_ac_int)
  1488 
  1489 lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1490 proof qed (auto simp add: lcm_ac_nat)
  1491 
  1492 lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  1493 proof qed (auto simp add: lcm_ac_int)
  1494 
  1495 
  1496 (* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
  1497 
  1498 lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1499 by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
  1500 
  1501 lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1502 by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
  1503 
  1504 lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
  1505 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
  1506 
  1507 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  1508 by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
  1509 
  1510 subsubsection {* The complete divisibility lattice *}
  1511 
  1512 
  1513 interpretation gcd_semilattice_nat: lower_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
  1514 proof
  1515   case goal3 thus ?case by(metis gcd_unique_nat)
  1516 qed auto
  1517 
  1518 interpretation lcm_semilattice_nat: upper_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
  1519 proof
  1520   case goal3 thus ?case by(metis lcm_unique_nat)
  1521 qed auto
  1522 
  1523 interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
  1524 
  1525 text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
  1526 GCD is defined via LCM to facilitate the proof that we have a complete lattice.
  1527 Later on we show that GCD and Gcd coincide on finite sets.
  1528 *}
  1529 context gcd
  1530 begin
  1531 
  1532 definition Gcd :: "'a set \<Rightarrow> 'a"
  1533 where "Gcd = fold gcd 0"
  1534 
  1535 definition Lcm :: "'a set \<Rightarrow> 'a"
  1536 where "Lcm = fold lcm 1"
  1537 
  1538 definition LCM :: "'a set \<Rightarrow> 'a" where
  1539 "LCM M = (if finite M then Lcm M else 0)"
  1540 
  1541 definition GCD :: "'a set \<Rightarrow> 'a" where
  1542 "GCD M = LCM(INT m:M. {d. d dvd m})"
  1543 
  1544 end
  1545 
  1546 lemma Gcd_empty[simp]: "Gcd {} = 0"
  1547 by(simp add:Gcd_def)
  1548 
  1549 lemma Lcm_empty[simp]: "Lcm {} = 1"
  1550 by(simp add:Lcm_def)
  1551 
  1552 lemma GCD_empty_nat[simp]: "GCD {} = (0::nat)"
  1553 by(simp add:GCD_def LCM_def)
  1554 
  1555 lemma LCM_eq_Lcm[simp]: "finite M \<Longrightarrow> LCM M = Lcm M"
  1556 by(simp add:LCM_def)
  1557 
  1558 lemma Lcm_insert_nat [simp]:
  1559   assumes "finite N"
  1560   shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
  1561 proof -
  1562   interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
  1563     by (rule fun_left_comm_idem_lcm_nat)
  1564   from assms show ?thesis by(simp add: Lcm_def)
  1565 qed
  1566 
  1567 lemma Lcm_insert_int [simp]:
  1568   assumes "finite N"
  1569   shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
  1570 proof -
  1571   interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
  1572     by (rule fun_left_comm_idem_lcm_int)
  1573   from assms show ?thesis by(simp add: Lcm_def)
  1574 qed
  1575 
  1576 lemma Gcd_insert_nat [simp]:
  1577   assumes "finite N"
  1578   shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
  1579 proof -
  1580   interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
  1581     by (rule fun_left_comm_idem_gcd_nat)
  1582   from assms show ?thesis by(simp add: Gcd_def)
  1583 qed
  1584 
  1585 lemma Gcd_insert_int [simp]:
  1586   assumes "finite N"
  1587   shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
  1588 proof -
  1589   interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
  1590     by (rule fun_left_comm_idem_gcd_int)
  1591   from assms show ?thesis by(simp add: Gcd_def)
  1592 qed
  1593 
  1594 lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
  1595 by(induct rule:finite_ne_induct) auto
  1596 
  1597 lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
  1598 by (metis Lcm0_iff empty_iff)
  1599 
  1600 lemma Gcd_dvd_nat [simp]:
  1601   assumes "finite M" and "(m::nat) \<in> M"
  1602   shows "Gcd M dvd m"
  1603 proof -
  1604   show ?thesis using gcd_semilattice_nat.fold_inf_le_inf[OF assms, of 0] by (simp add: Gcd_def)
  1605 qed
  1606 
  1607 lemma dvd_Gcd_nat[simp]:
  1608   assumes "finite M" and "ALL (m::nat) : M. n dvd m"
  1609   shows "n dvd Gcd M"
  1610 proof -
  1611   show ?thesis using gcd_semilattice_nat.inf_le_fold_inf[OF assms, of 0] by (simp add: Gcd_def)
  1612 qed
  1613 
  1614 lemma dvd_Lcm_nat [simp]:
  1615   assumes "finite M" and "(m::nat) \<in> M"
  1616   shows "m dvd Lcm M"
  1617 proof -
  1618   show ?thesis using lcm_semilattice_nat.sup_le_fold_sup[OF assms, of 1] by (simp add: Lcm_def)
  1619 qed
  1620 
  1621 lemma Lcm_dvd_nat[simp]:
  1622   assumes "finite M" and "ALL (m::nat) : M. m dvd n"
  1623   shows "Lcm M dvd n"
  1624 proof -
  1625   show ?thesis using lcm_semilattice_nat.fold_sup_le_sup[OF assms, of 1] by (simp add: Lcm_def)
  1626 qed
  1627 
  1628 interpretation gcd_lcm_complete_lattice_nat:
  1629   complete_lattice "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0 GCD LCM
  1630 proof
  1631   case goal1 show ?case by simp
  1632 next
  1633   case goal2 show ?case by simp
  1634 next
  1635   case goal5 thus ?case by (auto simp: LCM_def)
  1636 next
  1637   case goal6 thus ?case
  1638     by(auto simp: LCM_def)(metis finite_nat_set_iff_bounded_le gcd_proj2_if_dvd_nat gcd_le1_nat)
  1639 next
  1640   case goal3 thus ?case by (auto simp: GCD_def LCM_def)(metis finite_INT finite_divisors_nat)
  1641 next
  1642   case goal4 thus ?case by(auto simp: LCM_def GCD_def)
  1643 qed
  1644 
  1645 text{* Alternative characterizations of Gcd and GCD: *}
  1646 
  1647 lemma Gcd_eq_Max: "finite(M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> Gcd M = Max(\<Inter>m\<in>M. {d. d dvd m})"
  1648 apply(rule antisym)
  1649  apply(rule Max_ge)
  1650   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1651  apply simp
  1652 apply (rule Max_le_iff[THEN iffD2])
  1653   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1654  apply fastsimp
  1655 apply clarsimp
  1656 apply (metis Gcd_dvd_nat Max_in dvd_0_left dvd_Gcd_nat dvd_imp_le linorder_antisym_conv3 not_less0)
  1657 done
  1658 
  1659 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
  1660 apply(induct pred:finite)
  1661  apply simp
  1662 apply(case_tac "x=0")
  1663  apply simp
  1664 apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
  1665  apply simp
  1666 apply blast
  1667 done
  1668 
  1669 lemma Lcm_in_lcm_closed_set_nat:
  1670   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
  1671 apply(induct rule:finite_linorder_min_induct)
  1672  apply simp
  1673 apply simp
  1674 apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
  1675  apply simp
  1676  apply(case_tac "A={}")
  1677   apply simp
  1678  apply simp
  1679 apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  1680 done
  1681 
  1682 lemma Lcm_eq_Max_nat:
  1683   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M = Max M"
  1684 apply(rule antisym)
  1685  apply(rule Max_ge, assumption)
  1686  apply(erule (2) Lcm_in_lcm_closed_set_nat)
  1687 apply clarsimp
  1688 apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
  1689 done
  1690 
  1691 text{* Finally GCD is Gcd: *}
  1692 
  1693 lemma GCD_eq_Gcd[simp]: assumes "finite(M::nat set)" shows "GCD M = Gcd M"
  1694 proof-
  1695   have divisors_remove0_nat: "(\<Inter>m\<in>M. {d::nat. d dvd m}) = (\<Inter>m\<in>M-{0}. {d::nat. d dvd m})" by auto
  1696   show ?thesis
  1697   proof cases
  1698     assume "M={}" thus ?thesis by simp
  1699   next
  1700     assume "M\<noteq>{}"
  1701     show ?thesis
  1702     proof cases
  1703       assume "M={0}" thus ?thesis by(simp add:GCD_def LCM_def)
  1704     next
  1705       assume "M\<noteq>{0}"
  1706       with `M\<noteq>{}` assms show ?thesis
  1707 	apply(subst Gcd_remove0_nat[OF assms])
  1708 	apply(simp add:GCD_def)
  1709 	apply(subst divisors_remove0_nat)
  1710 	apply(simp add:LCM_def)
  1711 	apply rule
  1712 	 apply rule
  1713 	 apply(subst Gcd_eq_Max)
  1714 	    apply simp
  1715 	   apply blast
  1716 	  apply blast
  1717 	 apply(rule Lcm_eq_Max_nat)
  1718 	    apply simp
  1719 	   apply blast
  1720 	  apply fastsimp
  1721 	 apply clarsimp
  1722 	apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
  1723 	done
  1724     qed
  1725   qed
  1726 qed
  1727 
  1728 lemma Lcm_set_nat [code_unfold]:
  1729   "Lcm (set ns) = foldl lcm (1::nat) ns"
  1730 proof -
  1731   interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
  1732   show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
  1733 qed
  1734 
  1735 lemma Lcm_set_int [code_unfold]:
  1736   "Lcm (set is) = foldl lcm (1::int) is"
  1737 proof -
  1738   interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
  1739   show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
  1740 qed
  1741 
  1742 lemma Gcd_set_nat [code_unfold]:
  1743   "Gcd (set ns) = foldl gcd (0::nat) ns"
  1744 proof -
  1745   interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
  1746   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
  1747 qed
  1748 
  1749 lemma Gcd_set_int [code_unfold]:
  1750   "Gcd (set ns) = foldl gcd (0::int) ns"
  1751 proof -
  1752   interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
  1753   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
  1754 qed
  1755 
  1756 
  1757 subsection {* Primes *}
  1758 
  1759 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
  1760 
  1761 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
  1762   by (unfold prime_nat_def, auto)
  1763 
  1764 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
  1765   by (unfold prime_nat_def, auto)
  1766 
  1767 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
  1768   by (unfold prime_nat_def, auto)
  1769 
  1770 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
  1771   by (unfold prime_nat_def, auto)
  1772 
  1773 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
  1774   by (unfold prime_nat_def, auto)
  1775 
  1776 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
  1777   by (unfold prime_nat_def, auto)
  1778 
  1779 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
  1780   by (unfold prime_nat_def, auto)
  1781 
  1782 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
  1783   by (unfold prime_int_def prime_nat_def) auto
  1784 
  1785 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
  1786   by (unfold prime_int_def prime_nat_def, auto)
  1787 
  1788 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
  1789   by (unfold prime_int_def prime_nat_def, auto)
  1790 
  1791 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
  1792   by (unfold prime_int_def prime_nat_def, auto)
  1793 
  1794 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
  1795   by (unfold prime_int_def prime_nat_def, auto)
  1796 
  1797 
  1798 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
  1799     m = 1 \<or> m = p))"
  1800   using prime_nat_def [transferred]
  1801     apply (case_tac "p >= 0")
  1802     by (blast, auto simp add: prime_ge_0_int)
  1803 
  1804 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1805   apply (unfold prime_nat_def)
  1806   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
  1807   done
  1808 
  1809 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1810   apply (unfold prime_int_altdef)
  1811   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
  1812   done
  1813 
  1814 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1815   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
  1816 
  1817 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1818   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
  1819 
  1820 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
  1821     p dvd m * n = (p dvd m \<or> p dvd n)"
  1822   by (rule iffI, rule prime_dvd_mult_nat, auto)
  1823 
  1824 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
  1825     p dvd m * n = (p dvd m \<or> p dvd n)"
  1826   by (rule iffI, rule prime_dvd_mult_int, auto)
  1827 
  1828 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1829     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1830   unfolding prime_nat_def dvd_def apply auto
  1831   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)
  1832 
  1833 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1834     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1835   unfolding prime_int_altdef dvd_def
  1836   apply auto
  1837   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)
  1838 
  1839 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
  1840     n > 0 --> (p dvd x^n --> p dvd x)"
  1841   by (induct n rule: nat_induct, auto)
  1842 
  1843 lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
  1844     n > 0 --> (p dvd x^n --> p dvd x)"
  1845   apply (induct n rule: nat_induct, auto)
  1846   apply (frule prime_ge_0_int)
  1847   apply auto
  1848 done
  1849 
  1850 subsubsection{* Make prime naively executable *}
  1851 
  1852 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
  1853   by (simp add: prime_nat_def)
  1854 
  1855 lemma zero_not_prime_int [simp]: "~prime (0::int)"
  1856   by (simp add: prime_int_def)
  1857 
  1858 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
  1859   by (simp add: prime_nat_def)
  1860 
  1861 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
  1862   by (simp add: prime_nat_def One_nat_def)
  1863 
  1864 lemma one_not_prime_int [simp]: "~prime (1::int)"
  1865   by (simp add: prime_int_def)
  1866 
  1867 lemma prime_nat_code[code]:
  1868  "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
  1869 apply(simp add: Ball_def)
  1870 apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
  1871 done
  1872 
  1873 lemma prime_nat_simp:
  1874  "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
  1875 apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
  1876 apply(simp add:nat_number One_nat_def)
  1877 done
  1878 
  1879 lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard]
  1880 
  1881 lemma prime_int_code[code]:
  1882   "prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R")
  1883 proof
  1884   assume "?L" thus "?R"
  1885     by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
  1886 next
  1887     assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
  1888 qed
  1889 
  1890 lemma prime_int_simp:
  1891   "prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))"
  1892 apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto)
  1893 apply simp
  1894 done
  1895 
  1896 lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
  1897 
  1898 lemma two_is_prime_nat [simp]: "prime (2::nat)"
  1899 by simp
  1900 
  1901 lemma two_is_prime_int [simp]: "prime (2::int)"
  1902 by simp
  1903 
  1904 text{* A bit of regression testing: *}
  1905 
  1906 lemma "prime(97::nat)"
  1907 by simp
  1908 
  1909 lemma "prime(97::int)"
  1910 by simp
  1911 
  1912 lemma "prime(997::nat)"
  1913 by eval
  1914 
  1915 lemma "prime(997::int)"
  1916 by eval
  1917 
  1918 
  1919 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
  1920   apply (rule coprime_exp_nat)
  1921   apply (subst gcd_commute_nat)
  1922   apply (erule (1) prime_imp_coprime_nat)
  1923 done
  1924 
  1925 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
  1926   apply (rule coprime_exp_int)
  1927   apply (subst gcd_commute_int)
  1928   apply (erule (1) prime_imp_coprime_int)
  1929 done
  1930 
  1931 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1932   apply (rule prime_imp_coprime_nat, assumption)
  1933   apply (unfold prime_nat_def, auto)
  1934 done
  1935 
  1936 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1937   apply (rule prime_imp_coprime_int, assumption)
  1938   apply (unfold prime_int_altdef, clarify)
  1939   apply (drule_tac x = q in spec)
  1940   apply (drule_tac x = p in spec)
  1941   apply auto
  1942 done
  1943 
  1944 lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
  1945   by (rule coprime_exp2_nat, rule primes_coprime_nat)
  1946 
  1947 lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
  1948   by (rule coprime_exp2_int, rule primes_coprime_int)
  1949 
  1950 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
  1951   apply (induct n rule: nat_less_induct)
  1952   apply (case_tac "n = 0")
  1953   using two_is_prime_nat apply blast
  1954   apply (case_tac "prime n")
  1955   apply blast
  1956   apply (subgoal_tac "n > 1")
  1957   apply (frule (1) not_prime_eq_prod_nat)
  1958   apply (auto intro: dvd_mult dvd_mult2)
  1959 done
  1960 
  1961 (* An Isar version:
  1962 
  1963 lemma prime_factor_b_nat:
  1964   fixes n :: nat
  1965   assumes "n \<noteq> 1"
  1966   shows "\<exists>p. prime p \<and> p dvd n"
  1967 
  1968 using `n ~= 1`
  1969 proof (induct n rule: less_induct_nat)
  1970   fix n :: nat
  1971   assume "n ~= 1" and
  1972     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
  1973   thus "\<exists>p. prime p \<and> p dvd n"
  1974   proof -
  1975   {
  1976     assume "n = 0"
  1977     moreover note two_is_prime_nat
  1978     ultimately have ?thesis
  1979       by (auto simp del: two_is_prime_nat)
  1980   }
  1981   moreover
  1982   {
  1983     assume "prime n"
  1984     hence ?thesis by auto
  1985   }
  1986   moreover
  1987   {
  1988     assume "n ~= 0" and "~ prime n"
  1989     with `n ~= 1` have "n > 1" by auto
  1990     with `~ prime n` and not_prime_eq_prod_nat obtain m k where
  1991       "n = m * k" and "1 < m" and "m < n" by blast
  1992     with ih obtain p where "prime p" and "p dvd m" by blast
  1993     with `n = m * k` have ?thesis by auto
  1994   }
  1995   ultimately show ?thesis by blast
  1996   qed
  1997 qed
  1998 
  1999 *)
  2000 
  2001 text {* One property of coprimality is easier to prove via prime factors. *}
  2002 
  2003 lemma prime_divprod_pow_nat:
  2004   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
  2005   shows "p^n dvd a \<or> p^n dvd b"
  2006 proof-
  2007   {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
  2008       apply (cases "n=0", simp_all)
  2009       apply (cases "a=1", simp_all) done}
  2010   moreover
  2011   {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
  2012     then obtain m where m: "n = Suc m" by (cases n, auto)
  2013     from n have "p dvd p^n" by (intro dvd_power, auto)
  2014     also note pab
  2015     finally have pab': "p dvd a * b".
  2016     from prime_dvd_mult_nat[OF p pab']
  2017     have "p dvd a \<or> p dvd b" .
  2018     moreover
  2019     {assume pa: "p dvd a"
  2020       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  2021       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
  2022       with p have "coprime b p"
  2023         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
  2024       hence pnb: "coprime (p^n) b"
  2025         by (subst gcd_commute_nat, rule coprime_exp_nat)
  2026       from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
  2027     moreover
  2028     {assume pb: "p dvd b"
  2029       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  2030       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
  2031         by auto
  2032       with p have "coprime a p"
  2033         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
  2034       hence pna: "coprime (p^n) a"
  2035         by (subst gcd_commute_nat, rule coprime_exp_nat)
  2036       from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
  2037     ultimately have ?thesis by blast}
  2038   ultimately show ?thesis by blast
  2039 qed
  2040 
  2041 subsection {* Infinitely many primes *}
  2042 
  2043 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
  2044 proof-
  2045   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
  2046   from prime_factor_nat [OF f1]
  2047       obtain p where "prime p" and "p dvd fact n + 1" by auto
  2048   hence "p \<le> fact n + 1" 
  2049     by (intro dvd_imp_le, auto)
  2050   {assume "p \<le> n"
  2051     from `prime p` have "p \<ge> 1" 
  2052       by (cases p, simp_all)
  2053     with `p <= n` have "p dvd fact n" 
  2054       by (intro dvd_fact_nat)
  2055     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
  2056       by (rule dvd_diff_nat)
  2057     hence "p dvd 1" by simp
  2058     hence "p <= 1" by auto
  2059     moreover from `prime p` have "p > 1" by auto
  2060     ultimately have False by auto}
  2061   hence "n < p" by arith
  2062   with `prime p` and `p <= fact n + 1` show ?thesis by auto
  2063 qed
  2064 
  2065 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
  2066 using next_prime_bound by auto
  2067 
  2068 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
  2069 proof
  2070   assume "finite {(p::nat). prime p}"
  2071   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
  2072     by auto
  2073   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
  2074     by auto
  2075   with bigger_prime [of b] show False by auto
  2076 qed
  2077 
  2078 
  2079 end