src/HOL/Isar_examples/Group.thy
author wenzelm
Sat Oct 30 20:20:48 1999 +0200 (1999-10-30)
changeset 7982 d534b897ce39
parent 7968 964b65b4e433
child 8910 981ac87f905c
permissions -rw-r--r--
improved presentation;
     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 = Main:;
     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{inv} :: \alpha \To \alpha)$ are defined as
    15  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   inv :: "'a => 'a";
    22 
    23 axclass
    24   group < times
    25   group_assoc:         "(x * y) * z = x * (y * z)"
    26   group_left_unit:     "one * x = x"
    27   group_left_inverse:  "inv x * x = one";
    28 
    29 text {*
    30  The group axioms only state the properties of left unit and inverse,
    31  the right versions may be derived as follows.
    32 *};
    33 
    34 theorem group_right_inverse: "x * inv x = (one::'a::group)";
    35 proof -;
    36   have "x * inv x = one * (x * inv x)";
    37     by (simp only: group_left_unit);
    38   also; have "... = (one * x) * inv x";
    39     by (simp only: group_assoc);
    40   also; have "... = inv (inv x) * inv x * x * inv x";
    41     by (simp only: group_left_inverse);
    42   also; have "... = inv (inv x) * (inv x * x) * inv x";
    43     by (simp only: group_assoc);
    44   also; have "... = inv (inv x) * one * inv x";
    45     by (simp only: group_left_inverse);
    46   also; have "... = inv (inv x) * (one * inv x)";
    47     by (simp only: group_assoc);
    48   also; have "... = inv (inv x) * inv x";
    49     by (simp only: group_left_unit);
    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-unit}\label{thm:group-right-unit} is now
    58  established much easier.
    59 *};
    60 
    61 theorem group_right_unit: "x * one = (x::'a::group)";
    62 proof -;
    63   have "x * one = x * (inv x * x)";
    64     by (simp only: group_left_inverse);
    65   also; have "... = x * inv 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_unit);
    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 * (inv 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 * inv 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_unit);
   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_unit:   "one * x = x"
   149   monoid_right_unit:  "x * one = x";
   150 
   151 text {*
   152  Groups are \emph{not} yet monoids directly from the definition.  For
   153  monoids, \name{right-unit} had to be included as an axiom, but for
   154  groups both \name{right-unit} and \name{right-inverse} are derivable
   155  from the other axioms.  With \name{group-right-unit} derived as a
   156  theorem of group theory (see page~\pageref{thm:group-right-unit}), we
   157  may still instantiate $\idt{group} \subset \idt{monoid}$ properly as
   158  follows.
   159 *};
   160 
   161 instance group < monoid;
   162   by (intro_classes,
   163        rule group_assoc,
   164        rule group_left_unit,
   165        rule group_right_unit);
   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 end;