src/HOL/GCD.thy
author nipkow
Fri Jan 01 19:15:43 2010 +0100 (2010-01-01)
changeset 34223 dce32a1e05fe
parent 34222 e33ee7369ecb
child 34915 7894c7dab132
permissions -rw-r--r--
added lemmas
     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 {* Greates 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 n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
  1078   fix n a b
  1079   assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
  1080   have "a = b \<or> a < b \<or> b < a" by arith
  1081   moreover {assume eq: "a= b"
  1082     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1083     by simp}
  1084   moreover
  1085   {assume lt: "a < b"
  1086     hence "a + b - a < n \<or> a = 0"  using H(2) by arith
  1087     moreover
  1088     {assume "a =0" with z c have "P a b" by blast }
  1089     moreover
  1090     {assume ab: "a + b - a < n"
  1091       have th0: "a + b - a = a + (b - a)" using lt by arith
  1092       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1093       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 < n \<or> b = 0"  using H(2) by arith
  1098     moreover
  1099     {assume "b =0" with z c have "P a b" by blast }
  1100     moreover
  1101     {assume ab: "b + a - b < n"
  1102       have th0: "b + a - b = b + (a - b)" using lt by arith
  1103       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
  1104       have "P b a" by (simp add: th0[symmetric])
  1105       hence "P a b" using c by blast }
  1106     ultimately have "P a b" by blast}
  1107 ultimately  show "P a b" by blast
  1108 qed
  1109 
  1110 lemma bezout_lemma_nat:
  1111   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1112     (a * x = b * y + d \<or> b * x = a * y + d)"
  1113   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1114     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1115   using ex
  1116   apply clarsimp
  1117   apply (rule_tac x="d" in exI, simp add: dvd_add)
  1118   apply (case_tac "a * x = b * y + d" , simp_all)
  1119   apply (rule_tac x="x + y" in exI)
  1120   apply (rule_tac x="y" in exI)
  1121   apply algebra
  1122   apply (rule_tac x="x" in exI)
  1123   apply (rule_tac x="x + y" in exI)
  1124   apply algebra
  1125 done
  1126 
  1127 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1128     (a * x = b * y + d \<or> b * x = a * y + d)"
  1129   apply(induct a b rule: ind_euclid)
  1130   apply blast
  1131   apply clarify
  1132   apply (rule_tac x="a" in exI, simp add: dvd_add)
  1133   apply clarsimp
  1134   apply (rule_tac x="d" in exI)
  1135   apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
  1136   apply (rule_tac x="x+y" in exI)
  1137   apply (rule_tac x="y" in exI)
  1138   apply algebra
  1139   apply (rule_tac x="x" in exI)
  1140   apply (rule_tac x="x+y" in exI)
  1141   apply algebra
  1142 done
  1143 
  1144 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1145     (a * x - b * y = d \<or> b * x - a * y = d)"
  1146   using bezout_add_nat[of a b]
  1147   apply clarsimp
  1148   apply (rule_tac x="d" in exI, simp)
  1149   apply (rule_tac x="x" in exI)
  1150   apply (rule_tac x="y" in exI)
  1151   apply auto
  1152 done
  1153 
  1154 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1155   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1156 proof-
  1157  from nz have ap: "a > 0" by simp
  1158  from bezout_add_nat[of a b]
  1159  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1160    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1161  moreover
  1162     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1163      from H have ?thesis by blast }
  1164  moreover
  1165  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1166    {assume b0: "b = 0" with H  have ?thesis by simp}
  1167    moreover
  1168    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1169      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1170        by auto
  1171      moreover
  1172      {assume db: "d=b"
  1173        from prems have ?thesis apply simp
  1174          apply (rule exI[where x = b], simp)
  1175          apply (rule exI[where x = b])
  1176         by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1177     moreover
  1178     {assume db: "d < b"
  1179         {assume "x=0" hence ?thesis  using prems by simp }
  1180         moreover
  1181         {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1182           from db have "d \<le> b - 1" by simp
  1183           hence "d*b \<le> b*(b - 1)" by simp
  1184           with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1185           have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1186           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1187             by simp
  1188           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1189             by (simp only: mult_assoc right_distrib)
  1190           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1191             by algebra
  1192           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1193           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1194             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1195           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1196             by (simp only: diff_mult_distrib2 add_commute mult_ac)
  1197           hence ?thesis using H(1,2)
  1198             apply -
  1199             apply (rule exI[where x=d], simp)
  1200             apply (rule exI[where x="(b - 1) * y"])
  1201             by (rule exI[where x="x*(b - 1) - d"], simp)}
  1202         ultimately have ?thesis by blast}
  1203     ultimately have ?thesis by blast}
  1204   ultimately have ?thesis by blast}
  1205  ultimately show ?thesis by blast
  1206 qed
  1207 
  1208 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1209   shows "\<exists>x y. a * x = b * y + gcd a b"
  1210 proof-
  1211   let ?g = "gcd a b"
  1212   from bezout_add_strong_nat[OF a, of b]
  1213   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1214   from d(1,2) have "d dvd ?g" by simp
  1215   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1216   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1217   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1218   thus ?thesis by blast
  1219 qed
  1220 
  1221 
  1222 subsection {* LCM properties *}
  1223 
  1224 lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1225   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1226     zmult_int [symmetric] gcd_int_def)
  1227 
  1228 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1229   unfolding lcm_nat_def
  1230   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1231 
  1232 lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
  1233   unfolding lcm_int_def gcd_int_def
  1234   apply (subst int_mult [symmetric])
  1235   apply (subst prod_gcd_lcm_nat [symmetric])
  1236   apply (subst nat_abs_mult_distrib [symmetric])
  1237   apply (simp, simp add: abs_mult)
  1238 done
  1239 
  1240 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1241   unfolding lcm_nat_def by simp
  1242 
  1243 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1244   unfolding lcm_int_def by simp
  1245 
  1246 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1247   unfolding lcm_nat_def by simp
  1248 
  1249 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1250   unfolding lcm_int_def by simp
  1251 
  1252 lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
  1253   unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
  1254 
  1255 lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
  1256   unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
  1257 
  1258 
  1259 lemma lcm_pos_nat:
  1260   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1261 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1262 
  1263 lemma lcm_pos_int:
  1264   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1265   apply (subst lcm_abs_int)
  1266   apply (rule lcm_pos_nat [transferred])
  1267   apply auto
  1268 done
  1269 
  1270 lemma dvd_pos_nat:
  1271   fixes n m :: nat
  1272   assumes "n > 0" and "m dvd n"
  1273   shows "m > 0"
  1274 using assms by (cases m) auto
  1275 
  1276 lemma lcm_least_nat:
  1277   assumes "(m::nat) dvd k" and "n dvd k"
  1278   shows "lcm m n dvd k"
  1279 proof (cases k)
  1280   case 0 then show ?thesis by auto
  1281 next
  1282   case (Suc _) then have pos_k: "k > 0" by auto
  1283   from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1284   with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
  1285   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1286   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1287   from pos_k k_m have pos_p: "p > 0" by auto
  1288   from pos_k k_n have pos_q: "q > 0" by auto
  1289   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1290     by (simp add: mult_ac gcd_mult_distrib_nat)
  1291   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1292     by (simp add: k_m [symmetric] k_n [symmetric])
  1293   also have "\<dots> = k * p * q * gcd m n"
  1294     by (simp add: mult_ac gcd_mult_distrib_nat)
  1295   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1296     by (simp only: k_m [symmetric] k_n [symmetric])
  1297   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1298     by (simp add: mult_ac)
  1299   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1300     by simp
  1301   with prod_gcd_lcm_nat [of m n]
  1302   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1303     by (simp add: mult_ac)
  1304   with pos_gcd have "lcm m n * gcd q p = k" by auto
  1305   then show ?thesis using dvd_def by auto
  1306 qed
  1307 
  1308 lemma lcm_least_int:
  1309   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1310 apply (subst lcm_abs_int)
  1311 apply (rule dvd_trans)
  1312 apply (rule lcm_least_nat [transferred, of _ "abs k" _])
  1313 apply auto
  1314 done
  1315 
  1316 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
  1317 proof (cases m)
  1318   case 0 then show ?thesis by simp
  1319 next
  1320   case (Suc _)
  1321   then have mpos: "m > 0" by simp
  1322   show ?thesis
  1323   proof (cases n)
  1324     case 0 then show ?thesis by simp
  1325   next
  1326     case (Suc _)
  1327     then have npos: "n > 0" by simp
  1328     have "gcd m n dvd n" by simp
  1329     then obtain k where "n = gcd m n * k" using dvd_def by auto
  1330     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1331       by (simp add: mult_ac)
  1332     also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
  1333     finally show ?thesis by (simp add: lcm_nat_def)
  1334   qed
  1335 qed
  1336 
  1337 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1338   apply (subst lcm_abs_int)
  1339   apply (rule dvd_trans)
  1340   prefer 2
  1341   apply (rule lcm_dvd1_nat [transferred])
  1342   apply auto
  1343 done
  1344 
  1345 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1346   by (subst lcm_commute_nat, rule lcm_dvd1_nat)
  1347 
  1348 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1349   by (subst lcm_commute_int, rule lcm_dvd1_int)
  1350 
  1351 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1352 by(metis lcm_dvd1_nat dvd_trans)
  1353 
  1354 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1355 by(metis lcm_dvd2_nat dvd_trans)
  1356 
  1357 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1358 by(metis lcm_dvd1_int dvd_trans)
  1359 
  1360 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1361 by(metis lcm_dvd2_int dvd_trans)
  1362 
  1363 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1364     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1365   by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1366 
  1367 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1368     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1369   by (auto intro: dvd_antisym [transferred] lcm_least_int)
  1370 
  1371 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1372   apply (rule sym)
  1373   apply (subst lcm_unique_nat [symmetric])
  1374   apply auto
  1375 done
  1376 
  1377 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1378   apply (rule sym)
  1379   apply (subst lcm_unique_int [symmetric])
  1380   apply auto
  1381 done
  1382 
  1383 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1384 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
  1385 
  1386 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1387 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1388 
  1389 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1390 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1391 
  1392 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1393 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1394 
  1395 lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
  1396 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1397 
  1398 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
  1399 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1400 
  1401 lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
  1402 by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
  1403 
  1404 lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
  1405 by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
  1406 
  1407 lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
  1408 lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
  1409 
  1410 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1411 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1412 
  1413 lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1414 proof qed (auto simp add: gcd_ac_nat)
  1415 
  1416 lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  1417 proof qed (auto simp add: gcd_ac_int)
  1418 
  1419 lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1420 proof qed (auto simp add: lcm_ac_nat)
  1421 
  1422 lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  1423 proof qed (auto simp add: lcm_ac_int)
  1424 
  1425 
  1426 (* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
  1427 
  1428 lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1429 by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
  1430 
  1431 lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1432 by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
  1433 
  1434 lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
  1435 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
  1436 
  1437 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  1438 by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
  1439 
  1440 
  1441 subsubsection {* The complete divisibility lattice *}
  1442 
  1443 
  1444 interpretation gcd_semilattice_nat: lower_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
  1445 proof
  1446   case goal3 thus ?case by(metis gcd_unique_nat)
  1447 qed auto
  1448 
  1449 interpretation lcm_semilattice_nat: upper_semilattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
  1450 proof
  1451   case goal3 thus ?case by(metis lcm_unique_nat)
  1452 qed auto
  1453 
  1454 interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
  1455 
  1456 text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
  1457 GCD is defined via LCM to facilitate the proof that we have a complete lattice.
  1458 Later on we show that GCD and Gcd coincide on finite sets.
  1459 *}
  1460 context gcd
  1461 begin
  1462 
  1463 definition Gcd :: "'a set \<Rightarrow> 'a"
  1464 where "Gcd = fold gcd 0"
  1465 
  1466 definition Lcm :: "'a set \<Rightarrow> 'a"
  1467 where "Lcm = fold lcm 1"
  1468 
  1469 definition LCM :: "'a set \<Rightarrow> 'a" where
  1470 "LCM M = (if finite M then Lcm M else 0)"
  1471 
  1472 definition GCD :: "'a set \<Rightarrow> 'a" where
  1473 "GCD M = LCM(INT m:M. {d. d dvd m})"
  1474 
  1475 end
  1476 
  1477 lemma Gcd_empty[simp]: "Gcd {} = 0"
  1478 by(simp add:Gcd_def)
  1479 
  1480 lemma Lcm_empty[simp]: "Lcm {} = 1"
  1481 by(simp add:Lcm_def)
  1482 
  1483 lemma GCD_empty_nat[simp]: "GCD {} = (0::nat)"
  1484 by(simp add:GCD_def LCM_def)
  1485 
  1486 lemma LCM_eq_Lcm[simp]: "finite M \<Longrightarrow> LCM M = Lcm M"
  1487 by(simp add:LCM_def)
  1488 
  1489 lemma Lcm_insert_nat [simp]:
  1490   assumes "finite N"
  1491   shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
  1492 proof -
  1493   interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
  1494     by (rule fun_left_comm_idem_lcm_nat)
  1495   from assms show ?thesis by(simp add: Lcm_def)
  1496 qed
  1497 
  1498 lemma Lcm_insert_int [simp]:
  1499   assumes "finite N"
  1500   shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
  1501 proof -
  1502   interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
  1503     by (rule fun_left_comm_idem_lcm_int)
  1504   from assms show ?thesis by(simp add: Lcm_def)
  1505 qed
  1506 
  1507 lemma Gcd_insert_nat [simp]:
  1508   assumes "finite N"
  1509   shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
  1510 proof -
  1511   interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
  1512     by (rule fun_left_comm_idem_gcd_nat)
  1513   from assms show ?thesis by(simp add: Gcd_def)
  1514 qed
  1515 
  1516 lemma Gcd_insert_int [simp]:
  1517   assumes "finite N"
  1518   shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
  1519 proof -
  1520   interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
  1521     by (rule fun_left_comm_idem_gcd_int)
  1522   from assms show ?thesis by(simp add: Gcd_def)
  1523 qed
  1524 
  1525 lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
  1526 by(induct rule:finite_ne_induct) auto
  1527 
  1528 lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
  1529 by (metis Lcm0_iff empty_iff)
  1530 
  1531 lemma Gcd_dvd_nat [simp]:
  1532   assumes "finite M" and "(m::nat) \<in> M"
  1533   shows "Gcd M dvd m"
  1534 proof -
  1535   show ?thesis using gcd_semilattice_nat.fold_inf_le_inf[OF assms, of 0] by (simp add: Gcd_def)
  1536 qed
  1537 
  1538 lemma dvd_Gcd_nat[simp]:
  1539   assumes "finite M" and "ALL (m::nat) : M. n dvd m"
  1540   shows "n dvd Gcd M"
  1541 proof -
  1542   show ?thesis using gcd_semilattice_nat.inf_le_fold_inf[OF assms, of 0] by (simp add: Gcd_def)
  1543 qed
  1544 
  1545 lemma dvd_Lcm_nat [simp]:
  1546   assumes "finite M" and "(m::nat) \<in> M"
  1547   shows "m dvd Lcm M"
  1548 proof -
  1549   show ?thesis using lcm_semilattice_nat.sup_le_fold_sup[OF assms, of 1] by (simp add: Lcm_def)
  1550 qed
  1551 
  1552 lemma Lcm_dvd_nat[simp]:
  1553   assumes "finite M" and "ALL (m::nat) : M. m dvd n"
  1554   shows "Lcm M dvd n"
  1555 proof -
  1556   show ?thesis using lcm_semilattice_nat.fold_sup_le_sup[OF assms, of 1] by (simp add: Lcm_def)
  1557 qed
  1558 
  1559 interpretation gcd_lcm_complete_lattice_nat:
  1560   complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
  1561 proof
  1562   case goal1 show ?case by simp
  1563 next
  1564   case goal2 show ?case by simp
  1565 next
  1566   case goal5 thus ?case by (auto simp: LCM_def)
  1567 next
  1568   case goal6 thus ?case
  1569     by(auto simp: LCM_def)(metis finite_nat_set_iff_bounded_le gcd_proj2_if_dvd_nat gcd_le1_nat)
  1570 next
  1571   case goal3 thus ?case by (auto simp: GCD_def LCM_def)(metis finite_INT finite_divisors_nat)
  1572 next
  1573   case goal4 thus ?case by(auto simp: LCM_def GCD_def)
  1574 qed
  1575 
  1576 text{* Alternative characterizations of Gcd and GCD: *}
  1577 
  1578 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})"
  1579 apply(rule antisym)
  1580  apply(rule Max_ge)
  1581   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1582  apply simp
  1583 apply (rule Max_le_iff[THEN iffD2])
  1584   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  1585  apply fastsimp
  1586 apply clarsimp
  1587 apply (metis Gcd_dvd_nat Max_in dvd_0_left dvd_Gcd_nat dvd_imp_le linorder_antisym_conv3 not_less0)
  1588 done
  1589 
  1590 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
  1591 apply(induct pred:finite)
  1592  apply simp
  1593 apply(case_tac "x=0")
  1594  apply simp
  1595 apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
  1596  apply simp
  1597 apply blast
  1598 done
  1599 
  1600 lemma Lcm_in_lcm_closed_set_nat:
  1601   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
  1602 apply(induct rule:finite_linorder_min_induct)
  1603  apply simp
  1604 apply simp
  1605 apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
  1606  apply simp
  1607  apply(case_tac "A={}")
  1608   apply simp
  1609  apply simp
  1610 apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  1611 done
  1612 
  1613 lemma Lcm_eq_Max_nat:
  1614   "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"
  1615 apply(rule antisym)
  1616  apply(rule Max_ge, assumption)
  1617  apply(erule (2) Lcm_in_lcm_closed_set_nat)
  1618 apply clarsimp
  1619 apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
  1620 done
  1621 
  1622 text{* Finally GCD is Gcd: *}
  1623 
  1624 lemma GCD_eq_Gcd[simp]: assumes "finite(M::nat set)" shows "GCD M = Gcd M"
  1625 proof-
  1626   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
  1627   show ?thesis
  1628   proof cases
  1629     assume "M={}" thus ?thesis by simp
  1630   next
  1631     assume "M\<noteq>{}"
  1632     show ?thesis
  1633     proof cases
  1634       assume "M={0}" thus ?thesis by(simp add:GCD_def LCM_def)
  1635     next
  1636       assume "M\<noteq>{0}"
  1637       with `M\<noteq>{}` assms show ?thesis
  1638         apply(subst Gcd_remove0_nat[OF assms])
  1639         apply(simp add:GCD_def)
  1640         apply(subst divisors_remove0_nat)
  1641         apply(simp add:LCM_def)
  1642         apply rule
  1643          apply rule
  1644          apply(subst Gcd_eq_Max)
  1645             apply simp
  1646            apply blast
  1647           apply blast
  1648          apply(rule Lcm_eq_Max_nat)
  1649             apply simp
  1650            apply blast
  1651           apply fastsimp
  1652          apply clarsimp
  1653         apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
  1654         done
  1655     qed
  1656   qed
  1657 qed
  1658 
  1659 lemma Lcm_set_nat [code_unfold]:
  1660   "Lcm (set ns) = foldl lcm (1::nat) ns"
  1661 proof -
  1662   interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
  1663   show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
  1664 qed
  1665 
  1666 lemma Lcm_set_int [code_unfold]:
  1667   "Lcm (set is) = foldl lcm (1::int) is"
  1668 proof -
  1669   interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
  1670   show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
  1671 qed
  1672 
  1673 lemma Gcd_set_nat [code_unfold]:
  1674   "Gcd (set ns) = foldl gcd (0::nat) ns"
  1675 proof -
  1676   interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
  1677   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
  1678 qed
  1679 
  1680 lemma Gcd_set_int [code_unfold]:
  1681   "Gcd (set ns) = foldl gcd (0::int) ns"
  1682 proof -
  1683   interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
  1684   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
  1685 qed
  1686 
  1687 
  1688 lemma mult_inj_if_coprime_nat:
  1689   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
  1690    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
  1691 apply(auto simp add:inj_on_def)
  1692 apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
  1693              dvd.neq_le_trans dvd_triv_left)
  1694 apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
  1695              dvd.neq_le_trans dvd_triv_right mult_commute)
  1696 done
  1697 
  1698 text{* Nitpick: *}
  1699 
  1700 lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
  1701 apply (rule eq_reflection)
  1702 apply (induct x y rule: nat_gcd.induct)
  1703 by (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  1704 
  1705 lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \<equiv> Nitpick.nat_lcm x y"
  1706 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  1707 
  1708 end