(* 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 (* ************************************************************************** *) (* Contributed by Paulo E. de Vilhena. *) text ‹A quick detour› lemma add_pow_int_ge: "(k :: int) ≥ 0 ⟹ [ k ] ⋅⇘_{R⇙}a = [ nat k ] ⋅⇘_{R⇙}a" 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)" by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def) corollary (in semiring) add_pow_ldistr: 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: 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: 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: 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 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) (* Next lemma contributed by Paulo EmÃlio de Vilhena. *) lemma ring_hom_trans: "⟦ 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 @{text"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 @{text"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