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)