|
1 (* Title: HOL/GroupTheory/Ring |
|
2 ID: $Id$ |
|
3 Author: Florian Kammueller, with new proofs by L C Paulson |
|
4 Copyright 1998-2001 University of Cambridge |
|
5 |
|
6 Ring theory. Sigma version |
|
7 *) |
|
8 |
|
9 Goal |
|
10 "[| (| carrier = carrier R, bin_op = R .<f>, \ |
|
11 \ inverse = R .<inv>, unit = R .<e> |) \\<in> AbelianGroup;\ |
|
12 \ (R.<m>) \\<in> (carrier R) \\<rightarrow> (carrier R) \\<rightarrow> (carrier R); \ |
|
13 \ \\<forall>x \\<in> carrier R. \\<forall>y \\<in> carrier R. \\<forall>z \\<in> carrier R. (R.<m>) x ((R.<m>) y z) = (R.<m>) ((R.<m>) x y) z;\ |
|
14 \ distr_l (carrier R)(R.<m>)(R.<f>); distr_r (carrier R)(R.<m>)(R.<f>) |]\ |
|
15 \ ==> R \\<in> Ring"; |
|
16 by (afs [Ring_def] 1); |
|
17 qed "RingI"; |
|
18 |
|
19 Open_locale "ring"; |
|
20 |
|
21 val simp_R = simplify (simpset() addsimps [Ring_def]) (thm "Ring_R"); |
|
22 |
|
23 Addsimps [simp_R, thm "Ring_R", thm "rmult_def",thm "R_id_G"]; |
|
24 |
|
25 Goal "(| carrier = (carrier R), bin_op = (R.<f>), inverse = (R.<inv>), \ |
|
26 \ unit = (R.<e>) |) \\<in> AbelianGroup"; |
|
27 by (Asm_full_simp_tac 1); |
|
28 qed "R_Abel"; |
|
29 |
|
30 Goal "group_of R \\<in> AbelianGroup"; |
|
31 by (afs [group_of_def] 1); |
|
32 qed "R_forget"; |
|
33 |
|
34 Goal "((group_of R).<cr>) = (carrier R)"; |
|
35 by (afs [group_of_def] 1); |
|
36 qed "FR_carrier"; |
|
37 |
|
38 Goal "(G.<cr>) = (carrier R)"; |
|
39 by (simp_tac (simpset() addsimps [FR_carrier RS sym]) 1); |
|
40 qed "R_carrier_def"; |
|
41 |
|
42 Goal "((group_of R).<f>) = op ##"; |
|
43 by (afs [binop_def, thm "R_id_G"] 1); |
|
44 qed "FR_bin_op"; |
|
45 |
|
46 Goal "(R.<f>) = op ##"; |
|
47 by (afs [FR_bin_op RS sym, group_of_def] 1); |
|
48 qed "R_binop_def"; |
|
49 |
|
50 Goal "((group_of R).<inv>) = INV"; |
|
51 by (afs [thm "inv_def"] 1); |
|
52 qed "FR_inverse"; |
|
53 |
|
54 Goal "(R.<inv>) = INV"; |
|
55 by (afs [FR_inverse RS sym, group_of_def] 1); |
|
56 qed "R_inv_def"; |
|
57 |
|
58 Goal "((group_of R).<e>) = e"; |
|
59 by (afs [thm "e_def"] 1); |
|
60 qed "FR_unit"; |
|
61 |
|
62 Goal "(R.<e>) = e"; |
|
63 by (afs [FR_unit RS sym, group_of_def] 1); |
|
64 qed "R_unit_def"; |
|
65 |
|
66 Goal "G \\<in> AbelianGroup"; |
|
67 by (afs [group_of_def] 1); |
|
68 qed "G_abelian"; |
|
69 |
|
70 |
|
71 Delsimps [thm "R_id_G"]; (*needed below?*) |
|
72 |
|
73 Goal "[| x \\<in> (G.<cr>); y \\<in> (G.<cr>) |] ==> x ## y = y ## x"; |
|
74 by (afs [thm "binop_def", G_abelian RS Group_commute] 1); |
|
75 qed "binop_commute"; |
|
76 |
|
77 Goal "op ** \\<in> (carrier R) \\<rightarrow> (carrier R) \\<rightarrow> (carrier R)"; |
|
78 by (simp_tac (simpset() addsimps [thm "rmult_def"]) 1); |
|
79 qed "rmult_funcset"; |
|
80 |
|
81 Goal "[| x \\<in> (carrier R); y \\<in> (carrier R) |] ==> x ** y \\<in> (carrier R)"; |
|
82 by (blast_tac |
|
83 (claset() addIs [rmult_funcset RS funcset_mem RS funcset_mem]) 1); |
|
84 qed "rmult_closed"; |
|
85 |
|
86 Goal "[|x \\<in> (carrier R); y \\<in> (carrier R); z \\<in> (carrier R)|] \ |
|
87 \ ==> x **(y ** z) = (x ** y)** z"; |
|
88 by (Asm_full_simp_tac 1); |
|
89 qed "rmult_assoc"; |
|
90 |
|
91 Goal "[|x \\<in> (carrier R); y \\<in> (carrier R); z \\<in> (carrier R)|] \ |
|
92 \ ==> x **(y ## z) = (x ** y) ## (x ** z)"; |
|
93 by (cut_facts_tac [thm "Ring_R"] 1); |
|
94 by (asm_full_simp_tac (simpset() delsimps [thm "Ring_R", simp_R] |
|
95 addsimps [Ring_def, distr_l_def, R_binop_def]) 1); |
|
96 qed "R_distrib1"; |
|
97 |
|
98 |
|
99 (* The following have been in the earlier version without locales and the |
|
100 record extension proofs in which we needed to use conversion functions to |
|
101 establish these facts. We can transfer all facts that are |
|
102 derived for groups to rings now. The subsequent proofs are not really hard |
|
103 proofs, they are just instantiations of the known facts to rings. This is |
|
104 because the elements of the ring and the group are now identified!! Before, in |
|
105 the older version we could do something similar, but we always had to go the |
|
106 longer way, via the implication R \\<in> Ring ==> R \\<in> Abelian group and then |
|
107 conversion functions for the operators *) |
|
108 |
|
109 Goal "e \\<in> carrier R"; |
|
110 by (afs [R_carrier_def RS sym,e_closed] 1); |
|
111 qed "R_e_closed"; |
|
112 |
|
113 Goal "\\<forall>x \\<in> carrier R. e ## x = x"; |
|
114 by (afs [R_carrier_def RS sym,e_ax1] 1); |
|
115 qed "R_e_ax1"; |
|
116 |
|
117 Goal "op ## \\<in> carrier R \\<rightarrow> carrier R \\<rightarrow> carrier R"; |
|
118 by (afs [R_carrier_def RS sym, binop_funcset] 1); |
|
119 qed "rplus_funcset"; |
|
120 |
|
121 Goal "[| x \\<in> carrier R; y \\<in> carrier R |] ==> x ## y \\<in> carrier R"; |
|
122 by (afs [rplus_funcset RS funcset_mem RS funcset_mem] 1); |
|
123 qed "rplus_closed"; |
|
124 |
|
125 Goal "[| a \\<in> carrier R; a ## a = a |] ==> a = e"; |
|
126 by (afs [ R_carrier_def RS sym, idempotent_e] 1); |
|
127 qed "R_idempotent_e"; |
|
128 |
|
129 Delsimps [simp_R, thm "Ring_R", thm "rmult_def", thm "R_id_G"]; |
|
130 |
|
131 Goal "e ** e = e"; |
|
132 by (rtac R_idempotent_e 1); |
|
133 by (blast_tac (claset() addIs [rmult_closed, R_e_closed]) 1); |
|
134 by (simp_tac (simpset() addsimps [R_distrib1 RS sym, R_e_closed]) 1); |
|
135 qed "R_e_mult_base"; |
|
136 |
|
137 Close_locale "ring"; |
|
138 Close_locale "group"; |