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