author | wenzelm |
Thu, 01 Jul 2010 18:31:46 +0200 | |
changeset 37671 | fa53d267dab3 |
parent 35317 | d57da4abb47d |
child 55656 | eb07b0acbebc |
permissions | -rw-r--r-- |
33026 | 1 |
(* Title: HOL/Isar_Examples/Group.thy |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
3 |
*) |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
4 |
|
10007 | 5 |
header {* Basic group theory *} |
7748 | 6 |
|
31758 | 7 |
theory Group |
8 |
imports Main |
|
9 |
begin |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
10 |
|
10007 | 11 |
subsection {* Groups and calculational reasoning *} |
6784 | 12 |
|
37671 | 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. *} |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
17 |
|
35317 | 18 |
class group = times + one + inverse + |
37671 | 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" |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
22 |
|
37671 | 23 |
text {* The group axioms only state the properties of left one and |
24 |
inverse, the right versions may be derived as follows. *} |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
25 |
|
37671 | 26 |
theorem (in group) group_right_inverse: "x * inverse x = 1" |
10007 | 27 |
proof - |
37671 | 28 |
have "x * inverse x = 1 * (x * inverse x)" |
10141 | 29 |
by (simp only: group_left_one) |
37671 | 30 |
also have "... = 1 * x * inverse x" |
10007 | 31 |
by (simp only: group_assoc) |
10141 | 32 |
also have "... = inverse (inverse x) * inverse x * x * inverse x" |
10007 | 33 |
by (simp only: group_left_inverse) |
10141 | 34 |
also have "... = inverse (inverse x) * (inverse x * x) * inverse x" |
10007 | 35 |
by (simp only: group_assoc) |
37671 | 36 |
also have "... = inverse (inverse x) * 1 * inverse x" |
10007 | 37 |
by (simp only: group_left_inverse) |
37671 | 38 |
also have "... = inverse (inverse x) * (1 * inverse x)" |
10007 | 39 |
by (simp only: group_assoc) |
10141 | 40 |
also have "... = inverse (inverse x) * inverse x" |
41 |
by (simp only: group_left_one) |
|
37671 | 42 |
also have "... = 1" |
10007 | 43 |
by (simp only: group_left_inverse) |
44 |
finally show ?thesis . |
|
45 |
qed |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
46 |
|
37671 | 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. *} |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
50 |
|
37671 | 51 |
theorem (in group) group_right_one: "x * 1 = x" |
10007 | 52 |
proof - |
37671 | 53 |
have "x * 1 = x * (inverse x * x)" |
10007 | 54 |
by (simp only: group_left_inverse) |
10141 | 55 |
also have "... = x * inverse x * x" |
10007 | 56 |
by (simp only: group_assoc) |
37671 | 57 |
also have "... = 1 * x" |
10007 | 58 |
by (simp only: group_right_inverse) |
59 |
also have "... = x" |
|
10141 | 60 |
by (simp only: group_left_one) |
10007 | 61 |
finally show ?thesis . |
62 |
qed |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
63 |
|
37671 | 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. |
|
6784 | 69 |
|
37671 | 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. |
|
7874 | 76 |
|
37671 | 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. |
|
10007 | 85 |
*} |
6784 | 86 |
|
37671 | 87 |
theorem (in group) "x * 1 = x" |
10007 | 88 |
proof - |
37671 | 89 |
have "x * 1 = x * (inverse x * x)" |
10007 | 90 |
by (simp only: group_left_inverse) |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
91 |
|
7433 | 92 |
note calculation = this |
10007 | 93 |
-- {* first calculational step: init calculation register *} |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
94 |
|
10141 | 95 |
have "... = x * inverse x * x" |
10007 | 96 |
by (simp only: group_assoc) |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
97 |
|
7433 | 98 |
note calculation = trans [OF calculation this] |
10007 | 99 |
-- {* general calculational step: compose with transitivity rule *} |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
100 |
|
37671 | 101 |
have "... = 1 * x" |
10007 | 102 |
by (simp only: group_right_inverse) |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
103 |
|
7433 | 104 |
note calculation = trans [OF calculation this] |
10007 | 105 |
-- {* general calculational step: compose with transitivity rule *} |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
106 |
|
10007 | 107 |
have "... = x" |
10141 | 108 |
by (simp only: group_left_one) |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
109 |
|
7433 | 110 |
note calculation = trans [OF calculation this] |
10007 | 111 |
-- {* final calculational step: compose with transitivity rule ... *} |
6784 | 112 |
from calculation |
10007 | 113 |
-- {* ... and pick up the final result *} |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
114 |
|
10007 | 115 |
show ?thesis . |
116 |
qed |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
117 |
|
37671 | 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. *} |
|
7874 | 125 |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
126 |
|
10007 | 127 |
subsection {* Groups as monoids *} |
6793 | 128 |
|
37671 | 129 |
text {* Monoids over signature $({\times} :: \alpha \To \alpha \To |
130 |
\alpha, \idt{one} :: \alpha)$ are defined like this. |
|
10007 | 131 |
*} |
6793 | 132 |
|
35317 | 133 |
class monoid = times + one + |
37671 | 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" |
|
6793 | 137 |
|
37671 | 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. *} |
|
6793 | 145 |
|
10007 | 146 |
instance group < monoid |
37671 | 147 |
by intro_classes |
148 |
(rule group_assoc, |
|
149 |
rule group_left_one, |
|
150 |
rule group_right_one) |
|
6793 | 151 |
|
37671 | 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. *} |
|
158 |
||
7874 | 159 |
|
10141 | 160 |
subsection {* More theorems of group theory *} |
161 |
||
37671 | 162 |
text {* The one element is already uniquely determined by preserving |
163 |
an \emph{arbitrary} group element. *} |
|
10141 | 164 |
|
37671 | 165 |
theorem (in group) group_one_equality: |
166 |
assumes eq: "e * x = x" |
|
167 |
shows "1 = e" |
|
10141 | 168 |
proof - |
37671 | 169 |
have "1 = x * inverse x" |
10141 | 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) |
|
37671 | 175 |
also have "... = e * 1" |
10141 | 176 |
by (simp only: group_right_inverse) |
177 |
also have "... = e" |
|
178 |
by (simp only: group_right_one) |
|
179 |
finally show ?thesis . |
|
180 |
qed |
|
181 |
||
37671 | 182 |
text {* Likewise, the inverse is already determined by the cancel property. *} |
10141 | 183 |
|
37671 | 184 |
theorem (in group) group_inverse_equality: |
185 |
assumes eq: "x' * x = 1" |
|
186 |
shows "inverse x = x'" |
|
10141 | 187 |
proof - |
37671 | 188 |
have "inverse x = 1 * inverse x" |
10141 | 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) |
|
37671 | 194 |
also have "... = x' * 1" |
10141 | 195 |
by (simp only: group_right_inverse) |
196 |
also have "... = x'" |
|
197 |
by (simp only: group_right_one) |
|
198 |
finally show ?thesis . |
|
199 |
qed |
|
200 |
||
37671 | 201 |
text {* The inverse operation has some further characteristic properties. *} |
10141 | 202 |
|
37671 | 203 |
theorem (in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x" |
10141 | 204 |
proof (rule group_inverse_equality) |
37671 | 205 |
show "(inverse y * inverse x) * (x * y) = 1" |
10141 | 206 |
proof - |
207 |
have "(inverse y * inverse x) * (x * y) = |
|
208 |
(inverse y * (inverse x * x)) * y" |
|
209 |
by (simp only: group_assoc) |
|
37671 | 210 |
also have "... = (inverse y * 1) * y" |
10141 | 211 |
by (simp only: group_left_inverse) |
212 |
also have "... = inverse y * y" |
|
213 |
by (simp only: group_right_one) |
|
37671 | 214 |
also have "... = 1" |
10141 | 215 |
by (simp only: group_left_inverse) |
216 |
finally show ?thesis . |
|
217 |
qed |
|
218 |
qed |
|
219 |
||
37671 | 220 |
theorem (in group) inverse_inverse: "inverse (inverse x) = x" |
10141 | 221 |
proof (rule group_inverse_equality) |
222 |
show "x * inverse x = one" |
|
223 |
by (simp only: group_right_inverse) |
|
224 |
qed |
|
225 |
||
37671 | 226 |
theorem (in group) inverse_inject: |
227 |
assumes eq: "inverse x = inverse y" |
|
228 |
shows "x = y" |
|
10141 | 229 |
proof - |
37671 | 230 |
have "x = x * 1" |
10141 | 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) |
|
37671 | 238 |
also have "... = 1 * y" |
10141 | 239 |
by (simp only: group_right_inverse) |
240 |
also have "... = y" |
|
241 |
by (simp only: group_left_one) |
|
242 |
finally show ?thesis . |
|
243 |
qed |
|
244 |
||
245 |
end |