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