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

src/HOL/Isar_Examples/Group.thy

author | haftmann |

Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) | |

changeset 37659 | 14cabf5fa710 |

parent 35317 | d57da4abb47d |

child 37671 | fa53d267dab3 |

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

more speaking names

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

2 Author: Markus Wenzel, TU Muenchen

3 *)

5 header {* Basic group theory *}

7 theory Group

8 imports Main

9 begin

11 subsection {* Groups and calculational reasoning *}

13 text {*

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

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

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

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

18 *}

20 notation Groups.one ("one")

22 class group = times + one + inverse +

23 assumes group_assoc: "(x * y) * z = x * (y * z)"

24 assumes group_left_one: "one * x = x"

25 assumes group_left_inverse: "inverse x * x = one"

27 text {*

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

29 the right versions may be derived as follows.

30 *}

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

33 proof -

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

35 by (simp only: group_left_one)

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

37 by (simp only: group_assoc)

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

39 by (simp only: group_left_inverse)

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

41 by (simp only: group_assoc)

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

43 by (simp only: group_left_inverse)

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

45 by (simp only: group_assoc)

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

47 by (simp only: group_left_one)

48 also have "... = one"

49 by (simp only: group_left_inverse)

50 finally show ?thesis .

51 qed

53 text {*

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

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

56 much easier.

57 *}

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

60 proof -

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

62 by (simp only: group_left_inverse)

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

64 by (simp only: group_assoc)

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

66 by (simp only: group_right_inverse)

67 also have "... = x"

68 by (simp only: group_left_one)

69 finally show ?thesis .

70 qed

72 text {*

73 \medskip The calculational proof style above follows typical

74 presentations given in any introductory course on algebra. The basic

75 technique is to form a transitive chain of equations, which in turn

76 are established by simplifying with appropriate rules. The low-level

77 logical details of equational reasoning are left implicit.

79 Note that ``$\dots$'' is just a special term variable that is bound

80 automatically to the argument\footnote{The argument of a curried

81 infix expression happens to be its right-hand side.} of the last fact

82 achieved by any local assumption or proven statement. In contrast to

83 $\var{thesis}$, the ``$\dots$'' variable is bound \emph{after} the

84 proof is finished, though.

86 There are only two separate Isar language elements for calculational

87 proofs: ``\isakeyword{also}'' for initial or intermediate

88 calculational steps, and ``\isakeyword{finally}'' for exhibiting the

89 result of a calculation. These constructs are not hardwired into

90 Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.

91 Expanding the \isakeyword{also} and \isakeyword{finally} derived

92 language elements, calculations may be simulated by hand as

93 demonstrated below.

94 *}

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

97 proof -

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

99 by (simp only: group_left_inverse)

101 note calculation = this

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

104 have "... = x * inverse x * x"

105 by (simp only: group_assoc)

107 note calculation = trans [OF calculation this]

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

110 have "... = one * x"

111 by (simp only: group_right_inverse)

113 note calculation = trans [OF calculation this]

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

116 have "... = x"

117 by (simp only: group_left_one)

119 note calculation = trans [OF calculation this]

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

121 from calculation

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

124 show ?thesis .

125 qed

127 text {*

128 Note that this scheme of calculations is not restricted to plain

129 transitivity. Rules like anti-symmetry, or even forward and backward

130 substitution work as well. For the actual implementation of

131 \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains

132 separate context information of ``transitivity'' rules. Rule

133 selection takes place automatically by higher-order unification.

134 *}

137 subsection {* Groups as monoids *}

139 text {*

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

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

142 *}

144 class monoid = times + one +

145 assumes monoid_assoc: "(x * y) * z = x * (y * z)"

146 assumes monoid_left_one: "one * x = x"

147 assumes monoid_right_one: "x * one = x"

149 text {*

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

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

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

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

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

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

156 as follows.

157 *}

159 instance group < monoid

160 by (intro_classes,

161 rule group_assoc,

162 rule group_left_one,

163 rule group_right_one)

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 intended

171 type signature extension behind the scenes.

172 *}

174 subsection {* More theorems of group theory *}

176 text {*

177 The one element is already uniquely determined by preserving an

178 \emph{arbitrary} group element.

179 *}

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

182 proof -

183 assume eq: "e * x = x"

184 have "one = x * inverse x"

185 by (simp only: group_right_inverse)

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

187 by (simp only: eq)

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

189 by (simp only: group_assoc)

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

191 by (simp only: group_right_inverse)

192 also have "... = e"

193 by (simp only: group_right_one)

194 finally show ?thesis .

195 qed

197 text {*

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

199 *}

201 theorem group_inverse_equality:

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

203 proof -

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

205 have "inverse x = one * inverse x"

206 by (simp only: group_left_one)

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

208 by (simp only: eq)

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

210 by (simp only: group_assoc)

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

212 by (simp only: group_right_inverse)

213 also have "... = x'"

214 by (simp only: group_right_one)

215 finally show ?thesis .

216 qed

218 text {*

219 The inverse operation has some further characteristic properties.

220 *}

222 theorem group_inverse_times:

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

224 proof (rule group_inverse_equality)

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

226 proof -

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

228 (inverse y * (inverse x * x)) * y"

229 by (simp only: group_assoc)

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

231 by (simp only: group_left_inverse)

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

233 by (simp only: group_right_one)

234 also have "... = one"

235 by (simp only: group_left_inverse)

236 finally show ?thesis .

237 qed

238 qed

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

241 proof (rule group_inverse_equality)

242 show "x * inverse x = one"

243 by (simp only: group_right_inverse)

244 qed

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

247 proof -

248 assume eq: "inverse x = inverse y"

249 have "x = x * one"

250 by (simp only: group_right_one)

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

252 by (simp only: group_left_inverse)

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

254 by (simp only: eq)

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

256 by (simp only: group_assoc)

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

258 by (simp only: group_right_inverse)

259 also have "... = y"

260 by (simp only: group_left_one)

261 finally show ?thesis .

262 qed

264 end