author | paulson |
Fri, 18 Feb 2000 15:35:29 +0100 | |
changeset 8255 | 38f96394c099 |
parent 7982 | d534b897ce39 |
child 8910 | 981ac87f905c |
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 {* |
7982 | 56 |
With \name{group-right-inverse} already available, |
57 |
\name{group-right-unit}\label{thm:group-right-unit} is now |
|
58 |
established much easier. |
|
6784 | 59 |
*}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
60 |
|
6793 | 61 |
theorem group_right_unit: "x * one = (x::'a::group)"; |
7133 | 62 |
proof -; |
6784 | 63 |
have "x * one = x * (inv x * x)"; |
6908 | 64 |
by (simp only: group_left_inverse); |
6784 | 65 |
also; have "... = x * inv x * x"; |
6908 | 66 |
by (simp only: group_assoc); |
6784 | 67 |
also; have "... = one * x"; |
6908 | 68 |
by (simp only: group_right_inverse); |
6784 | 69 |
also; have "... = x"; |
6908 | 70 |
by (simp only: group_left_unit); |
7480 | 71 |
finally; show ?thesis; .; |
6784 | 72 |
qed; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
73 |
|
6784 | 74 |
text {* |
7874 | 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 |
|
7982 | 79 |
logical details of equational reasoning are left implicit. |
6784 | 80 |
|
7982 | 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. |
|
7874 | 87 |
|
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 |
|
7982 | 94 |
language elements, calculations may be simulated by hand as |
95 |
demonstrated below. |
|
6784 | 96 |
*}; |
97 |
||
6793 | 98 |
theorem "x * one = (x::'a::group)"; |
7133 | 99 |
proof -; |
6784 | 100 |
have "x * one = x * (inv x * x)"; |
6908 | 101 |
by (simp only: group_left_inverse); |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
102 |
|
7433 | 103 |
note calculation = this |
6793 | 104 |
-- {* first calculational step: init calculation register *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
105 |
|
6784 | 106 |
have "... = x * inv x * x"; |
6908 | 107 |
by (simp only: group_assoc); |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
108 |
|
7433 | 109 |
note calculation = trans [OF calculation this] |
6784 | 110 |
-- {* general calculational step: compose with transitivity rule *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
111 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
112 |
have "... = one * x"; |
6908 | 113 |
by (simp only: group_right_inverse); |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
114 |
|
7433 | 115 |
note calculation = trans [OF calculation this] |
6784 | 116 |
-- {* general calculational step: compose with transitivity rule *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
117 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
118 |
have "... = x"; |
6908 | 119 |
by (simp only: group_left_unit); |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
120 |
|
7433 | 121 |
note calculation = trans [OF calculation this] |
6784 | 122 |
-- {* final calculational step: compose with transitivity rule ... *}; |
123 |
from calculation |
|
7874 | 124 |
-- {* ... and pick up the final result *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
125 |
|
7480 | 126 |
show ?thesis; .; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
127 |
qed; |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
128 |
|
7874 | 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 |
|
7982 | 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. |
|
7874 | 136 |
*}; |
137 |
||
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
138 |
|
7761 | 139 |
subsection {* Groups as monoids *}; |
6793 | 140 |
|
141 |
text {* |
|
7874 | 142 |
Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha, |
143 |
\idt{one} :: \alpha)$ are defined like this. |
|
6793 | 144 |
*}; |
145 |
||
146 |
axclass monoid < times |
|
147 |
monoid_assoc: "(x * y) * z = x * (y * z)" |
|
148 |
monoid_left_unit: "one * x = x" |
|
149 |
monoid_right_unit: "x * one = x"; |
|
150 |
||
151 |
text {* |
|
7748 | 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 |
|
7982 | 154 |
groups both \name{right-unit} and \name{right-inverse} are derivable |
155 |
from the other axioms. With \name{group-right-unit} derived as a |
|
156 |
theorem of group theory (see page~\pageref{thm:group-right-unit}), we |
|
157 |
may still instantiate $\idt{group} \subset \idt{monoid}$ properly as |
|
158 |
follows. |
|
6793 | 159 |
*}; |
160 |
||
161 |
instance group < monoid; |
|
7356 | 162 |
by (intro_classes, |
6793 | 163 |
rule group_assoc, |
164 |
rule group_left_unit, |
|
165 |
rule group_right_unit); |
|
166 |
||
7874 | 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 |
|
7982 | 172 |
concluding the proof, the result is transformed into the intended |
7874 | 173 |
type signature extension behind the scenes. |
174 |
*}; |
|
175 |
||
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
176 |
end; |