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;