14883
|
1 |
(* Title: ZF/ex/Ring.thy
|
|
2 |
Id: $Id$
|
|
3 |
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Rings *}
|
|
7 |
|
16417
|
8 |
theory Ring imports Group begin
|
14883
|
9 |
|
|
10 |
(*First, we must simulate a record declaration:
|
|
11 |
record ring = monoid +
|
|
12 |
add :: "[i, i] => i" (infixl "\<oplus>\<index>" 65)
|
|
13 |
zero :: i ("\<zero>\<index>")
|
|
14 |
*)
|
|
15 |
|
|
16 |
constdefs
|
|
17 |
add_field :: "i => i"
|
|
18 |
"add_field(M) == fst(snd(snd(snd(M))))"
|
|
19 |
|
|
20 |
ring_add :: "[i, i, i] => i" (infixl "\<oplus>\<index>" 65)
|
|
21 |
"ring_add(M,x,y) == add_field(M) ` <x,y>"
|
|
22 |
|
|
23 |
zero :: "i => i" ("\<zero>\<index>")
|
|
24 |
"zero(M) == fst(snd(snd(snd(snd(M)))))"
|
|
25 |
|
|
26 |
|
|
27 |
lemma add_field_eq [simp]: "add_field(<C,M,I,A,z>) = A"
|
|
28 |
by (simp add: add_field_def)
|
|
29 |
|
|
30 |
lemma add_eq [simp]: "ring_add(<C,M,I,A,z>, x, y) = A ` <x,y>"
|
|
31 |
by (simp add: ring_add_def)
|
|
32 |
|
|
33 |
lemma zero_eq [simp]: "zero(<C,M,I,A,Z,z>) = Z"
|
|
34 |
by (simp add: zero_def)
|
|
35 |
|
|
36 |
|
|
37 |
text {* Derived operations. *}
|
|
38 |
|
|
39 |
constdefs (structure R)
|
|
40 |
a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80)
|
|
41 |
"a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
|
|
42 |
|
|
43 |
minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65)
|
|
44 |
"\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y == x \<oplus> (\<ominus> y)"
|
|
45 |
|
|
46 |
locale abelian_monoid = struct G +
|
|
47 |
assumes a_comm_monoid:
|
|
48 |
"comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
|
|
49 |
|
|
50 |
text {*
|
|
51 |
The following definition is redundant but simple to use.
|
|
52 |
*}
|
|
53 |
|
|
54 |
locale abelian_group = abelian_monoid +
|
|
55 |
assumes a_comm_group:
|
|
56 |
"comm_group (<carrier(G), add_field(G), zero(G), 0>)"
|
|
57 |
|
|
58 |
locale ring = abelian_group R + monoid R +
|
|
59 |
assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
|
|
60 |
\<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
|
|
61 |
and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
|
|
62 |
\<Longrightarrow> z \<cdot> (x \<oplus> y) = z \<cdot> x \<oplus> z \<cdot> y"
|
|
63 |
|
|
64 |
locale cring = ring + comm_monoid R
|
|
65 |
|
|
66 |
locale "domain" = cring +
|
|
67 |
assumes one_not_zero [simp]: "\<one> \<noteq> \<zero>"
|
|
68 |
and integral: "\<lbrakk>a \<cdot> b = \<zero>; a \<in> carrier(R); b \<in> carrier(R)\<rbrakk> \<Longrightarrow>
|
|
69 |
a = \<zero> | b = \<zero>"
|
|
70 |
|
|
71 |
|
|
72 |
subsection {* Basic Properties *}
|
|
73 |
|
|
74 |
lemma (in abelian_monoid) a_monoid:
|
|
75 |
"monoid (<carrier(G), add_field(G), zero(G), 0>)"
|
|
76 |
apply (insert a_comm_monoid)
|
|
77 |
apply (simp add: comm_monoid_def)
|
|
78 |
done
|
|
79 |
|
|
80 |
lemma (in abelian_group) a_group:
|
|
81 |
"group (<carrier(G), add_field(G), zero(G), 0>)"
|
|
82 |
apply (insert a_comm_group)
|
|
83 |
apply (simp add: comm_group_def group_def)
|
|
84 |
done
|
|
85 |
|
|
86 |
|
|
87 |
lemma (in abelian_monoid) l_zero [simp]:
|
|
88 |
"x \<in> carrier(G) \<Longrightarrow> \<zero> \<oplus> x = x"
|
|
89 |
apply (insert monoid.l_one [OF a_monoid])
|
|
90 |
apply (simp add: ring_add_def)
|
|
91 |
done
|
|
92 |
|
|
93 |
lemma (in abelian_monoid) zero_closed [intro, simp]:
|
|
94 |
"\<zero> \<in> carrier(G)"
|
|
95 |
by (rule monoid.one_closed [OF a_monoid, simplified])
|
|
96 |
|
|
97 |
lemma (in abelian_group) a_inv_closed [intro, simp]:
|
|
98 |
"x \<in> carrier(G) \<Longrightarrow> \<ominus> x \<in> carrier(G)"
|
|
99 |
by (simp add: a_inv_def group.inv_closed [OF a_group, simplified])
|
|
100 |
|
|
101 |
lemma (in abelian_monoid) a_closed [intro, simp]:
|
|
102 |
"[| x \<in> carrier(G); y \<in> carrier(G) |] ==> x \<oplus> y \<in> carrier(G)"
|
|
103 |
by (rule monoid.m_closed [OF a_monoid,
|
|
104 |
simplified, simplified ring_add_def [symmetric]])
|
|
105 |
|
|
106 |
lemma (in abelian_group) minus_closed [intro, simp]:
|
|
107 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<ominus> y \<in> carrier(G)"
|
|
108 |
by (simp add: minus_def)
|
|
109 |
|
|
110 |
lemma (in abelian_group) a_l_cancel [simp]:
|
|
111 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
|
|
112 |
\<Longrightarrow> (x \<oplus> y = x \<oplus> z) <-> (y = z)"
|
|
113 |
by (rule group.l_cancel [OF a_group,
|
|
114 |
simplified, simplified ring_add_def [symmetric]])
|
|
115 |
|
|
116 |
lemma (in abelian_group) a_r_cancel [simp]:
|
|
117 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
|
|
118 |
\<Longrightarrow> (y \<oplus> x = z \<oplus> x) <-> (y = z)"
|
|
119 |
by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
|
|
120 |
|
|
121 |
lemma (in abelian_monoid) a_assoc:
|
|
122 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
|
|
123 |
\<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
|
|
124 |
by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])
|
|
125 |
|
|
126 |
lemma (in abelian_group) l_neg:
|
|
127 |
"x \<in> carrier(G) \<Longrightarrow> \<ominus> x \<oplus> x = \<zero>"
|
|
128 |
by (simp add: a_inv_def
|
|
129 |
group.l_inv [OF a_group, simplified, simplified ring_add_def [symmetric]])
|
|
130 |
|
|
131 |
lemma (in abelian_monoid) a_comm:
|
|
132 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
|
|
133 |
by (rule comm_monoid.m_comm [OF a_comm_monoid,
|
|
134 |
simplified, simplified ring_add_def [symmetric]])
|
|
135 |
|
|
136 |
lemma (in abelian_monoid) a_lcomm:
|
|
137 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
|
|
138 |
\<Longrightarrow> x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
|
|
139 |
by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
|
|
140 |
simplified, simplified ring_add_def [symmetric]])
|
|
141 |
|
|
142 |
lemma (in abelian_monoid) r_zero [simp]:
|
|
143 |
"x \<in> carrier(G) \<Longrightarrow> x \<oplus> \<zero> = x"
|
|
144 |
using monoid.r_one [OF a_monoid]
|
|
145 |
by (simp add: ring_add_def [symmetric])
|
|
146 |
|
|
147 |
lemma (in abelian_group) r_neg:
|
|
148 |
"x \<in> carrier(G) \<Longrightarrow> x \<oplus> (\<ominus> x) = \<zero>"
|
|
149 |
using group.r_inv [OF a_group]
|
|
150 |
by (simp add: a_inv_def ring_add_def [symmetric])
|
|
151 |
|
|
152 |
lemma (in abelian_group) minus_zero [simp]:
|
|
153 |
"\<ominus> \<zero> = \<zero>"
|
|
154 |
by (simp add: a_inv_def
|
|
155 |
group.inv_one [OF a_group, simplified ])
|
|
156 |
|
|
157 |
lemma (in abelian_group) minus_minus [simp]:
|
|
158 |
"x \<in> carrier(G) \<Longrightarrow> \<ominus> (\<ominus> x) = x"
|
|
159 |
using group.inv_inv [OF a_group, simplified]
|
|
160 |
by (simp add: a_inv_def)
|
|
161 |
|
|
162 |
lemma (in abelian_group) minus_add:
|
|
163 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
|
|
164 |
using comm_group.inv_mult [OF a_comm_group]
|
|
165 |
by (simp add: a_inv_def ring_add_def [symmetric])
|
|
166 |
|
|
167 |
lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
|
|
168 |
|
|
169 |
text {*
|
|
170 |
The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
|
|
171 |
*}
|
|
172 |
|
|
173 |
lemma (in ring) l_null [simp]:
|
|
174 |
"x \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>"
|
|
175 |
proof -
|
|
176 |
assume R: "x \<in> carrier(R)"
|
|
177 |
then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x"
|
|
178 |
by (blast intro: l_distr [THEN sym])
|
|
179 |
also from R have "... = \<zero> \<cdot> x \<oplus> \<zero>" by simp
|
|
180 |
finally have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = \<zero> \<cdot> x \<oplus> \<zero>" .
|
|
181 |
with R show ?thesis by (simp del: r_zero)
|
|
182 |
qed
|
|
183 |
|
|
184 |
lemma (in ring) r_null [simp]:
|
|
185 |
"x \<in> carrier(R) \<Longrightarrow> x \<cdot> \<zero> = \<zero>"
|
|
186 |
proof -
|
|
187 |
assume R: "x \<in> carrier(R)"
|
|
188 |
then have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> (\<zero> \<oplus> \<zero>)"
|
|
189 |
by (simp add: r_distr del: l_zero r_zero)
|
|
190 |
also from R have "... = x \<cdot> \<zero> \<oplus> \<zero>" by simp
|
|
191 |
finally have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> \<zero> \<oplus> \<zero>" .
|
|
192 |
with R show ?thesis by (simp del: r_zero)
|
|
193 |
qed
|
|
194 |
|
|
195 |
lemma (in ring) l_minus:
|
|
196 |
"\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> \<ominus> x \<cdot> y = \<ominus> (x \<cdot> y)"
|
|
197 |
proof -
|
|
198 |
assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
|
|
199 |
then have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = (\<ominus> x \<oplus> x) \<cdot> y" by (simp add: l_distr)
|
|
200 |
also from R have "... = \<zero>" by (simp add: l_neg l_null)
|
|
201 |
finally have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = \<zero>" .
|
|
202 |
with R have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
|
|
203 |
with R show ?thesis by (simp add: a_assoc r_neg)
|
|
204 |
qed
|
|
205 |
|
|
206 |
lemma (in ring) r_minus:
|
|
207 |
"\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<cdot> \<ominus> y = \<ominus> (x \<cdot> y)"
|
|
208 |
proof -
|
|
209 |
assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
|
|
210 |
then have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = x \<cdot> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
|
|
211 |
also from R have "... = \<zero>" by (simp add: l_neg r_null)
|
|
212 |
finally have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = \<zero>" .
|
|
213 |
with R have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
|
|
214 |
with R show ?thesis by (simp add: a_assoc r_neg)
|
|
215 |
qed
|
|
216 |
|
|
217 |
lemma (in ring) minus_eq:
|
|
218 |
"\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y = x \<oplus> \<ominus> y"
|
|
219 |
by (simp only: minus_def)
|
|
220 |
|
|
221 |
|
|
222 |
subsection {* Morphisms *}
|
|
223 |
|
|
224 |
constdefs
|
|
225 |
ring_hom :: "[i,i] => i"
|
|
226 |
"ring_hom(R,S) ==
|
|
227 |
{h \<in> carrier(R) -> carrier(S).
|
|
228 |
(\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) -->
|
|
229 |
h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) &
|
|
230 |
h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)) &
|
|
231 |
h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
|
|
232 |
|
|
233 |
lemma ring_hom_memI:
|
|
234 |
assumes hom_type: "h \<in> carrier(R) \<rightarrow> carrier(S)"
|
|
235 |
and hom_mult: "\<And>x y. \<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow>
|
|
236 |
h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
|
|
237 |
and hom_add: "\<And>x y. \<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow>
|
|
238 |
h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
|
|
239 |
and hom_one: "h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
|
|
240 |
shows "h \<in> ring_hom(R,S)"
|
|
241 |
by (auto simp add: ring_hom_def prems)
|
|
242 |
|
|
243 |
lemma ring_hom_closed:
|
|
244 |
"\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(S)"
|
|
245 |
by (auto simp add: ring_hom_def)
|
|
246 |
|
|
247 |
lemma ring_hom_mult:
|
|
248 |
"\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
|
|
249 |
\<Longrightarrow> h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
|
|
250 |
by (simp add: ring_hom_def)
|
|
251 |
|
|
252 |
lemma ring_hom_add:
|
|
253 |
"\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
|
|
254 |
\<Longrightarrow> h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
|
|
255 |
by (simp add: ring_hom_def)
|
|
256 |
|
|
257 |
lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
|
|
258 |
by (simp add: ring_hom_def)
|
|
259 |
|
|
260 |
locale ring_hom_cring = cring R + cring S + var h +
|
|
261 |
assumes homh [simp, intro]: "h \<in> ring_hom(R,S)"
|
|
262 |
notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
|
|
263 |
and hom_mult [simp] = ring_hom_mult [OF homh]
|
|
264 |
and hom_add [simp] = ring_hom_add [OF homh]
|
|
265 |
and hom_one [simp] = ring_hom_one [OF homh]
|
|
266 |
|
|
267 |
lemma (in ring_hom_cring) hom_zero [simp]:
|
|
268 |
"h ` \<zero>\<^bsub>R\<^esub> = \<zero>\<^bsub>S\<^esub>"
|
|
269 |
proof -
|
|
270 |
have "h ` \<zero>\<^bsub>R\<^esub> \<oplus>\<^bsub>S\<^esub> h ` \<zero> = h ` \<zero>\<^bsub>R\<^esub> \<oplus>\<^bsub>S\<^esub> \<zero>\<^bsub>S\<^esub>"
|
|
271 |
by (simp add: hom_add [symmetric] del: hom_add)
|
|
272 |
then show ?thesis by (simp del: S.r_zero)
|
|
273 |
qed
|
|
274 |
|
|
275 |
lemma (in ring_hom_cring) hom_a_inv [simp]:
|
|
276 |
"x \<in> carrier(R) \<Longrightarrow> h ` (\<ominus>\<^bsub>R\<^esub> x) = \<ominus>\<^bsub>S\<^esub> h ` x"
|
|
277 |
proof -
|
|
278 |
assume R: "x \<in> carrier(R)"
|
|
279 |
then have "h ` x \<oplus>\<^bsub>S\<^esub> h ` (\<ominus> x) = h ` x \<oplus>\<^bsub>S\<^esub> (\<ominus>\<^bsub>S\<^esub> (h ` x))"
|
|
280 |
by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
|
|
281 |
with R show ?thesis by simp
|
|
282 |
qed
|
|
283 |
|
|
284 |
lemma (in ring) id_ring_hom [simp]: "id(carrier(R)) \<in> ring_hom(R,R)"
|
|
285 |
apply (rule ring_hom_memI)
|
|
286 |
apply (auto simp add: id_type)
|
|
287 |
done
|
|
288 |
|
|
289 |
end
|
|
290 |
|