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)