(*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,

                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow

This file deals with the functions gcd and lcm.  Definitions and

lemmas are proved uniformly for the natural numbers and integers.

This file combines and revises a number of prior developments.

The original theories "GCD" and "Primes" were by Christophe Tabacznyj

and Lawrence C. Paulson, based on \cite{davenport92}. They introduced

gcd, lcm, and prime for the natural numbers.

The original theory "IntPrimes" was by Thomas M. Rasmussen, and

extended gcd, lcm, primes to the integers. Amine Chaieb provided

another extension of the notions to the integers, and added a number

of results to "Primes" and "GCD". IntPrimes also defined and developed

the congruence relations on the integers. The notion was extended to

the natural numbers by Chaieb.

Jeremy Avigad combined all of these, made everything uniform for the

natural numbers and the integers, and added a number of new theorems.

Tobias Nipkow cleaned up a lot.

*)

header {* Greatest common divisor and least common multiple *}

theory GCD

imports Fact Parity

begin

declare One_nat_def [simp del]

subsection {* GCD and LCM definitions *}

class gcd = zero + one + dvd +

  fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

    and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

begin

abbreviation

  coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

where

  "coprime x y == (gcd x y = 1)"

end

instantiation nat :: gcd

begin

fun

  gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"

where

  "gcd_nat x y =

   (if y = 0 then x else gcd y (x mod y))"

definition

  lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"

where

  "lcm_nat x y = x * y div (gcd x y)"

instance proof qed

end

instantiation int :: gcd

begin

definition

  gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"

where

  "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"

definition

  lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"

where

  "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"

instance proof qed

end

subsection {* Transfer setup *}

lemma transfer_nat_int_gcd:

  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"

  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"

  unfolding gcd_int_def lcm_int_def

  by auto

lemma transfer_nat_int_gcd_closures:

  "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"

  "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"

  by (auto simp add: gcd_int_def lcm_int_def)

declare transfer_morphism_nat_int[transfer add return:

    transfer_nat_int_gcd transfer_nat_int_gcd_closures]

lemma transfer_int_nat_gcd:

  "gcd (int x) (int y) = int (gcd x y)"

  "lcm (int x) (int y) = int (lcm x y)"

  by (unfold gcd_int_def lcm_int_def, auto)

lemma transfer_int_nat_gcd_closures:

  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"

  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"

  by (auto simp add: gcd_int_def lcm_int_def)

declare transfer_morphism_int_nat[transfer add return:

    transfer_int_nat_gcd transfer_int_nat_gcd_closures]

subsection {* GCD properties *}

(* was gcd_induct *)

lemma gcd_nat_induct:

  fixes m n :: nat

  assumes "\<And>m. P m 0"

    and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"

  shows "P m n"

  apply (rule gcd_nat.induct)

  apply (case_tac "y = 0")

  using assms apply simp_all

done

(* specific to int *)

lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"

  by (simp add: gcd_int_def)

lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"

  by (simp add: gcd_int_def)

lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"

by(simp add: gcd_int_def)

lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"

by (simp add: gcd_int_def)

lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"

by (metis abs_idempotent gcd_abs_int)

lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"

by (metis abs_idempotent gcd_abs_int)

lemma gcd_cases_int:

  fixes x :: int and y

  assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"

      and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"

      and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"

      and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"

  shows "P (gcd x y)"

by (insert assms, auto, arith)

lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"

  by (simp add: gcd_int_def)

lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"

  by (simp add: lcm_int_def)

lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"

  by (simp add: lcm_int_def)

lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"

  by (simp add: lcm_int_def)

lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"

by(simp add:lcm_int_def)

lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"

by (metis abs_idempotent lcm_int_def)

lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"

by (metis abs_idempotent lcm_int_def)

lemma lcm_cases_int:

  fixes x :: int and y

  assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"

      and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"

      and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"

      and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"

  shows "P (lcm x y)"

  using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith

lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"

  by (simp add: lcm_int_def)

(* was gcd_0, etc. *)

lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"

  by simp

(* was igcd_0, etc. *)

lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"

  by (unfold gcd_int_def, auto)

lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"

  by simp

lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"

  by (unfold gcd_int_def, auto)

lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"

  by (case_tac "y = 0", auto)

(* weaker, but useful for the simplifier *)

lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"

  by simp

lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"

  by simp

lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"

  by (simp add: One_nat_def)

lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"

  by (simp add: gcd_int_def)

lemma gcd_idem_nat: "gcd (x::nat) x = x"

by simp

lemma gcd_idem_int: "gcd (x::int) x = abs x"

by (auto simp add: gcd_int_def)

declare gcd_nat.simps [simp del]

text {*

  \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The

  conjunctions don't seem provable separately.

*}

lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"

  and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"

  apply (induct m n rule: gcd_nat_induct)

  apply (simp_all add: gcd_non_0_nat)

  apply (blast dest: dvd_mod_imp_dvd)

done

lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"

by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)

lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"

by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)

lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"

by(metis gcd_dvd1_nat dvd_trans)

lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"

by(metis gcd_dvd2_nat dvd_trans)

lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"

by(metis gcd_dvd1_int dvd_trans)

lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"

by(metis gcd_dvd2_int dvd_trans)

lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"

  by (rule dvd_imp_le, auto)

lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"

  by (rule dvd_imp_le, auto)

lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"

  by (rule zdvd_imp_le, auto)

lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"

  by (rule zdvd_imp_le, auto)

lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"

by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)

lemma gcd_greatest_int:

  "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"

  apply (subst gcd_abs_int)

  apply (subst abs_dvd_iff [symmetric])

  apply (rule gcd_greatest_nat [transferred])

  apply auto

done

lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =

    (k dvd m & k dvd n)"

  by (blast intro!: gcd_greatest_nat intro: dvd_trans)

lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"

  by (blast intro!: gcd_greatest_int intro: dvd_trans)

lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"

  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)

lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"

  by (auto simp add: gcd_int_def)

lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"

  by (insert gcd_zero_nat [of m n], arith)

lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"

  by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)

interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"

proof

qed (auto intro: dvd_antisym dvd_trans)

interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"

proof

qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)

lemmas gcd_assoc_nat = gcd_nat.assoc

lemmas gcd_commute_nat = gcd_nat.commute

lemmas gcd_left_commute_nat = gcd_nat.left_commute

lemmas gcd_assoc_int = gcd_int.assoc

lemmas gcd_commute_int = gcd_int.commute

lemmas gcd_left_commute_int = gcd_int.left_commute

lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat

lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int

lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>

    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"

  apply auto

  apply (rule dvd_antisym)

  apply (erule (1) gcd_greatest_nat)

  apply auto

done

lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>

    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"

apply (case_tac "d = 0")

 apply simp

apply (rule iffI)

 apply (rule zdvd_antisym_nonneg)

 apply (auto intro: gcd_greatest_int)

done

lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"

by (metis dvd.eq_iff gcd_unique_nat)

lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"

by (metis dvd.eq_iff gcd_unique_nat)

lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"

by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)

lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"

by (metis gcd_proj1_if_dvd_int gcd_commute_int)

text {*

  \medskip Multiplication laws

*}

lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"

    -- {* \cite[page 27]{davenport92} *}

  apply (induct m n rule: gcd_nat_induct)

  apply simp

  apply (case_tac "k = 0")

  apply (simp_all add: gcd_non_0_nat)

done

lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"

  apply (subst (1 2) gcd_abs_int)

  apply (subst (1 2) abs_mult)

  apply (rule gcd_mult_distrib_nat [transferred])

  apply auto

done

lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"

  apply (insert gcd_mult_distrib_nat [of m k n])

  apply simp

  apply (erule_tac t = m in ssubst)

  apply simp

  done

lemma coprime_dvd_mult_int:

  "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"

apply (subst abs_dvd_iff [symmetric])

apply (subst dvd_abs_iff [symmetric])

apply (subst (asm) gcd_abs_int)

apply (rule coprime_dvd_mult_nat [transferred])

    prefer 4 apply assumption

   apply auto

apply (subst abs_mult [symmetric], auto)

done

lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>

    (k dvd m * n) = (k dvd m)"

  by (auto intro: coprime_dvd_mult_nat)

lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>

    (k dvd m * n) = (k dvd m)"

  by (auto intro: coprime_dvd_mult_int)

lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"

  apply (rule dvd_antisym)

  apply (rule gcd_greatest_nat)

  apply (rule_tac n = k in coprime_dvd_mult_nat)

  apply (simp add: gcd_assoc_nat)

  apply (simp add: gcd_commute_nat)

  apply (simp_all add: mult_commute)

done

lemma gcd_mult_cancel_int:

  "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"

apply (subst (1 2) gcd_abs_int)

apply (subst abs_mult)

apply (rule gcd_mult_cancel_nat [transferred], auto)

done

lemma coprime_crossproduct_nat:

  fixes a b c d :: nat

  assumes "coprime a d" and "coprime b c"

  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" (is "?lhs \<longleftrightarrow> ?rhs")

proof

  assume ?rhs then show ?lhs by simp

next

  assume ?lhs

  from `?lhs` have "a dvd b * d" by (auto intro: dvdI dest: sym)

  with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)

  from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym)

  with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)

  from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult_commute)

  with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)

  from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult_commute)

  with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)

  from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym)

  moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym)

  ultimately show ?rhs ..

qed

lemma coprime_crossproduct_int:

  fixes a b c d :: int

  assumes "coprime a d" and "coprime b c"

  shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"

  using assms by (intro coprime_crossproduct_nat [transferred]) auto

text {* \medskip Addition laws *}

lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"

  apply (case_tac "n = 0")

  apply (simp_all add: gcd_non_0_nat)

done

lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"

  apply (subst (1 2) gcd_commute_nat)

  apply (subst add_commute)

  apply simp

done

(* to do: add the other variations? *)

lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"

  by (subst gcd_add1_nat [symmetric], auto)

lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"

  apply (subst gcd_commute_nat)

  apply (subst gcd_diff1_nat [symmetric])

  apply auto

  apply (subst gcd_commute_nat)

  apply (subst gcd_diff1_nat)

  apply assumption

  apply (rule gcd_commute_nat)

done

lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"

  apply (frule_tac b = y and a = x in pos_mod_sign)

  apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)

  apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]

    zmod_zminus1_eq_if)

  apply (frule_tac a = x in pos_mod_bound)

  apply (subst (1 2) gcd_commute_nat)

  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat

    nat_le_eq_zle)

done

lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"

  apply (case_tac "y = 0")

  apply force

  apply (case_tac "y > 0")

  apply (subst gcd_non_0_int, auto)

  apply (insert gcd_non_0_int [of "-y" "-x"])

  apply auto

done

lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"

by (metis gcd_red_int mod_add_self1 add_commute)

lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"

by (metis gcd_add1_int gcd_commute_int add_commute)

lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"

by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)

lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"

by (metis gcd_commute_int gcd_red_int mod_mult_self1 add_commute)

(* to do: differences, and all variations of addition rules

    as simplification rules for nat and int *)

(* FIXME remove iff *)

lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n"

  using mult_dvd_mono [of 1] by auto

(* to do: add the three variations of these, and for ints? *)

lemma finite_divisors_nat[simp]:

  assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"

proof-

  have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)

  from finite_subset[OF _ this] show ?thesis using assms

    by(bestsimp intro!:dvd_imp_le)

qed

lemma finite_divisors_int[simp]:

  assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"

proof-

  have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)

  hence "finite{d. abs d <= abs i}" by simp

  from finite_subset[OF _ this] show ?thesis using assms

    by(bestsimp intro!:dvd_imp_le_int)

qed

lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"

apply(rule antisym)

 apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)

apply simp

done

lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"

apply(rule antisym)

 apply(rule Max_le_iff [THEN iffD2])

  apply (auto intro: abs_le_D1 dvd_imp_le_int)

done

lemma gcd_is_Max_divisors_nat:

  "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"

apply(rule Max_eqI[THEN sym])

  apply (metis finite_Collect_conjI finite_divisors_nat)

 apply simp

 apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)

apply simp

done

lemma gcd_is_Max_divisors_int:

  "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"

apply(rule Max_eqI[THEN sym])

  apply (metis finite_Collect_conjI finite_divisors_int)

 apply simp

 apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)

apply simp

done

lemma gcd_code_int [code]:

  "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"

  by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)

subsection {* Coprimality *}

lemma div_gcd_coprime_nat:

  assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"

  shows "coprime (a div gcd a b) (b div gcd a b)"

proof -

  let ?g = "gcd a b"

  let ?a' = "a div ?g"

  let ?b' = "b div ?g"

  let ?g' = "gcd ?a' ?b'"

  have dvdg: "?g dvd a" "?g dvd b" by simp_all

  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all

  from dvdg dvdg' obtain ka kb ka' kb' where

      kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"

    unfolding dvd_def by blast

  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"

    by simp_all

  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"

    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]

      dvd_mult_div_cancel [OF dvdg(2)] dvd_def)

  have "?g \<noteq> 0" using nz by simp

  then have gp: "?g > 0" by arith

  from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .

  with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp

qed

lemma div_gcd_coprime_int:

  assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"

  shows "coprime (a div gcd a b) (b div gcd a b)"

apply (subst (1 2 3) gcd_abs_int)

apply (subst (1 2) abs_div)

  apply simp

 apply simp

apply(subst (1 2) abs_gcd_int)

apply (rule div_gcd_coprime_nat [transferred])

using nz apply (auto simp add: gcd_abs_int [symmetric])

done

lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"

  using gcd_unique_nat[of 1 a b, simplified] by auto

lemma coprime_Suc_0_nat:

    "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"

  using coprime_nat by (simp add: One_nat_def)

lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>

    (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"

  using gcd_unique_int [of 1 a b]

  apply clarsimp

  apply (erule subst)

  apply (rule iffI)

  apply force

  apply (drule_tac x = "abs e" in exI)

  apply (case_tac "e >= 0")

  apply force

  apply force

done

lemma gcd_coprime_nat:

  assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and

    b: "b = b' * gcd a b"

  shows    "coprime a' b'"

  apply (subgoal_tac "a' = a div gcd a b")

  apply (erule ssubst)

  apply (subgoal_tac "b' = b div gcd a b")

  apply (erule ssubst)

  apply (rule div_gcd_coprime_nat)

  using z apply force

  apply (subst (1) b)

  using z apply force

  apply (subst (1) a)

  using z apply force

  done

lemma gcd_coprime_int:

  assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and

    b: "b = b' * gcd a b"

  shows    "coprime a' b'"

  apply (subgoal_tac "a' = a div gcd a b")

  apply (erule ssubst)

  apply (subgoal_tac "b' = b div gcd a b")

  apply (erule ssubst)

  apply (rule div_gcd_coprime_int)

  using z apply force

  apply (subst (1) b)

  using z apply force

  apply (subst (1) a)

  using z apply force

  done

lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"

    shows "coprime d (a * b)"

  apply (subst gcd_commute_nat)

  using da apply (subst gcd_mult_cancel_nat)

  apply (subst gcd_commute_nat, assumption)

  apply (subst gcd_commute_nat, rule db)

done

lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"

    shows "coprime d (a * b)"

  apply (subst gcd_commute_int)

  using da apply (subst gcd_mult_cancel_int)

  apply (subst gcd_commute_int, assumption)

  apply (subst gcd_commute_int, rule db)

done

lemma coprime_lmult_nat:

  assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"

proof -

  have "gcd d a dvd gcd d (a * b)"

    by (rule gcd_greatest_nat, auto)

  with dab show ?thesis

    by auto

qed

lemma coprime_lmult_int:

  assumes "coprime (d::int) (a * b)" shows "coprime d a"

proof -

  have "gcd d a dvd gcd d (a * b)"

    by (rule gcd_greatest_int, auto)

  with assms show ?thesis

    by auto

qed

lemma coprime_rmult_nat:

  assumes "coprime (d::nat) (a * b)" shows "coprime d b"

proof -

  have "gcd d b dvd gcd d (a * b)"

    by (rule gcd_greatest_nat, auto intro: dvd_mult)

  with assms show ?thesis

    by auto

qed

lemma coprime_rmult_int:

  assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"

proof -

  have "gcd d b dvd gcd d (a * b)"

    by (rule gcd_greatest_int, auto intro: dvd_mult)

  with dab show ?thesis

    by auto

qed

lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>

    coprime d a \<and>  coprime d b"

  using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]

    coprime_mult_nat[of d a b]

  by blast

lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>

    coprime d a \<and>  coprime d b"

  using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]

    coprime_mult_int[of d a b]

  by blast

lemma gcd_coprime_exists_nat:

    assumes nz: "gcd (a::nat) b \<noteq> 0"

    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"

  apply (rule_tac x = "a div gcd a b" in exI)

  apply (rule_tac x = "b div gcd a b" in exI)

  using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)

done

lemma gcd_coprime_exists_int:

    assumes nz: "gcd (a::int) b \<noteq> 0"

    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"

  apply (rule_tac x = "a div gcd a b" in exI)

  apply (rule_tac x = "b div gcd a b" in exI)

  using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self)

done

lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"

  by (induct n, simp_all add: coprime_mult_nat)

lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"

  by (induct n, simp_all add: coprime_mult_int)

lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"

  apply (rule coprime_exp_nat)

  apply (subst gcd_commute_nat)

  apply (rule coprime_exp_nat)

  apply (subst gcd_commute_nat, assumption)

done

lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"

  apply (rule coprime_exp_int)

  apply (subst gcd_commute_int)

  apply (rule coprime_exp_int)

  apply (subst gcd_commute_int, assumption)

done

lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"

proof (cases)

  assume "a = 0 & b = 0"

  thus ?thesis by simp

  next assume "~(a = 0 & b = 0)"

  hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"

    by (auto simp:div_gcd_coprime_nat)

  hence "gcd ((a div gcd a b)^n * (gcd a b)^n)

      ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"

    apply (subst (1 2) mult_commute)

    apply (subst gcd_mult_distrib_nat [symmetric])

    apply simp

    done

  also have "(a div gcd a b)^n * (gcd a b)^n = a^n"

    apply (subst div_power)

    apply auto

    apply (rule dvd_div_mult_self)

    apply (rule dvd_power_same)

    apply auto

    done

  also have "(b div gcd a b)^n * (gcd a b)^n = b^n"

    apply (subst div_power)

    apply auto

    apply (rule dvd_div_mult_self)

    apply (rule dvd_power_same)

    apply auto

    done

  finally show ?thesis .

qed

lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"

  apply (subst (1 2) gcd_abs_int)

  apply (subst (1 2) power_abs)

  apply (rule gcd_exp_nat [where n = n, transferred])

  apply auto

done

lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"

  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"

proof-

  let ?g = "gcd a b"

  {assume "?g = 0" with dc have ?thesis by auto}

  moreover

  {assume z: "?g \<noteq> 0"

    from gcd_coprime_exists_nat[OF z]

    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"

      by blast

    have thb: "?g dvd b" by auto

    from ab'(1) have "a' dvd a"  unfolding dvd_def by blast

    with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp

    from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto

    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)

    with z have th_1: "a' dvd b' * c" by auto

    from coprime_dvd_mult_nat[OF ab'(3)] th_1

    have thc: "a' dvd c" by (subst (asm) mult_commute, blast)

    from ab' have "a = ?g*a'" by algebra

    with thb thc have ?thesis by blast }

  ultimately show ?thesis by blast

qed

lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"

  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"

proof-

  let ?g = "gcd a b"

  {assume "?g = 0" with dc have ?thesis by auto}

  moreover

  {assume z: "?g \<noteq> 0"

    from gcd_coprime_exists_int[OF z]

    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"

      by blast

    have thb: "?g dvd b" by auto

    from ab'(1) have "a' dvd a"  unfolding dvd_def by blast

    with dc have th0: "a' dvd b*c"

      using dvd_trans[of a' a "b*c"] by simp

    from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto

    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)

    with z have th_1: "a' dvd b' * c" by auto

    from coprime_dvd_mult_int[OF ab'(3)] th_1

    have thc: "a' dvd c" by (subst (asm) mult_commute, blast)

    from ab' have "a = ?g*a'" by algebra

    with thb thc have ?thesis by blast }

  ultimately show ?thesis by blast

qed

lemma pow_divides_pow_nat:

  assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"

  shows "a dvd b"

proof-

  let ?g = "gcd a b"

  from n obtain m where m: "n = Suc m" by (cases n, simp_all)

  {assume "?g = 0" with ab n have ?thesis by auto }

  moreover

  {assume z: "?g \<noteq> 0"

    hence zn: "?g ^ n \<noteq> 0" using n by simp

    from gcd_coprime_exists_nat[OF z]

    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"

      by blast

    from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"

      by (simp add: ab'(1,2)[symmetric])

    hence "?g^n*a'^n dvd ?g^n *b'^n"

      by (simp only: power_mult_distrib mult_commute)

    with zn z n have th0:"a'^n dvd b'^n" by auto

    have "a' dvd a'^n" by (simp add: m)

    with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp

    hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)

    from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1

    have "a' dvd b'" by (subst (asm) mult_commute, blast)

    hence "a'*?g dvd b'*?g" by simp

    with ab'(1,2)  have ?thesis by simp }

  ultimately show ?thesis by blast

qed

lemma pow_divides_pow_int:

  assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"

  shows "a dvd b"

proof-

  let ?g = "gcd a b"

  from n obtain m where m: "n = Suc m" by (cases n, simp_all)

  {assume "?g = 0" with ab n have ?thesis by auto }

  moreover

  {assume z: "?g \<noteq> 0"

    hence zn: "?g ^ n \<noteq> 0" using n by simp

    from gcd_coprime_exists_int[OF z]

    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"

      by blast

    from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"

      by (simp add: ab'(1,2)[symmetric])

    hence "?g^n*a'^n dvd ?g^n *b'^n"

      by (simp only: power_mult_distrib mult_commute)

    with zn z n have th0:"a'^n dvd b'^n" by auto

    have "a' dvd a'^n" by (simp add: m)

    with th0 have "a' dvd b'^n"

      using dvd_trans[of a' "a'^n" "b'^n"] by simp

    hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)

    from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1

    have "a' dvd b'" by (subst (asm) mult_commute, blast)

    hence "a'*?g dvd b'*?g" by simp

    with ab'(1,2)  have ?thesis by simp }

  ultimately show ?thesis by blast

qed

lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"

  by (auto intro: pow_divides_pow_nat dvd_power_same)

lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"

  by (auto intro: pow_divides_pow_int dvd_power_same)

lemma divides_mult_nat:

  assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"

  shows "m * n dvd r"

proof-

  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"

    unfolding dvd_def by blast

  from mr n' have "m dvd n'*n" by (simp add: mult_commute)

  hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp

  then obtain k where k: "n' = m*k" unfolding dvd_def by blast

  from n' k show ?thesis unfolding dvd_def by auto

qed

lemma divides_mult_int:

  assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"

  shows "m * n dvd r"

proof-

  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"

    unfolding dvd_def by blast

  from mr n' have "m dvd n'*n" by (simp add: mult_commute)

  hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp

  then obtain k where k: "n' = m*k" unfolding dvd_def by blast

  from n' k show ?thesis unfolding dvd_def by auto

qed

lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"

  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")

  apply force

  apply (rule dvd_diff_nat)

  apply auto

done

lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"

  using coprime_plus_one_nat by (simp add: One_nat_def)

lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"

  apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")

  apply force

  apply (rule dvd_diff)

  apply auto

done

lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"

  using coprime_plus_one_nat [of "n - 1"]

    gcd_commute_nat [of "n - 1" n] by auto

lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"

  using coprime_plus_one_int [of "n - 1"]

    gcd_commute_int [of "n - 1" n] by auto

lemma setprod_coprime_nat [rule_format]:

    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"

  apply (case_tac "finite A")

  apply (induct set: finite)

  apply (auto simp add: gcd_mult_cancel_nat)

done

lemma setprod_coprime_int [rule_format]:

    "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"

  apply (case_tac "finite A")

  apply (induct set: finite)

  apply (auto simp add: gcd_mult_cancel_int)

done

lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>

    x dvd b \<Longrightarrow> x = 1"

  apply (subgoal_tac "x dvd gcd a b")

  apply simp

  apply (erule (1) gcd_greatest_nat)

done

lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>

    x dvd b \<Longrightarrow> abs x = 1"

  apply (subgoal_tac "x dvd gcd a b")

  apply simp

  apply (erule (1) gcd_greatest_int)

done

lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>

    coprime d e"

  apply (auto simp add: dvd_def)

  apply (frule coprime_lmult_int)

  apply (subst gcd_commute_int)

  apply (subst (asm) (2) gcd_commute_int)

  apply (erule coprime_lmult_int)

done

lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"

apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)

done

lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"

apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)

done