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