# Theory IntRing

theory IntRing
imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
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¦"
by (metis dvd_if_abs_eq lcm.commute lcm_proj1_iff_int)
subsection ‹‹𝒵›: The Set of Integers as Algebraic Structure›
abbreviation int_ring :: "int ring" ("𝒵")
where "int_ring ≡ ⦇carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)⦈"
lemma int_Zcarr [intro!, simp]: "k ∈ carrier 𝒵"
by simp
lemma int_is_cring: "cring 𝒵"
proof (rule cringI)
show "abelian_group 𝒵"
by (rule abelian_groupI) (auto intro: left_minus)
show "Group.comm_monoid 𝒵"
by (simp add: Group.monoid.intro monoid.monoid_comm_monoidI)
qed (auto simp: distrib_right)
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 -
show "monoid 𝒵" by standard auto
then interpret int: monoid 𝒵 .
show "carrier 𝒵 = UNIV" by simp
{ 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 -
show "comm_monoid 𝒵" by standard auto
then interpret int: comm_monoid 𝒵 .
{ 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_add_eq: "add 𝒵 x y = x + y"
and int_finsum_eq: "finsum 𝒵 f A = sum f A"
proof -
show "abelian_monoid 𝒵" by standard auto
then interpret int: abelian_monoid 𝒵 .
show "carrier 𝒵 = UNIV" by simp
{ fix x y show "add 𝒵 x y = x + y" by simp }
note add = this
show zero: "zero 𝒵 = 0"
by simp
show "finsum 𝒵 f A = sum f A"
by (induct A rule: infinite_finite_induct, auto)
qed