src/HOL/Isar_examples/Group.thy
author wenzelm
Fri Oct 15 16:44:37 1999 +0200 (1999-10-15)
changeset 7874 180364256231
parent 7800 8ee919e42174
child 7968 964b65b4e433
permissions -rw-r--r--
improved presentation;
wenzelm@6763
     1
(*  Title:      HOL/Isar_examples/Group.thy
wenzelm@6763
     2
    ID:         $Id$
wenzelm@6763
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6763
     4
*)
wenzelm@6763
     5
wenzelm@7748
     6
header {* Basic group theory *};
wenzelm@7748
     7
wenzelm@6763
     8
theory Group = Main:;
wenzelm@6763
     9
wenzelm@7874
    10
subsection {* Groups and calculational reasoning *}; 
wenzelm@6784
    11
wenzelm@6784
    12
text {*
wenzelm@7874
    13
 We define an axiomatic type class of groups over signature $({\times}
wenzelm@7874
    14
 :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha, \idt{inv} ::
wenzelm@7874
    15
 \alpha \To \alpha)$.  Note that the parent class $\idt{times}$ is
wenzelm@7874
    16
 provided by the basic HOL theory.
wenzelm@6784
    17
*};
wenzelm@6763
    18
wenzelm@6763
    19
consts
wenzelm@6784
    20
  one :: "'a"
wenzelm@6784
    21
  inv :: "'a => 'a";
wenzelm@6763
    22
wenzelm@6763
    23
axclass
wenzelm@6763
    24
  group < times
wenzelm@6793
    25
  group_assoc:         "(x * y) * z = x * (y * z)"
wenzelm@6793
    26
  group_left_unit:     "one * x = x"
wenzelm@6793
    27
  group_left_inverse:  "inv x * x = one";
wenzelm@6763
    28
wenzelm@6784
    29
text {*
wenzelm@6793
    30
 The group axioms only state the properties of left unit and inverse,
wenzelm@7874
    31
 the right versions may be derived as follows.
wenzelm@6784
    32
*};
wenzelm@6763
    33
wenzelm@6793
    34
theorem group_right_inverse: "x * inv x = (one::'a::group)";
wenzelm@7133
    35
proof -;
wenzelm@6784
    36
  have "x * inv x = one * (x * inv x)";
wenzelm@6908
    37
    by (simp only: group_left_unit);
wenzelm@6784
    38
  also; have "... = (one * x) * inv x";
wenzelm@6908
    39
    by (simp only: group_assoc);
wenzelm@6784
    40
  also; have "... = inv (inv x) * inv x * x * inv x";
wenzelm@6908
    41
    by (simp only: group_left_inverse);
wenzelm@6784
    42
  also; have "... = inv (inv x) * (inv x * x) * inv x";
wenzelm@6908
    43
    by (simp only: group_assoc);
wenzelm@6784
    44
  also; have "... = inv (inv x) * one * inv x";
wenzelm@6908
    45
    by (simp only: group_left_inverse);
wenzelm@6784
    46
  also; have "... = inv (inv x) * (one * inv x)";
wenzelm@6908
    47
    by (simp only: group_assoc);
wenzelm@6784
    48
  also; have "... = inv (inv x) * inv x";
wenzelm@6908
    49
    by (simp only: group_left_unit);
wenzelm@6784
    50
  also; have "... = one";
wenzelm@6908
    51
    by (simp only: group_left_inverse);
wenzelm@7480
    52
  finally; show ?thesis; .;
wenzelm@6784
    53
qed;
wenzelm@6763
    54
wenzelm@6784
    55
text {*
wenzelm@7748
    56
 With \name{group-right-inverse} already at our disposal,
wenzelm@7874
    57
 \name{group-right-unit} is now obtained much easier.
wenzelm@6784
    58
*};
wenzelm@6763
    59
wenzelm@6793
    60
theorem group_right_unit: "x * one = (x::'a::group)";
wenzelm@7133
    61
proof -;
wenzelm@6784
    62
  have "x * one = x * (inv x * x)";
wenzelm@6908
    63
    by (simp only: group_left_inverse);
wenzelm@6784
    64
  also; have "... = x * inv x * x";
wenzelm@6908
    65
    by (simp only: group_assoc);
wenzelm@6784
    66
  also; have "... = one * x";
wenzelm@6908
    67
    by (simp only: group_right_inverse);
wenzelm@6784
    68
  also; have "... = x";
wenzelm@6908
    69
    by (simp only: group_left_unit);
wenzelm@7480
    70
  finally; show ?thesis; .;
wenzelm@6784
    71
qed;
wenzelm@6763
    72
wenzelm@6784
    73
text {*
wenzelm@7874
    74
 \medskip The calculational proof style above follows typical
wenzelm@7874
    75
 presentations given in any introductory course on algebra.  The basic
wenzelm@7874
    76
 technique is to form a transitive chain of equations, which in turn
wenzelm@7874
    77
 are established by simplifying with appropriate rules.  The low-level
wenzelm@7874
    78
 logical parts of equational reasoning are left implicit.
wenzelm@6784
    79
wenzelm@7874
    80
 Note that ``$\dots$'' is just a special term variable that happens to
wenzelm@7874
    81
 be bound automatically to the argument\footnote{The argument of a
wenzelm@7874
    82
 curried infix expression happens to be its right-hand side.} of the
wenzelm@7874
    83
 last fact achieved by any local assumption or proven statement.  In
wenzelm@7874
    84
 contrast to $\var{thesis}$, the ``$\dots$'' variable is bound
wenzelm@7874
    85
 \emph{after} the proof is finished.
wenzelm@7874
    86
wenzelm@7874
    87
 There are only two separate Isar language elements for calculational
wenzelm@7874
    88
 proofs: ``\isakeyword{also}'' for initial or intermediate
wenzelm@7874
    89
 calculational steps, and ``\isakeyword{finally}'' for exhibiting the
wenzelm@7874
    90
 result of a calculation.  These constructs are not hardwired into
wenzelm@7874
    91
 Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
wenzelm@7874
    92
 Expanding the \isakeyword{also} and \isakeyword{finally} derived
wenzelm@7874
    93
 language elements, calculations may be simulated as demonstrated
wenzelm@7874
    94
 below.
wenzelm@6784
    95
*};
wenzelm@6784
    96
wenzelm@6793
    97
theorem "x * one = (x::'a::group)";
wenzelm@7133
    98
proof -;
wenzelm@6784
    99
  have "x * one = x * (inv x * x)";
wenzelm@6908
   100
    by (simp only: group_left_inverse);
wenzelm@6763
   101
wenzelm@7433
   102
  note calculation = this
wenzelm@6793
   103
    -- {* first calculational step: init calculation register *};
wenzelm@6763
   104
wenzelm@6784
   105
  have "... = x * inv x * x";
wenzelm@6908
   106
    by (simp only: group_assoc);
wenzelm@6763
   107
wenzelm@7433
   108
  note calculation = trans [OF calculation this]
wenzelm@6784
   109
    -- {* general calculational step: compose with transitivity rule *};
wenzelm@6763
   110
wenzelm@6763
   111
  have "... = one * x";
wenzelm@6908
   112
    by (simp only: group_right_inverse);
wenzelm@6763
   113
wenzelm@7433
   114
  note calculation = trans [OF calculation this]
wenzelm@6784
   115
    -- {* general calculational step: compose with transitivity rule *};
wenzelm@6763
   116
wenzelm@6763
   117
  have "... = x";
wenzelm@6908
   118
    by (simp only: group_left_unit);
wenzelm@6763
   119
wenzelm@7433
   120
  note calculation = trans [OF calculation this]
wenzelm@6784
   121
    -- {* final calculational step: compose with transitivity rule ... *};
wenzelm@6784
   122
  from calculation
wenzelm@7874
   123
    -- {* ... and pick up the final result *};
wenzelm@6763
   124
wenzelm@7480
   125
  show ?thesis; .;
wenzelm@6763
   126
qed;
wenzelm@6763
   127
wenzelm@7874
   128
text {*
wenzelm@7874
   129
 Note that this scheme of calculations is not restricted to plain
wenzelm@7874
   130
 transitivity.  Rules like anti-symmetry, or even forward and backward
wenzelm@7874
   131
 substitution work as well.  For the actual \isacommand{also} and
wenzelm@7874
   132
 \isacommand{finally} commands, Isabelle/Isar maintains separate
wenzelm@7874
   133
 context information of ``transitivity'' rules.  Rule selection takes
wenzelm@7874
   134
 place automatically by higher-order unification.
wenzelm@7874
   135
*};
wenzelm@7874
   136
wenzelm@6763
   137
wenzelm@7761
   138
subsection {* Groups as monoids *};
wenzelm@6793
   139
wenzelm@6793
   140
text {*
wenzelm@7874
   141
 Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,
wenzelm@7874
   142
 \idt{one} :: \alpha)$ are defined like this.
wenzelm@6793
   143
*};
wenzelm@6793
   144
wenzelm@6793
   145
axclass monoid < times
wenzelm@6793
   146
  monoid_assoc:       "(x * y) * z = x * (y * z)"
wenzelm@6793
   147
  monoid_left_unit:   "one * x = x"
wenzelm@6793
   148
  monoid_right_unit:  "x * one = x";
wenzelm@6793
   149
wenzelm@6793
   150
text {*
wenzelm@7748
   151
 Groups are \emph{not} yet monoids directly from the definition.  For
wenzelm@7748
   152
 monoids, \name{right-unit} had to be included as an axiom, but for
wenzelm@7748
   153
 groups both \name{right-unit} and \name{right-inverse} are
wenzelm@7748
   154
 derivable from the other axioms.  With \name{group-right-unit}
wenzelm@7748
   155
 derived as a theorem of group theory (see above), we may still
wenzelm@7748
   156
 instantiate $\idt{group} \subset \idt{monoid}$ properly as follows.
wenzelm@6793
   157
*};
wenzelm@6793
   158
wenzelm@6793
   159
instance group < monoid;
wenzelm@7356
   160
  by (intro_classes,
wenzelm@6793
   161
       rule group_assoc,
wenzelm@6793
   162
       rule group_left_unit,
wenzelm@6793
   163
       rule group_right_unit);
wenzelm@6793
   164
wenzelm@7874
   165
text {*
wenzelm@7874
   166
 The \isacommand{instance} command actually is a version of
wenzelm@7874
   167
 \isacommand{theorem}, setting up a goal that reflects the intended
wenzelm@7874
   168
 class relation (or type constructor arity).  Thus any Isar proof
wenzelm@7874
   169
 language element may be involved to establish this statement.  When
wenzelm@7874
   170
 concluding the proof, the result is transformed into the original
wenzelm@7874
   171
 type signature extension behind the scenes.
wenzelm@7874
   172
*};
wenzelm@7874
   173
wenzelm@6763
   174
end;