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 finsum_cong = add.finprod_cong text\<open>Usually, if this rule causes a failed congruence proof error,
the reason is that the premise \<open>g \<in> B \<rightarrow> carrier G\<close> cannot be shown.
Adding @{thm [source] Pi_def} to the simpset is often useful.\<close>
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)
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 \<open>Rings\<close>
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 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 \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" shows"cring R" proof (intro cring.intro ring.intro) show"ring_axioms R" \<comment> \<open>Right-distributivity follows from left-distributivity and
commutativity.\<close> 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]) alsofrom R have"... = x \ z \ y \ z" by (simp add: l_distr) alsofrom R have"... = z \ x \ z \ y" by (simp add: comm_monoid.m_comm [OF comm_monoid.intro]) finallyshow"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 \<open>Normaliser for Rings\<close>
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" thenhave"(\ 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" thenhave"(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\<open>
The following proofs are from Jacobson, Basic Algebra I, pp.~88--89. \<close>
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" thenhave"\ \ x \ \ \ x = (\ \ \) \ x" by (simp del: l_zero r_zero) alsofrom R have"... = \ \ x \ \" by simp finallyhave"\ \ 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) alsofrom R have"... = x \ \ \ \" by simp finallyhave"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" thenhave"(\ x) \ y \ x \ y = (\ x \ x) \ y" by (simp add: l_distr) alsofrom R have"... = \" by (simp add: l_neg) finallyhave"(\ 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" thenhave"x \ (\ y) \ x \ y = x \ (\ y \ y)" by (simp add: r_distr) alsofrom R have"... = \" by (simp add: l_neg) finallyhave"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\<open>Setup algebra method:
compute distributive normal form inlocale contexts\<close>
ML_file \<open>ringsimp.ML\<close>
attribute_setup algebra = \<open>
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)) \<close> "theorems controlling algebra method"
method_setup algebra = \<open>
Scan.succeed (SIMPLE_METHOD' o Ringsimp.algebra_tac) \<close> "normalisation of algebraic structure"
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 thenshow"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\<open>Two examples for use of method algebra\<close>
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 \\<^bsub>S\<^esub> d = d \\<^bsub>S\<^esub> 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 \<open>Sums over Finite Sets\<close>
lemma (in semiring) finsum_ldistr: "\ finite A; a \ carrier R; f: A \ carrier R \ \
(\<Oplus> i \<in> A. (f i)) \<otimes> a = (\<Oplus> i \<in> A. ((f i) \<otimes> a))" proof (induct set: finite) case empty thenshow ?caseby simp next case (insert x F) thenshow ?caseby (simp add: Pi_def l_distr) qed
lemma (in semiring) finsum_rdistr: "\ finite A; a \ carrier R; f: A \ carrier R \ \
a \<otimes> (\<Oplus> i \<in> A. (f i)) = (\<Oplus> i \<in> A. (a \<otimes> (f i)))" proof (induct set: finite) case empty thenshow ?caseby simp next case (insert x F) thenshow ?caseby (simp add: Pi_def r_distr) qed
text\<open>A quick detour\<close>
lemma add_pow_int_ge: "(k :: int) \ 0 \ [ k ] \\<^bsub>R\<^esub> a = [ nat k ] \\<^bsub>R\<^esub> a" \<^marker>\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 ] \\<^bsub>R\<^esub> a = \\<^bsub>R\<^esub> ([ nat (- k) ] \\<^bsub>R\<^esub> a)" \<^marker>\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: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> 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 "{..] by simp alsohave" ... = (\ i \ {..< k}. (a \ b))" using finsum_ldistr[of "{.. b "\x. a"] assms by simp alsohave" ... = [k] \ (a \ b)" using add.finprod_const[of "a \ b" "{.. finallyshow ?thesis . qed
corollary (in semiring) add_pow_rdistr: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> 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 "{..] by simp alsohave" ... = (\ i \ {..< k}. (a \ b))" using finsum_rdistr[of "{.. a "\x. b"] assms by simp alsohave" ... = [k] \ (a \ b)" using add.finprod_const[of "a \ b" "{.. finallyshow ?thesis . qed
(* For integers, we need the uniqueness of the additive inverse *) lemma (in ring) add_pow_ldistr_int: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> 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: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> 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 \<open>Integral Domains\<close>
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 = \" thenshow"a = \ \ b = \" by (simp add: integral) next assume"a \ carrier R" "b \ carrier R" "a = \ \ b = \" thenshow"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 alsofrom R have"b \ (b \ c) = c" by algebra finallyshow"b = c" . next assume"b = c"thenshow"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 \<open>Fields\<close>
text\<open>Field would not need to be derived from domain, the properties fordomain follow from the assumptions of field\<close>
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 moreoverhave"\ \ Units R" by fast ultimatelyshow"\ \ \" 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 alsofrom aUnit acarr have"... = (inv a \ a) \ b" by simp alsofrom acarr bcarr aUnit[THEN Units_inv_closed] have"... = (inv a) \ (a \ b)" by algebra alsofrom ab and acarr bcarr aUnit have"... = (inv a) \ \" by simp alsofrom aUnit[THEN Units_inv_closed] have"... = \" by algebra finallyhave"b = \" . thenshow"a = \ \ b = \" by simp qed qed (rule field_Units)
text\<open>Another variant to show that something is a field\<close> 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\<open>x \<noteq> \<zero>\<close> 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 \<open>Morphisms\<close>
definition
ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set" where"ring_hom R S =
{h. h \<in> carrier R \<rightarrow> carrier S \<and>
(\<forall>x y. x \<in> carrier R \<and> y \<in> carrier R \<longrightarrow>
h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y \<and> h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) \<and>
h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
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 \\<^bsub>S\<^esub> h y" and"\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" and"h \ = \\<^bsub>S\<^esub>" 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 \\<^bsub>S\<^esub> h y" and"\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" and"h \ = \\<^bsub>S\<^esub>" 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 \\<^bsub>S\<^esub> 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 \\<^bsub>S\<^esub> 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 \ = \\<^bsub>S\<^esub>" 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 \ = \\<^bsub>S\<^esub>" proof - have"h \ = h \ \\<^bsub>S\<^esub> h \" using ring_hom_add[OF assms(1), of \<zero> \<zero>] 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 \ = \\<^bsub>S\<^esub>" proof - have"h \ \\<^bsub>S\<^esub> h \ = h \ \\<^bsub>S\<^esub> \\<^bsub>S\<^esub>" by (simp add: hom_add [symmetric] del: hom_add) thenshow ?thesis by (simp del: S.r_zero) qed
lemma (in ring_hom_cring) hom_a_inv [simp]: "x \ carrier R \ h (\ x) = \\<^bsub>S\<^esub> h x" proof - assume R: "x \ carrier R" thenhave"h x \\<^bsub>S\<^esub> h (\ x) = h x \\<^bsub>S\<^esub> (\\<^bsub>S\<^esub> 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) = (\\<^bsub>S\<^esub> 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) = (\\<^bsub>S\<^esub> 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: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> "\ 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)
(* 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 (indomain) 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) alsofrom\<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>" by (simp add: ring_simprules) finallyhave"(x \ \) \ (x \ \ \) = \" . thenhave"(x \ \) = \ \ (x \ \ \) = \" by (intro integral) auto thenshow ?thesis by (metis add.inv_closed add.inv_solve_right assms(1) l_zero one_closed zero_closed) qed
lemma (indomain) inv_eq_self: "x \ Units R \ x = inv x \ x = \ \ x = \\" by (metis Units_closed Units_l_inv square_eq_one)
text\<open>
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.) \<close>
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 [^]\<^bsub>units_of G\<^esub> n = x [^]\<^bsub>G\<^esub> 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)
lemma (in cring) field_intro2: assumes"\\<^bsub>R\<^esub> \ \\<^bsub>R\<^esub>" and un: "\x. x \ carrier R - {\\<^bsub>R\<^esub>} \ x \ Units R" shows"field R" proof unfold_locales show"\ \ \" using assms by auto show"\a \ b = \; a \ carrier R;
b \<in> carrier R\<rbrakk> \<Longrightarrow> a = \<zero> \<or> b = \<zero>" for a b by (metis un Units_l_cancel insert_Diff_single insert_iff r_null zero_closed) qed (use assms in\<open>auto simp: Units_def\<close>)
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 [dest!]: "inv x = inv y \ x \ Units G \ y \ Units G \ 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
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
