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

src/HOL/Isar_Examples/Group.thy

author | blanchet |

Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) | |

changeset 58306 | 117ba6cbe414 |

parent 55656 | eb07b0acbebc |

child 58614 | 7338eb25226c |

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

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

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 {* 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. *}

18 class group = times + one + inverse +

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"

23 text {* The group axioms only state the properties of left one and

24 inverse, the right versions may be derived as follows. *}

26 theorem (in group) group_right_inverse: "x * inverse x = 1"

27 proof -

28 have "x * inverse x = 1 * (x * inverse x)"

29 by (simp only: group_left_one)

30 also have "\<dots> = 1 * x * inverse x"

31 by (simp only: group_assoc)

32 also have "\<dots> = inverse (inverse x) * inverse x * x * inverse x"

33 by (simp only: group_left_inverse)

34 also have "\<dots> = inverse (inverse x) * (inverse x * x) * inverse x"

35 by (simp only: group_assoc)

36 also have "\<dots> = inverse (inverse x) * 1 * inverse x"

37 by (simp only: group_left_inverse)

38 also have "\<dots> = inverse (inverse x) * (1 * inverse x)"

39 by (simp only: group_assoc)

40 also have "\<dots> = inverse (inverse x) * inverse x"

41 by (simp only: group_left_one)

42 also have "\<dots> = 1"

43 by (simp only: group_left_inverse)

44 finally show ?thesis .

45 qed

47 text {* With \name{group-right-inverse} already available,

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

49 much easier. *}

51 theorem (in group) group_right_one: "x * 1 = x"

52 proof -

53 have "x * 1 = x * (inverse x * x)"

54 by (simp only: group_left_inverse)

55 also have "\<dots> = x * inverse x * x"

56 by (simp only: group_assoc)

57 also have "\<dots> = 1 * x"

58 by (simp only: group_right_inverse)

59 also have "\<dots> = x"

60 by (simp only: group_left_one)

61 finally show ?thesis .

62 qed

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 low-level logical details of equational reasoning are left implicit.

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 right-hand 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.

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.

85 *}

87 theorem (in group) "x * 1 = x"

88 proof -

89 have "x * 1 = x * (inverse x * x)"

90 by (simp only: group_left_inverse)

92 note calculation = this

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

95 have "\<dots> = x * inverse x * x"

96 by (simp only: group_assoc)

98 note calculation = trans [OF calculation this]

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

101 have "\<dots> = 1 * x"

102 by (simp only: group_right_inverse)

104 note calculation = trans [OF calculation this]

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

107 have "\<dots> = x"

108 by (simp only: group_left_one)

110 note calculation = trans [OF calculation this]

111 -- {* final calculational step: compose with transitivity rule \dots *}

112 from calculation

113 -- {* \dots\ and pick up the final result *}

115 show ?thesis .

116 qed

118 text {* Note that this scheme of calculations is not restricted to

119 plain transitivity. Rules like anti-symmetry, 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 higher-order

124 unification. *}

127 subsection {* Groups as monoids *}

129 text {* Monoids over signature $({\times} :: \alpha \To \alpha \To

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

131 *}

133 class monoid = times + one +

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"

138 text {* Groups are \emph{not} yet monoids directly from the

139 definition. For monoids, \name{right-one} had to be included as an

140 axiom, but for groups both \name{right-one} and \name{right-inverse}

141 are derivable from the other axioms. With \name{group-right-one}

142 derived as a theorem of group theory (see

143 page~\pageref{thm:group-right-one}), we may still instantiate

144 $\idt{group} \subseteq \idt{monoid}$ properly as follows. *}

146 instance group < monoid

147 by intro_classes

148 (rule group_assoc,

149 rule group_left_one,

150 rule group_right_one)

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. *}

160 subsection {* More theorems of group theory *}

162 text {* The one element is already uniquely determined by preserving

163 an \emph{arbitrary} group element. *}

165 theorem (in group) group_one_equality:

166 assumes eq: "e * x = x"

167 shows "1 = e"

168 proof -

169 have "1 = x * inverse x"

170 by (simp only: group_right_inverse)

171 also have "\<dots> = (e * x) * inverse x"

172 by (simp only: eq)

173 also have "\<dots> = e * (x * inverse x)"

174 by (simp only: group_assoc)

175 also have "\<dots> = e * 1"

176 by (simp only: group_right_inverse)

177 also have "\<dots> = e"

178 by (simp only: group_right_one)

179 finally show ?thesis .

180 qed

182 text {* Likewise, the inverse is already determined by the cancel property. *}

184 theorem (in group) group_inverse_equality:

185 assumes eq: "x' * x = 1"

186 shows "inverse x = x'"

187 proof -

188 have "inverse x = 1 * inverse x"

189 by (simp only: group_left_one)

190 also have "\<dots> = (x' * x) * inverse x"

191 by (simp only: eq)

192 also have "\<dots> = x' * (x * inverse x)"

193 by (simp only: group_assoc)

194 also have "\<dots> = x' * 1"

195 by (simp only: group_right_inverse)

196 also have "\<dots> = x'"

197 by (simp only: group_right_one)

198 finally show ?thesis .

199 qed

201 text {* The inverse operation has some further characteristic properties. *}

203 theorem (in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x"

204 proof (rule group_inverse_equality)

205 show "(inverse y * inverse x) * (x * y) = 1"

206 proof -

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

208 (inverse y * (inverse x * x)) * y"

209 by (simp only: group_assoc)

210 also have "\<dots> = (inverse y * 1) * y"

211 by (simp only: group_left_inverse)

212 also have "\<dots> = inverse y * y"

213 by (simp only: group_right_one)

214 also have "\<dots> = 1"

215 by (simp only: group_left_inverse)

216 finally show ?thesis .

217 qed

218 qed

220 theorem (in group) inverse_inverse: "inverse (inverse x) = x"

221 proof (rule group_inverse_equality)

222 show "x * inverse x = one"

223 by (simp only: group_right_inverse)

224 qed

226 theorem (in group) inverse_inject:

227 assumes eq: "inverse x = inverse y"

228 shows "x = y"

229 proof -

230 have "x = x * 1"

231 by (simp only: group_right_one)

232 also have "\<dots> = x * (inverse y * y)"

233 by (simp only: group_left_inverse)

234 also have "\<dots> = x * (inverse x * y)"

235 by (simp only: eq)

236 also have "\<dots> = (x * inverse x) * y"

237 by (simp only: group_assoc)

238 also have "\<dots> = 1 * y"

239 by (simp only: group_right_inverse)

240 also have "\<dots> = y"

241 by (simp only: group_left_one)

242 finally show ?thesis .

243 qed

245 end