(* Title: ZF/ex/Ring.thy *) section ‹Rings› theory Ring imports Group begin no_notation cadd (infixl "⊕" 65) and cmult (infixl "⊗" 70) (*First, we must simulate a record declaration: record ring = monoid + add :: "[i, i] => i" (infixl "⊕ı" 65) zero :: i ("𝟬ı") *) definition add_field :: "i => i" where "add_field(M) = fst(snd(snd(snd(M))))" definition ring_add :: "[i, i, i] => i" (infixl "⊕ı" 65) where "ring_add(M,x,y) = add_field(M) ` <x,y>" definition zero :: "i => i" ("𝟬ı") where "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.› definition a_inv :: "[i,i] => i" ("⊖ı _" [81] 80) where "a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)" definition minus :: "[i,i,i] => i" (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(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 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" 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 = 𝟬" 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) ⟹ 𝟬 ⊕ 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]: "𝟬 ∈ carrier(G)" by (rule monoid.one_closed [OF a_monoid, simplified]) lemma (in abelian_group) a_inv_closed [intro, simp]: "x ∈ carrier(G) ⟹ ⊖ 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 ⊖ 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) ⟹ ⊖ x ⊕ x = 𝟬" 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 ⊕ 𝟬 = 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 ⊕ (⊖ x) = 𝟬" using group.r_inv [OF a_group] by (simp add: a_inv_def ring_add_def [symmetric]) lemma (in abelian_group) minus_zero [simp]: "⊖ 𝟬 = 𝟬" by (simp add: a_inv_def group.inv_one [OF a_group, simplified ]) lemma (in abelian_group) minus_minus [simp]: "x ∈ carrier(G) ⟹ ⊖ (⊖ 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)⟧ ⟹ ⊖ (x ⊕ y) = ⊖ x ⊕ ⊖ 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 › context ring begin lemma l_null [simp]: "x ∈ carrier(R) ⟹ 𝟬 ⋅ x = 𝟬" proof - assume R: "x ∈ carrier(R)" then have "𝟬 ⋅ x ⊕ 𝟬 ⋅ x = (𝟬 ⊕ 𝟬) ⋅ x" by (blast intro: l_distr [THEN sym]) also from R have "... = 𝟬 ⋅ x ⊕ 𝟬" by simp finally have "𝟬 ⋅ x ⊕ 𝟬 ⋅ x = 𝟬 ⋅ x ⊕ 𝟬" . with R show ?thesis by (simp del: r_zero) qed lemma r_null [simp]: "x ∈ carrier(R) ⟹ x ⋅ 𝟬 = 𝟬" proof - assume R: "x ∈ carrier(R)" then have "x ⋅ 𝟬 ⊕ x ⋅ 𝟬 = x ⋅ (𝟬 ⊕ 𝟬)" by (simp add: r_distr del: l_zero r_zero) also from R have "... = x ⋅ 𝟬 ⊕ 𝟬" by simp finally have "x ⋅ 𝟬 ⊕ x ⋅ 𝟬 = x ⋅ 𝟬 ⊕ 𝟬" . with R show ?thesis by (simp del: r_zero) 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 lemma minus_eq: "⟦x ∈ carrier(R); y ∈ carrier(R)⟧ ⟹ x ⊖ y = x ⊕ ⊖ y" by (simp only: minus_def) end subsection ‹Morphisms› definition ring_hom :: "[i,i] => i" where "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 ` 𝟭⇘_{R⇙}= 𝟭⇘_{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 ` 𝟭⇘_{R⇙}= 𝟭⇘_{S⇙}" shows "h ∈ ring_hom(R,S)" by (auto simp add: ring_hom_def assms) 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 ` 𝟭⇘_{R⇙}= 𝟭⇘_{S⇙}" by (simp add: ring_hom_def) locale ring_hom_cring = R: cring R + S: cring S for R (structure) and S (structure) and 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 ` 𝟬⇘_{R⇙}= 𝟬⇘_{S⇙}" proof - have "h ` 𝟬⇘_{R⇙}⊕⇘_{S⇙}h ` 𝟬 = h ` 𝟬⇘_{R⇙}⊕⇘_{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 ` (⊖⇘_{R⇙}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) id_ring_hom [simp]: "id(carrier(R)) ∈ ring_hom(R,R)" apply (rule ring_hom_memI) apply (auto simp add: id_type) done end