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