9 |
9 |
10 subsection {* Groups and calculational reasoning *} |
10 subsection {* Groups and calculational reasoning *} |
11 |
11 |
12 text {* |
12 text {* |
13 Groups over signature $({\times} :: \alpha \To \alpha \To \alpha, |
13 Groups over signature $({\times} :: \alpha \To \alpha \To \alpha, |
14 \idt{one} :: \alpha, \idt{inv} :: \alpha \To \alpha)$ are defined as |
14 \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined |
15 an axiomatic type class as follows. Note that the parent class |
15 as an axiomatic type class as follows. Note that the parent class |
16 $\idt{times}$ is provided by the basic HOL theory. |
16 $\idt{times}$ is provided by the basic HOL theory. |
17 *} |
17 *} |
18 |
18 |
19 consts |
19 consts |
20 one :: "'a" |
20 one :: "'a" |
21 inv :: "'a => 'a" |
21 inverse :: "'a => 'a" |
22 |
22 |
23 axclass |
23 axclass |
24 group < times |
24 group < times |
25 group_assoc: "(x * y) * z = x * (y * z)" |
25 group_assoc: "(x * y) * z = x * (y * z)" |
26 group_left_unit: "one * x = x" |
26 group_left_one: "one * x = x" |
27 group_left_inverse: "inv x * x = one" |
27 group_left_inverse: "inverse x * x = one" |
28 |
28 |
29 text {* |
29 text {* |
30 The group axioms only state the properties of left unit and inverse, |
30 The group axioms only state the properties of left one and inverse, |
31 the right versions may be derived as follows. |
31 the right versions may be derived as follows. |
32 *} |
32 *} |
33 |
33 |
34 theorem group_right_inverse: "x * inv x = (one::'a::group)" |
34 theorem group_right_inverse: "x * inverse x = (one::'a::group)" |
35 proof - |
35 proof - |
36 have "x * inv x = one * (x * inv x)" |
36 have "x * inverse x = one * (x * inverse x)" |
37 by (simp only: group_left_unit) |
37 by (simp only: group_left_one) |
38 also have "... = one * x * inv x" |
38 also have "... = one * x * inverse x" |
39 by (simp only: group_assoc) |
39 by (simp only: group_assoc) |
40 also have "... = inv (inv x) * inv x * x * inv x" |
40 also have "... = inverse (inverse x) * inverse x * x * inverse x" |
41 by (simp only: group_left_inverse) |
41 by (simp only: group_left_inverse) |
42 also have "... = inv (inv x) * (inv x * x) * inv x" |
42 also have "... = inverse (inverse x) * (inverse x * x) * inverse x" |
43 by (simp only: group_assoc) |
43 by (simp only: group_assoc) |
44 also have "... = inv (inv x) * one * inv x" |
44 also have "... = inverse (inverse x) * one * inverse x" |
45 by (simp only: group_left_inverse) |
45 by (simp only: group_left_inverse) |
46 also have "... = inv (inv x) * (one * inv x)" |
46 also have "... = inverse (inverse x) * (one * inverse x)" |
47 by (simp only: group_assoc) |
47 by (simp only: group_assoc) |
48 also have "... = inv (inv x) * inv x" |
48 also have "... = inverse (inverse x) * inverse x" |
49 by (simp only: group_left_unit) |
49 by (simp only: group_left_one) |
50 also have "... = one" |
50 also have "... = one" |
51 by (simp only: group_left_inverse) |
51 by (simp only: group_left_inverse) |
52 finally show ?thesis . |
52 finally show ?thesis . |
53 qed |
53 qed |
54 |
54 |
55 text {* |
55 text {* |
56 With \name{group-right-inverse} already available, |
56 With \name{group-right-inverse} already available, |
57 \name{group-right-unit}\label{thm:group-right-unit} is now |
57 \name{group-right-one}\label{thm:group-right-one} is now established |
58 established much easier. |
58 much easier. |
59 *} |
59 *} |
60 |
60 |
61 theorem group_right_unit: "x * one = (x::'a::group)" |
61 theorem group_right_one: "x * one = (x::'a::group)" |
62 proof - |
62 proof - |
63 have "x * one = x * (inv x * x)" |
63 have "x * one = x * (inverse x * x)" |
64 by (simp only: group_left_inverse) |
64 by (simp only: group_left_inverse) |
65 also have "... = x * inv x * x" |
65 also have "... = x * inverse x * x" |
66 by (simp only: group_assoc) |
66 by (simp only: group_assoc) |
67 also have "... = one * x" |
67 also have "... = one * x" |
68 by (simp only: group_right_inverse) |
68 by (simp only: group_right_inverse) |
69 also have "... = x" |
69 also have "... = x" |
70 by (simp only: group_left_unit) |
70 by (simp only: group_left_one) |
71 finally show ?thesis . |
71 finally show ?thesis . |
72 qed |
72 qed |
73 |
73 |
74 text {* |
74 text {* |
75 \medskip The calculational proof style above follows typical |
75 \medskip The calculational proof style above follows typical |
143 \idt{one} :: \alpha)$ are defined like this. |
143 \idt{one} :: \alpha)$ are defined like this. |
144 *} |
144 *} |
145 |
145 |
146 axclass monoid < times |
146 axclass monoid < times |
147 monoid_assoc: "(x * y) * z = x * (y * z)" |
147 monoid_assoc: "(x * y) * z = x * (y * z)" |
148 monoid_left_unit: "one * x = x" |
148 monoid_left_one: "one * x = x" |
149 monoid_right_unit: "x * one = x" |
149 monoid_right_one: "x * one = x" |
150 |
150 |
151 text {* |
151 text {* |
152 Groups are \emph{not} yet monoids directly from the definition. For |
152 Groups are \emph{not} yet monoids directly from the definition. For |
153 monoids, \name{right-unit} had to be included as an axiom, but for |
153 monoids, \name{right-one} had to be included as an axiom, but for |
154 groups both \name{right-unit} and \name{right-inverse} are derivable |
154 groups both \name{right-one} and \name{right-inverse} are derivable |
155 from the other axioms. With \name{group-right-unit} derived as a |
155 from the other axioms. With \name{group-right-one} derived as a |
156 theorem of group theory (see page~\pageref{thm:group-right-unit}), we |
156 theorem of group theory (see page~\pageref{thm:group-right-one}), we |
157 may still instantiate $\idt{group} \subset \idt{monoid}$ properly as |
157 may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly |
158 follows. |
158 as follows. |
159 *} |
159 *} |
160 |
160 |
161 instance group < monoid |
161 instance group < monoid |
162 by (intro_classes, |
162 by (intro_classes, |
163 rule group_assoc, |
163 rule group_assoc, |
164 rule group_left_unit, |
164 rule group_left_one, |
165 rule group_right_unit) |
165 rule group_right_one) |
166 |
166 |
167 text {* |
167 text {* |
168 The \isacommand{instance} command actually is a version of |
168 The \isacommand{instance} command actually is a version of |
169 \isacommand{theorem}, setting up a goal that reflects the intended |
169 \isacommand{theorem}, setting up a goal that reflects the intended |
170 class relation (or type constructor arity). Thus any Isar proof |
170 class relation (or type constructor arity). Thus any Isar proof |
171 language element may be involved to establish this statement. When |
171 language element may be involved to establish this statement. When |
172 concluding the proof, the result is transformed into the intended |
172 concluding the proof, the result is transformed into the intended |
173 type signature extension behind the scenes. |
173 type signature extension behind the scenes. |
174 *} |
174 *} |
175 |
175 |
|
176 subsection {* More theorems of group theory *} |
|
177 |
|
178 text {* |
|
179 The one element is already uniquely determined by preserving an |
|
180 \emph{arbitrary} group element. |
|
181 *} |
|
182 |
|
183 theorem group_one_equality: "e * x = x ==> one = (e::'a::group)" |
|
184 proof - |
|
185 assume eq: "e * x = x" |
|
186 have "one = x * inverse x" |
|
187 by (simp only: group_right_inverse) |
|
188 also have "... = (e * x) * inverse x" |
|
189 by (simp only: eq) |
|
190 also have "... = e * (x * inverse x)" |
|
191 by (simp only: group_assoc) |
|
192 also have "... = e * one" |
|
193 by (simp only: group_right_inverse) |
|
194 also have "... = e" |
|
195 by (simp only: group_right_one) |
|
196 finally show ?thesis . |
|
197 qed |
|
198 |
|
199 text {* |
|
200 Likewise, the inverse is already determined by the cancel property. |
|
201 *} |
|
202 |
|
203 theorem group_inverse_equality: |
|
204 "x' * x = one ==> inverse x = (x'::'a::group)" |
|
205 proof - |
|
206 assume eq: "x' * x = one" |
|
207 have "inverse x = one * inverse x" |
|
208 by (simp only: group_left_one) |
|
209 also have "... = (x' * x) * inverse x" |
|
210 by (simp only: eq) |
|
211 also have "... = x' * (x * inverse x)" |
|
212 by (simp only: group_assoc) |
|
213 also have "... = x' * one" |
|
214 by (simp only: group_right_inverse) |
|
215 also have "... = x'" |
|
216 by (simp only: group_right_one) |
|
217 finally show ?thesis . |
|
218 qed |
|
219 |
|
220 text {* |
|
221 The inverse operation has some further characteristic properties. |
|
222 *} |
|
223 |
|
224 theorem group_inverse_times: |
|
225 "inverse (x * y) = inverse y * inverse (x::'a::group)" |
|
226 proof (rule group_inverse_equality) |
|
227 show "(inverse y * inverse x) * (x * y) = one" |
|
228 proof - |
|
229 have "(inverse y * inverse x) * (x * y) = |
|
230 (inverse y * (inverse x * x)) * y" |
|
231 by (simp only: group_assoc) |
|
232 also have "... = (inverse y * one) * y" |
|
233 by (simp only: group_left_inverse) |
|
234 also have "... = inverse y * y" |
|
235 by (simp only: group_right_one) |
|
236 also have "... = one" |
|
237 by (simp only: group_left_inverse) |
|
238 finally show ?thesis . |
|
239 qed |
|
240 qed |
|
241 |
|
242 theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)" |
|
243 proof (rule group_inverse_equality) |
|
244 show "x * inverse x = one" |
|
245 by (simp only: group_right_inverse) |
|
246 qed |
|
247 |
|
248 theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)" |
|
249 proof - |
|
250 assume eq: "inverse x = inverse y" |
|
251 have "x = x * one" |
|
252 by (simp only: group_right_one) |
|
253 also have "... = x * (inverse y * y)" |
|
254 by (simp only: group_left_inverse) |
|
255 also have "... = x * (inverse x * y)" |
|
256 by (simp only: eq) |
|
257 also have "... = (x * inverse x) * y" |
|
258 by (simp only: group_assoc) |
|
259 also have "... = one * y" |
|
260 by (simp only: group_right_inverse) |
|
261 also have "... = y" |
|
262 by (simp only: group_left_one) |
|
263 finally show ?thesis . |
|
264 qed |
|
265 |
176 end |
266 end |