# Theory IntRing

theory IntRing
imports Primes QuotRing
```(*  Title:      HOL/Algebra/IntRing.thy
Author:     Stephan Hohe, TU Muenchen
Author:     Clemens Ballarin
*)

theory IntRing
imports "HOL-Computational_Algebra.Primes" QuotRing Lattice HOL.Int
begin

section ‹The Ring of Integers›

subsection ‹Some properties of @{typ int}›

lemma dvds_eq_abseq:
fixes k :: int
shows "l dvd k ∧ k dvd l ⟷ ¦l¦ = ¦k¦"
apply rule
done

subsection ‹‹𝒵›: The Set of Integers as Algebraic Structure›

abbreviation int_ring :: "int ring" ("𝒵")
where "int_ring ≡ ⦇carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +⦈"

lemma int_Zcarr [intro!, simp]: "k ∈ carrier 𝒵"
by simp

lemma int_is_cring: "cring 𝒵"
apply (rule cringI)
apply (rule abelian_groupI, simp_all)
defer 1
apply (rule comm_monoidI, simp_all)
apply (rule distrib_right)
apply (fast intro: left_minus)
done

(*
lemma int_is_domain:
"domain 𝒵"
apply (intro domain.intro domain_axioms.intro)
apply (rule int_is_cring)
apply (unfold int_ring_def, simp+)
done
*)

subsection ‹Interpretations›

text ‹Since definitions of derived operations are global, their
interpretation needs to be done as early as possible --- that is,
with as few assumptions as possible.›

interpretation int: monoid 𝒵
rewrites "carrier 𝒵 = UNIV"
and "mult 𝒵 x y = x * y"
and "one 𝒵 = 1"
and "pow 𝒵 x n = x^n"
proof -
― "Specification"
show "monoid 𝒵" by standard auto
then interpret int: monoid 𝒵 .

― "Carrier"
show "carrier 𝒵 = UNIV" by simp

― "Operations"
{ fix x y show "mult 𝒵 x y = x * y" by simp }
show "one 𝒵 = 1" by simp
show "pow 𝒵 x n = x^n" by (induct n) simp_all
qed

interpretation int: comm_monoid 𝒵
rewrites "finprod 𝒵 f A = prod f A"
proof -
― "Specification"
show "comm_monoid 𝒵" by standard auto
then interpret int: comm_monoid 𝒵 .

― "Operations"
{ fix x y have "mult 𝒵 x y = x * y" by simp }
note mult = this
have one: "one 𝒵 = 1" by simp
show "finprod 𝒵 f A = prod f A"
by (induct A rule: infinite_finite_induct, auto)
qed

interpretation int: abelian_monoid 𝒵
rewrites int_carrier_eq: "carrier 𝒵 = UNIV"
and int_zero_eq: "zero 𝒵 = 0"
and int_finsum_eq: "finsum 𝒵 f A = sum f A"
proof -
― "Specification"
show "abelian_monoid 𝒵" by standard auto
then interpret int: abelian_monoid 𝒵 .

― "Carrier"
show "carrier 𝒵 = UNIV" by simp

― "Operations"
{ fix x y show "add 𝒵 x y = x + y" by simp }
show zero: "zero 𝒵 = 0"
by simp
show "finsum 𝒵 f A = sum f A"
by (induct A rule: infinite_finite_induct, auto)
qed

interpretation int: abelian_group 𝒵
(* The equations from the interpretation of abelian_monoid need to be repeated.
Since the morphisms through which the abelian structures are interpreted are
not the identity, the equations of these interpretations are not inherited. *)
(* FIXME *)
rewrites "carrier 𝒵 = UNIV"
and "zero 𝒵 = 0"
and "add 𝒵 x y = x + y"
and "finsum 𝒵 f A = sum f A"
and int_a_inv_eq: "a_inv 𝒵 x = - x"
and int_a_minus_eq: "a_minus 𝒵 x y = x - y"
proof -
― "Specification"
show "abelian_group 𝒵"
proof (rule abelian_groupI)
fix x
assume "x ∈ carrier 𝒵"
then show "∃y ∈ carrier 𝒵. y ⊕⇘𝒵⇙ x = 𝟬⇘𝒵⇙"
by simp arith
qed auto
then interpret int: abelian_group 𝒵 .
― "Operations"
{ fix x y have "add 𝒵 x y = x + y" by simp }
have zero: "zero 𝒵 = 0" by simp
{
fix x
have "add 𝒵 (- x) x = zero 𝒵"
then show "a_inv 𝒵 x = - x"
}
note a_inv = this
show "a_minus 𝒵 x y = x - y"

interpretation int: "domain" 𝒵
rewrites "carrier 𝒵 = UNIV"
and "zero 𝒵 = 0"
and "add 𝒵 x y = x + y"
and "finsum 𝒵 f A = sum f A"
and "a_inv 𝒵 x = - x"
and "a_minus 𝒵 x y = x - y"
proof -
show "domain 𝒵"
by unfold_locales (auto simp: distrib_right distrib_left)

text ‹Removal of occurrences of @{term UNIV} in interpretation result
--- experimental.›

lemma UNIV:
"x ∈ UNIV ⟷ True"
"A ⊆ UNIV ⟷ True"
"(∀x ∈ UNIV. P x) ⟷ (∀x. P x)"
"(EX x : UNIV. P x) ⟷ (EX x. P x)"
"(True ⟶ Q) ⟷ Q"
"(True ⟹ PROP R) ≡ PROP R"
by simp_all

interpretation int (* FIXME [unfolded UNIV] *) :
partial_order "⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈"
rewrites "carrier ⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈ = UNIV"
and "le ⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈ x y = (x ≤ y)"
and "lless ⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈ x y = (x < y)"
proof -
show "partial_order ⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈"
by standard simp_all
show "carrier ⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈ = UNIV"
by simp
show "le ⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈ x y = (x ≤ y)"
by simp
show "lless ⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈ x y = (x < y)"
qed

interpretation int (* FIXME [unfolded UNIV] *) :
lattice "⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈"
rewrites "join ⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈ x y = max x y"
and "meet ⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈ x y = min x y"
proof -
let ?Z = "⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈"
show "lattice ?Z"
apply unfold_locales
apply arith
apply arith
done
then interpret int: lattice "?Z" .
show "join ?Z x y = max x y"
apply (rule int.joinI)
apply arith
done
show "meet ?Z x y = min x y"
apply (rule int.meetI)
apply arith
done
qed

interpretation int (* [unfolded UNIV] *) :
total_order "⦇carrier = UNIV::int set, eq = op =, le = op ≤⦈"
by standard clarsimp

subsection ‹Generated Ideals of ‹𝒵››

lemma int_Idl: "Idl⇘𝒵⇙ {a} = {x * a | x. True}"
apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp
done

lemma multiples_principalideal: "principalideal {x * a | x. True } 𝒵"
by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)

lemma prime_primeideal:
assumes prime: "prime p"
shows "primeideal (Idl⇘𝒵⇙ {p}) 𝒵"
apply (rule primeidealI)
apply (rule int.genideal_ideal, simp)
apply (rule int_is_cring)
apply clarsimp defer 1
apply (elim exE)
proof -
fix a b x
assume "a * b = x * p"
then have "p dvd a * b" by simp
then have "p dvd a ∨ p dvd b"
by (metis prime prime_dvd_mult_eq_int)
then show "(∃x. a = x * p) ∨ (∃x. b = x * p)"
by (metis dvd_def mult.commute)
next
assume "UNIV = {uu. EX x. uu = x * p}"
then obtain x where "1 = x * p" by best
then have "¦p * x¦ = 1" by (simp add: mult.commute)
then show False using prime
by (auto dest!: abs_zmult_eq_1 simp: prime_def)
qed

subsection ‹Ideals and Divisibility›

lemma int_Idl_subset_ideal: "Idl⇘𝒵⇙ {k} ⊆ Idl⇘𝒵⇙ {l} = (k ∈ Idl⇘𝒵⇙ {l})"
by (rule int.Idl_subset_ideal') simp_all

lemma Idl_subset_eq_dvd: "Idl⇘𝒵⇙ {k} ⊆ Idl⇘𝒵⇙ {l} ⟷ l dvd k"
apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
apply (rule, clarify)
done

lemma dvds_eq_Idl: "l dvd k ∧ k dvd l ⟷ Idl⇘𝒵⇙ {k} = Idl⇘𝒵⇙ {l}"
proof -
have a: "l dvd k ⟷ (Idl⇘𝒵⇙ {k} ⊆ Idl⇘𝒵⇙ {l})"
by (rule Idl_subset_eq_dvd[symmetric])
have b: "k dvd l ⟷ (Idl⇘𝒵⇙ {l} ⊆ Idl⇘𝒵⇙ {k})"
by (rule Idl_subset_eq_dvd[symmetric])

have "l dvd k ∧ k dvd l ⟷ Idl⇘𝒵⇙ {k} ⊆ Idl⇘𝒵⇙ {l} ∧ Idl⇘𝒵⇙ {l} ⊆ Idl⇘𝒵⇙ {k}"
by (subst a, subst b, simp)
also have "Idl⇘𝒵⇙ {k} ⊆ Idl⇘𝒵⇙ {l} ∧ Idl⇘𝒵⇙ {l} ⊆ Idl⇘𝒵⇙ {k} ⟷ Idl⇘𝒵⇙ {k} = Idl⇘𝒵⇙ {l}"
by blast
finally show ?thesis .
qed

lemma Idl_eq_abs: "Idl⇘𝒵⇙ {k} = Idl⇘𝒵⇙ {l} ⟷ ¦l¦ = ¦k¦"
apply (subst dvds_eq_abseq[symmetric])
apply (rule dvds_eq_Idl[symmetric])
done

subsection ‹Ideals and the Modulus›

definition ZMod :: "int ⇒ int ⇒ int set"
where "ZMod k r = (Idl⇘𝒵⇙ {k}) +>⇘𝒵⇙ r"

lemmas ZMod_defs =
ZMod_def genideal_def

lemma rcos_zfact:
assumes kIl: "k ∈ ZMod l r"
shows "∃x. k = x * l + r"
proof -
from kIl[unfolded ZMod_def] have "∃xl∈Idl⇘𝒵⇙ {l}. k = xl + r"
then obtain xl where xl: "xl ∈ Idl⇘𝒵⇙ {l}" and k: "k = xl + r"
by auto
from xl obtain x where "xl = x * l"
by (auto simp: int_Idl)
with k have "k = x * l + r"
by simp
then show "∃x. k = x * l + r" ..
qed

lemma ZMod_imp_zmod:
assumes zmods: "ZMod m a = ZMod m b"
shows "a mod m = b mod m"
proof -
interpret ideal "Idl⇘𝒵⇙ {m}" 𝒵
by (rule int.genideal_ideal) fast
from zmods have "b ∈ ZMod m a"
unfolding ZMod_def by (simp add: a_repr_independenceD)
then have "∃x. b = x * m + a"
by (rule rcos_zfact)
then obtain x where "b = x * m + a"
by fast
then have "b mod m = (x * m + a) mod m"
by simp
also have "… = ((x * m) mod m) + (a mod m)"
also have "… = a mod m"
by simp
finally have "b mod m = a mod m" .
then show "a mod m = b mod m" ..
qed

lemma ZMod_mod: "ZMod m a = ZMod m (a mod m)"
proof -
interpret ideal "Idl⇘𝒵⇙ {m}" 𝒵
by (rule int.genideal_ideal) fast
show ?thesis
unfolding ZMod_def
apply (rule a_repr_independence'[symmetric])
proof -
have "a = m * (a div m) + (a mod m)"
then have "a = (a div m) * m + (a mod m)"
by simp
then show "∃h. (∃x. h = x * m) ∧ a = h + a mod m"
by fast
qed simp
qed

lemma zmod_imp_ZMod:
assumes modeq: "a mod m = b mod m"
shows "ZMod m a = ZMod m b"
proof -
have "ZMod m a = ZMod m (a mod m)"
by (rule ZMod_mod)
also have "… = ZMod m (b mod m)"
also have "… = ZMod m b"
by (rule ZMod_mod[symmetric])
finally show ?thesis .
qed

corollary ZMod_eq_mod: "ZMod m a = ZMod m b ⟷ a mod m = b mod m"
apply (rule iffI)
apply (erule ZMod_imp_zmod)
apply (erule zmod_imp_ZMod)
done

subsection ‹Factorization›

definition ZFact :: "int ⇒ int set ring"
where "ZFact k = 𝒵 Quot (Idl⇘𝒵⇙ {k})"

lemmas ZFact_defs = ZFact_def FactRing_def

lemma ZFact_is_cring: "cring (ZFact k)"
apply (unfold ZFact_def)
apply (rule ideal.quotient_is_cring)
apply (intro ring.genideal_ideal)
apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
apply simp
apply (rule int_is_cring)
done

lemma ZFact_zero: "carrier (ZFact 0) = (⋃a. {{a}})"
apply (insert int.genideal_zero)
apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def)
done

lemma ZFact_one: "carrier (ZFact 1) = {UNIV}"
apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
apply (subst int.genideal_one)
apply (rule, rule, clarsimp)
apply (rule, rule, clarsimp)
apply (rule, clarsimp, arith)
apply (rule, clarsimp)
apply (rule exI[of _ "0"], clarsimp)
done

lemma ZFact_prime_is_domain:
assumes pprime: "prime p"
shows "domain (ZFact p)"
apply (unfold ZFact_def)
apply (rule primeideal.quotient_is_domain)
apply (rule prime_primeideal[OF pprime])
done

end
```