(* 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) where "add_pow R k a = pow (add_monoid R) a k" locale abelian_monoid = fixes G (structure) assumes a_comm_monoid: "comm_monoid (add_monoid G)" 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: "comm_group (add_monoid G)" 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: "monoid (add_monoid G)" by (rule comm_monoid.axioms, rule a_comm_monoid) lemma (in abelian_group) a_group: "group (add_monoid 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 "(add_monoid G)" rewrites "carrier (add_monoid G) = carrier G" and "mult (add_monoid G) = add G" and "one (add_monoid G) = zero G" and "(λa k. pow (add_monoid G) a k) = (λa k. add_pow G k a)" by (rule a_monoid) (auto simp add: add_pow_def) 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 "(add_monoid G)" rewrites "carrier (add_monoid G) = carrier G" and "mult (add_monoid G) = add G" and "one (add_monoid G) = zero G" and "finprod (add_monoid G) = finsum G" and "pow (add_monoid G) = (λa k. add_pow G k a)" by (rule a_comm_monoid) (auto simp: finsum_def add_pow_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_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 "(add_monoid G)" rewrites "carrier (add_monoid G) = carrier G" and "mult (add_monoid G) = add G" and "one (add_monoid G) = zero G" and "m_inv (add_monoid G) = a_inv G" and "pow (add_monoid G) = (λa k. add_pow G k a)" by (rule a_group) (auto simp: m_inv_def a_inv_def add_pow_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 l_neg = add.l_inv [simp del] lemmas r_neg = add.r_inv [simp del] 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 "(add_monoid G)" rewrites "carrier (add_monoid G) = carrier G" and "mult (add_monoid G) = add G" and "one (add_monoid G) = zero G" and "m_inv (add_monoid G) = a_inv G" and "finprod (add_monoid G) = finsum G" and "pow (add_monoid G) = (λa k. add_pow G k a)" by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def add_pow_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 (add_monoid G)" shows "abelian_group G" proof - interpret comm_group "(add_monoid G)" 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]: "⊖ 𝟬 = 𝟬" by (simp add: a_inv_def) 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 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 ⊖ 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 ≠ {𝟬}) = (𝟭 ≠ 𝟬)" 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 ⟧ ⟹ (⨁ 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›› by (simp add: add_pow_def int_pow_def nat_pow_def) lemma add_pow_int_lt: "(k :: int) < 0 ⟹ [ k ] ⋅⇘_{R⇙}a = ⊖⇘_{R⇙}([ nat (- k) ] ⋅⇘_{R⇙}a)" ✐‹contributor ‹Paulo EmÃlio de Vilhena›› by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def) 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 using add_pow_int_ge[of k R] add_pow_ldistr[OF assms] by auto next case False thus ?thesis using add_pow_int_lt[of k R a] add_pow_int_lt[of k R "a ⊗ b"] 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 using add_pow_int_ge[of k R] add_pow_rdistr[OF assms] by auto next case False thus ?thesis using add_pow_int_lt[of k R b] add_pow_int_lt[of k R "a ⊗ b"] 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" 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) 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) by (simp add: ring.ring_simprules(2) ring.ring_simprules(15)) 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_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]: 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" by (rule ring_hom_memI) (auto simp add: ring_hom_closed ring_hom_mult ring_hom_add ring_hom_one) subsection‹Jeremy Avigad's ‹More_Finite_Product› material› (* 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 ⊕ ⊖ 𝟭" by (simp add: ring_simprules) also from ‹x ⊗ x = 𝟭› have "… = 𝟬" by (simp add: ring_simprules) finally have "(x ⊕ 𝟭) ⊗ (x ⊕ ⊖ 𝟭) = 𝟬" . then have "(x ⊕ 𝟭) = 𝟬 ∨ (x ⊕ ⊖ 𝟭) = 𝟬" by (intro integral) auto then show ?thesis by (metis add.inv_closed add.inv_solve_right assms(1) l_zero one_closed zero_closed) 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 following translates theorems about groups to the facts about 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) subsection‹Jeremy Avigad's ‹More_Ring› material› 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" by (simp add: inv_char m_comm) 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" by (simp add: Units_def) (metis add.l_inv_ex local.minus_minus minus_equality one_closed r_minus r_one) lemma (in ring) inv_eq_neg_one_eq: "x ∈ Units R ⟹ inv x = ⊖ 𝟭 ⟷ x = ⊖ 𝟭" by (metis Units_inv_inv inv_neg_one) lemma (in monoid) inv_eq_one_eq: "x ∈ Units G ⟹ inv x = 𝟭 ⟷ x = 𝟭" by (metis Units_inv_inv inv_one) end