author | wenzelm |
Sat, 04 Sep 1999 21:13:01 +0200 | |
changeset 7480 | 0a0e0dbe1269 |
parent 7433 | 27887c52b9c8 |
child 7740 | 2fbe5ce9845f |
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 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
6 |
theory Group = Main:; |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
7 |
|
6793 | 8 |
title {* Basic group theory *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
9 |
|
6784 | 10 |
section {* Groups *}; |
11 |
||
12 |
text {* |
|
6793 | 13 |
We define an axiomatic type class of general groups over signature |
6784 | 14 |
(op *, one, inv). |
15 |
*}; |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
16 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
17 |
consts |
6784 | 18 |
one :: "'a" |
19 |
inv :: "'a => 'a"; |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
20 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
21 |
axclass |
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
22 |
group < times |
6793 | 23 |
group_assoc: "(x * y) * z = x * (y * z)" |
24 |
group_left_unit: "one * x = x" |
|
25 |
group_left_inverse: "inv x * x = one"; |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
26 |
|
6784 | 27 |
text {* |
6793 | 28 |
The group axioms only state the properties of left unit and inverse, |
29 |
the right versions are derivable as follows. The calculational proof |
|
30 |
style below closely follows typical presentations given in any basic |
|
31 |
course on algebra. |
|
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 {* |
6793 | 56 |
With group_right_inverse already at our disposal, group_right_unit is |
57 |
now obtained much easier as follows. |
|
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 {* |
6793 | 74 |
There are only two Isar language elements for calculational proofs: |
75 |
'also' for initial or intermediate calculational steps, and 'finally' |
|
76 |
for building the result of a calculation. These constructs are not |
|
77 |
hardwired into Isabelle/Isar, but defined on top of the basic Isar/VM |
|
78 |
interpreter. Expanding the 'also' or 'finally' derived language |
|
79 |
elements, calculations may be simulated as demonstrated below. |
|
6784 | 80 |
|
6793 | 81 |
Note that "..." is just a special term binding that happens to be |
82 |
bound automatically to the argument of the last fact established by |
|
7480 | 83 |
assume or any local goal. In contrast to ?thesis, "..." is bound |
6793 | 84 |
after the proof is finished. |
6784 | 85 |
*}; |
86 |
||
6793 | 87 |
theorem "x * one = (x::'a::group)"; |
7133 | 88 |
proof -; |
6784 | 89 |
have "x * one = x * (inv x * x)"; |
6908 | 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 |
6793 | 93 |
-- {* first calculational step: init calculation register *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
94 |
|
6784 | 95 |
have "... = x * inv x * x"; |
6908 | 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] |
6784 | 99 |
-- {* general calculational step: compose with transitivity rule *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
100 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
101 |
have "... = one * x"; |
6908 | 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] |
6784 | 105 |
-- {* general calculational step: compose with transitivity rule *}; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
106 |
|
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
107 |
have "... = x"; |
6908 | 108 |
by (simp only: group_left_unit); |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
109 |
|
7433 | 110 |
note calculation = trans [OF calculation this] |
6784 | 111 |
-- {* final calculational step: compose with transitivity rule ... *}; |
112 |
from calculation |
|
113 |
-- {* ... and pick up final result *}; |
|
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
114 |
|
7480 | 115 |
show ?thesis; .; |
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
116 |
qed; |
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 |
|
6793 | 119 |
section {* Groups and monoids *}; |
120 |
||
121 |
text {* |
|
122 |
Monoids are usually defined like this. |
|
123 |
*}; |
|
124 |
||
125 |
axclass monoid < times |
|
126 |
monoid_assoc: "(x * y) * z = x * (y * z)" |
|
127 |
monoid_left_unit: "one * x = x" |
|
128 |
monoid_right_unit: "x * one = x"; |
|
129 |
||
130 |
text {* |
|
7005 | 131 |
Groups are *not* yet monoids directly from the definition. For |
6793 | 132 |
monoids, right_unit had to be included as an axiom, but for groups |
133 |
both right_unit and right_inverse are derivable from the other |
|
134 |
axioms. With group_right_unit derived as a theorem of group theory |
|
135 |
(see above), we may still instantiate group < monoid properly as |
|
136 |
follows. |
|
137 |
*}; |
|
138 |
||
139 |
instance group < monoid; |
|
7356 | 140 |
by (intro_classes, |
6793 | 141 |
rule group_assoc, |
142 |
rule group_left_unit, |
|
143 |
rule group_right_unit); |
|
144 |
||
145 |
||
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset
|
146 |
end; |