summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_examples/Group.thy

author | paulson |

Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) | |

changeset 16587 | b34c8aa657a5 |

parent 16417 | 9bc16273c2d4 |

child 31758 | 3edd5f813f01 |

permissions | -rw-r--r-- |

Constant "If" is now local

1 (* Title: HOL/Isar_examples/Group.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

4 *)

6 header {* Basic group theory *}

8 theory Group imports Main begin

10 subsection {* Groups and calculational reasoning *}

12 text {*

13 Groups over signature $({\times} :: \alpha \To \alpha \To \alpha,

14 \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined

15 as an axiomatic type class as follows. Note that the parent class

16 $\idt{times}$ is provided by the basic HOL theory.

17 *}

19 consts

20 one :: "'a"

21 inverse :: "'a => 'a"

23 axclass

24 group < times

25 group_assoc: "(x * y) * z = x * (y * z)"

26 group_left_one: "one * x = x"

27 group_left_inverse: "inverse x * x = one"

29 text {*

30 The group axioms only state the properties of left one and inverse,

31 the right versions may be derived as follows.

32 *}

34 theorem group_right_inverse: "x * inverse x = (one::'a::group)"

35 proof -

36 have "x * inverse x = one * (x * inverse x)"

37 by (simp only: group_left_one)

38 also have "... = one * x * inverse x"

39 by (simp only: group_assoc)

40 also have "... = inverse (inverse x) * inverse x * x * inverse x"

41 by (simp only: group_left_inverse)

42 also have "... = inverse (inverse x) * (inverse x * x) * inverse x"

43 by (simp only: group_assoc)

44 also have "... = inverse (inverse x) * one * inverse x"

45 by (simp only: group_left_inverse)

46 also have "... = inverse (inverse x) * (one * inverse x)"

47 by (simp only: group_assoc)

48 also have "... = inverse (inverse x) * inverse x"

49 by (simp only: group_left_one)

50 also have "... = one"

51 by (simp only: group_left_inverse)

52 finally show ?thesis .

53 qed

55 text {*

56 With \name{group-right-inverse} already available,

57 \name{group-right-one}\label{thm:group-right-one} is now established

58 much easier.

59 *}

61 theorem group_right_one: "x * one = (x::'a::group)"

62 proof -

63 have "x * one = x * (inverse x * x)"

64 by (simp only: group_left_inverse)

65 also have "... = x * inverse x * x"

66 by (simp only: group_assoc)

67 also have "... = one * x"

68 by (simp only: group_right_inverse)

69 also have "... = x"

70 by (simp only: group_left_one)

71 finally show ?thesis .

72 qed

74 text {*

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

79 logical details of equational reasoning are left implicit.

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.

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

94 language elements, calculations may be simulated by hand as

95 demonstrated below.

96 *}

98 theorem "x * one = (x::'a::group)"

99 proof -

100 have "x * one = x * (inverse x * x)"

101 by (simp only: group_left_inverse)

103 note calculation = this

104 -- {* first calculational step: init calculation register *}

106 have "... = x * inverse x * x"

107 by (simp only: group_assoc)

109 note calculation = trans [OF calculation this]

110 -- {* general calculational step: compose with transitivity rule *}

112 have "... = one * x"

113 by (simp only: group_right_inverse)

115 note calculation = trans [OF calculation this]

116 -- {* general calculational step: compose with transitivity rule *}

118 have "... = x"

119 by (simp only: group_left_one)

121 note calculation = trans [OF calculation this]

122 -- {* final calculational step: compose with transitivity rule ... *}

123 from calculation

124 -- {* ... and pick up the final result *}

126 show ?thesis .

127 qed

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

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.

136 *}

139 subsection {* Groups as monoids *}

141 text {*

142 Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,

143 \idt{one} :: \alpha)$ are defined like this.

144 *}

146 axclass monoid < times

147 monoid_assoc: "(x * y) * z = x * (y * z)"

148 monoid_left_one: "one * x = x"

149 monoid_right_one: "x * one = x"

151 text {*

152 Groups are \emph{not} yet monoids directly from the definition. For

153 monoids, \name{right-one} had to be included as an axiom, but for

154 groups both \name{right-one} and \name{right-inverse} are derivable

155 from the other axioms. With \name{group-right-one} derived as a

156 theorem of group theory (see page~\pageref{thm:group-right-one}), we

157 may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly

158 as follows.

159 *}

161 instance group < monoid

162 by (intro_classes,

163 rule group_assoc,

164 rule group_left_one,

165 rule group_right_one)

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

172 concluding the proof, the result is transformed into the intended

173 type signature extension behind the scenes.

174 *}

176 subsection {* More theorems of group theory *}

178 text {*

179 The one element is already uniquely determined by preserving an

180 \emph{arbitrary} group element.

181 *}

183 theorem group_one_equality: "e * x = x ==> one = (e::'a::group)"

184 proof -

185 assume eq: "e * x = x"

186 have "one = x * inverse x"

187 by (simp only: group_right_inverse)

188 also have "... = (e * x) * inverse x"

189 by (simp only: eq)

190 also have "... = e * (x * inverse x)"

191 by (simp only: group_assoc)

192 also have "... = e * one"

193 by (simp only: group_right_inverse)

194 also have "... = e"

195 by (simp only: group_right_one)

196 finally show ?thesis .

197 qed

199 text {*

200 Likewise, the inverse is already determined by the cancel property.

201 *}

203 theorem group_inverse_equality:

204 "x' * x = one ==> inverse x = (x'::'a::group)"

205 proof -

206 assume eq: "x' * x = one"

207 have "inverse x = one * inverse x"

208 by (simp only: group_left_one)

209 also have "... = (x' * x) * inverse x"

210 by (simp only: eq)

211 also have "... = x' * (x * inverse x)"

212 by (simp only: group_assoc)

213 also have "... = x' * one"

214 by (simp only: group_right_inverse)

215 also have "... = x'"

216 by (simp only: group_right_one)

217 finally show ?thesis .

218 qed

220 text {*

221 The inverse operation has some further characteristic properties.

222 *}

224 theorem group_inverse_times:

225 "inverse (x * y) = inverse y * inverse (x::'a::group)"

226 proof (rule group_inverse_equality)

227 show "(inverse y * inverse x) * (x * y) = one"

228 proof -

229 have "(inverse y * inverse x) * (x * y) =

230 (inverse y * (inverse x * x)) * y"

231 by (simp only: group_assoc)

232 also have "... = (inverse y * one) * y"

233 by (simp only: group_left_inverse)

234 also have "... = inverse y * y"

235 by (simp only: group_right_one)

236 also have "... = one"

237 by (simp only: group_left_inverse)

238 finally show ?thesis .

239 qed

240 qed

242 theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)"

243 proof (rule group_inverse_equality)

244 show "x * inverse x = one"

245 by (simp only: group_right_inverse)

246 qed

248 theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)"

249 proof -

250 assume eq: "inverse x = inverse y"

251 have "x = x * one"

252 by (simp only: group_right_one)

253 also have "... = x * (inverse y * y)"

254 by (simp only: group_left_inverse)

255 also have "... = x * (inverse x * y)"

256 by (simp only: eq)

257 also have "... = (x * inverse x) * y"

258 by (simp only: group_assoc)

259 also have "... = one * y"

260 by (simp only: group_right_inverse)

261 also have "... = y"

262 by (simp only: group_left_one)

263 finally show ?thesis .

264 qed

266 end