src/HOL/GCD.thy
author nipkow
Fri Dec 04 08:52:09 2009 +0100 (2009-12-04)
changeset 33946 fcc20072df9a
parent 33657 a4179bf442d1
child 34030 829eb528b226
permissions -rw-r--r--
removed redundant lemma
     1 (*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     2                 Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
     3 
     4 
     5 This file deals with the functions gcd and lcm.  Definitions and
     6 lemmas are proved uniformly for the natural numbers and integers.
     7 
     8 This file combines and revises a number of prior developments.
     9 
    10 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    11 and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
    12 gcd, lcm, and prime for the natural numbers.
    13 
    14 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    15 extended gcd, lcm, primes to the integers. Amine Chaieb provided
    16 another extension of the notions to the integers, and added a number
    17 of results to "Primes" and "GCD". IntPrimes also defined and developed
    18 the congruence relations on the integers. The notion was extended to
    19 the natural numbers by Chiaeb.
    20 
    21 Jeremy Avigad combined all of these, made everything uniform for the
    22 natural numbers and the integers, and added a number of new theorems.
    23 
    24 Tobias Nipkow cleaned up a lot.
    25 *)
    26 
    27 
    28 header {* GCD *}
    29 
    30 theory GCD
    31 imports Fact Parity
    32 begin
    33 
    34 declare One_nat_def [simp del]
    35 
    36 subsection {* gcd *}
    37 
    38 class gcd = zero + one + dvd +
    39 
    40 fixes
    41   gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
    42   lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    43 
    44 begin
    45 
    46 abbreviation
    47   coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    48 where
    49   "coprime x y == (gcd x y = 1)"
    50 
    51 end
    52 
    53 
    54 (* definitions for the natural numbers *)
    55 
    56 instantiation nat :: gcd
    57 
    58 begin
    59 
    60 fun
    61   gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    62 where
    63   "gcd_nat x y =
    64    (if y = 0 then x else gcd y (x mod y))"
    65 
    66 definition
    67   lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    68 where
    69   "lcm_nat x y = x * y div (gcd x y)"
    70 
    71 instance proof qed
    72 
    73 end
    74 
    75 
    76 (* definitions for the integers *)
    77 
    78 instantiation int :: gcd
    79 
    80 begin
    81 
    82 definition
    83   gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
    84 where
    85   "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
    86 
    87 definition
    88   lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
    89 where
    90   "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
    91 
    92 instance proof qed
    93 
    94 end
    95 
    96 
    97 subsection {* Set up Transfer *}
    98 
    99 
   100 lemma transfer_nat_int_gcd:
   101   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   102   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   103   unfolding gcd_int_def lcm_int_def
   104   by auto
   105 
   106 lemma transfer_nat_int_gcd_closures:
   107   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
   108   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   109   by (auto simp add: gcd_int_def lcm_int_def)
   110 
   111 declare TransferMorphism_nat_int[transfer add return:
   112     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   113 
   114 lemma transfer_int_nat_gcd:
   115   "gcd (int x) (int y) = int (gcd x y)"
   116   "lcm (int x) (int y) = int (lcm x y)"
   117   by (unfold gcd_int_def lcm_int_def, auto)
   118 
   119 lemma transfer_int_nat_gcd_closures:
   120   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   121   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   122   by (auto simp add: gcd_int_def lcm_int_def)
   123 
   124 declare TransferMorphism_int_nat[transfer add return:
   125     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   126 
   127 
   128 subsection {* GCD *}
   129 
   130 (* was gcd_induct *)
   131 lemma gcd_nat_induct:
   132   fixes m n :: nat
   133   assumes "\<And>m. P m 0"
   134     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   135   shows "P m n"
   136   apply (rule gcd_nat.induct)
   137   apply (case_tac "y = 0")
   138   using assms apply simp_all
   139 done
   140 
   141 (* specific to int *)
   142 
   143 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
   144   by (simp add: gcd_int_def)
   145 
   146 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
   147   by (simp add: gcd_int_def)
   148 
   149 lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
   150 by(simp add: gcd_int_def)
   151 
   152 lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"
   153 by (simp add: gcd_int_def)
   154 
   155 lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
   156 by (metis abs_idempotent gcd_abs_int)
   157 
   158 lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
   159 by (metis abs_idempotent gcd_abs_int)
   160 
   161 lemma gcd_cases_int:
   162   fixes x :: int and y
   163   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   164       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   165       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   166       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   167   shows "P (gcd x y)"
   168 by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith)
   169 
   170 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   171   by (simp add: gcd_int_def)
   172 
   173 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
   174   by (simp add: lcm_int_def)
   175 
   176 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
   177   by (simp add: lcm_int_def)
   178 
   179 lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"
   180   by (simp add: lcm_int_def)
   181 
   182 lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
   183 by(simp add:lcm_int_def)
   184 
   185 lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
   186 by (metis abs_idempotent lcm_int_def)
   187 
   188 lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
   189 by (metis abs_idempotent lcm_int_def)
   190 
   191 lemma lcm_cases_int:
   192   fixes x :: int and y
   193   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   194       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   195       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   196       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   197   shows "P (lcm x y)"
   198 by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith)
   199 
   200 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   201   by (simp add: lcm_int_def)
   202 
   203 (* was gcd_0, etc. *)
   204 lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
   205   by simp
   206 
   207 (* was igcd_0, etc. *)
   208 lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
   209   by (unfold gcd_int_def, auto)
   210 
   211 lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
   212   by simp
   213 
   214 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
   215   by (unfold gcd_int_def, auto)
   216 
   217 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
   218   by (case_tac "y = 0", auto)
   219 
   220 (* weaker, but useful for the simplifier *)
   221 
   222 lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   223   by simp
   224 
   225 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   226   by simp
   227 
   228 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   229   by (simp add: One_nat_def)
   230 
   231 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   232   by (simp add: gcd_int_def)
   233 
   234 lemma gcd_idem_nat: "gcd (x::nat) x = x"
   235 by simp
   236 
   237 lemma gcd_idem_int: "gcd (x::int) x = abs x"
   238 by (auto simp add: gcd_int_def)
   239 
   240 declare gcd_nat.simps [simp del]
   241 
   242 text {*
   243   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
   244   conjunctions don't seem provable separately.
   245 *}
   246 
   247 lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
   248   and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
   249   apply (induct m n rule: gcd_nat_induct)
   250   apply (simp_all add: gcd_non_0_nat)
   251   apply (blast dest: dvd_mod_imp_dvd)
   252 done
   253 
   254 lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"
   255 by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)
   256 
   257 lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"
   258 by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)
   259 
   260 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   261 by(metis gcd_dvd1_nat dvd_trans)
   262 
   263 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   264 by(metis gcd_dvd2_nat dvd_trans)
   265 
   266 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   267 by(metis gcd_dvd1_int dvd_trans)
   268 
   269 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   270 by(metis gcd_dvd2_int dvd_trans)
   271 
   272 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   273   by (rule dvd_imp_le, auto)
   274 
   275 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   276   by (rule dvd_imp_le, auto)
   277 
   278 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   279   by (rule zdvd_imp_le, auto)
   280 
   281 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   282   by (rule zdvd_imp_le, auto)
   283 
   284 lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   285 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
   286 
   287 lemma gcd_greatest_int:
   288   "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   289   apply (subst gcd_abs_int)
   290   apply (subst abs_dvd_iff [symmetric])
   291   apply (rule gcd_greatest_nat [transferred])
   292   apply auto
   293 done
   294 
   295 lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
   296     (k dvd m & k dvd n)"
   297   by (blast intro!: gcd_greatest_nat intro: dvd_trans)
   298 
   299 lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   300   by (blast intro!: gcd_greatest_int intro: dvd_trans)
   301 
   302 lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   303   by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
   304 
   305 lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   306   by (auto simp add: gcd_int_def)
   307 
   308 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   309   by (insert gcd_zero_nat [of m n], arith)
   310 
   311 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   312   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
   313 
   314 lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
   315   by (rule dvd_antisym, auto)
   316 
   317 lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
   318   by (auto simp add: gcd_int_def gcd_commute_nat)
   319 
   320 lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
   321   apply (rule dvd_antisym)
   322   apply (blast intro: dvd_trans)+
   323 done
   324 
   325 lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
   326   by (auto simp add: gcd_int_def gcd_assoc_nat)
   327 
   328 lemmas gcd_left_commute_nat =
   329   mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat]
   330 
   331 lemmas gcd_left_commute_int =
   332   mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int]
   333 
   334 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
   335   -- {* gcd is an AC-operator *}
   336 
   337 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
   338 
   339 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
   340     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   341   apply auto
   342   apply (rule dvd_antisym)
   343   apply (erule (1) gcd_greatest_nat)
   344   apply auto
   345 done
   346 
   347 lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   348     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   349 apply (case_tac "d = 0")
   350  apply simp
   351 apply (rule iffI)
   352  apply (rule zdvd_antisym_nonneg)
   353  apply (auto intro: gcd_greatest_int)
   354 done
   355 
   356 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   357 by (metis dvd.eq_iff gcd_unique_nat)
   358 
   359 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   360 by (metis dvd.eq_iff gcd_unique_nat)
   361 
   362 lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   363 by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
   364 
   365 lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   366 by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   367 
   368 
   369 text {*
   370   \medskip Multiplication laws
   371 *}
   372 
   373 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   374     -- {* \cite[page 27]{davenport92} *}
   375   apply (induct m n rule: gcd_nat_induct)
   376   apply simp
   377   apply (case_tac "k = 0")
   378   apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
   379 done
   380 
   381 lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   382   apply (subst (1 2) gcd_abs_int)
   383   apply (subst (1 2) abs_mult)
   384   apply (rule gcd_mult_distrib_nat [transferred])
   385   apply auto
   386 done
   387 
   388 lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   389   apply (insert gcd_mult_distrib_nat [of m k n])
   390   apply simp
   391   apply (erule_tac t = m in ssubst)
   392   apply simp
   393   done
   394 
   395 lemma coprime_dvd_mult_int:
   396   "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   397 apply (subst abs_dvd_iff [symmetric])
   398 apply (subst dvd_abs_iff [symmetric])
   399 apply (subst (asm) gcd_abs_int)
   400 apply (rule coprime_dvd_mult_nat [transferred])
   401     prefer 4 apply assumption
   402    apply auto
   403 apply (subst abs_mult [symmetric], auto)
   404 done
   405 
   406 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   407     (k dvd m * n) = (k dvd m)"
   408   by (auto intro: coprime_dvd_mult_nat)
   409 
   410 lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   411     (k dvd m * n) = (k dvd m)"
   412   by (auto intro: coprime_dvd_mult_int)
   413 
   414 lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   415   apply (rule dvd_antisym)
   416   apply (rule gcd_greatest_nat)
   417   apply (rule_tac n = k in coprime_dvd_mult_nat)
   418   apply (simp add: gcd_assoc_nat)
   419   apply (simp add: gcd_commute_nat)
   420   apply (simp_all add: mult_commute)
   421 done
   422 
   423 lemma gcd_mult_cancel_int:
   424   "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
   425 apply (subst (1 2) gcd_abs_int)
   426 apply (subst abs_mult)
   427 apply (rule gcd_mult_cancel_nat [transferred], auto)
   428 done
   429 
   430 text {* \medskip Addition laws *}
   431 
   432 lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   433   apply (case_tac "n = 0")
   434   apply (simp_all add: gcd_non_0_nat)
   435 done
   436 
   437 lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   438   apply (subst (1 2) gcd_commute_nat)
   439   apply (subst add_commute)
   440   apply simp
   441 done
   442 
   443 (* to do: add the other variations? *)
   444 
   445 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   446   by (subst gcd_add1_nat [symmetric], auto)
   447 
   448 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   449   apply (subst gcd_commute_nat)
   450   apply (subst gcd_diff1_nat [symmetric])
   451   apply auto
   452   apply (subst gcd_commute_nat)
   453   apply (subst gcd_diff1_nat)
   454   apply assumption
   455   apply (rule gcd_commute_nat)
   456 done
   457 
   458 lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   459   apply (frule_tac b = y and a = x in pos_mod_sign)
   460   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   461   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
   462     zmod_zminus1_eq_if)
   463   apply (frule_tac a = x in pos_mod_bound)
   464   apply (subst (1 2) gcd_commute_nat)
   465   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   466     nat_le_eq_zle)
   467 done
   468 
   469 lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
   470   apply (case_tac "y = 0")
   471   apply force
   472   apply (case_tac "y > 0")
   473   apply (subst gcd_non_0_int, auto)
   474   apply (insert gcd_non_0_int [of "-y" "-x"])
   475   apply (auto simp add: gcd_neg1_int gcd_neg2_int)
   476 done
   477 
   478 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
   479 by (metis gcd_red_int mod_add_self1 zadd_commute)
   480 
   481 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   482 by (metis gcd_add1_int gcd_commute_int zadd_commute)
   483 
   484 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   485 by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
   486 
   487 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   488 by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
   489 
   490 
   491 (* to do: differences, and all variations of addition rules
   492     as simplification rules for nat and int *)
   493 
   494 (* FIXME remove iff *)
   495 lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n"
   496   using mult_dvd_mono [of 1] by auto
   497 
   498 (* to do: add the three variations of these, and for ints? *)
   499 
   500 lemma finite_divisors_nat[simp]:
   501   assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
   502 proof-
   503   have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
   504   from finite_subset[OF _ this] show ?thesis using assms
   505     by(bestsimp intro!:dvd_imp_le)
   506 qed
   507 
   508 lemma finite_divisors_int[simp]:
   509   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
   510 proof-
   511   have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
   512   hence "finite{d. abs d <= abs i}" by simp
   513   from finite_subset[OF _ this] show ?thesis using assms
   514     by(bestsimp intro!:dvd_imp_le_int)
   515 qed
   516 
   517 lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
   518 apply(rule antisym)
   519  apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
   520 apply simp
   521 done
   522 
   523 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
   524 apply(rule antisym)
   525  apply(rule Max_le_iff[THEN iffD2])
   526    apply simp
   527   apply fastsimp
   528  apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
   529 apply simp
   530 done
   531 
   532 lemma gcd_is_Max_divisors_nat:
   533   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
   534 apply(rule Max_eqI[THEN sym])
   535   apply (metis finite_Collect_conjI finite_divisors_nat)
   536  apply simp
   537  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
   538 apply simp
   539 done
   540 
   541 lemma gcd_is_Max_divisors_int:
   542   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
   543 apply(rule Max_eqI[THEN sym])
   544   apply (metis finite_Collect_conjI finite_divisors_int)
   545  apply simp
   546  apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
   547 apply simp
   548 done
   549 
   550 
   551 subsection {* Coprimality *}
   552 
   553 lemma div_gcd_coprime_nat:
   554   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   555   shows "coprime (a div gcd a b) (b div gcd a b)"
   556 proof -
   557   let ?g = "gcd a b"
   558   let ?a' = "a div ?g"
   559   let ?b' = "b div ?g"
   560   let ?g' = "gcd ?a' ?b'"
   561   have dvdg: "?g dvd a" "?g dvd b" by simp_all
   562   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   563   from dvdg dvdg' obtain ka kb ka' kb' where
   564       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   565     unfolding dvd_def by blast
   566   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   567     by simp_all
   568   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   569     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   570       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   571   have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat)
   572   then have gp: "?g > 0" by arith
   573   from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
   574   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   575 qed
   576 
   577 lemma div_gcd_coprime_int:
   578   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   579   shows "coprime (a div gcd a b) (b div gcd a b)"
   580 apply (subst (1 2 3) gcd_abs_int)
   581 apply (subst (1 2) abs_div)
   582   apply simp
   583  apply simp
   584 apply(subst (1 2) abs_gcd_int)
   585 apply (rule div_gcd_coprime_nat [transferred])
   586 using nz apply (auto simp add: gcd_abs_int [symmetric])
   587 done
   588 
   589 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   590   using gcd_unique_nat[of 1 a b, simplified] by auto
   591 
   592 lemma coprime_Suc_0_nat:
   593     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   594   using coprime_nat by (simp add: One_nat_def)
   595 
   596 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
   597     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   598   using gcd_unique_int [of 1 a b]
   599   apply clarsimp
   600   apply (erule subst)
   601   apply (rule iffI)
   602   apply force
   603   apply (drule_tac x = "abs e" in exI)
   604   apply (case_tac "e >= 0")
   605   apply force
   606   apply force
   607 done
   608 
   609 lemma gcd_coprime_nat:
   610   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   611     b: "b = b' * gcd a b"
   612   shows    "coprime a' b'"
   613 
   614   apply (subgoal_tac "a' = a div gcd a b")
   615   apply (erule ssubst)
   616   apply (subgoal_tac "b' = b div gcd a b")
   617   apply (erule ssubst)
   618   apply (rule div_gcd_coprime_nat)
   619   using prems
   620   apply force
   621   apply (subst (1) b)
   622   using z apply force
   623   apply (subst (1) a)
   624   using z apply force
   625 done
   626 
   627 lemma gcd_coprime_int:
   628   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   629     b: "b = b' * gcd a b"
   630   shows    "coprime a' b'"
   631 
   632   apply (subgoal_tac "a' = a div gcd a b")
   633   apply (erule ssubst)
   634   apply (subgoal_tac "b' = b div gcd a b")
   635   apply (erule ssubst)
   636   apply (rule div_gcd_coprime_int)
   637   using prems
   638   apply force
   639   apply (subst (1) b)
   640   using z apply force
   641   apply (subst (1) a)
   642   using z apply force
   643 done
   644 
   645 lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   646     shows "coprime d (a * b)"
   647   apply (subst gcd_commute_nat)
   648   using da apply (subst gcd_mult_cancel_nat)
   649   apply (subst gcd_commute_nat, assumption)
   650   apply (subst gcd_commute_nat, rule db)
   651 done
   652 
   653 lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
   654     shows "coprime d (a * b)"
   655   apply (subst gcd_commute_int)
   656   using da apply (subst gcd_mult_cancel_int)
   657   apply (subst gcd_commute_int, assumption)
   658   apply (subst gcd_commute_int, rule db)
   659 done
   660 
   661 lemma coprime_lmult_nat:
   662   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   663 proof -
   664   have "gcd d a dvd gcd d (a * b)"
   665     by (rule gcd_greatest_nat, auto)
   666   with dab show ?thesis
   667     by auto
   668 qed
   669 
   670 lemma coprime_lmult_int:
   671   assumes "coprime (d::int) (a * b)" shows "coprime d a"
   672 proof -
   673   have "gcd d a dvd gcd d (a * b)"
   674     by (rule gcd_greatest_int, auto)
   675   with assms show ?thesis
   676     by auto
   677 qed
   678 
   679 lemma coprime_rmult_nat:
   680   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   681 proof -
   682   have "gcd d b dvd gcd d (a * b)"
   683     by (rule gcd_greatest_nat, auto intro: dvd_mult)
   684   with assms show ?thesis
   685     by auto
   686 qed
   687 
   688 lemma coprime_rmult_int:
   689   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   690 proof -
   691   have "gcd d b dvd gcd d (a * b)"
   692     by (rule gcd_greatest_int, auto intro: dvd_mult)
   693   with dab show ?thesis
   694     by auto
   695 qed
   696 
   697 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   698     coprime d a \<and>  coprime d b"
   699   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   700     coprime_mult_nat[of d a b]
   701   by blast
   702 
   703 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   704     coprime d a \<and>  coprime d b"
   705   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   706     coprime_mult_int[of d a b]
   707   by blast
   708 
   709 lemma gcd_coprime_exists_nat:
   710     assumes nz: "gcd (a::nat) b \<noteq> 0"
   711     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   712   apply (rule_tac x = "a div gcd a b" in exI)
   713   apply (rule_tac x = "b div gcd a b" in exI)
   714   using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)
   715 done
   716 
   717 lemma gcd_coprime_exists_int:
   718     assumes nz: "gcd (a::int) b \<noteq> 0"
   719     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   720   apply (rule_tac x = "a div gcd a b" in exI)
   721   apply (rule_tac x = "b div gcd a b" in exI)
   722   using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self)
   723 done
   724 
   725 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   726   by (induct n, simp_all add: coprime_mult_nat)
   727 
   728 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   729   by (induct n, simp_all add: coprime_mult_int)
   730 
   731 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   732   apply (rule coprime_exp_nat)
   733   apply (subst gcd_commute_nat)
   734   apply (rule coprime_exp_nat)
   735   apply (subst gcd_commute_nat, assumption)
   736 done
   737 
   738 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   739   apply (rule coprime_exp_int)
   740   apply (subst gcd_commute_int)
   741   apply (rule coprime_exp_int)
   742   apply (subst gcd_commute_int, assumption)
   743 done
   744 
   745 lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   746 proof (cases)
   747   assume "a = 0 & b = 0"
   748   thus ?thesis by simp
   749   next assume "~(a = 0 & b = 0)"
   750   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   751     by (auto simp:div_gcd_coprime_nat)
   752   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   753       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   754     apply (subst (1 2) mult_commute)
   755     apply (subst gcd_mult_distrib_nat [symmetric])
   756     apply simp
   757     done
   758   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   759     apply (subst div_power)
   760     apply auto
   761     apply (rule dvd_div_mult_self)
   762     apply (rule dvd_power_same)
   763     apply auto
   764     done
   765   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
   766     apply (subst div_power)
   767     apply auto
   768     apply (rule dvd_div_mult_self)
   769     apply (rule dvd_power_same)
   770     apply auto
   771     done
   772   finally show ?thesis .
   773 qed
   774 
   775 lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   776   apply (subst (1 2) gcd_abs_int)
   777   apply (subst (1 2) power_abs)
   778   apply (rule gcd_exp_nat [where n = n, transferred])
   779   apply auto
   780 done
   781 
   782 lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
   783   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   784 proof-
   785   let ?g = "gcd a b"
   786   {assume "?g = 0" with dc have ?thesis by auto}
   787   moreover
   788   {assume z: "?g \<noteq> 0"
   789     from gcd_coprime_exists_nat[OF z]
   790     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   791       by blast
   792     have thb: "?g dvd b" by auto
   793     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   794     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   795     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   796     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   797     with z have th_1: "a' dvd b' * c" by auto
   798     from coprime_dvd_mult_nat[OF ab'(3)] th_1
   799     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   800     from ab' have "a = ?g*a'" by algebra
   801     with thb thc have ?thesis by blast }
   802   ultimately show ?thesis by blast
   803 qed
   804 
   805 lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
   806   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   807 proof-
   808   let ?g = "gcd a b"
   809   {assume "?g = 0" with dc have ?thesis by auto}
   810   moreover
   811   {assume z: "?g \<noteq> 0"
   812     from gcd_coprime_exists_int[OF z]
   813     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   814       by blast
   815     have thb: "?g dvd b" by auto
   816     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
   817     with dc have th0: "a' dvd b*c"
   818       using dvd_trans[of a' a "b*c"] by simp
   819     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   820     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   821     with z have th_1: "a' dvd b' * c" by auto
   822     from coprime_dvd_mult_int[OF ab'(3)] th_1
   823     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   824     from ab' have "a = ?g*a'" by algebra
   825     with thb thc have ?thesis by blast }
   826   ultimately show ?thesis by blast
   827 qed
   828 
   829 lemma pow_divides_pow_nat:
   830   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   831   shows "a dvd b"
   832 proof-
   833   let ?g = "gcd a b"
   834   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   835   {assume "?g = 0" with ab n have ?thesis by auto }
   836   moreover
   837   {assume z: "?g \<noteq> 0"
   838     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   839     from gcd_coprime_exists_nat[OF z]
   840     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   841       by blast
   842     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   843       by (simp add: ab'(1,2)[symmetric])
   844     hence "?g^n*a'^n dvd ?g^n *b'^n"
   845       by (simp only: power_mult_distrib mult_commute)
   846     with zn z n have th0:"a'^n dvd b'^n" by auto
   847     have "a' dvd a'^n" by (simp add: m)
   848     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   849     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   850     from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
   851     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   852     hence "a'*?g dvd b'*?g" by simp
   853     with ab'(1,2)  have ?thesis by simp }
   854   ultimately show ?thesis by blast
   855 qed
   856 
   857 lemma pow_divides_pow_int:
   858   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
   859   shows "a dvd b"
   860 proof-
   861   let ?g = "gcd a b"
   862   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   863   {assume "?g = 0" with ab n have ?thesis by auto }
   864   moreover
   865   {assume z: "?g \<noteq> 0"
   866     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   867     from gcd_coprime_exists_int[OF z]
   868     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   869       by blast
   870     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   871       by (simp add: ab'(1,2)[symmetric])
   872     hence "?g^n*a'^n dvd ?g^n *b'^n"
   873       by (simp only: power_mult_distrib mult_commute)
   874     with zn z n have th0:"a'^n dvd b'^n" by auto
   875     have "a' dvd a'^n" by (simp add: m)
   876     with th0 have "a' dvd b'^n"
   877       using dvd_trans[of a' "a'^n" "b'^n"] by simp
   878     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   879     from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
   880     have "a' dvd b'" by (subst (asm) mult_commute, blast)
   881     hence "a'*?g dvd b'*?g" by simp
   882     with ab'(1,2)  have ?thesis by simp }
   883   ultimately show ?thesis by blast
   884 qed
   885 
   886 (* FIXME move to Divides(?) *)
   887 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   888   by (auto intro: pow_divides_pow_nat dvd_power_same)
   889 
   890 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   891   by (auto intro: pow_divides_pow_int dvd_power_same)
   892 
   893 lemma divides_mult_nat:
   894   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   895   shows "m * n dvd r"
   896 proof-
   897   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   898     unfolding dvd_def by blast
   899   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   900   hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
   901   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   902   from n' k show ?thesis unfolding dvd_def by auto
   903 qed
   904 
   905 lemma divides_mult_int:
   906   assumes mr: "(m::int) 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 coprime_dvd_mult_iff_int[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 coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   918   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   919   apply force
   920   apply (rule dvd_diff_nat)
   921   apply auto
   922 done
   923 
   924 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
   925   using coprime_plus_one_nat by (simp add: One_nat_def)
   926 
   927 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
   928   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   929   apply force
   930   apply (rule dvd_diff)
   931   apply auto
   932 done
   933 
   934 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   935   using coprime_plus_one_nat [of "n - 1"]
   936     gcd_commute_nat [of "n - 1" n] by auto
   937 
   938 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
   939   using coprime_plus_one_int [of "n - 1"]
   940     gcd_commute_int [of "n - 1" n] by auto
   941 
   942 lemma setprod_coprime_nat [rule_format]:
   943     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
   944   apply (case_tac "finite A")
   945   apply (induct set: finite)
   946   apply (auto simp add: gcd_mult_cancel_nat)
   947 done
   948 
   949 lemma setprod_coprime_int [rule_format]:
   950     "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
   951   apply (case_tac "finite A")
   952   apply (induct set: finite)
   953   apply (auto simp add: gcd_mult_cancel_int)
   954 done
   955 
   956 lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
   957     x dvd b \<Longrightarrow> x = 1"
   958   apply (subgoal_tac "x dvd gcd a b")
   959   apply simp
   960   apply (erule (1) gcd_greatest_nat)
   961 done
   962 
   963 lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
   964     x dvd b \<Longrightarrow> abs x = 1"
   965   apply (subgoal_tac "x dvd gcd a b")
   966   apply simp
   967   apply (erule (1) gcd_greatest_int)
   968 done
   969 
   970 lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
   971     coprime d e"
   972   apply (auto simp add: dvd_def)
   973   apply (frule coprime_lmult_int)
   974   apply (subst gcd_commute_int)
   975   apply (subst (asm) (2) gcd_commute_int)
   976   apply (erule coprime_lmult_int)
   977 done
   978 
   979 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
   980 apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
   981 done
   982 
   983 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
   984 apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
   985 done
   986 
   987 
   988 subsection {* Bezout's theorem *}
   989 
   990 (* Function bezw returns a pair of witnesses to Bezout's theorem --
   991    see the theorems that follow the definition. *)
   992 fun
   993   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
   994 where
   995   "bezw x y =
   996   (if y = 0 then (1, 0) else
   997       (snd (bezw y (x mod y)),
   998        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
   999 
  1000 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1001 
  1002 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1003        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1004   by simp
  1005 
  1006 declare bezw.simps [simp del]
  1007 
  1008 lemma bezw_aux [rule_format]:
  1009     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1010 proof (induct x y rule: gcd_nat_induct)
  1011   fix m :: nat
  1012   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1013     by auto
  1014   next fix m :: nat and n
  1015     assume ngt0: "n > 0" and
  1016       ih: "fst (bezw n (m mod n)) * int n +
  1017         snd (bezw n (m mod n)) * int (m mod n) =
  1018         int (gcd n (m mod n))"
  1019     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1020       apply (simp add: bezw_non_0 gcd_non_0_nat)
  1021       apply (erule subst)
  1022       apply (simp add: ring_simps)
  1023       apply (subst mod_div_equality [of m n, symmetric])
  1024       (* applying simp here undoes the last substitution!
  1025          what is procedure cancel_div_mod? *)
  1026       apply (simp only: ring_simps zadd_int [symmetric]
  1027         zmult_int [symmetric])
  1028       done
  1029 qed
  1030 
  1031 lemma bezout_int:
  1032   fixes x y
  1033   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1034 proof -
  1035   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1036       EX u v. u * x + v * y = gcd x y"
  1037     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1038     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1039     apply (unfold gcd_int_def)
  1040     apply simp
  1041     apply (subst bezw_aux [symmetric])
  1042     apply auto
  1043     done
  1044   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1045       (x \<le> 0 \<and> y \<le> 0)"
  1046     by auto
  1047   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1048     by (erule (1) bezout_aux)
  1049   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1050     apply (insert bezout_aux [of x "-y"])
  1051     apply auto
  1052     apply (rule_tac x = u in exI)
  1053     apply (rule_tac x = "-v" in exI)
  1054     apply (subst gcd_neg2_int [symmetric])
  1055     apply auto
  1056     done
  1057   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1058     apply (insert bezout_aux [of "-x" y])
  1059     apply auto
  1060     apply (rule_tac x = "-u" in exI)
  1061     apply (rule_tac x = v in exI)
  1062     apply (subst gcd_neg1_int [symmetric])
  1063     apply auto
  1064     done
  1065   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1066     apply (insert bezout_aux [of "-x" "-y"])
  1067     apply auto
  1068     apply (rule_tac x = "-u" in exI)
  1069     apply (rule_tac x = "-v" in exI)
  1070     apply (subst gcd_neg1_int [symmetric])
  1071     apply (subst gcd_neg2_int [symmetric])
  1072     apply auto
  1073     done
  1074   ultimately show ?thesis by blast
  1075 qed
  1076 
  1077 text {* versions of Bezout for nat, by Amine Chaieb *}
  1078 
  1079 lemma ind_euclid:
  1080   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1081   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1082   shows "P a b"
  1083 proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
  1084   fix n a b
  1085   assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
  1086   have "a = b \<or> a < b \<or> b < a" by arith
  1087   moreover {assume eq: "a= b"
  1088     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1089     by simp}
  1090   moreover
  1091   {assume lt: "a < b"
  1092     hence "a + b - a < n \<or> a = 0"  using H(2) by arith
  1093     moreover
  1094     {assume "a =0" with z c have "P a b" by blast }
  1095     moreover
  1096     {assume ab: "a + b - a < n"
  1097       have th0: "a + b - a = a + (b - a)" using lt by arith
  1098       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1099       have "P a b" by (simp add: th0[symmetric])}
  1100     ultimately have "P a b" by blast}
  1101   moreover
  1102   {assume lt: "a > b"
  1103     hence "b + a - b < n \<or> b = 0"  using H(2) by arith
  1104     moreover
  1105     {assume "b =0" with z c have "P a b" by blast }
  1106     moreover
  1107     {assume ab: "b + a - b < n"
  1108       have th0: "b + a - b = b + (a - b)" using lt by arith
  1109       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1110       have "P b a" by (simp add: th0[symmetric])
  1111       hence "P a b" using c by blast }
  1112     ultimately have "P a b" by blast}
  1113 ultimately  show "P a b" by blast
  1114 qed
  1115 
  1116 lemma bezout_lemma_nat:
  1117   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1118     (a * x = b * y + d \<or> b * x = a * y + d)"
  1119   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1120     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1121   using ex
  1122   apply clarsimp
  1123   apply (rule_tac x="d" in exI, simp add: dvd_add)
  1124   apply (case_tac "a * x = b * y + d" , simp_all)
  1125   apply (rule_tac x="x + y" in exI)
  1126   apply (rule_tac x="y" in exI)
  1127   apply algebra
  1128   apply (rule_tac x="x" in exI)
  1129   apply (rule_tac x="x + y" in exI)
  1130   apply algebra
  1131 done
  1132 
  1133 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1134     (a * x = b * y + d \<or> b * x = a * y + d)"
  1135   apply(induct a b rule: ind_euclid)
  1136   apply blast
  1137   apply clarify
  1138   apply (rule_tac x="a" in exI, simp add: dvd_add)
  1139   apply clarsimp
  1140   apply (rule_tac x="d" in exI)
  1141   apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  1142   apply (rule_tac x="x+y" in exI)
  1143   apply (rule_tac x="y" in exI)
  1144   apply algebra
  1145   apply (rule_tac x="x" in exI)
  1146   apply (rule_tac x="x+y" in exI)
  1147   apply algebra
  1148 done
  1149 
  1150 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1151     (a * x - b * y = d \<or> b * x - a * y = d)"
  1152   using bezout_add_nat[of a b]
  1153   apply clarsimp
  1154   apply (rule_tac x="d" in exI, simp)
  1155   apply (rule_tac x="x" in exI)
  1156   apply (rule_tac x="y" in exI)
  1157   apply auto
  1158 done
  1159 
  1160 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1161   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1162 proof-
  1163  from nz have ap: "a > 0" by simp
  1164  from bezout_add_nat[of a b]
  1165  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1166    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1167  moreover
  1168     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1169      from H have ?thesis by blast }
  1170  moreover
  1171  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1172    {assume b0: "b = 0" with H  have ?thesis by simp}
  1173    moreover
  1174    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1175      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1176        by auto
  1177      moreover
  1178      {assume db: "d=b"
  1179        from prems have ?thesis apply simp
  1180          apply (rule exI[where x = b], simp)
  1181          apply (rule exI[where x = b])
  1182         by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1183     moreover
  1184     {assume db: "d < b"
  1185         {assume "x=0" hence ?thesis  using prems by simp }
  1186         moreover
  1187         {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1188           from db have "d \<le> b - 1" by simp
  1189           hence "d*b \<le> b*(b - 1)" by simp
  1190           with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1191           have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1192           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1193             by simp
  1194           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1195             by (simp only: mult_assoc right_distrib)
  1196           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1197             by algebra
  1198           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1199           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1200             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1201           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1202             by (simp only: diff_mult_distrib2 add_commute mult_ac)
  1203           hence ?thesis using H(1,2)
  1204             apply -
  1205             apply (rule exI[where x=d], simp)
  1206             apply (rule exI[where x="(b - 1) * y"])
  1207             by (rule exI[where x="x*(b - 1) - d"], simp)}
  1208         ultimately have ?thesis by blast}
  1209     ultimately have ?thesis by blast}
  1210   ultimately have ?thesis by blast}
  1211  ultimately show ?thesis by blast
  1212 qed
  1213 
  1214 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1215   shows "\<exists>x y. a * x = b * y + gcd a b"
  1216 proof-
  1217   let ?g = "gcd a b"
  1218   from bezout_add_strong_nat[OF a, of b]
  1219   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1220   from d(1,2) have "d dvd ?g" by simp
  1221   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1222   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1223   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1224   thus ?thesis by blast
  1225 qed
  1226 
  1227 
  1228 subsection {* LCM *}
  1229 
  1230 lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1231   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1232     zmult_int [symmetric] gcd_int_def)
  1233 
  1234 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1235   unfolding lcm_nat_def
  1236   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1237 
  1238 lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
  1239   unfolding lcm_int_def gcd_int_def
  1240   apply (subst int_mult [symmetric])
  1241   apply (subst prod_gcd_lcm_nat [symmetric])
  1242   apply (subst nat_abs_mult_distrib [symmetric])
  1243   apply (simp, simp add: abs_mult)
  1244 done
  1245 
  1246 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1247   unfolding lcm_nat_def by simp
  1248 
  1249 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1250   unfolding lcm_int_def by simp
  1251 
  1252 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1253   unfolding lcm_nat_def by simp
  1254 
  1255 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1256   unfolding lcm_int_def by simp
  1257 
  1258 lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
  1259   unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
  1260 
  1261 lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
  1262   unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
  1263 
  1264 
  1265 lemma lcm_pos_nat:
  1266   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1267 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1268 
  1269 lemma lcm_pos_int:
  1270   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1271   apply (subst lcm_abs_int)
  1272   apply (rule lcm_pos_nat [transferred])
  1273   apply auto
  1274 done
  1275 
  1276 lemma dvd_pos_nat:
  1277   fixes n m :: nat
  1278   assumes "n > 0" and "m dvd n"
  1279   shows "m > 0"
  1280 using assms by (cases m) auto
  1281 
  1282 lemma lcm_least_nat:
  1283   assumes "(m::nat) dvd k" and "n dvd k"
  1284   shows "lcm m n dvd k"
  1285 proof (cases k)
  1286   case 0 then show ?thesis by auto
  1287 next
  1288   case (Suc _) then have pos_k: "k > 0" by auto
  1289   from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1290   with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
  1291   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1292   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1293   from pos_k k_m have pos_p: "p > 0" by auto
  1294   from pos_k k_n have pos_q: "q > 0" by auto
  1295   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1296     by (simp add: mult_ac gcd_mult_distrib_nat)
  1297   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1298     by (simp add: k_m [symmetric] k_n [symmetric])
  1299   also have "\<dots> = k * p * q * gcd m n"
  1300     by (simp add: mult_ac gcd_mult_distrib_nat)
  1301   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1302     by (simp only: k_m [symmetric] k_n [symmetric])
  1303   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1304     by (simp add: mult_ac)
  1305   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1306     by simp
  1307   with prod_gcd_lcm_nat [of m n]
  1308   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1309     by (simp add: mult_ac)
  1310   with pos_gcd have "lcm m n * gcd q p = k" by auto
  1311   then show ?thesis using dvd_def by auto
  1312 qed
  1313 
  1314 lemma lcm_least_int:
  1315   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1316 apply (subst lcm_abs_int)
  1317 apply (rule dvd_trans)
  1318 apply (rule lcm_least_nat [transferred, of _ "abs k" _])
  1319 apply auto
  1320 done
  1321 
  1322 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
  1323 proof (cases m)
  1324   case 0 then show ?thesis by simp
  1325 next
  1326   case (Suc _)
  1327   then have mpos: "m > 0" by simp
  1328   show ?thesis
  1329   proof (cases n)
  1330     case 0 then show ?thesis by simp
  1331   next
  1332     case (Suc _)
  1333     then have npos: "n > 0" by simp
  1334     have "gcd m n dvd n" by simp
  1335     then obtain k where "n = gcd m n * k" using dvd_def by auto
  1336     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1337       by (simp add: mult_ac)
  1338     also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
  1339     finally show ?thesis by (simp add: lcm_nat_def)
  1340   qed
  1341 qed
  1342 
  1343 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1344   apply (subst lcm_abs_int)
  1345   apply (rule dvd_trans)
  1346   prefer 2
  1347   apply (rule lcm_dvd1_nat [transferred])
  1348   apply auto
  1349 done
  1350 
  1351 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1352   by (subst lcm_commute_nat, rule lcm_dvd1_nat)
  1353 
  1354 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1355   by (subst lcm_commute_int, rule lcm_dvd1_int)
  1356 
  1357 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1358 by(metis lcm_dvd1_nat dvd_trans)
  1359 
  1360 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1361 by(metis lcm_dvd2_nat dvd_trans)
  1362 
  1363 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1364 by(metis lcm_dvd1_int dvd_trans)
  1365 
  1366 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1367 by(metis lcm_dvd2_int dvd_trans)
  1368 
  1369 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1370     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1371   by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1372 
  1373 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1374     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1375   by (auto intro: dvd_antisym [transferred] lcm_least_int)
  1376 
  1377 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1378   apply (rule sym)
  1379   apply (subst lcm_unique_nat [symmetric])
  1380   apply auto
  1381 done
  1382 
  1383 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1384   apply (rule sym)
  1385   apply (subst lcm_unique_int [symmetric])
  1386   apply auto
  1387 done
  1388 
  1389 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1390 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
  1391 
  1392 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1393 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1394 
  1395 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1396 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1397 
  1398 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1399 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1400 
  1401 lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
  1402 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1403 
  1404 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
  1405 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1406 
  1407 lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
  1408 by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
  1409 
  1410 lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
  1411 by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
  1412 
  1413 lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
  1414 lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
  1415 
  1416 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1417 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1418 
  1419 lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1420 proof qed (auto simp add: gcd_ac_nat)
  1421 
  1422 lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  1423 proof qed (auto simp add: gcd_ac_int)
  1424 
  1425 lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1426 proof qed (auto simp add: lcm_ac_nat)
  1427 
  1428 lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  1429 proof qed (auto simp add: lcm_ac_int)
  1430 
  1431 
  1432 (* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
  1433 
  1434 lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1435 by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
  1436 
  1437 lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1438 by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
  1439 
  1440 lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
  1441 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
  1442 
  1443 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  1444 by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
  1445 
  1446 subsubsection {* The complete divisibility lattice *}
  1447 
  1448 
  1449 interpretation gcd_semilattice_nat: lower_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
  1450 proof
  1451   case goal3 thus ?case by(metis gcd_unique_nat)
  1452 qed auto
  1453 
  1454 interpretation lcm_semilattice_nat: upper_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
  1455 proof
  1456   case goal3 thus ?case by(metis lcm_unique_nat)
  1457 qed auto
  1458 
  1459 interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
  1460 
  1461 text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
  1462 GCD is defined via LCM to facilitate the proof that we have a complete lattice.
  1463 Later on we show that GCD and Gcd coincide on finite sets.
  1464 *}
  1465 context gcd
  1466 begin
  1467 
  1468 definition Gcd :: "'a set \<Rightarrow> 'a"
  1469 where "Gcd = fold gcd 0"
  1470 
  1471 definition Lcm :: "'a set \<Rightarrow> 'a"
  1472 where "Lcm = fold lcm 1"
  1473 
  1474 definition LCM :: "'a set \<Rightarrow> 'a" where
  1475 "LCM M = (if finite M then Lcm M else 0)"
  1476 
  1477 definition GCD :: "'a set \<Rightarrow> 'a" where
  1478 "GCD M = LCM(INT m:M. {d. d dvd m})"
  1479 
  1480 end
  1481 
  1482 lemma Gcd_empty[simp]: "Gcd {} = 0"
  1483 by(simp add:Gcd_def)
  1484 
  1485 lemma Lcm_empty[simp]: "Lcm {} = 1"
  1486 by(simp add:Lcm_def)
  1487 
  1488 lemma GCD_empty_nat[simp]: "GCD {} = (0::nat)"
  1489 by(simp add:GCD_def LCM_def)
  1490 
  1491 lemma LCM_eq_Lcm[simp]: "finite M \<Longrightarrow> LCM M = Lcm M"
  1492 by(simp add:LCM_def)
  1493 
  1494 lemma Lcm_insert_nat [simp]:
  1495   assumes "finite N"
  1496   shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
  1497 proof -
  1498   interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
  1499     by (rule fun_left_comm_idem_lcm_nat)
  1500   from assms show ?thesis by(simp add: Lcm_def)
  1501 qed
  1502 
  1503 lemma Lcm_insert_int [simp]:
  1504   assumes "finite N"
  1505   shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
  1506 proof -
  1507   interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
  1508     by (rule fun_left_comm_idem_lcm_int)
  1509   from assms show ?thesis by(simp add: Lcm_def)
  1510 qed
  1511 
  1512 lemma Gcd_insert_nat [simp]:
  1513   assumes "finite N"
  1514   shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
  1515 proof -
  1516   interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
  1517     by (rule fun_left_comm_idem_gcd_nat)
  1518   from assms show ?thesis by(simp add: Gcd_def)
  1519 qed
  1520 
  1521 lemma Gcd_insert_int [simp]:
  1522   assumes "finite N"
  1523   shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
  1524 proof -
  1525   interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
  1526     by (rule fun_left_comm_idem_gcd_int)
  1527   from assms show ?thesis by(simp add: Gcd_def)
  1528 qed
  1529 
  1530 lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
  1531 by(induct rule:finite_ne_induct) auto
  1532 
  1533 lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
  1534 by (metis Lcm0_iff empty_iff)
  1535 
  1536 lemma Gcd_dvd_nat [simp]:
  1537   assumes "finite M" and "(m::nat) \<in> M"
  1538   shows "Gcd M dvd m"
  1539 proof -
  1540   show ?thesis using gcd_semilattice_nat.fold_inf_le_inf[OF assms, of 0] by (simp add: Gcd_def)
  1541 qed
  1542 
  1543 lemma dvd_Gcd_nat[simp]:
  1544   assumes "finite M" and "ALL (m::nat) : M. n dvd m"
  1545   shows "n dvd Gcd M"
  1546 proof -
  1547   show ?thesis using gcd_semilattice_nat.inf_le_fold_inf[OF assms, of 0] by (simp add: Gcd_def)
  1548 qed
  1549 
  1550 lemma dvd_Lcm_nat [simp]:
  1551   assumes "finite M" and "(m::nat) \<in> M"
  1552   shows "m dvd Lcm M"
  1553 proof -
  1554   show ?thesis using lcm_semilattice_nat.sup_le_fold_sup[OF assms, of 1] by (simp add: Lcm_def)
  1555 qed
  1556 
  1557 lemma Lcm_dvd_nat[simp]:
  1558   assumes "finite M" and "ALL (m::nat) : M. m dvd n"
  1559   shows "Lcm M dvd n"
  1560 proof -
  1561   show ?thesis using lcm_semilattice_nat.fold_sup_le_sup[OF assms, of 1] by (simp add: Lcm_def)
  1562 qed
  1563 
  1564 interpretation gcd_lcm_complete_lattice_nat:
  1565   complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
  1566 proof
  1567   case goal1 show ?case by simp
  1568 next
  1569   case goal2 show ?case by simp
  1570 next
  1571   case goal5 thus ?case by (auto simp: LCM_def)
  1572 next
  1573   case goal6 thus ?case
  1574     by(auto simp: LCM_def)(metis finite_nat_set_iff_bounded_le gcd_proj2_if_dvd_nat gcd_le1_nat)
  1575 next
  1576   case goal3 thus ?case by (auto simp: GCD_def LCM_def)(metis finite_INT finite_divisors_nat)
  1577 next
  1578   case goal4 thus ?case by(auto simp: LCM_def GCD_def)
  1579 qed
  1580 
  1581 text{* Alternative characterizations of Gcd and GCD: *}
  1582 
  1583 lemma Gcd_eq_Max: "finite(M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> Gcd M = Max(\<Inter>m\<in>M. {d. d dvd m})"
  1584 apply(rule antisym)
  1585  apply(rule Max_ge)
  1586   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1587  apply simp
  1588 apply (rule Max_le_iff[THEN iffD2])
  1589   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1590  apply fastsimp
  1591 apply clarsimp
  1592 apply (metis Gcd_dvd_nat Max_in dvd_0_left dvd_Gcd_nat dvd_imp_le linorder_antisym_conv3 not_less0)
  1593 done
  1594 
  1595 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
  1596 apply(induct pred:finite)
  1597  apply simp
  1598 apply(case_tac "x=0")
  1599  apply simp
  1600 apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
  1601  apply simp
  1602 apply blast
  1603 done
  1604 
  1605 lemma Lcm_in_lcm_closed_set_nat:
  1606   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
  1607 apply(induct rule:finite_linorder_min_induct)
  1608  apply simp
  1609 apply simp
  1610 apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
  1611  apply simp
  1612  apply(case_tac "A={}")
  1613   apply simp
  1614  apply simp
  1615 apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  1616 done
  1617 
  1618 lemma Lcm_eq_Max_nat:
  1619   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M = Max M"
  1620 apply(rule antisym)
  1621  apply(rule Max_ge, assumption)
  1622  apply(erule (2) Lcm_in_lcm_closed_set_nat)
  1623 apply clarsimp
  1624 apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
  1625 done
  1626 
  1627 text{* Finally GCD is Gcd: *}
  1628 
  1629 lemma GCD_eq_Gcd[simp]: assumes "finite(M::nat set)" shows "GCD M = Gcd M"
  1630 proof-
  1631   have divisors_remove0_nat: "(\<Inter>m\<in>M. {d::nat. d dvd m}) = (\<Inter>m\<in>M-{0}. {d::nat. d dvd m})" by auto
  1632   show ?thesis
  1633   proof cases
  1634     assume "M={}" thus ?thesis by simp
  1635   next
  1636     assume "M\<noteq>{}"
  1637     show ?thesis
  1638     proof cases
  1639       assume "M={0}" thus ?thesis by(simp add:GCD_def LCM_def)
  1640     next
  1641       assume "M\<noteq>{0}"
  1642       with `M\<noteq>{}` assms show ?thesis
  1643         apply(subst Gcd_remove0_nat[OF assms])
  1644         apply(simp add:GCD_def)
  1645         apply(subst divisors_remove0_nat)
  1646         apply(simp add:LCM_def)
  1647         apply rule
  1648          apply rule
  1649          apply(subst Gcd_eq_Max)
  1650             apply simp
  1651            apply blast
  1652           apply blast
  1653          apply(rule Lcm_eq_Max_nat)
  1654             apply simp
  1655            apply blast
  1656           apply fastsimp
  1657          apply clarsimp
  1658         apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
  1659         done
  1660     qed
  1661   qed
  1662 qed
  1663 
  1664 lemma Lcm_set_nat [code_unfold]:
  1665   "Lcm (set ns) = foldl lcm (1::nat) ns"
  1666 proof -
  1667   interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
  1668   show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
  1669 qed
  1670 
  1671 lemma Lcm_set_int [code_unfold]:
  1672   "Lcm (set is) = foldl lcm (1::int) is"
  1673 proof -
  1674   interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
  1675   show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
  1676 qed
  1677 
  1678 lemma Gcd_set_nat [code_unfold]:
  1679   "Gcd (set ns) = foldl gcd (0::nat) ns"
  1680 proof -
  1681   interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
  1682   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
  1683 qed
  1684 
  1685 lemma Gcd_set_int [code_unfold]:
  1686   "Gcd (set ns) = foldl gcd (0::int) ns"
  1687 proof -
  1688   interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
  1689   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
  1690 qed
  1691 
  1692 lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
  1693 apply (rule eq_reflection)
  1694 apply (induct x y rule: nat_gcd.induct)
  1695 by (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  1696 
  1697 lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \<equiv> Nitpick.nat_lcm x y"
  1698 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  1699 
  1700 end