# Theory HOL-Algebra.Ring

```(*  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" ("βΔ± _" [81] 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)

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 [dest!]: "inv x = inv y βΉ x β Units G βΉ y β Units G βΉ x = y"
by (metis Units_inv_inv)

lemma (in ring) Units_minus_one_closed [intro]: "β π­ β Units R"