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

src/HOL/Isar_Examples/Group.thy

changeset 37671 | fa53d267dab3 |

parent 35317 | d57da4abb47d |

child 55656 | eb07b0acbebc |

1.1 --- a/src/HOL/Isar_Examples/Group.thy Thu Jul 01 14:32:57 2010 +0200 1.2 +++ b/src/HOL/Isar_Examples/Group.thy Thu Jul 01 18:31:46 2010 +0200 1.3 @@ -10,92 +10,83 @@ 1.4 1.5 subsection {* Groups and calculational reasoning *} 1.6 1.7 -text {* 1.8 - Groups over signature $({\times} :: \alpha \To \alpha \To \alpha, 1.9 - \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined 1.10 - as an axiomatic type class as follows. Note that the parent class 1.11 - $\idt{times}$ is provided by the basic HOL theory. 1.12 -*} 1.13 - 1.14 -notation Groups.one ("one") 1.15 +text {* Groups over signature $({\times} :: \alpha \To \alpha \To 1.16 + \alpha, \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ 1.17 + are defined as an axiomatic type class as follows. Note that the 1.18 + parent class $\idt{times}$ is provided by the basic HOL theory. *} 1.19 1.20 class group = times + one + inverse + 1.21 - assumes group_assoc: "(x * y) * z = x * (y * z)" 1.22 - assumes group_left_one: "one * x = x" 1.23 - assumes group_left_inverse: "inverse x * x = one" 1.24 + assumes group_assoc: "(x * y) * z = x * (y * z)" 1.25 + and group_left_one: "1 * x = x" 1.26 + and group_left_inverse: "inverse x * x = 1" 1.27 1.28 -text {* 1.29 - The group axioms only state the properties of left one and inverse, 1.30 - the right versions may be derived as follows. 1.31 -*} 1.32 +text {* The group axioms only state the properties of left one and 1.33 + inverse, the right versions may be derived as follows. *} 1.34 1.35 -theorem group_right_inverse: "x * inverse x = (one::'a::group)" 1.36 +theorem (in group) group_right_inverse: "x * inverse x = 1" 1.37 proof - 1.38 - have "x * inverse x = one * (x * inverse x)" 1.39 + have "x * inverse x = 1 * (x * inverse x)" 1.40 by (simp only: group_left_one) 1.41 - also have "... = one * x * inverse x" 1.42 + also have "... = 1 * x * inverse x" 1.43 by (simp only: group_assoc) 1.44 also have "... = inverse (inverse x) * inverse x * x * inverse x" 1.45 by (simp only: group_left_inverse) 1.46 also have "... = inverse (inverse x) * (inverse x * x) * inverse x" 1.47 by (simp only: group_assoc) 1.48 - also have "... = inverse (inverse x) * one * inverse x" 1.49 + also have "... = inverse (inverse x) * 1 * inverse x" 1.50 by (simp only: group_left_inverse) 1.51 - also have "... = inverse (inverse x) * (one * inverse x)" 1.52 + also have "... = inverse (inverse x) * (1 * inverse x)" 1.53 by (simp only: group_assoc) 1.54 also have "... = inverse (inverse x) * inverse x" 1.55 by (simp only: group_left_one) 1.56 - also have "... = one" 1.57 + also have "... = 1" 1.58 by (simp only: group_left_inverse) 1.59 finally show ?thesis . 1.60 qed 1.61 1.62 -text {* 1.63 - With \name{group-right-inverse} already available, 1.64 - \name{group-right-one}\label{thm:group-right-one} is now established 1.65 - much easier. 1.66 -*} 1.67 +text {* With \name{group-right-inverse} already available, 1.68 + \name{group-right-one}\label{thm:group-right-one} is now established 1.69 + much easier. *} 1.70 1.71 -theorem group_right_one: "x * one = (x::'a::group)" 1.72 +theorem (in group) group_right_one: "x * 1 = x" 1.73 proof - 1.74 - have "x * one = x * (inverse x * x)" 1.75 + have "x * 1 = x * (inverse x * x)" 1.76 by (simp only: group_left_inverse) 1.77 also have "... = x * inverse x * x" 1.78 by (simp only: group_assoc) 1.79 - also have "... = one * x" 1.80 + also have "... = 1 * x" 1.81 by (simp only: group_right_inverse) 1.82 also have "... = x" 1.83 by (simp only: group_left_one) 1.84 finally show ?thesis . 1.85 qed 1.86 1.87 -text {* 1.88 - \medskip The calculational proof style above follows typical 1.89 - presentations given in any introductory course on algebra. The basic 1.90 - technique is to form a transitive chain of equations, which in turn 1.91 - are established by simplifying with appropriate rules. The low-level 1.92 - logical details of equational reasoning are left implicit. 1.93 +text {* \medskip The calculational proof style above follows typical 1.94 + presentations given in any introductory course on algebra. The 1.95 + basic technique is to form a transitive chain of equations, which in 1.96 + turn are established by simplifying with appropriate rules. The 1.97 + low-level logical details of equational reasoning are left implicit. 1.98 1.99 - Note that ``$\dots$'' is just a special term variable that is bound 1.100 - automatically to the argument\footnote{The argument of a curried 1.101 - infix expression happens to be its right-hand side.} of the last fact 1.102 - achieved by any local assumption or proven statement. In contrast to 1.103 - $\var{thesis}$, the ``$\dots$'' variable is bound \emph{after} the 1.104 - proof is finished, though. 1.105 + Note that ``$\dots$'' is just a special term variable that is bound 1.106 + automatically to the argument\footnote{The argument of a curried 1.107 + infix expression happens to be its right-hand side.} of the last 1.108 + fact achieved by any local assumption or proven statement. In 1.109 + contrast to $\var{thesis}$, the ``$\dots$'' variable is bound 1.110 + \emph{after} the proof is finished, though. 1.111 1.112 - There are only two separate Isar language elements for calculational 1.113 - proofs: ``\isakeyword{also}'' for initial or intermediate 1.114 - calculational steps, and ``\isakeyword{finally}'' for exhibiting the 1.115 - result of a calculation. These constructs are not hardwired into 1.116 - Isabelle/Isar, but defined on top of the basic Isar/VM interpreter. 1.117 - Expanding the \isakeyword{also} and \isakeyword{finally} derived 1.118 - language elements, calculations may be simulated by hand as 1.119 - demonstrated below. 1.120 + There are only two separate Isar language elements for calculational 1.121 + proofs: ``\isakeyword{also}'' for initial or intermediate 1.122 + calculational steps, and ``\isakeyword{finally}'' for exhibiting the 1.123 + result of a calculation. These constructs are not hardwired into 1.124 + Isabelle/Isar, but defined on top of the basic Isar/VM interpreter. 1.125 + Expanding the \isakeyword{also} and \isakeyword{finally} derived 1.126 + language elements, calculations may be simulated by hand as 1.127 + demonstrated below. 1.128 *} 1.129 1.130 -theorem "x * one = (x::'a::group)" 1.131 +theorem (in group) "x * 1 = x" 1.132 proof - 1.133 - have "x * one = x * (inverse x * x)" 1.134 + have "x * 1 = x * (inverse x * x)" 1.135 by (simp only: group_left_inverse) 1.136 1.137 note calculation = this 1.138 @@ -107,7 +98,7 @@ 1.139 note calculation = trans [OF calculation this] 1.140 -- {* general calculational step: compose with transitivity rule *} 1.141 1.142 - have "... = one * x" 1.143 + have "... = 1 * x" 1.144 by (simp only: group_right_inverse) 1.145 1.146 note calculation = trans [OF calculation this] 1.147 @@ -124,129 +115,119 @@ 1.148 show ?thesis . 1.149 qed 1.150 1.151 -text {* 1.152 - Note that this scheme of calculations is not restricted to plain 1.153 - transitivity. Rules like anti-symmetry, or even forward and backward 1.154 - substitution work as well. For the actual implementation of 1.155 - \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains 1.156 - separate context information of ``transitivity'' rules. Rule 1.157 - selection takes place automatically by higher-order unification. 1.158 -*} 1.159 +text {* Note that this scheme of calculations is not restricted to 1.160 + plain transitivity. Rules like anti-symmetry, or even forward and 1.161 + backward substitution work as well. For the actual implementation 1.162 + of \isacommand{also} and \isacommand{finally}, Isabelle/Isar 1.163 + maintains separate context information of ``transitivity'' rules. 1.164 + Rule selection takes place automatically by higher-order 1.165 + unification. *} 1.166 1.167 1.168 subsection {* Groups as monoids *} 1.169 1.170 -text {* 1.171 - Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha, 1.172 - \idt{one} :: \alpha)$ are defined like this. 1.173 +text {* Monoids over signature $({\times} :: \alpha \To \alpha \To 1.174 + \alpha, \idt{one} :: \alpha)$ are defined like this. 1.175 *} 1.176 1.177 class monoid = times + one + 1.178 - assumes monoid_assoc: "(x * y) * z = x * (y * z)" 1.179 - assumes monoid_left_one: "one * x = x" 1.180 - assumes monoid_right_one: "x * one = x" 1.181 + assumes monoid_assoc: "(x * y) * z = x * (y * z)" 1.182 + and monoid_left_one: "1 * x = x" 1.183 + and monoid_right_one: "x * 1 = x" 1.184 1.185 -text {* 1.186 - Groups are \emph{not} yet monoids directly from the definition. For 1.187 - monoids, \name{right-one} had to be included as an axiom, but for 1.188 - groups both \name{right-one} and \name{right-inverse} are derivable 1.189 - from the other axioms. With \name{group-right-one} derived as a 1.190 - theorem of group theory (see page~\pageref{thm:group-right-one}), we 1.191 - may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly 1.192 - as follows. 1.193 -*} 1.194 +text {* Groups are \emph{not} yet monoids directly from the 1.195 + definition. For monoids, \name{right-one} had to be included as an 1.196 + axiom, but for groups both \name{right-one} and \name{right-inverse} 1.197 + are derivable from the other axioms. With \name{group-right-one} 1.198 + derived as a theorem of group theory (see 1.199 + page~\pageref{thm:group-right-one}), we may still instantiate 1.200 + $\idt{group} \subseteq \idt{monoid}$ properly as follows. *} 1.201 1.202 instance group < monoid 1.203 - by (intro_classes, 1.204 - rule group_assoc, 1.205 - rule group_left_one, 1.206 - rule group_right_one) 1.207 + by intro_classes 1.208 + (rule group_assoc, 1.209 + rule group_left_one, 1.210 + rule group_right_one) 1.211 1.212 -text {* 1.213 - The \isacommand{instance} command actually is a version of 1.214 - \isacommand{theorem}, setting up a goal that reflects the intended 1.215 - class relation (or type constructor arity). Thus any Isar proof 1.216 - language element may be involved to establish this statement. When 1.217 - concluding the proof, the result is transformed into the intended 1.218 - type signature extension behind the scenes. 1.219 -*} 1.220 +text {* The \isacommand{instance} command actually is a version of 1.221 + \isacommand{theorem}, setting up a goal that reflects the intended 1.222 + class relation (or type constructor arity). Thus any Isar proof 1.223 + language element may be involved to establish this statement. When 1.224 + concluding the proof, the result is transformed into the intended 1.225 + type signature extension behind the scenes. *} 1.226 + 1.227 1.228 subsection {* More theorems of group theory *} 1.229 1.230 -text {* 1.231 - The one element is already uniquely determined by preserving an 1.232 - \emph{arbitrary} group element. 1.233 -*} 1.234 +text {* The one element is already uniquely determined by preserving 1.235 + an \emph{arbitrary} group element. *} 1.236 1.237 -theorem group_one_equality: "e * x = x ==> one = (e::'a::group)" 1.238 +theorem (in group) group_one_equality: 1.239 + assumes eq: "e * x = x" 1.240 + shows "1 = e" 1.241 proof - 1.242 - assume eq: "e * x = x" 1.243 - have "one = x * inverse x" 1.244 + have "1 = x * inverse x" 1.245 by (simp only: group_right_inverse) 1.246 also have "... = (e * x) * inverse x" 1.247 by (simp only: eq) 1.248 also have "... = e * (x * inverse x)" 1.249 by (simp only: group_assoc) 1.250 - also have "... = e * one" 1.251 + also have "... = e * 1" 1.252 by (simp only: group_right_inverse) 1.253 also have "... = e" 1.254 by (simp only: group_right_one) 1.255 finally show ?thesis . 1.256 qed 1.257 1.258 -text {* 1.259 - Likewise, the inverse is already determined by the cancel property. 1.260 -*} 1.261 +text {* Likewise, the inverse is already determined by the cancel property. *} 1.262 1.263 -theorem group_inverse_equality: 1.264 - "x' * x = one ==> inverse x = (x'::'a::group)" 1.265 +theorem (in group) group_inverse_equality: 1.266 + assumes eq: "x' * x = 1" 1.267 + shows "inverse x = x'" 1.268 proof - 1.269 - assume eq: "x' * x = one" 1.270 - have "inverse x = one * inverse x" 1.271 + have "inverse x = 1 * inverse x" 1.272 by (simp only: group_left_one) 1.273 also have "... = (x' * x) * inverse x" 1.274 by (simp only: eq) 1.275 also have "... = x' * (x * inverse x)" 1.276 by (simp only: group_assoc) 1.277 - also have "... = x' * one" 1.278 + also have "... = x' * 1" 1.279 by (simp only: group_right_inverse) 1.280 also have "... = x'" 1.281 by (simp only: group_right_one) 1.282 finally show ?thesis . 1.283 qed 1.284 1.285 -text {* 1.286 - The inverse operation has some further characteristic properties. 1.287 -*} 1.288 +text {* The inverse operation has some further characteristic properties. *} 1.289 1.290 -theorem group_inverse_times: 1.291 - "inverse (x * y) = inverse y * inverse (x::'a::group)" 1.292 +theorem (in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x" 1.293 proof (rule group_inverse_equality) 1.294 - show "(inverse y * inverse x) * (x * y) = one" 1.295 + show "(inverse y * inverse x) * (x * y) = 1" 1.296 proof - 1.297 have "(inverse y * inverse x) * (x * y) = 1.298 (inverse y * (inverse x * x)) * y" 1.299 by (simp only: group_assoc) 1.300 - also have "... = (inverse y * one) * y" 1.301 + also have "... = (inverse y * 1) * y" 1.302 by (simp only: group_left_inverse) 1.303 also have "... = inverse y * y" 1.304 by (simp only: group_right_one) 1.305 - also have "... = one" 1.306 + also have "... = 1" 1.307 by (simp only: group_left_inverse) 1.308 finally show ?thesis . 1.309 qed 1.310 qed 1.311 1.312 -theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)" 1.313 +theorem (in group) inverse_inverse: "inverse (inverse x) = x" 1.314 proof (rule group_inverse_equality) 1.315 show "x * inverse x = one" 1.316 by (simp only: group_right_inverse) 1.317 qed 1.318 1.319 -theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)" 1.320 +theorem (in group) inverse_inject: 1.321 + assumes eq: "inverse x = inverse y" 1.322 + shows "x = y" 1.323 proof - 1.324 - assume eq: "inverse x = inverse y" 1.325 - have "x = x * one" 1.326 + have "x = x * 1" 1.327 by (simp only: group_right_one) 1.328 also have "... = x * (inverse y * y)" 1.329 by (simp only: group_left_inverse) 1.330 @@ -254,7 +235,7 @@ 1.331 by (simp only: eq) 1.332 also have "... = (x * inverse x) * y" 1.333 by (simp only: group_assoc) 1.334 - also have "... = one * y" 1.335 + also have "... = 1 * y" 1.336 by (simp only: group_right_inverse) 1.337 also have "... = y" 1.338 by (simp only: group_left_one)