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