Theory Ring

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

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)

text ‹Derived operations.›

definition
  a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("⊖ı _" [81] 80)
  where "a_inv R = m_inv ⦇carrier = carrier R, mult = add R, one = zero R⦈"

definition
  a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "⊖ı" 65)
  where "[| x ∈ carrier R; y ∈ carrier R |] ==> x ⊖R y = x ⊕R (⊖R y)"

locale abelian_monoid =
  fixes G (structure)
  assumes a_comm_monoid:
     "comm_monoid ⦇carrier = carrier G, mult = add G, one = zero G⦈"

definition
  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
  "finsum G = finprod ⦇carrier = carrier G, mult = add G, one = zero G⦈"

syntax
  "_finsum" :: "index => idt => 'a set => 'b => 'b"
      ("(3⨁__∈_. _)" [1000, 0, 51, 10] 10)
translations
  "⨁Gi∈A. b"  "CONST finsum G (%i. b) A"
   ‹Beware of argument permutation!›


locale abelian_group = abelian_monoid +
  assumes a_comm_group:
     "comm_group ⦇carrier = carrier G, mult = add G, one = zero G⦈"


subsection ‹Basic Properties›

lemma abelian_monoidI:
  fixes R (structure)
  assumes a_closed:
      "!!x y. [| x ∈ carrier R; y ∈ carrier R |] ==> x ⊕ y ∈ carrier R"
    and zero_closed: "𝟬 ∈ carrier R"
    and a_assoc:
      "!!x y z. [| x ∈ carrier R; y ∈ carrier R; z ∈ carrier R |] ==>
      (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
    and l_zero: "!!x. x ∈ carrier R ==> 𝟬 ⊕ x = x"
    and a_comm:
      "!!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_groupI:
  fixes R (structure)
  assumes a_closed:
      "!!x y. [| x ∈ carrier R; y ∈ carrier R |] ==> x ⊕ y ∈ carrier R"
    and zero_closed: "zero R ∈ carrier R"
    and a_assoc:
      "!!x y z. [| x ∈ carrier R; y ∈ carrier R; z ∈ carrier R |] ==>
      (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
    and a_comm:
      "!!x y. [| x ∈ carrier R; y ∈ carrier R |] ==> x ⊕ y = y ⊕ x"
    and l_zero: "!!x. x ∈ carrier R ==> 𝟬 ⊕ x = x"
    and l_inv_ex: "!!x. x ∈ carrier R ==> EX 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 (in abelian_monoid) a_monoid:
  "monoid ⦇carrier = carrier G, mult = add G, one = zero G⦈"
by (rule comm_monoid.axioms, rule a_comm_monoid) 

lemma (in abelian_group) a_group:
  "group ⦇carrier = carrier G, mult = add G, one = zero G⦈"
  by (simp add: group_def a_monoid)
    (simp add: comm_group.axioms group.axioms a_comm_group)

lemmas monoid_record_simps = partial_object.simps monoid.simps

text ‹Transfer facts from multiplicative structures via interpretation.›

sublocale abelian_monoid <
  add: monoid "⦇carrier = carrier G, mult = add G, one = zero G⦈"
  rewrites "carrier ⦇carrier = carrier G, mult = add G, one = zero G⦈ = carrier G"
    and "mult ⦇carrier = carrier G, mult = add G, one = zero G⦈ = add G"
    and "one ⦇carrier = carrier G, mult = add G, one = zero G⦈ = zero G"
  by (rule a_monoid) auto

context abelian_monoid begin

lemmas a_closed = add.m_closed 
lemmas zero_closed = add.one_closed
lemmas a_assoc = add.m_assoc
lemmas l_zero = add.l_one
lemmas r_zero = add.r_one
lemmas minus_unique = add.inv_unique

end

sublocale abelian_monoid <
  add: comm_monoid "⦇carrier = carrier G, mult = add G, one = zero G⦈"
  rewrites "carrier ⦇carrier = carrier G, mult = add G, one = zero G⦈ = carrier G"
    and "mult ⦇carrier = carrier G, mult = add G, one = zero G⦈ = add G"
    and "one ⦇carrier = carrier G, mult = add G, one = zero G⦈ = zero G"
    and "finprod ⦇carrier = carrier G, mult = add G, one = zero G⦈ = finsum G"
  by (rule a_comm_monoid) (auto simp: finsum_def)

context abelian_monoid begin

lemmas a_comm = add.m_comm
lemmas a_lcomm = add.m_lcomm
lemmas a_ac = a_assoc a_comm a_lcomm

lemmas finsum_empty = add.finprod_empty
lemmas finsum_insert = add.finprod_insert
lemmas finsum_zero = add.finprod_one
lemmas finsum_closed = add.finprod_closed
lemmas finsum_Un_Int = add.finprod_Un_Int
lemmas finsum_Un_disjoint = add.finprod_Un_disjoint
lemmas finsum_addf = add.finprod_multf
lemmas finsum_cong' = add.finprod_cong'
lemmas finsum_0 = add.finprod_0
lemmas finsum_Suc = add.finprod_Suc
lemmas finsum_Suc2 = add.finprod_Suc2
lemmas finsum_add = add.finprod_mult
lemmas finsum_infinite = add.finprod_infinite

lemmas finsum_cong = add.finprod_cong
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.›

lemmas finsum_reindex = add.finprod_reindex

(* 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 (force simp add: Pi_def)
  apply (subst m_comm)
  apply auto
done
*)

lemmas finsum_singleton = add.finprod_singleton

end

sublocale abelian_group <
  add: group "⦇carrier = carrier G, mult = add G, one = zero G⦈"
  rewrites "carrier ⦇carrier = carrier G, mult = add G, one = zero G⦈ = carrier G"
    and "mult ⦇carrier = carrier G, mult = add G, one = zero G⦈ = add G"
    and "one ⦇carrier = carrier G, mult = add G, one = zero G⦈ = zero G"
    and "m_inv ⦇carrier = carrier G, mult = add G, one = zero G⦈ = a_inv G"
  by (rule a_group) (auto simp: m_inv_def a_inv_def)

context abelian_group
begin

lemmas a_inv_closed = add.inv_closed

lemma minus_closed [intro, simp]:
  "[| x ∈ carrier G; y ∈ carrier G |] ==> x ⊖ y ∈ carrier G"
  by (simp add: a_minus_def)

lemmas a_l_cancel = add.l_cancel
lemmas a_r_cancel = add.r_cancel
lemmas l_neg = add.l_inv [simp del]
lemmas r_neg = add.r_inv [simp del]
lemmas minus_zero = add.inv_one
lemmas minus_minus = add.inv_inv
lemmas a_inv_inj = add.inv_inj
lemmas minus_equality = add.inv_equality

end

sublocale abelian_group <
  add: comm_group "⦇carrier = carrier G, mult = add G, one = zero G⦈"
  rewrites "carrier ⦇carrier = carrier G, mult = add G, one = zero G⦈ = carrier G"
    and "mult ⦇carrier = carrier G, mult = add G, one = zero G⦈ = add G"
    and "one ⦇carrier = carrier G, mult = add G, one = zero G⦈ = zero G"
    and "m_inv ⦇carrier = carrier G, mult = add G, one = zero G⦈ = a_inv G"
    and "finprod ⦇carrier = carrier G, mult = add G, one = zero G⦈ = finsum G"
  by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def)

lemmas (in abelian_group) minus_add = add.inv_mult
 
text ‹Derive an ‹abelian_group› from a ‹comm_group››

lemma comm_group_abelian_groupI:
  fixes G (structure)
  assumes cg: "comm_group ⦇carrier = carrier G, mult = add G, one = zero G⦈"
  shows "abelian_group G"
proof -
  interpret comm_group "⦇carrier = carrier G, mult = add G, one = zero G⦈"
    by (rule cg)
  show "abelian_group G" ..
qed


subsection ‹Rings: Basic Definitions›

locale semiring = abelian_monoid R + monoid 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 R + monoid 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 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: "abelian_group R"
    and monoid: "monoid R"
    and l_distr: "!!x y z. [| x ∈ carrier R; y ∈ carrier R; z ∈ carrier R |]
      ==> (x ⊕ y) ⊗ z = x ⊗ z ⊕ y ⊗ z"
    and r_distr: "!!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)

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

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 (in cring) is_comm_monoid:
  "comm_monoid R"
  by (auto intro!: comm_monoidI m_assoc m_comm)
*)

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


subsubsection ‹Normaliser for Rings›

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
    by (simp add: a_ac)
qed

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

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 ∈ carrier G; y ∈ carrier G |] ==> x ⊖ y = x ⊕ ⊖ y"
  by (simp only: 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 = {𝟬}) = (𝟭 = 𝟬)"
  apply rule
   apply (erule one_zeroI)
  apply (erule one_zeroD)
  done

lemma carrier_one_not_zero: "(carrier R ≠ {𝟬}) = (𝟭 ≠ 𝟬)"
  by (simp add: carrier_one_zero)

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 |] ==>
   finsum R f A ⊗ a = finsum R (%i. f i ⊗ a) 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 ⊗ finsum R f A = finsum R (%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 r_distr)
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 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"
  apply (rule cring_fieldI, simp add: Units_def)
  apply (rule, clarsimp)
  apply (simp add: notzero)
proof (clarsimp)
  fix x
  assume xcarr: "x ∈ carrier R"
    and "x ≠ 𝟬"
  then have "∃y∈carrier R. x ⊗ y = 𝟭" by (rule invex)
  then obtain y where ycarr: "y ∈ carrier R" and xy: "x ⊗ y = 𝟭" by fast
  from xy xcarr ycarr have "y ⊗ x = 𝟭" by (simp add: m_comm)
  with ycarr and xy show "∃y∈carrier R. y ⊗ x = 𝟭 ∧ x ⊗ y = 𝟭" by fast
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 &
      (ALL 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 hom_closed: "!!x. x ∈ carrier R ==> h x ∈ carrier S"
    and hom_mult: "!!x y. [| x ∈ carrier R; y ∈ carrier R |] ==>
      h (x ⊗ y) = h x ⊗S h y"
    and hom_add: "!!x y. [| x ∈ carrier R; y ∈ carrier R |] ==>
      h (x ⊕ y) = h x ⊕S h y"
    and hom_one: "h 𝟭 = 𝟭S"
  shows "h ∈ ring_hom R S"
  by (auto simp add: ring_hom_def assms Pi_def)

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"
    by (simp add: ring_hom_def)

lemma ring_hom_add:
  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"
    by (simp add: ring_hom_def)

lemma ring_hom_one:
  fixes R (structure) and S (structure)
  shows "h ∈ ring_hom R S ==> h 𝟭 = 𝟭S"
  by (simp add: ring_hom_def)

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_add [simp] = ring_hom_add [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"
    by (simp add: hom_add [symmetric] del: hom_add)
  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)"
    by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
  with R show ?thesis by simp
qed

lemma (in ring_hom_cring) hom_finsum [simp]:
  "f ∈ A → carrier R ==>
  h (finsum R f A) = finsum S (h o f) A"
  by (induct A rule: infinite_finite_induct, auto simp: Pi_def)

lemma (in ring_hom_cring) hom_finprod:
  "f ∈ A → carrier R ==>
  h (finprod R f A) = finprod S (h o f) A"
  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)

end