author | wenzelm |
Thu, 28 Oct 1999 19:57:34 +0200 | |
changeset 7968 | 964b65b4e433 |
parent 7874 | 180364256231 |
child 7982 | d534b897ce39 |
permissions | -rw-r--r-- |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Isar_examples/Group.thy |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
4 |
*) |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
5 |
|
7748 | 6 |
header {* Basic group theory *}; |
7 |
||
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
8 |
theory Group = Main:; |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
9 |
|
7874 | 10 |
subsection {* Groups and calculational reasoning *}; |
6784 | 11 |
|
12 |
text {* |
|
7968 | 13 |
Groups over signature $({\times} :: \alpha \To \alpha \To \alpha, |
14 |
\idt{one} :: \alpha, \idt{inv} :: \alpha \To \alpha)$ are defined as |
|
15 |
an axiomatic type class as follows. Note that the parent class |
|
16 |
$\idt{times}$ is provided by the basic HOL theory. |
|
6784 | 17 |
*}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
18 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
19 |
consts |
6784 | 20 |
one :: "'a" |
21 |
inv :: "'a => 'a"; |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
22 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
23 |
axclass |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
24 |
group < times |
6793 | 25 |
group_assoc: "(x * y) * z = x * (y * z)" |
26 |
group_left_unit: "one * x = x" |
|
27 |
group_left_inverse: "inv x * x = one"; |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
28 |
|
6784 | 29 |
text {* |
6793 | 30 |
The group axioms only state the properties of left unit and inverse, |
7874 | 31 |
the right versions may be derived as follows. |
6784 | 32 |
*}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
33 |
|
6793 | 34 |
theorem group_right_inverse: "x * inv x = (one::'a::group)"; |
7133 | 35 |
proof -; |
6784 | 36 |
have "x * inv x = one * (x * inv x)"; |
6908 | 37 |
by (simp only: group_left_unit); |
6784 | 38 |
also; have "... = (one * x) * inv x"; |
6908 | 39 |
by (simp only: group_assoc); |
6784 | 40 |
also; have "... = inv (inv x) * inv x * x * inv x"; |
6908 | 41 |
by (simp only: group_left_inverse); |
6784 | 42 |
also; have "... = inv (inv x) * (inv x * x) * inv x"; |
6908 | 43 |
by (simp only: group_assoc); |
6784 | 44 |
also; have "... = inv (inv x) * one * inv x"; |
6908 | 45 |
by (simp only: group_left_inverse); |
6784 | 46 |
also; have "... = inv (inv x) * (one * inv x)"; |
6908 | 47 |
by (simp only: group_assoc); |
6784 | 48 |
also; have "... = inv (inv x) * inv x"; |
6908 | 49 |
by (simp only: group_left_unit); |
6784 | 50 |
also; have "... = one"; |
6908 | 51 |
by (simp only: group_left_inverse); |
7480 | 52 |
finally; show ?thesis; .; |
6784 | 53 |
qed; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
54 |
|
6784 | 55 |
text {* |
7748 | 56 |
With \name{group-right-inverse} already at our disposal, |
7874 | 57 |
\name{group-right-unit} is now obtained much easier. |
6784 | 58 |
*}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
59 |
|
6793 | 60 |
theorem group_right_unit: "x * one = (x::'a::group)"; |
7133 | 61 |
proof -; |
6784 | 62 |
have "x * one = x * (inv x * x)"; |
6908 | 63 |
by (simp only: group_left_inverse); |
6784 | 64 |
also; have "... = x * inv x * x"; |
6908 | 65 |
by (simp only: group_assoc); |
6784 | 66 |
also; have "... = one * x"; |
6908 | 67 |
by (simp only: group_right_inverse); |
6784 | 68 |
also; have "... = x"; |
6908 | 69 |
by (simp only: group_left_unit); |
7480 | 70 |
finally; show ?thesis; .; |
6784 | 71 |
qed; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
72 |
|
6784 | 73 |
text {* |
7874 | 74 |
\medskip The calculational proof style above follows typical |
75 |
presentations given in any introductory course on algebra. The basic |
|
76 |
technique is to form a transitive chain of equations, which in turn |
|
77 |
are established by simplifying with appropriate rules. The low-level |
|
78 |
logical parts of equational reasoning are left implicit. |
|
6784 | 79 |
|
7874 | 80 |
Note that ``$\dots$'' is just a special term variable that happens to |
81 |
be bound automatically to the argument\footnote{The argument of a |
|
82 |
curried infix expression happens to be its right-hand side.} of the |
|
83 |
last fact achieved by any local assumption or proven statement. In |
|
84 |
contrast to $\var{thesis}$, the ``$\dots$'' variable is bound |
|
85 |
\emph{after} the proof is finished. |
|
86 |
||
87 |
There are only two separate Isar language elements for calculational |
|
88 |
proofs: ``\isakeyword{also}'' for initial or intermediate |
|
89 |
calculational steps, and ``\isakeyword{finally}'' for exhibiting the |
|
90 |
result of a calculation. These constructs are not hardwired into |
|
91 |
Isabelle/Isar, but defined on top of the basic Isar/VM interpreter. |
|
92 |
Expanding the \isakeyword{also} and \isakeyword{finally} derived |
|
93 |
language elements, calculations may be simulated as demonstrated |
|
94 |
below. |
|
6784 | 95 |
*}; |
96 |
||
6793 | 97 |
theorem "x * one = (x::'a::group)"; |
7133 | 98 |
proof -; |
6784 | 99 |
have "x * one = x * (inv x * x)"; |
6908 | 100 |
by (simp only: group_left_inverse); |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
101 |
|
7433 | 102 |
note calculation = this |
6793 | 103 |
-- {* first calculational step: init calculation register *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
104 |
|
6784 | 105 |
have "... = x * inv x * x"; |
6908 | 106 |
by (simp only: group_assoc); |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
107 |
|
7433 | 108 |
note calculation = trans [OF calculation this] |
6784 | 109 |
-- {* general calculational step: compose with transitivity rule *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
110 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
111 |
have "... = one * x"; |
6908 | 112 |
by (simp only: group_right_inverse); |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
113 |
|
7433 | 114 |
note calculation = trans [OF calculation this] |
6784 | 115 |
-- {* general calculational step: compose with transitivity rule *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
116 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
117 |
have "... = x"; |
6908 | 118 |
by (simp only: group_left_unit); |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
119 |
|
7433 | 120 |
note calculation = trans [OF calculation this] |
6784 | 121 |
-- {* final calculational step: compose with transitivity rule ... *}; |
122 |
from calculation |
|
7874 | 123 |
-- {* ... and pick up the final result *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
124 |
|
7480 | 125 |
show ?thesis; .; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
126 |
qed; |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
127 |
|
7874 | 128 |
text {* |
129 |
Note that this scheme of calculations is not restricted to plain |
|
130 |
transitivity. Rules like anti-symmetry, or even forward and backward |
|
131 |
substitution work as well. For the actual \isacommand{also} and |
|
132 |
\isacommand{finally} commands, Isabelle/Isar maintains separate |
|
133 |
context information of ``transitivity'' rules. Rule selection takes |
|
134 |
place automatically by higher-order unification. |
|
135 |
*}; |
|
136 |
||
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
137 |
|
7761 | 138 |
subsection {* Groups as monoids *}; |
6793 | 139 |
|
140 |
text {* |
|
7874 | 141 |
Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha, |
142 |
\idt{one} :: \alpha)$ are defined like this. |
|
6793 | 143 |
*}; |
144 |
||
145 |
axclass monoid < times |
|
146 |
monoid_assoc: "(x * y) * z = x * (y * z)" |
|
147 |
monoid_left_unit: "one * x = x" |
|
148 |
monoid_right_unit: "x * one = x"; |
|
149 |
||
150 |
text {* |
|
7748 | 151 |
Groups are \emph{not} yet monoids directly from the definition. For |
152 |
monoids, \name{right-unit} had to be included as an axiom, but for |
|
153 |
groups both \name{right-unit} and \name{right-inverse} are |
|
154 |
derivable from the other axioms. With \name{group-right-unit} |
|
155 |
derived as a theorem of group theory (see above), we may still |
|
156 |
instantiate $\idt{group} \subset \idt{monoid}$ properly as follows. |
|
6793 | 157 |
*}; |
158 |
||
159 |
instance group < monoid; |
|
7356 | 160 |
by (intro_classes, |
6793 | 161 |
rule group_assoc, |
162 |
rule group_left_unit, |
|
163 |
rule group_right_unit); |
|
164 |
||
7874 | 165 |
text {* |
166 |
The \isacommand{instance} command actually is a version of |
|
167 |
\isacommand{theorem}, setting up a goal that reflects the intended |
|
168 |
class relation (or type constructor arity). Thus any Isar proof |
|
169 |
language element may be involved to establish this statement. When |
|
170 |
concluding the proof, the result is transformed into the original |
|
171 |
type signature extension behind the scenes. |
|
172 |
*}; |
|
173 |
||
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
174 |
end; |