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