src/HOL/Isar_Examples/Group.thy
author haftmann
Wed Jun 30 16:46:44 2010 +0200 (2010-06-30)
changeset 37659 14cabf5fa710
parent 35317 d57da4abb47d
child 37671 fa53d267dab3
permissions -rw-r--r--
more speaking names
     1 (*  Title:      HOL/Isar_Examples/Group.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 header {* Basic group theory *}
     6 
     7 theory Group
     8 imports Main
     9 begin
    10 
    11 subsection {* Groups and calculational reasoning *} 
    12 
    13 text {*
    14  Groups over signature $({\times} :: \alpha \To \alpha \To \alpha,
    15  \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined
    16  as an axiomatic type class as follows.  Note that the parent class
    17  $\idt{times}$ is provided by the basic HOL theory.
    18 *}
    19 
    20 notation Groups.one ("one")
    21 
    22 class group = times + one + inverse +
    23   assumes group_assoc:         "(x * y) * z = x * (y * z)"
    24   assumes group_left_one:      "one * x = x"
    25   assumes group_left_inverse:  "inverse x * x = one"
    26 
    27 text {*
    28  The group axioms only state the properties of left one and inverse,
    29  the right versions may be derived as follows.
    30 *}
    31 
    32 theorem group_right_inverse: "x * inverse x = (one::'a::group)"
    33 proof -
    34   have "x * inverse x = one * (x * inverse x)"
    35     by (simp only: group_left_one)
    36   also have "... = one * x * inverse x"
    37     by (simp only: group_assoc)
    38   also have "... = inverse (inverse x) * inverse x * x * inverse x"
    39     by (simp only: group_left_inverse)
    40   also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
    41     by (simp only: group_assoc)
    42   also have "... = inverse (inverse x) * one * inverse x"
    43     by (simp only: group_left_inverse)
    44   also have "... = inverse (inverse x) * (one * inverse x)"
    45     by (simp only: group_assoc)
    46   also have "... = inverse (inverse x) * inverse x"
    47     by (simp only: group_left_one)
    48   also have "... = one"
    49     by (simp only: group_left_inverse)
    50   finally show ?thesis .
    51 qed
    52 
    53 text {*
    54  With \name{group-right-inverse} already available,
    55  \name{group-right-one}\label{thm:group-right-one} is now established
    56  much easier.
    57 *}
    58 
    59 theorem group_right_one: "x * one = (x::'a::group)"
    60 proof -
    61   have "x * one = x * (inverse x * x)"
    62     by (simp only: group_left_inverse)
    63   also have "... = x * inverse x * x"
    64     by (simp only: group_assoc)
    65   also have "... = one * x"
    66     by (simp only: group_right_inverse)
    67   also have "... = x"
    68     by (simp only: group_left_one)
    69   finally show ?thesis .
    70 qed
    71 
    72 text {*
    73  \medskip The calculational proof style above follows typical
    74  presentations given in any introductory course on algebra.  The basic
    75  technique is to form a transitive chain of equations, which in turn
    76  are established by simplifying with appropriate rules.  The low-level
    77  logical details of equational reasoning are left implicit.
    78 
    79  Note that ``$\dots$'' is just a special term variable that is bound
    80  automatically to the argument\footnote{The argument of a curried
    81  infix expression happens to be its right-hand side.} of the last fact
    82  achieved by any local assumption or proven statement.  In contrast to
    83  $\var{thesis}$, the ``$\dots$'' variable is bound \emph{after} the
    84  proof is finished, though.
    85 
    86  There are only two separate Isar language elements for calculational
    87  proofs: ``\isakeyword{also}'' for initial or intermediate
    88  calculational steps, and ``\isakeyword{finally}'' for exhibiting the
    89  result of a calculation.  These constructs are not hardwired into
    90  Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
    91  Expanding the \isakeyword{also} and \isakeyword{finally} derived
    92  language elements, calculations may be simulated by hand as
    93  demonstrated below.
    94 *}
    95 
    96 theorem "x * one = (x::'a::group)"
    97 proof -
    98   have "x * one = x * (inverse x * x)"
    99     by (simp only: group_left_inverse)
   100 
   101   note calculation = this
   102     -- {* first calculational step: init calculation register *}
   103 
   104   have "... = x * inverse x * x"
   105     by (simp only: group_assoc)
   106 
   107   note calculation = trans [OF calculation this]
   108     -- {* general calculational step: compose with transitivity rule *}
   109 
   110   have "... = one * x"
   111     by (simp only: group_right_inverse)
   112 
   113   note calculation = trans [OF calculation this]
   114     -- {* general calculational step: compose with transitivity rule *}
   115 
   116   have "... = x"
   117     by (simp only: group_left_one)
   118 
   119   note calculation = trans [OF calculation this]
   120     -- {* final calculational step: compose with transitivity rule ... *}
   121   from calculation
   122     -- {* ... and pick up the final result *}
   123 
   124   show ?thesis .
   125 qed
   126 
   127 text {*
   128  Note that this scheme of calculations is not restricted to plain
   129  transitivity.  Rules like anti-symmetry, or even forward and backward
   130  substitution work as well.  For the actual implementation of
   131  \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
   132  separate context information of ``transitivity'' rules.  Rule
   133  selection takes place automatically by higher-order unification.
   134 *}
   135 
   136 
   137 subsection {* Groups as monoids *}
   138 
   139 text {*
   140  Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,
   141  \idt{one} :: \alpha)$ are defined like this.
   142 *}
   143 
   144 class monoid = times + one +
   145   assumes monoid_assoc:       "(x * y) * z = x * (y * z)"
   146   assumes monoid_left_one:   "one * x = x"
   147   assumes monoid_right_one:  "x * one = x"
   148 
   149 text {*
   150  Groups are \emph{not} yet monoids directly from the definition.  For
   151  monoids, \name{right-one} had to be included as an axiom, but for
   152  groups both \name{right-one} and \name{right-inverse} are derivable
   153  from the other axioms.  With \name{group-right-one} derived as a
   154  theorem of group theory (see page~\pageref{thm:group-right-one}), we
   155  may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly
   156  as follows.
   157 *}
   158 
   159 instance group < monoid
   160   by (intro_classes,
   161        rule group_assoc,
   162        rule group_left_one,
   163        rule group_right_one)
   164 
   165 text {*
   166  The \isacommand{instance} command actually is a version of
   167  \isacommand{theorem}, setting up a goal that reflects the intended
   168  class relation (or type constructor arity).  Thus any Isar proof
   169  language element may be involved to establish this statement.  When
   170  concluding the proof, the result is transformed into the intended
   171  type signature extension behind the scenes.
   172 *}
   173 
   174 subsection {* More theorems of group theory *}
   175 
   176 text {*
   177  The one element is already uniquely determined by preserving an
   178  \emph{arbitrary} group element.
   179 *}
   180 
   181 theorem group_one_equality: "e * x = x ==> one = (e::'a::group)"
   182 proof -
   183   assume eq: "e * x = x"
   184   have "one = x * inverse x"
   185     by (simp only: group_right_inverse)
   186   also have "... = (e * x) * inverse x"
   187     by (simp only: eq)
   188   also have "... = e * (x * inverse x)"
   189     by (simp only: group_assoc)
   190   also have "... = e * one"
   191     by (simp only: group_right_inverse)
   192   also have "... = e"
   193     by (simp only: group_right_one)
   194   finally show ?thesis .
   195 qed
   196 
   197 text {*
   198  Likewise, the inverse is already determined by the cancel property.
   199 *}
   200 
   201 theorem group_inverse_equality:
   202   "x' * x = one ==> inverse x = (x'::'a::group)"
   203 proof -
   204   assume eq: "x' * x = one"
   205   have "inverse x = one * inverse x"
   206     by (simp only: group_left_one)
   207   also have "... = (x' * x) * inverse x"
   208     by (simp only: eq)
   209   also have "... = x' * (x * inverse x)"
   210     by (simp only: group_assoc)
   211   also have "... = x' * one"
   212     by (simp only: group_right_inverse)
   213   also have "... = x'"
   214     by (simp only: group_right_one)
   215   finally show ?thesis .
   216 qed
   217 
   218 text {*
   219  The inverse operation has some further characteristic properties.
   220 *}
   221 
   222 theorem group_inverse_times:
   223   "inverse (x * y) = inverse y * inverse (x::'a::group)"
   224 proof (rule group_inverse_equality)
   225   show "(inverse y * inverse x) * (x * y) = one"
   226   proof -
   227     have "(inverse y * inverse x) * (x * y) =
   228         (inverse y * (inverse x * x)) * y"
   229       by (simp only: group_assoc)
   230     also have "... = (inverse y * one) * y"
   231       by (simp only: group_left_inverse)
   232     also have "... = inverse y * y"
   233       by (simp only: group_right_one)
   234     also have "... = one"
   235       by (simp only: group_left_inverse)
   236     finally show ?thesis .
   237   qed
   238 qed
   239 
   240 theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)"
   241 proof (rule group_inverse_equality)
   242   show "x * inverse x = one"
   243     by (simp only: group_right_inverse)
   244 qed
   245 
   246 theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)"
   247 proof -
   248   assume eq: "inverse x = inverse y"
   249   have "x = x * one"
   250     by (simp only: group_right_one)
   251   also have "... = x * (inverse y * y)"
   252     by (simp only: group_left_inverse)
   253   also have "... = x * (inverse x * y)"
   254     by (simp only: eq)
   255   also have "... = (x * inverse x) * y"
   256     by (simp only: group_assoc)
   257   also have "... = one * y"
   258     by (simp only: group_right_inverse)
   259   also have "... = y"
   260     by (simp only: group_left_one)
   261   finally show ?thesis .
   262 qed
   263 
   264 end