# Theory Ring

theory Ring
imports FiniteProduct
```(*  Title:      HOL/Algebra/Ring.thy
Author:     Clemens Ballarin, started 9 December 1996

With contributions by Martin Baillon.
*)

theory Ring
imports FiniteProduct
begin

section ‹The Algebraic Hierarchy of Rings›

subsection ‹Abelian Groups›

record 'a ring = "'a monoid" +
zero :: 'a ("𝟬ı")
add :: "['a, 'a] ⇒ 'a" (infixl "⊕ı" 65)

abbreviation
add_monoid :: "('a, 'm) ring_scheme ⇒ ('a, 'm) monoid_scheme"
where "add_monoid R ≡ ⦇ carrier = carrier R, mult = add R, one = zero R, … = (undefined :: 'm) ⦈"

text ‹Derived operations.›

definition
a_inv :: "[('a, 'm) ring_scheme, 'a ] ⇒ 'a" ("⊖ı _"  80)
where "a_inv R = m_inv (add_monoid R)"

definition
a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" ("(_ ⊖ı _)" [65,66] 65)
where "x ⊖⇘R⇙ y = x ⊕⇘R⇙ (⊖⇘R⇙ y)"

definition
add_pow :: "[_, ('b :: semiring_1), 'a] ⇒ 'a" ("[_] ⋅ı _" [81, 81] 80)

locale abelian_monoid =
fixes G (structure)
assumes a_comm_monoid:

definition
finsum :: "[('b, 'm) ring_scheme, 'a ⇒ 'b, 'a set] ⇒ 'b" where
"finsum G = finprod (add_monoid G)"

syntax
"_finsum" :: "index ⇒ idt ⇒ 'a set ⇒ 'b ⇒ 'b"
("(3⨁__∈_. _)" [1000, 0, 51, 10] 10)
translations
"⨁⇘G⇙i∈A. b" ⇌ "CONST finsum G (λi. b) A"
― ‹Beware of argument permutation!›

locale abelian_group = abelian_monoid +
assumes a_comm_group:

subsection ‹Basic Properties›

lemma abelian_monoidI:
fixes R (structure)
assumes "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ x ⊕ y ∈ carrier R"
and "𝟬 ∈ carrier R"
and "⋀x y z. ⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
and "⋀x. x ∈ carrier R ⟹ 𝟬 ⊕ x = x"
and "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ x ⊕ y = y ⊕ x"
shows "abelian_monoid R"
by (auto intro!: abelian_monoid.intro comm_monoidI intro: assms)

lemma abelian_monoidE:
fixes R (structure)
assumes "abelian_monoid R"
shows "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ x ⊕ y ∈ carrier R"
and "𝟬 ∈ carrier R"
and "⋀x y z. ⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
and "⋀x. x ∈ carrier R ⟹ 𝟬 ⊕ x = x"
and "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ x ⊕ y = y ⊕ x"
using assms unfolding abelian_monoid_def comm_monoid_def comm_monoid_axioms_def monoid_def by auto

lemma abelian_groupI:
fixes R (structure)
assumes "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ x ⊕ y ∈ carrier R"
and "𝟬 ∈ carrier R"
and "⋀x y z. ⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
and "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ x ⊕ y = y ⊕ x"
and "⋀x. x ∈ carrier R ⟹ 𝟬 ⊕ x = x"
and "⋀x. x ∈ carrier R ⟹ ∃y ∈ carrier R. y ⊕ x = 𝟬"
shows "abelian_group R"
by (auto intro!: abelian_group.intro abelian_monoidI
abelian_group_axioms.intro comm_monoidI comm_groupI
intro: assms)

lemma abelian_groupE:
fixes R (structure)
assumes "abelian_group R"
shows "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ x ⊕ y ∈ carrier R"
and "𝟬 ∈ carrier R"
and "⋀x y z. ⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
and "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ x ⊕ y = y ⊕ x"
and "⋀x. x ∈ carrier R ⟹ 𝟬 ⊕ x = x"
and "⋀x. x ∈ carrier R ⟹ ∃y ∈ carrier R. y ⊕ x = 𝟬"
using abelian_group.a_comm_group assms comm_groupE by fastforce+

lemma (in abelian_monoid) a_monoid:
by (rule comm_monoid.axioms, rule a_comm_monoid)

lemma (in abelian_group) a_group:

lemmas monoid_record_simps = partial_object.simps monoid.simps

text ‹Transfer facts from multiplicative structures via interpretation.›

sublocale abelian_monoid <
rewrites "carrier (add_monoid G) = carrier G"
and "one     (add_monoid G) = zero G"
and "(λa k. pow (add_monoid G) a k) = (λa k. add_pow G k a)"

context abelian_monoid
begin

end

sublocale abelian_monoid <
rewrites "carrier (add_monoid G) = carrier G"
and "one     (add_monoid G) = zero G"
and "finprod (add_monoid G) = finsum G"
by (rule a_comm_monoid) (auto simp: finsum_def add_pow_def)

context abelian_monoid begin

lemmas a_ac = a_assoc a_comm a_lcomm

text ‹Usually, if this rule causes a failed congruence proof error,
the reason is that the premise ‹g ∈ B → carrier G› cannot be shown.
Adding @{thm [source] Pi_def} to the simpset is often useful.›

(* The following would be wrong.  Needed is the equivalent of [^] for addition,
or indeed the canonical embedding from Nat into the monoid.

lemma finsum_const:
assumes fin [simp]: "finite A"
and a [simp]: "a : carrier G"
shows "finsum G (%x. a) A = a [^] card A"
using fin apply induct
apply force
apply (subst finsum_insert)
apply auto
apply (subst m_comm)
apply auto
done
*)

end

sublocale abelian_group <
rewrites "carrier (add_monoid G) = carrier G"
and "one     (add_monoid G) = zero G"
and "m_inv   (add_monoid G) = a_inv G"
by (rule a_group) (auto simp: m_inv_def a_inv_def add_pow_def)

context abelian_group
begin

lemma minus_closed [intro, simp]:
"[| x ∈ carrier G; y ∈ carrier G |] ==> x ⊖ y ∈ carrier G"

lemmas l_neg = add.l_inv [simp del]
lemmas r_neg = add.r_inv [simp del]

end

sublocale abelian_group <
rewrites "carrier (add_monoid G) = carrier G"
and "one     (add_monoid G) = zero G"
and "m_inv   (add_monoid G) = a_inv G"
and "finprod (add_monoid G) = finsum G"
by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def add_pow_def)

text ‹Derive an ‹abelian_group› from a ‹comm_group››

lemma comm_group_abelian_groupI:
fixes G (structure)
shows "abelian_group G"
proof -
by (rule cg)
show "abelian_group G" ..
qed

subsection ‹Rings: Basic Definitions›

locale semiring = abelian_monoid (* for add *) R + monoid (* for mult *) R for R (structure) +
assumes l_distr: "⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ (x ⊕ y) ⊗ z = x ⊗ z ⊕ y ⊗ z"
and r_distr: "⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ z ⊗ (x ⊕ y) = z ⊗ x ⊕ z ⊗ y"
and l_null[simp]: "x ∈ carrier R ⟹ 𝟬 ⊗ x = 𝟬"
and r_null[simp]: "x ∈ carrier R ⟹ x ⊗ 𝟬 = 𝟬"

locale ring = abelian_group (* for add *) R + monoid (* for mult *) R for R (structure) +
assumes "⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ (x ⊕ y) ⊗ z = x ⊗ z ⊕ y ⊗ z"
and "⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ z ⊗ (x ⊕ y) = z ⊗ x ⊕ z ⊗ y"

locale cring = ring + comm_monoid (* for mult *) R

locale "domain" = cring +
assumes one_not_zero [simp]: "𝟭 ≠ 𝟬"
and integral: "⟦ a ⊗ b = 𝟬; a ∈ carrier R; b ∈ carrier R ⟧ ⟹ a = 𝟬 ∨ b = 𝟬"

locale field = "domain" +
assumes field_Units: "Units R = carrier R - {𝟬}"

subsection ‹Rings›

lemma ringI:
fixes R (structure)
assumes "abelian_group R"
and "monoid R"
and "⋀x y z. ⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ (x ⊕ y) ⊗ z = x ⊗ z ⊕ y ⊗ z"
and "⋀x y z. ⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ z ⊗ (x ⊕ y) = z ⊗ x ⊕ z ⊗ y"
shows "ring R"
by (auto intro: ring.intro
abelian_group.axioms ring_axioms.intro assms)

lemma ringE:
fixes R (structure)
assumes "ring R"
shows "abelian_group R"
and "monoid R"
and "⋀x y z. ⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ (x ⊕ y) ⊗ z = x ⊗ z ⊕ y ⊗ z"
and "⋀x y z. ⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ z ⊗ (x ⊕ y) = z ⊗ x ⊕ z ⊗ y"
using assms unfolding ring_def ring_axioms_def by auto

context ring begin

lemma is_abelian_group: "abelian_group R" ..

lemma is_monoid: "monoid R"
by (auto intro!: monoidI m_assoc)

lemma is_ring: "ring R"
by (rule ring_axioms)

end
thm monoid_record_simps
lemmas ring_record_simps = monoid_record_simps ring.simps

lemma cringI:
fixes R (structure)
assumes abelian_group: "abelian_group R"
and comm_monoid: "comm_monoid R"
and l_distr: "⋀x y z. ⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹
(x ⊕ y) ⊗ z = x ⊗ z ⊕ y ⊗ z"
shows "cring R"
proof (intro cring.intro ring.intro)
show "ring_axioms R"
― ‹Right-distributivity follows from left-distributivity and
commutativity.›
proof (rule ring_axioms.intro)
fix x y z
assume R: "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R"
note [simp] = comm_monoid.axioms [OF comm_monoid]
abelian_group.axioms [OF abelian_group]
abelian_monoid.a_closed

from R have "z ⊗ (x ⊕ y) = (x ⊕ y) ⊗ z"
by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
also from R have "... = x ⊗ z ⊕ y ⊗ z" by (simp add: l_distr)
also from R have "... = z ⊗ x ⊕ z ⊗ y"
by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
finally show "z ⊗ (x ⊕ y) = z ⊗ x ⊕ z ⊗ y" .
qed (rule l_distr)
qed (auto intro: cring.intro
abelian_group.axioms comm_monoid.axioms ring_axioms.intro assms)

lemma cringE:
fixes R (structure)
assumes "cring R"
shows "comm_monoid R"
and "⋀x y z. ⟦ x ∈ carrier R; y ∈ carrier R; z ∈ carrier R ⟧ ⟹ (x ⊕ y) ⊗ z = x ⊗ z ⊕ y ⊗ z"
using assms cring_def by auto (simp add: assms cring.axioms(1) ringE(3))

lemma (in cring) is_cring:
"cring R" by (rule cring_axioms)

lemma (in ring) minus_zero [simp]: "⊖ 𝟬 = 𝟬"

subsubsection ‹Normaliser for Rings›

lemma (in abelian_group) r_neg1:
"⟦ x ∈ carrier G; y ∈ carrier G ⟧ ⟹ (⊖ x) ⊕ (x ⊕ y) = y"
proof -
assume G: "x ∈ carrier G" "y ∈ carrier G"
then have "(⊖ x ⊕ x) ⊕ y = y"
by (simp only: l_neg l_zero)
with G show ?thesis by (simp add: a_ac)
qed

lemma (in abelian_group) r_neg2:
"⟦ x ∈ carrier G; y ∈ carrier G ⟧ ⟹ x ⊕ ((⊖ x) ⊕ y) = y"
proof -
assume G: "x ∈ carrier G" "y ∈ carrier G"
then have "(x ⊕ ⊖ x) ⊕ y = y"
by (simp only: r_neg l_zero)
with G show ?thesis
qed

context ring begin

text ‹
The following proofs are from Jacobson, Basic Algebra I, pp.~88--89.
›

sublocale semiring
proof -
note [simp] = ring_axioms[unfolded ring_def ring_axioms_def]
show "semiring R"
proof (unfold_locales)
fix x
assume R: "x ∈ carrier R"
then have "𝟬 ⊗ x ⊕ 𝟬 ⊗ x = (𝟬 ⊕ 𝟬) ⊗ x"
by (simp del: l_zero r_zero)
also from R have "... = 𝟬 ⊗ x ⊕ 𝟬" by simp
finally have "𝟬 ⊗ x ⊕ 𝟬 ⊗ x = 𝟬 ⊗ x ⊕ 𝟬" .
with R show "𝟬 ⊗ x = 𝟬" by (simp del: r_zero)
from R have "x ⊗ 𝟬 ⊕ x ⊗ 𝟬 = x ⊗ (𝟬 ⊕ 𝟬)"
by (simp del: l_zero r_zero)
also from R have "... = x ⊗ 𝟬 ⊕ 𝟬" by simp
finally have "x ⊗ 𝟬 ⊕ x ⊗ 𝟬 = x ⊗ 𝟬 ⊕ 𝟬" .
with R show "x ⊗ 𝟬 = 𝟬" by (simp del: r_zero)
qed auto
qed

lemma l_minus:
"⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ (⊖ x) ⊗ y = ⊖ (x ⊗ y)"
proof -
assume R: "x ∈ carrier R" "y ∈ carrier R"
then have "(⊖ x) ⊗ y ⊕ x ⊗ y = (⊖ x ⊕ x) ⊗ y" by (simp add: l_distr)
also from R have "... = 𝟬" by (simp add: l_neg)
finally have "(⊖ x) ⊗ y ⊕ x ⊗ y = 𝟬" .
with R have "(⊖ x) ⊗ y ⊕ x ⊗ y ⊕ ⊖ (x ⊗ y) = 𝟬 ⊕ ⊖ (x ⊗ y)" by simp
with R show ?thesis by (simp add: a_assoc r_neg)
qed

lemma r_minus:
"⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ x ⊗ (⊖ y) = ⊖ (x ⊗ y)"
proof -
assume R: "x ∈ carrier R" "y ∈ carrier R"
then have "x ⊗ (⊖ y) ⊕ x ⊗ y = x ⊗ (⊖ y ⊕ y)" by (simp add: r_distr)
also from R have "... = 𝟬" by (simp add: l_neg)
finally have "x ⊗ (⊖ y) ⊕ x ⊗ y = 𝟬" .
with R have "x ⊗ (⊖ y) ⊕ x ⊗ y ⊕ ⊖ (x ⊗ y) = 𝟬 ⊕ ⊖ (x ⊗ y)" by simp
with R show ?thesis by (simp add: a_assoc r_neg )
qed

end

lemma (in abelian_group) minus_eq: "x ⊖ y = x ⊕ (⊖ y)"
by (rule a_minus_def)

text ‹Setup algebra method:
compute distributive normal form in locale contexts›

ML_file ‹ringsimp.ML›

attribute_setup algebra = ‹
Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
-- Scan.lift Args.name -- Scan.repeat Args.term
>> (fn ((b, n), ts) => if b then Ringsimp.add_struct (n, ts) else Ringsimp.del_struct (n, ts))
› "theorems controlling algebra method"

method_setup algebra = ‹
Scan.succeed (SIMPLE_METHOD' o Ringsimp.algebra_tac)
› "normalisation of algebraic structure"

lemmas (in semiring) semiring_simprules
[algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
a_closed zero_closed  m_closed one_closed
a_assoc l_zero  a_comm m_assoc l_one l_distr r_zero
a_lcomm r_distr l_null r_null

lemmas (in ring) ring_simprules
[algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq
r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
a_lcomm r_distr l_null r_null l_minus r_minus

lemmas (in cring)
[algebra del: ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
_

lemmas (in cring) cring_simprules
[algebra add: cring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus

lemma (in semiring) nat_pow_zero:
"(n::nat) ≠ 0 ⟹ 𝟬 [^] n = 𝟬"
by (induct n) simp_all

context semiring begin

lemma one_zeroD:
assumes onezero: "𝟭 = 𝟬"
shows "carrier R = {𝟬}"
proof (rule, rule)
fix x
assume xcarr: "x ∈ carrier R"
from xcarr have "x = x ⊗ 𝟭" by simp
with onezero have "x = x ⊗ 𝟬" by simp
with xcarr have "x = 𝟬" by simp
then show "x ∈ {𝟬}" by fast
qed fast

lemma one_zeroI:
assumes carrzero: "carrier R = {𝟬}"
shows "𝟭 = 𝟬"
proof -
from one_closed and carrzero
show "𝟭 = 𝟬" by simp
qed

lemma carrier_one_zero: "(carrier R = {𝟬}) = (𝟭 = 𝟬)"
using one_zeroD by blast

lemma carrier_one_not_zero: "(carrier R ≠ {𝟬}) = (𝟭 ≠ 𝟬)"

end

text ‹Two examples for use of method algebra›

lemma
fixes R (structure) and S (structure)
assumes "ring R" "cring S"
assumes RS: "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier S" "d ∈ carrier S"
shows "a ⊕ (⊖ (a ⊕ (⊖ b))) = b ∧ c ⊗⇘S⇙ d = d ⊗⇘S⇙ c"
proof -
interpret ring R by fact
interpret cring S by fact
from RS show ?thesis by algebra
qed

lemma
fixes R (structure)
assumes "ring R"
assumes R: "a ∈ carrier R" "b ∈ carrier R"
shows "a ⊖ (a ⊖ b) = b"
proof -
interpret ring R by fact
from R show ?thesis by algebra
qed

subsubsection ‹Sums over Finite Sets›

lemma (in semiring) finsum_ldistr:
"⟦ finite A; a ∈ carrier R; f: A → carrier R ⟧ ⟹
(⨁ i ∈ A. (f i)) ⊗ a = (⨁ i ∈ A. ((f i) ⊗ a))"
proof (induct set: finite)
case empty then show ?case by simp
next
case (insert x F) then show ?case by (simp add: Pi_def l_distr)
qed

lemma (in semiring) finsum_rdistr:
"⟦ finite A; a ∈ carrier R; f: A → carrier R ⟧ ⟹
a ⊗ (⨁ i ∈ A. (f i)) = (⨁ i ∈ A. (a ⊗ (f i)))"
proof (induct set: finite)
case empty then show ?case by simp
next
case (insert x F) then show ?case by (simp add: Pi_def r_distr)
qed

text ‹A quick detour›

lemma add_pow_int_ge: "(k :: int) ≥ 0 ⟹ [ k ] ⋅⇘R⇙ a = [ nat k ] ⋅⇘R⇙ a" ✐‹contributor ‹Paulo Emílio de Vilhena››

lemma add_pow_int_lt: "(k :: int) < 0 ⟹ [ k ] ⋅⇘R⇙ a = ⊖⇘R⇙ ([ nat (- k) ] ⋅⇘R⇙ a)" ✐‹contributor ‹Paulo Emílio de Vilhena››

corollary (in semiring) add_pow_ldistr: ✐‹contributor ‹Paulo Emílio de Vilhena››
assumes "a ∈ carrier R" "b ∈ carrier R"
shows "([(k :: nat)] ⋅ a) ⊗ b = [k] ⋅ (a ⊗ b)"
proof -
have "([k] ⋅ a) ⊗ b = (⨁ i ∈ {..< k}. a) ⊗ b"
using add.finprod_const[OF assms(1), of "{..<k}"] by simp
also have " ... = (⨁ i ∈ {..< k}. (a ⊗ b))"
using finsum_ldistr[of "{..<k}" b "λx. a"] assms by simp
also have " ... = [k] ⋅ (a ⊗ b)"
using add.finprod_const[of "a ⊗ b" "{..<k}"] assms by simp
finally show ?thesis .
qed

corollary (in semiring) add_pow_rdistr: ✐‹contributor ‹Paulo Emílio de Vilhena››
assumes "a ∈ carrier R" "b ∈ carrier R"
shows "a ⊗ ([(k :: nat)] ⋅ b) = [k] ⋅ (a ⊗ b)"
proof -
have "a ⊗ ([k] ⋅ b) = a ⊗ (⨁ i ∈ {..< k}. b)"
using add.finprod_const[OF assms(2), of "{..<k}"] by simp
also have " ... = (⨁ i ∈ {..< k}. (a ⊗ b))"
using finsum_rdistr[of "{..<k}" a "λx. b"] assms by simp
also have " ... = [k] ⋅ (a ⊗ b)"
using add.finprod_const[of "a ⊗ b" "{..<k}"] assms by simp
finally show ?thesis .
qed

(* For integers, we need the uniqueness of the additive inverse *)
lemma (in ring) add_pow_ldistr_int: ✐‹contributor ‹Paulo Emílio de Vilhena››
assumes "a ∈ carrier R" "b ∈ carrier R"
shows "([(k :: int)] ⋅ a) ⊗ b = [k] ⋅ (a ⊗ b)"
proof (cases "k ≥ 0")
case True thus ?thesis
next
case False thus ?thesis
add_pow_ldistr[OF assms, of "nat (- k)"] assms l_minus by auto
qed

lemma (in ring) add_pow_rdistr_int: ✐‹contributor ‹Paulo Emílio de Vilhena››
assumes "a ∈ carrier R" "b ∈ carrier R"
shows "a ⊗ ([(k :: int)] ⋅ b) = [k] ⋅ (a ⊗ b)"
proof (cases "k ≥ 0")
case True thus ?thesis
next
case False thus ?thesis
add_pow_rdistr[OF assms, of "nat (- k)"] assms r_minus by auto
qed

subsection ‹Integral Domains›

context "domain" begin

lemma zero_not_one [simp]: "𝟬 ≠ 𝟭"
by (rule not_sym) simp

lemma integral_iff: (* not by default a simp rule! *)
"⟦ a ∈ carrier R; b ∈ carrier R ⟧ ⟹ (a ⊗ b = 𝟬) = (a = 𝟬 ∨ b = 𝟬)"
proof
assume "a ∈ carrier R" "b ∈ carrier R" "a ⊗ b = 𝟬"
then show "a = 𝟬 ∨ b = 𝟬" by (simp add: integral)
next
assume "a ∈ carrier R" "b ∈ carrier R" "a = 𝟬 ∨ b = 𝟬"
then show "a ⊗ b = 𝟬" by auto
qed

lemma m_lcancel:
assumes prem: "a ≠ 𝟬"
and R: "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R"
shows "(a ⊗ b = a ⊗ c) = (b = c)"
proof
assume eq: "a ⊗ b = a ⊗ c"
with R have "a ⊗ (b ⊖ c) = 𝟬" by algebra
with R have "a = 𝟬 ∨ (b ⊖ c) = 𝟬" by (simp add: integral_iff)
with prem and R have "b ⊖ c = 𝟬" by auto
with R have "b = b ⊖ (b ⊖ c)" by algebra
also from R have "b ⊖ (b ⊖ c) = c" by algebra
finally show "b = c" .
next
assume "b = c" then show "a ⊗ b = a ⊗ c" by simp
qed

lemma m_rcancel:
assumes prem: "a ≠ 𝟬"
and R: "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R"
shows conc: "(b ⊗ a = c ⊗ a) = (b = c)"
proof -
from prem and R have "(a ⊗ b = a ⊗ c) = (b = c)" by (rule m_lcancel)
with R show ?thesis by algebra
qed

end

subsection ‹Fields›

text ‹Field would not need to be derived from domain, the properties
for domain follow from the assumptions of field›

lemma (in field) is_ring: "ring R"
using ring_axioms .

lemma fieldE :
fixes R (structure)
assumes "field R"
shows "cring R"
and one_not_zero : "𝟭 ≠ 𝟬"
and integral: "⋀a b. ⟦ a ⊗ b = 𝟬; a ∈ carrier R; b ∈ carrier R ⟧ ⟹ a = 𝟬 ∨ b = 𝟬"
and field_Units: "Units R = carrier R - {𝟬}"
using assms unfolding field_def field_axioms_def domain_def domain_axioms_def by simp_all

lemma (in cring) cring_fieldI:
assumes field_Units: "Units R = carrier R - {𝟬}"
shows "field R"
proof
from field_Units have "𝟬 ∉ Units R" by fast
moreover have "𝟭 ∈ Units R" by fast
ultimately show "𝟭 ≠ 𝟬" by force
next
fix a b
assume acarr: "a ∈ carrier R"
and bcarr: "b ∈ carrier R"
and ab: "a ⊗ b = 𝟬"
show "a = 𝟬 ∨ b = 𝟬"
proof (cases "a = 𝟬", simp)
assume "a ≠ 𝟬"
with field_Units and acarr have aUnit: "a ∈ Units R" by fast
from bcarr have "b = 𝟭 ⊗ b" by algebra
also from aUnit acarr have "... = (inv a ⊗ a) ⊗ b" by simp
also from acarr bcarr aUnit[THEN Units_inv_closed]
have "... = (inv a) ⊗ (a ⊗ b)" by algebra
also from ab and acarr bcarr aUnit have "... = (inv a) ⊗ 𝟬" by simp
also from aUnit[THEN Units_inv_closed] have "... = 𝟬" by algebra
finally have "b = 𝟬" .
then show "a = 𝟬 ∨ b = 𝟬" by simp
qed
qed (rule field_Units)

text ‹Another variant to show that something is a field›
lemma (in cring) cring_fieldI2:
assumes notzero: "𝟬 ≠ 𝟭"
and invex: "⋀a. ⟦a ∈ carrier R; a ≠ 𝟬⟧ ⟹ ∃b∈carrier R. a ⊗ b = 𝟭"
shows "field R"
proof -
have *: "carrier R - {𝟬} ⊆ {y ∈ carrier R. ∃x∈carrier R. x ⊗ y = 𝟭 ∧ y ⊗ x = 𝟭}"
proof (clarsimp)
fix x
assume xcarr: "x ∈ carrier R" and "x ≠ 𝟬"
obtain y where ycarr: "y ∈ carrier R" and xy: "x ⊗ y = 𝟭"
using ‹x ≠ 𝟬› invex xcarr by blast
with ycarr and xy show "∃y∈carrier R. y ⊗ x = 𝟭 ∧ x ⊗ y = 𝟭"
using m_comm xcarr by fastforce
qed
show ?thesis
apply (rule cring_fieldI, simp add: Units_def)
using *
using group_l_invI notzero set_diff_eq by auto
qed

subsection ‹Morphisms›

definition
ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
where "ring_hom R S =
{h. h ∈ carrier R → carrier S ∧
(∀x y. x ∈ carrier R ∧ y ∈ carrier R ⟶
h (x ⊗⇘R⇙ y) = h x ⊗⇘S⇙ h y ∧ h (x ⊕⇘R⇙ y) = h x ⊕⇘S⇙ h y) ∧
h 𝟭⇘R⇙ = 𝟭⇘S⇙}"

lemma ring_hom_memI:
fixes R (structure) and S (structure)
assumes "⋀x. x ∈ carrier R ⟹ h x ∈ carrier S"
and "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ h (x ⊗ y) = h x ⊗⇘S⇙ h y"
and "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ h (x ⊕ y) = h x ⊕⇘S⇙ h y"
and "h 𝟭 = 𝟭⇘S⇙"
shows "h ∈ ring_hom R S"
by (auto simp add: ring_hom_def assms Pi_def)

lemma ring_hom_memE:
fixes R (structure) and S (structure)
assumes "h ∈ ring_hom R S"
shows "⋀x. x ∈ carrier R ⟹ h x ∈ carrier S"
and "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ h (x ⊗ y) = h x ⊗⇘S⇙ h y"
and "⋀x y. ⟦ x ∈ carrier R; y ∈ carrier R ⟧ ⟹ h (x ⊕ y) = h x ⊕⇘S⇙ h y"
and "h 𝟭 = 𝟭⇘S⇙"
using assms unfolding ring_hom_def by auto

lemma ring_hom_closed:
"⟦ h ∈ ring_hom R S; x ∈ carrier R ⟧ ⟹ h x ∈ carrier S"
by (auto simp add: ring_hom_def funcset_mem)

lemma ring_hom_mult:
fixes R (structure) and S (structure)
shows "⟦ h ∈ ring_hom R S; x ∈ carrier R; y ∈ carrier R ⟧ ⟹ h (x ⊗ y) = h x ⊗⇘S⇙ h y"

fixes R (structure) and S (structure)
shows "⟦ h ∈ ring_hom R S; x ∈ carrier R; y ∈ carrier R ⟧ ⟹ h (x ⊕ y) = h x ⊕⇘S⇙ h y"

lemma ring_hom_one:
fixes R (structure) and S (structure)
shows "h ∈ ring_hom R S ⟹ h 𝟭 = 𝟭⇘S⇙"

lemma ring_hom_zero:
fixes R (structure) and S (structure)
assumes "h ∈ ring_hom R S" "ring R" "ring S"
shows "h 𝟬 = 𝟬⇘S⇙"
proof -
have "h 𝟬 = h 𝟬 ⊕⇘S⇙ h 𝟬"
using ring_hom_add[OF assms(1), of 𝟬 𝟬] assms(2)
thus ?thesis
by (metis abelian_group.l_neg assms ring.is_abelian_group ring.ring_simprules(18) ring.ring_simprules(2) ring_hom_closed)
qed

locale ring_hom_cring =
R?: cring R + S?: cring S for R (structure) and S (structure) + fixes h
assumes homh [simp, intro]: "h ∈ ring_hom R S"
notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
and hom_mult [simp] = ring_hom_mult [OF homh]
and hom_one [simp] = ring_hom_one [OF homh]

lemma (in ring_hom_cring) hom_zero [simp]: "h 𝟬 = 𝟬⇘S⇙"
proof -
have "h 𝟬 ⊕⇘S⇙ h 𝟬 = h 𝟬 ⊕⇘S⇙ 𝟬⇘S⇙"
then show ?thesis by (simp del: S.r_zero)
qed

lemma (in ring_hom_cring) hom_a_inv [simp]:
"x ∈ carrier R ⟹ h (⊖ x) = ⊖⇘S⇙ h x"
proof -
assume R: "x ∈ carrier R"
then have "h x ⊕⇘S⇙ h (⊖ x) = h x ⊕⇘S⇙ (⊖⇘S⇙ h x)"
with R show ?thesis by simp
qed

lemma (in ring_hom_cring) hom_finsum [simp]:
assumes "f: A → carrier R"
shows "h (⨁ i ∈ A. f i) = (⨁⇘S⇙ i ∈ A. (h o f) i)"
using assms by (induct A rule: infinite_finite_induct, auto simp: Pi_def)

lemma (in ring_hom_cring) hom_finprod:
assumes "f: A → carrier R"
shows "h (⨂ i ∈ A. f i) = (⨂⇘S⇙ i ∈ A. (h o f) i)"
using assms by (induct A rule: infinite_finite_induct, auto simp: Pi_def)

declare ring_hom_cring.hom_finprod [simp]

lemma id_ring_hom [simp]: "id ∈ ring_hom R R"
by (auto intro!: ring_hom_memI)

lemma ring_hom_trans: ✐‹contributor ‹Paulo Emílio de Vilhena››
"⟦ f ∈ ring_hom R S; g ∈ ring_hom S T ⟧ ⟹ g ∘ f ∈ ring_hom R T"

(* need better simplification rules for rings *)
(* the next one holds more generally for abelian groups *)

lemma (in cring) sum_zero_eq_neg: "x ∈ carrier R ⟹ y ∈ carrier R ⟹ x ⊕ y = 𝟬 ⟹ x = ⊖ y"
by (metis minus_equality)

lemma (in domain) square_eq_one:
fixes x
assumes [simp]: "x ∈ carrier R"
and "x ⊗ x = 𝟭"
shows "x = 𝟭 ∨ x = ⊖𝟭"
proof -
have "(x ⊕ 𝟭) ⊗ (x ⊕ ⊖ 𝟭) = x ⊗ x ⊕ ⊖ 𝟭"
also from ‹x ⊗ x = 𝟭› have "… = 𝟬"
finally have "(x ⊕ 𝟭) ⊗ (x ⊕ ⊖ 𝟭) = 𝟬" .
then have "(x ⊕ 𝟭) = 𝟬 ∨ (x ⊕ ⊖ 𝟭) = 𝟬"
by (intro integral) auto
then show ?thesis
qed

lemma (in domain) inv_eq_self: "x ∈ Units R ⟹ x = inv x ⟹ x = 𝟭 ∨ x = ⊖𝟭"
by (metis Units_closed Units_l_inv square_eq_one)

text ‹
the units of a ring. (The list should be expanded as more things are
needed.)
›

lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) ⟹ finite (Units R)"
by (rule finite_subset) auto

lemma (in monoid) units_of_pow:
fixes n :: nat
shows "x ∈ Units G ⟹ x [^]⇘units_of G⇙ n = x [^]⇘G⇙ n"
apply (induct n)
apply (auto simp add: units_group group.is_monoid
monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
done

lemma (in cring) units_power_order_eq_one:
"finite (Units R) ⟹ a ∈ Units R ⟹ a [^] card(Units R) = 𝟭"
by (metis comm_group.power_order_eq_one units_comm_group units_of_carrier units_of_one units_of_pow)

lemma (in cring) field_intro2:
assumes "𝟬⇘R⇙ ≠ 𝟭⇘R⇙" and un: "⋀x. x ∈ carrier R - {𝟬⇘R⇙} ⟹ x ∈ Units R"
shows "field R"
proof unfold_locales
show "𝟭 ≠ 𝟬" using assms by auto
show "⟦a ⊗ b = 𝟬; a ∈ carrier R;
b ∈ carrier R⟧
⟹ a = 𝟬 ∨ b = 𝟬" for a b
by (metis un Units_l_cancel insert_Diff_single insert_iff r_null zero_closed)
qed (use assms in ‹auto simp: Units_def›)

lemma (in monoid) inv_char:
assumes "x ∈ carrier G" "y ∈ carrier G" "x ⊗ y = 𝟭" "y ⊗ x = 𝟭"
shows "inv x = y"
using assms inv_unique' by auto

lemma (in comm_monoid) comm_inv_char: "x ∈ carrier G ⟹ y ∈ carrier G ⟹ x ⊗ y = 𝟭 ⟹ inv x = y"

lemma (in ring) inv_neg_one [simp]: "inv (⊖ 𝟭) = ⊖ 𝟭"
by (simp add: inv_char local.ring_axioms ring.r_minus)

lemma (in monoid) inv_eq_imp_eq: "x ∈ Units G ⟹ y ∈ Units G ⟹ inv x = inv y ⟹ x = y"
by (metis Units_inv_inv)

lemma (in ring) Units_minus_one_closed [intro]: "⊖ 𝟭 ∈ Units R"