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

src/HOL/Isar_Examples/Group.thy

author | wenzelm |

Tue Sep 26 20:54:40 2017 +0200 (23 months ago) | |

changeset 66695 | 91500c024c7f |

parent 63585 | f4a308fdf664 |

child 69855 | 60b924cda764 |

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

tuned;

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

2 Author: Makarius

3 *)

5 section \<open>Basic group theory\<close>

7 theory Group

8 imports Main

9 begin

11 subsection \<open>Groups and calculational reasoning\<close>

13 text \<open>

14 Groups over signature \<open>(* :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, 1 :: \<alpha>, inverse :: \<alpha> \<Rightarrow> \<alpha>)\<close> are

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

16 \<open>times\<close> is provided by the basic HOL theory.

17 \<close>

19 class group = times + one + inverse +

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

21 and group_left_one: "1 * x = x"

22 and group_left_inverse: "inverse x * x = 1"

24 text \<open>

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

26 right versions may be derived as follows.

27 \<close>

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

30 proof -

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

32 by (simp only: group_left_one)

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

34 by (simp only: group_assoc)

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

36 by (simp only: group_left_inverse)

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

38 by (simp only: group_assoc)

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

40 by (simp only: group_left_inverse)

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

42 by (simp only: group_assoc)

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

44 by (simp only: group_left_one)

45 also have "\<dots> = 1"

46 by (simp only: group_left_inverse)

47 finally show ?thesis .

48 qed

50 text \<open>

51 With \<open>group_right_inverse\<close> already available, \<open>group_right_one\<close>

52 is now established much easier.

53 \<close>

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

56 proof -

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

58 by (simp only: group_left_inverse)

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

60 by (simp only: group_assoc)

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

62 by (simp only: group_right_inverse)

63 also have "\<dots> = x"

64 by (simp only: group_left_one)

65 finally show ?thesis .

66 qed

68 text \<open>

69 \<^medskip>

70 The calculational proof style above follows typical presentations given in

71 any introductory course on algebra. The basic technique is to form a

72 transitive chain of equations, which in turn are established by simplifying

73 with appropriate rules. The low-level logical details of equational

74 reasoning are left implicit.

76 Note that ``\<open>\<dots>\<close>'' is just a special term variable that is bound

77 automatically to the argument\<^footnote>\<open>The argument of a curried infix expression

78 happens to be its right-hand side.\<close> of the last fact achieved by any local

79 assumption or proven statement. In contrast to \<open>?thesis\<close>, the ``\<open>\<dots>\<close>''

80 variable is bound \<^emph>\<open>after\<close> the proof is finished.

82 There are only two separate Isar language elements for calculational proofs:

83 ``\<^theory_text>\<open>also\<close>'' for initial or intermediate calculational steps, and

84 ``\<^theory_text>\<open>finally\<close>'' for exhibiting the result of a calculation. These constructs

85 are not hardwired into Isabelle/Isar, but defined on top of the basic

86 Isar/VM interpreter. Expanding the \<^theory_text>\<open>also\<close> and \<^theory_text>\<open>finally\<close> derived language

87 elements, calculations may be simulated by hand as demonstrated below.

88 \<close>

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

91 proof -

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

93 by (simp only: group_left_inverse)

95 note calculation = this

96 \<comment> \<open>first calculational step: init calculation register\<close>

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

99 by (simp only: group_assoc)

101 note calculation = trans [OF calculation this]

102 \<comment> \<open>general calculational step: compose with transitivity rule\<close>

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

105 by (simp only: group_right_inverse)

107 note calculation = trans [OF calculation this]

108 \<comment> \<open>general calculational step: compose with transitivity rule\<close>

110 have "\<dots> = x"

111 by (simp only: group_left_one)

113 note calculation = trans [OF calculation this]

114 \<comment> \<open>final calculational step: compose with transitivity rule \dots\<close>

115 from calculation

116 \<comment> \<open>\dots\ and pick up the final result\<close>

118 show ?thesis .

119 qed

121 text \<open>

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

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

124 substitution work as well. For the actual implementation of \<^theory_text>\<open>also\<close> and

125 \<^theory_text>\<open>finally\<close>, Isabelle/Isar maintains separate context information of

126 ``transitivity'' rules. Rule selection takes place automatically by

127 higher-order unification.

128 \<close>

131 subsection \<open>Groups as monoids\<close>

133 text \<open>

134 Monoids over signature \<open>(* :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, 1 :: \<alpha>)\<close> are defined like this.

135 \<close>

137 class monoid = times + one +

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

139 and monoid_left_one: "1 * x = x"

140 and monoid_right_one: "x * 1 = x"

142 text \<open>

143 Groups are \<^emph>\<open>not\<close> yet monoids directly from the definition. For monoids,

144 \<open>right_one\<close> had to be included as an axiom, but for groups both \<open>right_one\<close>

145 and \<open>right_inverse\<close> are derivable from the other axioms. With

146 \<open>group_right_one\<close> derived as a theorem of group theory (see @{thm

147 group_right_one}), we may still instantiate \<open>group \<subseteq> monoid\<close> properly as

148 follows.

149 \<close>

151 instance group \<subseteq> monoid

152 by intro_classes

153 (rule group_assoc,

154 rule group_left_one,

155 rule group_right_one)

157 text \<open>

158 The \<^theory_text>\<open>instance\<close> command actually is a version of \<^theory_text>\<open>theorem\<close>, setting up a

159 goal that reflects the intended class relation (or type constructor arity).

160 Thus any Isar proof language element may be involved to establish this

161 statement. When concluding the proof, the result is transformed into the

162 intended type signature extension behind the scenes.

163 \<close>

166 subsection \<open>More theorems of group theory\<close>

168 text \<open>

169 The one element is already uniquely determined by preserving an \<^emph>\<open>arbitrary\<close>

170 group element.

171 \<close>

173 theorem (in group) group_one_equality:

174 assumes eq: "e * x = x"

175 shows "1 = e"

176 proof -

177 have "1 = x * inverse x"

178 by (simp only: group_right_inverse)

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

180 by (simp only: eq)

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

182 by (simp only: group_assoc)

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

184 by (simp only: group_right_inverse)

185 also have "\<dots> = e"

186 by (simp only: group_right_one)

187 finally show ?thesis .

188 qed

190 text \<open>

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

192 \<close>

194 theorem (in group) group_inverse_equality:

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

196 shows "inverse x = x'"

197 proof -

198 have "inverse x = 1 * inverse x"

199 by (simp only: group_left_one)

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

201 by (simp only: eq)

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

203 by (simp only: group_assoc)

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

205 by (simp only: group_right_inverse)

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

207 by (simp only: group_right_one)

208 finally show ?thesis .

209 qed

211 text \<open>

212 The inverse operation has some further characteristic properties.

213 \<close>

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

216 proof (rule group_inverse_equality)

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

218 proof -

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

220 (inverse y * (inverse x * x)) * y"

221 by (simp only: group_assoc)

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

223 by (simp only: group_left_inverse)

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

225 by (simp only: group_right_one)

226 also have "\<dots> = 1"

227 by (simp only: group_left_inverse)

228 finally show ?thesis .

229 qed

230 qed

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

233 proof (rule group_inverse_equality)

234 show "x * inverse x = one"

235 by (simp only: group_right_inverse)

236 qed

238 theorem (in group) inverse_inject:

239 assumes eq: "inverse x = inverse y"

240 shows "x = y"

241 proof -

242 have "x = x * 1"

243 by (simp only: group_right_one)

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

245 by (simp only: group_left_inverse)

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

247 by (simp only: eq)

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

249 by (simp only: group_assoc)

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

251 by (simp only: group_right_inverse)

252 also have "\<dots> = y"

253 by (simp only: group_left_one)

254 finally show ?thesis .

255 qed

257 end