author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 37671  fa53d267dab3 
child 55656  eb07b0acbebc 
permissions  rwrr 
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{grouprightinverse} already available, 
48 
\name{grouprightone}\label{thm:grouprightone} 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 
lowlevel 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 righthand 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 antisymmetry, 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 higherorder 

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{rightone} had to be included as an 

140 
axiom, but for groups both \name{rightone} and \name{rightinverse} 

141 
are derivable from the other axioms. With \name{grouprightone} 

142 
derived as a theorem of group theory (see 

143 
page~\pageref{thm:grouprightone}), 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 