# Theory Ring

Up to index of Isabelle/ZF/ex

theory Ring
imports Group
begin

    (* Title:  ZF/ex/Ring.thy
      Id:     $Id: Ring.thy,v 1.3 2005/09/05 14:47:28 wenzelm Exp $

    *)

    header {* Rings *}

    theory Ring imports Group begin

    (*First, we must simulate a record declaration:
    record ring = monoid +
      add :: "[i, i] => i" (infixl "⊕\<index>" 65)
      zero :: i ("\<zero>\<index>")
    *)

    constdefs
      add_field :: "i => i"
       "add_field(M) == fst(snd(snd(snd(M))))"

      ring_add :: "[i, i, i] => i" (infixl "⊕\<index>" 65)
       "ring_add(M,x,y) == add_field(M) ` <x,y>"

      zero :: "i => i" ("\<zero>\<index>")
       "zero(M) == fst(snd(snd(snd(snd(M)))))"

    lemma add_field_eq [simp]: "add_field(<C,M,I,A,z>) = A"
      by (simp add: add_field_def)

    lemma add_eq [simp]: "ring_add(<C,M,I,A,z>, x, y) = A ` <x,y>"
      by (simp add: ring_add_def)

    lemma zero_eq [simp]: "zero(<C,M,I,A,Z,z>) = Z"
      by (simp add: zero_def)

    text {* Derived operations. *}

    constdefs (structure R)
      a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80)
      "a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"

      minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65)
      "[|x ∈ carrier(R); y ∈ carrier(R)|] ==> x \<ominus> y == x ⊕ (\<ominus> y)"

    locale abelian_monoid = struct G +
      assumes a_comm_monoid:
        "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"

    text {*
      The following definition is redundant but simple to use.
    *}

    locale abelian_group = abelian_monoid +
      assumes a_comm_group:
        "comm_group (<carrier(G), add_field(G), zero(G), 0>)"

    locale ring = abelian_group R + monoid R +
      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"

    locale cring = ring + comm_monoid R

    locale "domain" = cring +
      assumes one_not_zero [simp]: "\<one> ≠ \<zero>"
        and integral: "[|a · b = \<zero>; a ∈ carrier(R); b ∈ carrier(R)|] ==>
                      a = \<zero> | b = \<zero>"

    subsection {* Basic Properties *}

    lemma (in abelian_monoid) a_monoid:
         "monoid (<carrier(G), add_field(G), zero(G), 0>)"
    apply (insert a_comm_monoid)
    apply (simp add: comm_monoid_def)
    done

    lemma (in abelian_group) a_group:
         "group (<carrier(G), add_field(G), zero(G), 0>)"
    apply (insert a_comm_group)
    apply (simp add: comm_group_def group_def)
    done

    lemma (in abelian_monoid) l_zero [simp]:
         "x ∈ carrier(G) ==> \<zero> ⊕ x = x"
    apply (insert monoid.l_one [OF a_monoid])
    apply (simp add: ring_add_def)
    done

    lemma (in abelian_monoid) zero_closed [intro, simp]:
         "\<zero> ∈ carrier(G)"
    by (rule monoid.one_closed [OF a_monoid, simplified])

    lemma (in abelian_group) a_inv_closed [intro, simp]:
         "x ∈ carrier(G) ==> \<ominus> x ∈ carrier(G)"
    by (simp add: a_inv_def  group.inv_closed [OF a_group, simplified])

    lemma (in abelian_monoid) a_closed [intro, simp]:
         "[| x ∈ carrier(G); y ∈ carrier(G) |] ==> x ⊕ y ∈ carrier(G)"
    by (rule monoid.m_closed [OF a_monoid,
                      simplified, simplified ring_add_def [symmetric]])

    lemma (in abelian_group) minus_closed [intro, simp]:
         "[|x ∈ carrier(G); y ∈ carrier(G)|] ==> x \<ominus> y ∈ carrier(G)"
    by (simp add: minus_def)

    lemma (in abelian_group) a_l_cancel [simp]:
         "[|x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G)|]
          ==> (x ⊕ y = x ⊕ z) <-> (y = z)"
    by (rule group.l_cancel [OF a_group,
                 simplified, simplified ring_add_def [symmetric]])

    lemma (in abelian_group) a_r_cancel [simp]:
         "[|x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G)|]
          ==> (y ⊕ x = z ⊕ x) <-> (y = z)"
    by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])

    lemma (in abelian_monoid) a_assoc:
      "[|x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G)|]
       ==> (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
    by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])

    lemma (in abelian_group) l_neg:
         "x ∈ carrier(G) ==> \<ominus> x ⊕ x = \<zero>"
    by (simp add: a_inv_def
         group.l_inv [OF a_group, simplified, simplified ring_add_def [symmetric]])

    lemma (in abelian_monoid) a_comm:
         "[|x ∈ carrier(G); y ∈ carrier(G)|] ==> x ⊕ y = y ⊕ x"
    by (rule comm_monoid.m_comm [OF a_comm_monoid,
        simplified, simplified ring_add_def [symmetric]])

    lemma (in abelian_monoid) a_lcomm:
         "[|x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G)|]
          ==> x ⊕ (y ⊕ z) = y ⊕ (x ⊕ z)"
    by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
        simplified, simplified ring_add_def [symmetric]])

    lemma (in abelian_monoid) r_zero [simp]:
         "x ∈ carrier(G) ==> x ⊕ \<zero> = x"
      using monoid.r_one [OF a_monoid]
      by (simp add: ring_add_def [symmetric])

    lemma (in abelian_group) r_neg:
         "x ∈ carrier(G) ==> x ⊕ (\<ominus> x) = \<zero>"
      using group.r_inv [OF a_group]
      by (simp add: a_inv_def ring_add_def [symmetric])

    lemma (in abelian_group) minus_zero [simp]:
         "\<ominus> \<zero> = \<zero>"
      by (simp add: a_inv_def
        group.inv_one [OF a_group, simplified ])

    lemma (in abelian_group) minus_minus [simp]:
         "x ∈ carrier(G) ==> \<ominus> (\<ominus> x) = x"
      using group.inv_inv [OF a_group, simplified]
      by (simp add: a_inv_def)

    lemma (in abelian_group) minus_add:
         "[|x ∈ carrier(G); y ∈ carrier(G)|] ==> \<ominus> (x ⊕ y) = \<ominus> x ⊕ \<ominus> y"
      using comm_group.inv_mult [OF a_comm_group]
      by (simp add: a_inv_def ring_add_def [symmetric])

    lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm

    text {*
      The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
    *}

    lemma (in ring) l_null [simp]:
      "x ∈ carrier(R) ==> \<zero> · x = \<zero>"
    proof -
      assume R: "x ∈ carrier(R)"
      then have "\<zero> · x ⊕ \<zero> · x = (\<zero> ⊕ \<zero>) · x"
        by (blast intro: l_distr [THEN sym])
      also from R have "... = \<zero> · x ⊕ \<zero>" by simp
      finally have "\<zero> · x ⊕ \<zero> · x = \<zero> · x ⊕ \<zero>" .
      with R show ?thesis by (simp del: r_zero)
    qed

    lemma (in ring) r_null [simp]:
      "x ∈ carrier(R) ==> x · \<zero> = \<zero>"
    proof -
      assume R: "x ∈ carrier(R)"
      then have "x · \<zero> ⊕ x · \<zero> = x · (\<zero> ⊕ \<zero>)"
        by (simp add: r_distr del: l_zero r_zero)
      also from R have "... = x · \<zero> ⊕ \<zero>" by simp
      finally have "x · \<zero> ⊕ x · \<zero> = x · \<zero> ⊕ \<zero>" .
      with R show ?thesis by (simp del: r_zero)
    qed

    lemma (in ring) l_minus:
      "[|x ∈ carrier(R); y ∈ carrier(R)|] ==> \<ominus> x · y = \<ominus> (x · y)"
    proof -
      assume R: "x ∈ carrier(R)" "y ∈ carrier(R)"
      then have "(\<ominus> x) · y ⊕ x · y = (\<ominus> x ⊕ x) · y" by (simp add: l_distr)
      also from R have "... = \<zero>" by (simp add: l_neg l_null)
      finally have "(\<ominus> x) · y ⊕ x · y = \<zero>" .
      with R have "(\<ominus> x) · y ⊕ x · y ⊕ \<ominus> (x · y) = \<zero> ⊕ \<ominus> (x · y)" by simp
      with R show ?thesis by (simp add: a_assoc r_neg)
    qed

    lemma (in ring) r_minus:
      "[|x ∈ carrier(R); y ∈ carrier(R)|] ==> x · \<ominus> y = \<ominus> (x · y)"
    proof -
      assume R: "x ∈ carrier(R)" "y ∈ carrier(R)"
      then have "x · (\<ominus> y) ⊕ x · y = x · (\<ominus> y ⊕ y)" by (simp add: r_distr)
      also from R have "... = \<zero>" by (simp add: l_neg r_null)
      finally have "x · (\<ominus> y) ⊕ x · y = \<zero>" .
      with R have "x · (\<ominus> y) ⊕ x · y ⊕ \<ominus> (x · y) = \<zero> ⊕ \<ominus> (x · y)" by simp
      with R show ?thesis by (simp add: a_assoc r_neg)
    qed

    lemma (in ring) minus_eq:
      "[|x ∈ carrier(R); y ∈ carrier(R)|] ==> x \<ominus> y = x ⊕ \<ominus> y"
      by (simp only: minus_def)

    subsection {* Morphisms *}

    constdefs
      ring_hom :: "[i,i] => i"
      "ring_hom(R,S) ==
        {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 ` \<one>R = \<one>S}"

    lemma ring_hom_memI:
      assumes hom_type: "h ∈ carrier(R) -> carrier(S)"
        and hom_mult: "!!x y. [|x ∈ carrier(R); y ∈ carrier(R)|] ==>
          h ` (x ·R y) = (h ` x) ·S (h ` y)"
        and hom_add: "!!x y. [|x ∈ carrier(R); y ∈ carrier(R)|] ==>
          h ` (x ⊕R y) = (h ` x) ⊕S (h ` y)"
        and hom_one: "h ` \<one>R = \<one>S"
      shows "h ∈ ring_hom(R,S)"
    by (auto simp add: ring_hom_def prems)

    lemma ring_hom_closed:
         "[|h ∈ ring_hom(R,S); x ∈ carrier(R)|] ==> h ` x ∈ carrier(S)"
    by (auto simp add: ring_hom_def)

    lemma ring_hom_mult:
         "[|h ∈ ring_hom(R,S); x ∈ carrier(R); y ∈ carrier(R)|]
          ==> h ` (x ·R y) = (h ` x) ·S (h ` y)"
    by (simp add: ring_hom_def)

    lemma ring_hom_add:
         "[|h ∈ ring_hom(R,S); x ∈ carrier(R); y ∈ carrier(R)|]
          ==> h ` (x ⊕R y) = (h ` x) ⊕S (h ` y)"
    by (simp add: ring_hom_def)

    lemma ring_hom_one: "h ∈ ring_hom(R,S) ==> h ` \<one>R = \<one>S"
    by (simp add: ring_hom_def)

    locale ring_hom_cring = cring R + cring S + var 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 ` \<zero>R = \<zero>S"
    proof -
      have "h ` \<zero>R ⊕S h ` \<zero> = h ` \<zero>R ⊕S \<zero>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 ` (\<ominus>R x) = \<ominus>S h ` x"
    proof -
      assume R: "x ∈ carrier(R)"
      then have "h ` x ⊕S h ` (\<ominus> x) = h ` x ⊕S (\<ominus>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) id_ring_hom [simp]: "id(carrier(R)) ∈ ring_hom(R,R)"
    apply (rule ring_hom_memI)
    apply (auto simp add: id_type)
    done

    end

lemma add_field_eq:

      add_field(⟨C, M, I, A, z⟩) = A

lemma add_eq:

      x ⊕⟨C, M, I, A, z⟩ y = A ` ⟨x, y⟩

lemma zero_eq:

      \<zero>⟨C, M, I, A, Z, z⟩ = Z

### Basic Properties

lemma a_monoid:

      abelian_monoid(G) ==> monoid(⟨carrier(G), add_field(G), \<zero>G, 0⟩)

lemma a_group:

      abelian_group(G) ==> group(⟨carrier(G), add_field(G), \<zero>G, 0⟩)

lemma l_zero:

      [| abelian_monoid(G); x ∈ carrier(G) |] ==> \<zero>G ⊕G x = x

lemma zero_closed:

      abelian_monoid(G) ==> \<zero>G ∈ carrier(G)

lemma a_inv_closed:

      [| abelian_group(G); x ∈ carrier(G) |] ==> \<ominus>G x ∈ carrier(G)

lemma a_closed:

      [| abelian_monoid(G); x ∈ carrier(G); y ∈ carrier(G) |] ==> x ⊕G y ∈ carrier(G)

lemma minus_closed:

      [| abelian_group(G); x ∈ carrier(G); y ∈ carrier(G) |]
      ==> x \<ominus>G y ∈ carrier(G)

lemma a_l_cancel:

      [| abelian_group(G); x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G) |]
      ==> x ⊕G y = x ⊕G z <-> y = z

lemma a_r_cancel:

      [| abelian_group(G); x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G) |]
      ==> y ⊕G x = z ⊕G x <-> y = z

lemma a_assoc:

      [| abelian_monoid(G); x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G) |]
      ==> x ⊕G y ⊕G z = x ⊕G (y ⊕G z)

lemma l_neg:

      [| abelian_group(G); x ∈ carrier(G) |] ==> \<ominus>G x ⊕G x = \<zero>G

lemma a_comm:

      [| abelian_monoid(G); x ∈ carrier(G); y ∈ carrier(G) |] ==> x ⊕G y = y ⊕G x

lemma a_lcomm:

      [| abelian_monoid(G); x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G) |]
      ==> x ⊕G (y ⊕G z) = y ⊕G (x ⊕G z)

lemma r_zero:

      [| abelian_monoid(G); x ∈ carrier(G) |] ==> x ⊕G \<zero>G = x

lemma r_neg:

      [| abelian_group(G); x ∈ carrier(G) |] ==> x ⊕G \<ominus>G x = \<zero>G

lemma minus_zero:

      abelian_group(G) ==> \<ominus>G \<zero>G = \<zero>G

lemma minus_minus:

      [| abelian_group(G); x ∈ carrier(G) |] ==> \<ominus>G (\<ominus>G x) = x

lemma minus_add:

      [| abelian_group(G); x ∈ carrier(G); y ∈ carrier(G) |]
      ==> \<ominus>G (x ⊕G y) = \<ominus>G x ⊕G \<ominus>G y

lemmas a_ac:

      [| abelian_monoid(G); x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G) |]
      ==> x ⊕G y ⊕G z = x ⊕G (y ⊕G z)

      [| abelian_monoid(G); x ∈ carrier(G); y ∈ carrier(G) |] ==> x ⊕G y = y ⊕G x

      [| abelian_monoid(G); x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G) |]
      ==> x ⊕G (y ⊕G z) = y ⊕G (x ⊕G z)

lemma l_null:

      [| ring(R); x ∈ carrier(R) |] ==> \<zero>R ·R x = \<zero>R

lemma r_null:

      [| ring(R); x ∈ carrier(R) |] ==> x ·R \<zero>R = \<zero>R

lemma l_minus:

      [| ring(R); x ∈ carrier(R); y ∈ carrier(R) |]
      ==> \<ominus>R x ·R y = \<ominus>R (x ·R y)

lemma r_minus:

      [| ring(R); x ∈ carrier(R); y ∈ carrier(R) |]
      ==> x ·R \<ominus>R y = \<ominus>R (x ·R y)

lemma minus_eq:

      [| ring(R); x ∈ carrier(R); y ∈ carrier(R) |]
      ==> x \<ominus>R y = x ⊕R \<ominus>R y

### Morphisms

lemma ring_hom_memI:

      [| h ∈ carrier(R) -> carrier(S);
         !!x y. [| x ∈ carrier(R); y ∈ carrier(R) |]
                ==> h ` (x ·R y) = h ` x ·S h ` y;
         !!x y. [| x ∈ carrier(R); y ∈ carrier(R) |]
                ==> h ` (x ⊕R y) = h ` x ⊕S h ` y;
         h ` \<one>R = \<one>S |]
      ==> h ∈ ring_hom(R, S)

lemma ring_hom_closed:

      [| h ∈ ring_hom(R, S); x ∈ carrier(R) |] ==> h ` x ∈ carrier(S)

lemma ring_hom_mult:

      [| h ∈ ring_hom(R, S); x ∈ carrier(R); y ∈ carrier(R) |]
      ==> h ` (x ·R y) = h ` x ·S h ` y

lemma ring_hom_add:

      [| h ∈ ring_hom(R, S); x ∈ carrier(R); y ∈ carrier(R) |]
      ==> h ` (x ⊕R y) = h ` x ⊕S h ` y

lemma ring_hom_one:

      h ∈ ring_hom(R, S) ==> h ` \<one>R = \<one>S

lemma hom_zero:

      ring_hom_cring(R, S, h) ==> h ` \<zero>R = \<zero>S

lemma hom_a_inv:

      [| ring_hom_cring(R, S, h); x ∈ carrier(R) |]
      ==> h ` (\<ominus>R x) = \<ominus>S h ` x

lemma id_ring_hom:

      ring(R) ==> id(carrier(R)) ∈ ring_hom(R, R)