src/HOL/Isar_examples/Group.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16417 9bc16273c2d4 child 31758 3edd5f813f01 permissions -rw-r--r--
Constant "If" is now local
1 (*  Title:      HOL/Isar_examples/Group.thy
2     ID:         $Id$
3     Author:     Markus Wenzel, TU Muenchen
4 *)
6 header {* Basic group theory *}
8 theory Group imports Main begin
10 subsection {* Groups and calculational reasoning *}
12 text {*
13  Groups over signature $({\times} :: \alpha \To \alpha \To \alpha, 14 \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined
15  as an axiomatic type class as follows.  Note that the parent class
16  $\idt{times}$ is provided by the basic HOL theory.
17 *}
19 consts
20   one :: "'a"
21   inverse :: "'a => 'a"
23 axclass
24   group < times
25   group_assoc:         "(x * y) * z = x * (y * z)"
26   group_left_one:      "one * x = x"
27   group_left_inverse:  "inverse x * x = one"
29 text {*
30  The group axioms only state the properties of left one and inverse,
31  the right versions may be derived as follows.
32 *}
34 theorem group_right_inverse: "x * inverse x = (one::'a::group)"
35 proof -
36   have "x * inverse x = one * (x * inverse x)"
37     by (simp only: group_left_one)
38   also have "... = one * x * inverse x"
39     by (simp only: group_assoc)
40   also have "... = inverse (inverse x) * inverse x * x * inverse x"
41     by (simp only: group_left_inverse)
42   also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
43     by (simp only: group_assoc)
44   also have "... = inverse (inverse x) * one * inverse x"
45     by (simp only: group_left_inverse)
46   also have "... = inverse (inverse x) * (one * inverse x)"
47     by (simp only: group_assoc)
48   also have "... = inverse (inverse x) * inverse x"
49     by (simp only: group_left_one)
50   also have "... = one"
51     by (simp only: group_left_inverse)
52   finally show ?thesis .
53 qed
55 text {*
56  With \name{group-right-inverse} already available,
57  \name{group-right-one}\label{thm:group-right-one} is now established
58  much easier.
59 *}
61 theorem group_right_one: "x * one = (x::'a::group)"
62 proof -
63   have "x * one = x * (inverse x * x)"
64     by (simp only: group_left_inverse)
65   also have "... = x * inverse x * x"
66     by (simp only: group_assoc)
67   also have "... = one * x"
68     by (simp only: group_right_inverse)
69   also have "... = x"
70     by (simp only: group_left_one)
71   finally show ?thesis .
72 qed
74 text {*
75  \medskip The calculational proof style above follows typical
76  presentations given in any introductory course on algebra.  The basic
77  technique is to form a transitive chain of equations, which in turn
78  are established by simplifying with appropriate rules.  The low-level
79  logical details of equational reasoning are left implicit.
81  Note that $\dots$'' is just a special term variable that is bound
82  automatically to the argument\footnote{The argument of a curried
83  infix expression happens to be its right-hand side.} of the last fact
84  achieved by any local assumption or proven statement.  In contrast to
85  $\var{thesis}$, the $\dots$'' variable is bound \emph{after} the
86  proof is finished, though.
88  There are only two separate Isar language elements for calculational
89  proofs: \isakeyword{also}'' for initial or intermediate
90  calculational steps, and \isakeyword{finally}'' for exhibiting the
91  result of a calculation.  These constructs are not hardwired into
92  Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
93  Expanding the \isakeyword{also} and \isakeyword{finally} derived
94  language elements, calculations may be simulated by hand as
95  demonstrated below.
96 *}
98 theorem "x * one = (x::'a::group)"
99 proof -
100   have "x * one = x * (inverse x * x)"
101     by (simp only: group_left_inverse)
103   note calculation = this
104     -- {* first calculational step: init calculation register *}
106   have "... = x * inverse x * x"
107     by (simp only: group_assoc)
109   note calculation = trans [OF calculation this]
110     -- {* general calculational step: compose with transitivity rule *}
112   have "... = one * x"
113     by (simp only: group_right_inverse)
115   note calculation = trans [OF calculation this]
116     -- {* general calculational step: compose with transitivity rule *}
118   have "... = x"
119     by (simp only: group_left_one)
121   note calculation = trans [OF calculation this]
122     -- {* final calculational step: compose with transitivity rule ... *}
123   from calculation
124     -- {* ... and pick up the final result *}
126   show ?thesis .
127 qed
129 text {*
130  Note that this scheme of calculations is not restricted to plain
131  transitivity.  Rules like anti-symmetry, or even forward and backward
132  substitution work as well.  For the actual implementation of
133  \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
134  separate context information of transitivity'' rules.  Rule
135  selection takes place automatically by higher-order unification.
136 *}
139 subsection {* Groups as monoids *}
141 text {*
142  Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha, 143 \idt{one} :: \alpha)$ are defined like this.
144 *}
146 axclass monoid < times
147   monoid_assoc:       "(x * y) * z = x * (y * z)"
148   monoid_left_one:   "one * x = x"
149   monoid_right_one:  "x * one = x"
151 text {*
152  Groups are \emph{not} yet monoids directly from the definition.  For
153  monoids, \name{right-one} had to be included as an axiom, but for
154  groups both \name{right-one} and \name{right-inverse} are derivable
155  from the other axioms.  With \name{group-right-one} derived as a
156  theorem of group theory (see page~\pageref{thm:group-right-one}), we
157  may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly
158  as follows.
159 *}
161 instance group < monoid
162   by (intro_classes,
163        rule group_assoc,
164        rule group_left_one,
165        rule group_right_one)
167 text {*
168  The \isacommand{instance} command actually is a version of
169  \isacommand{theorem}, setting up a goal that reflects the intended
170  class relation (or type constructor arity).  Thus any Isar proof
171  language element may be involved to establish this statement.  When
172  concluding the proof, the result is transformed into the intended
173  type signature extension behind the scenes.
174 *}
176 subsection {* More theorems of group theory *}
178 text {*
179  The one element is already uniquely determined by preserving an
180  \emph{arbitrary} group element.
181 *}
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
199 text {*
200  Likewise, the inverse is already determined by the cancel property.
201 *}
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
220 text {*
221  The inverse operation has some further characteristic properties.
222 *}
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
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
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
266 end