src/HOL/Isar_Examples/Group.thy
 author hoelzl Tue Mar 26 12:20:58 2013 +0100 (2013-03-26) changeset 51526 155263089e7b parent 37671 fa53d267dab3 child 55656 eb07b0acbebc permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
1 (*  Title:      HOL/Isar_Examples/Group.thy
2     Author:     Markus Wenzel, TU Muenchen
3 *)
5 header {* Basic group theory *}
7 theory Group
8 imports Main
9 begin
11 subsection {* Groups and calculational reasoning *}
13 text {* Groups over signature $({\times} :: \alpha \To \alpha \To 14 \alpha, \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$
15   are defined as an axiomatic type class as follows.  Note that the
16   parent class $\idt{times}$ is provided by the basic HOL theory. *}
18 class group = times + one + inverse +
19   assumes group_assoc: "(x * y) * z = x * (y * z)"
20     and group_left_one: "1 * x = x"
21     and group_left_inverse: "inverse x * x = 1"
23 text {* The group axioms only state the properties of left one and
24   inverse, the right versions may be derived as follows. *}
26 theorem (in group) group_right_inverse: "x * inverse x = 1"
27 proof -
28   have "x * inverse x = 1 * (x * inverse x)"
29     by (simp only: group_left_one)
30   also have "... = 1 * x * inverse x"
31     by (simp only: group_assoc)
32   also have "... = inverse (inverse x) * inverse x * x * inverse x"
33     by (simp only: group_left_inverse)
34   also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
35     by (simp only: group_assoc)
36   also have "... = inverse (inverse x) * 1 * inverse x"
37     by (simp only: group_left_inverse)
38   also have "... = inverse (inverse x) * (1 * inverse x)"
39     by (simp only: group_assoc)
40   also have "... = inverse (inverse x) * inverse x"
41     by (simp only: group_left_one)
42   also have "... = 1"
43     by (simp only: group_left_inverse)
44   finally show ?thesis .
45 qed
47 text {* With \name{group-right-inverse} already available,
48   \name{group-right-one}\label{thm:group-right-one} is now established
49   much easier. *}
51 theorem (in group) group_right_one: "x * 1 = x"
52 proof -
53   have "x * 1 = x * (inverse x * x)"
54     by (simp only: group_left_inverse)
55   also have "... = x * inverse x * x"
56     by (simp only: group_assoc)
57   also have "... = 1 * x"
58     by (simp only: group_right_inverse)
59   also have "... = x"
60     by (simp only: group_left_one)
61   finally show ?thesis .
62 qed
64 text {* \medskip The calculational proof style above follows typical
65   presentations given in any introductory course on algebra.  The
66   basic technique is to form a transitive chain of equations, which in
67   turn are established by simplifying with appropriate rules.  The
68   low-level logical details of equational reasoning are left implicit.
70   Note that $\dots$'' is just a special term variable that is bound
71   automatically to the argument\footnote{The argument of a curried
72   infix expression happens to be its right-hand side.} of the last
73   fact achieved by any local assumption or proven statement.  In
74   contrast to $\var{thesis}$, the $\dots$'' variable is bound
75   \emph{after} the proof is finished, though.
77   There are only two separate Isar language elements for calculational
78   proofs: \isakeyword{also}'' for initial or intermediate
79   calculational steps, and \isakeyword{finally}'' for exhibiting the
80   result of a calculation.  These constructs are not hardwired into
81   Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
82   Expanding the \isakeyword{also} and \isakeyword{finally} derived
83   language elements, calculations may be simulated by hand as
84   demonstrated below.
85 *}
87 theorem (in group) "x * 1 = x"
88 proof -
89   have "x * 1 = x * (inverse x * x)"
90     by (simp only: group_left_inverse)
92   note calculation = this
93     -- {* first calculational step: init calculation register *}
95   have "... = x * inverse x * x"
96     by (simp only: group_assoc)
98   note calculation = trans [OF calculation this]
99     -- {* general calculational step: compose with transitivity rule *}
101   have "... = 1 * x"
102     by (simp only: group_right_inverse)
104   note calculation = trans [OF calculation this]
105     -- {* general calculational step: compose with transitivity rule *}
107   have "... = x"
108     by (simp only: group_left_one)
110   note calculation = trans [OF calculation this]
111     -- {* final calculational step: compose with transitivity rule ... *}
112   from calculation
113     -- {* ... and pick up the final result *}
115   show ?thesis .
116 qed
118 text {* Note that this scheme of calculations is not restricted to
119   plain transitivity.  Rules like anti-symmetry, or even forward and
120   backward substitution work as well.  For the actual implementation
121   of \isacommand{also} and \isacommand{finally}, Isabelle/Isar
122   maintains separate context information of transitivity'' rules.
123   Rule selection takes place automatically by higher-order
124   unification. *}
127 subsection {* Groups as monoids *}
129 text {* Monoids over signature $({\times} :: \alpha \To \alpha \To 130 \alpha, \idt{one} :: \alpha)$ are defined like this.
131 *}
133 class monoid = times + one +
134   assumes monoid_assoc: "(x * y) * z = x * (y * z)"
135     and monoid_left_one: "1 * x = x"
136     and monoid_right_one: "x * 1 = x"
138 text {* Groups are \emph{not} yet monoids directly from the
139   definition.  For monoids, \name{right-one} had to be included as an
140   axiom, but for groups both \name{right-one} and \name{right-inverse}
141   are derivable from the other axioms.  With \name{group-right-one}
142   derived as a theorem of group theory (see
143   page~\pageref{thm:group-right-one}), we may still instantiate
144   $\idt{group} \subseteq \idt{monoid}$ properly as follows. *}
146 instance group < monoid
147   by intro_classes
148     (rule group_assoc,
149       rule group_left_one,
150       rule group_right_one)
152 text {* The \isacommand{instance} command actually is a version of
153   \isacommand{theorem}, setting up a goal that reflects the intended
154   class relation (or type constructor arity).  Thus any Isar proof
155   language element may be involved to establish this statement.  When
156   concluding the proof, the result is transformed into the intended
157   type signature extension behind the scenes. *}
160 subsection {* More theorems of group theory *}
162 text {* The one element is already uniquely determined by preserving
163   an \emph{arbitrary} group element. *}
165 theorem (in group) group_one_equality:
166   assumes eq: "e * x = x"
167   shows "1 = e"
168 proof -
169   have "1 = x * inverse x"
170     by (simp only: group_right_inverse)
171   also have "... = (e * x) * inverse x"
172     by (simp only: eq)
173   also have "... = e * (x * inverse x)"
174     by (simp only: group_assoc)
175   also have "... = e * 1"
176     by (simp only: group_right_inverse)
177   also have "... = e"
178     by (simp only: group_right_one)
179   finally show ?thesis .
180 qed
182 text {* Likewise, the inverse is already determined by the cancel property. *}
184 theorem (in group) group_inverse_equality:
185   assumes eq: "x' * x = 1"
186   shows "inverse x = x'"
187 proof -
188   have "inverse x = 1 * inverse x"
189     by (simp only: group_left_one)
190   also have "... = (x' * x) * inverse x"
191     by (simp only: eq)
192   also have "... = x' * (x * inverse x)"
193     by (simp only: group_assoc)
194   also have "... = x' * 1"
195     by (simp only: group_right_inverse)
196   also have "... = x'"
197     by (simp only: group_right_one)
198   finally show ?thesis .
199 qed
201 text {* The inverse operation has some further characteristic properties. *}
203 theorem (in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x"
204 proof (rule group_inverse_equality)
205   show "(inverse y * inverse x) * (x * y) = 1"
206   proof -
207     have "(inverse y * inverse x) * (x * y) =
208         (inverse y * (inverse x * x)) * y"
209       by (simp only: group_assoc)
210     also have "... = (inverse y * 1) * y"
211       by (simp only: group_left_inverse)
212     also have "... = inverse y * y"
213       by (simp only: group_right_one)
214     also have "... = 1"
215       by (simp only: group_left_inverse)
216     finally show ?thesis .
217   qed
218 qed
220 theorem (in group) inverse_inverse: "inverse (inverse x) = x"
221 proof (rule group_inverse_equality)
222   show "x * inverse x = one"
223     by (simp only: group_right_inverse)
224 qed
226 theorem (in group) inverse_inject:
227   assumes eq: "inverse x = inverse y"
228   shows "x = y"
229 proof -
230   have "x = x * 1"
231     by (simp only: group_right_one)
232   also have "... = x * (inverse y * y)"
233     by (simp only: group_left_inverse)
234   also have "... = x * (inverse x * y)"
235     by (simp only: eq)
236   also have "... = (x * inverse x) * y"
237     by (simp only: group_assoc)
238   also have "... = 1 * y"
239     by (simp only: group_right_inverse)
240   also have "... = y"
241     by (simp only: group_left_one)
242   finally show ?thesis .
243 qed
245 end