src/HOL/Isar_examples/Group.thy
author wenzelm
Tue Oct 03 18:56:44 2000 +0200 (2000-10-03)
changeset 10141 964d9dc47041
parent 10007 64bf7da1994a
child 16417 9bc16273c2d4
permissions -rw-r--r--
tuned names;
added more theorems of group theory (from old AxClasses/Group/Group.ML);
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@10141
    14
 \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined
wenzelm@10141
    15
 as 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@10141
    21
  inverse :: "'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@10141
    26
  group_left_one:      "one * x = x"
wenzelm@10141
    27
  group_left_inverse:  "inverse x * x = one"
wenzelm@6763
    28
wenzelm@6784
    29
text {*
wenzelm@10141
    30
 The group axioms only state the properties of left one and inverse,
wenzelm@7874
    31
 the right versions may be derived as follows.
wenzelm@10007
    32
*}
wenzelm@6763
    33
wenzelm@10141
    34
theorem group_right_inverse: "x * inverse x = (one::'a::group)"
wenzelm@10007
    35
proof -
wenzelm@10141
    36
  have "x * inverse x = one * (x * inverse x)"
wenzelm@10141
    37
    by (simp only: group_left_one)
wenzelm@10141
    38
  also have "... = one * x * inverse x"
wenzelm@10007
    39
    by (simp only: group_assoc)
wenzelm@10141
    40
  also have "... = inverse (inverse x) * inverse x * x * inverse x"
wenzelm@10007
    41
    by (simp only: group_left_inverse)
wenzelm@10141
    42
  also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
wenzelm@10007
    43
    by (simp only: group_assoc)
wenzelm@10141
    44
  also have "... = inverse (inverse x) * one * inverse x"
wenzelm@10007
    45
    by (simp only: group_left_inverse)
wenzelm@10141
    46
  also have "... = inverse (inverse x) * (one * inverse x)"
wenzelm@10007
    47
    by (simp only: group_assoc)
wenzelm@10141
    48
  also have "... = inverse (inverse x) * inverse x"
wenzelm@10141
    49
    by (simp only: group_left_one)
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@10141
    57
 \name{group-right-one}\label{thm:group-right-one} is now established
wenzelm@10141
    58
 much easier.
wenzelm@10007
    59
*}
wenzelm@6763
    60
wenzelm@10141
    61
theorem group_right_one: "x * one = (x::'a::group)"
wenzelm@10007
    62
proof -
wenzelm@10141
    63
  have "x * one = x * (inverse x * x)"
wenzelm@10007
    64
    by (simp only: group_left_inverse)
wenzelm@10141
    65
  also have "... = x * inverse 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@10141
    70
    by (simp only: group_left_one)
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@10141
   100
  have "x * one = x * (inverse 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@10141
   106
  have "... = x * inverse 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@10141
   119
    by (simp only: group_left_one)
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@10141
   148
  monoid_left_one:   "one * x = x"
wenzelm@10141
   149
  monoid_right_one:  "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@10141
   153
 monoids, \name{right-one} had to be included as an axiom, but for
wenzelm@10141
   154
 groups both \name{right-one} and \name{right-inverse} are derivable
wenzelm@10141
   155
 from the other axioms.  With \name{group-right-one} derived as a
wenzelm@10141
   156
 theorem of group theory (see page~\pageref{thm:group-right-one}), we
wenzelm@10141
   157
 may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly
wenzelm@10141
   158
 as 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@10141
   164
       rule group_left_one,
wenzelm@10141
   165
       rule group_right_one)
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@10141
   176
subsection {* More theorems of group theory *}
wenzelm@10141
   177
wenzelm@10141
   178
text {*
wenzelm@10141
   179
 The one element is already uniquely determined by preserving an
wenzelm@10141
   180
 \emph{arbitrary} group element.
wenzelm@10141
   181
*}
wenzelm@10141
   182
wenzelm@10141
   183
theorem group_one_equality: "e * x = x ==> one = (e::'a::group)"
wenzelm@10141
   184
proof -
wenzelm@10141
   185
  assume eq: "e * x = x"
wenzelm@10141
   186
  have "one = x * inverse x"
wenzelm@10141
   187
    by (simp only: group_right_inverse)
wenzelm@10141
   188
  also have "... = (e * x) * inverse x"
wenzelm@10141
   189
    by (simp only: eq)
wenzelm@10141
   190
  also have "... = e * (x * inverse x)"
wenzelm@10141
   191
    by (simp only: group_assoc)
wenzelm@10141
   192
  also have "... = e * one"
wenzelm@10141
   193
    by (simp only: group_right_inverse)
wenzelm@10141
   194
  also have "... = e"
wenzelm@10141
   195
    by (simp only: group_right_one)
wenzelm@10141
   196
  finally show ?thesis .
wenzelm@10141
   197
qed
wenzelm@10141
   198
wenzelm@10141
   199
text {*
wenzelm@10141
   200
 Likewise, the inverse is already determined by the cancel property.
wenzelm@10141
   201
*}
wenzelm@10141
   202
wenzelm@10141
   203
theorem group_inverse_equality:
wenzelm@10141
   204
  "x' * x = one ==> inverse x = (x'::'a::group)"
wenzelm@10141
   205
proof -
wenzelm@10141
   206
  assume eq: "x' * x = one"
wenzelm@10141
   207
  have "inverse x = one * inverse x"
wenzelm@10141
   208
    by (simp only: group_left_one)
wenzelm@10141
   209
  also have "... = (x' * x) * inverse x"
wenzelm@10141
   210
    by (simp only: eq)
wenzelm@10141
   211
  also have "... = x' * (x * inverse x)"
wenzelm@10141
   212
    by (simp only: group_assoc)
wenzelm@10141
   213
  also have "... = x' * one"
wenzelm@10141
   214
    by (simp only: group_right_inverse)
wenzelm@10141
   215
  also have "... = x'"
wenzelm@10141
   216
    by (simp only: group_right_one)
wenzelm@10141
   217
  finally show ?thesis .
wenzelm@10141
   218
qed
wenzelm@10141
   219
wenzelm@10141
   220
text {*
wenzelm@10141
   221
 The inverse operation has some further characteristic properties.
wenzelm@10141
   222
*}
wenzelm@10141
   223
wenzelm@10141
   224
theorem group_inverse_times:
wenzelm@10141
   225
  "inverse (x * y) = inverse y * inverse (x::'a::group)"
wenzelm@10141
   226
proof (rule group_inverse_equality)
wenzelm@10141
   227
  show "(inverse y * inverse x) * (x * y) = one"
wenzelm@10141
   228
  proof -
wenzelm@10141
   229
    have "(inverse y * inverse x) * (x * y) =
wenzelm@10141
   230
        (inverse y * (inverse x * x)) * y"
wenzelm@10141
   231
      by (simp only: group_assoc)
wenzelm@10141
   232
    also have "... = (inverse y * one) * y"
wenzelm@10141
   233
      by (simp only: group_left_inverse)
wenzelm@10141
   234
    also have "... = inverse y * y"
wenzelm@10141
   235
      by (simp only: group_right_one)
wenzelm@10141
   236
    also have "... = one"
wenzelm@10141
   237
      by (simp only: group_left_inverse)
wenzelm@10141
   238
    finally show ?thesis .
wenzelm@10141
   239
  qed
wenzelm@10141
   240
qed
wenzelm@10141
   241
wenzelm@10141
   242
theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)"
wenzelm@10141
   243
proof (rule group_inverse_equality)
wenzelm@10141
   244
  show "x * inverse x = one"
wenzelm@10141
   245
    by (simp only: group_right_inverse)
wenzelm@10141
   246
qed
wenzelm@10141
   247
wenzelm@10141
   248
theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)"
wenzelm@10141
   249
proof -
wenzelm@10141
   250
  assume eq: "inverse x = inverse y"
wenzelm@10141
   251
  have "x = x * one"
wenzelm@10141
   252
    by (simp only: group_right_one)
wenzelm@10141
   253
  also have "... = x * (inverse y * y)"
wenzelm@10141
   254
    by (simp only: group_left_inverse)
wenzelm@10141
   255
  also have "... = x * (inverse x * y)"
wenzelm@10141
   256
    by (simp only: eq)
wenzelm@10141
   257
  also have "... = (x * inverse x) * y"
wenzelm@10141
   258
    by (simp only: group_assoc)
wenzelm@10141
   259
  also have "... = one * y"
wenzelm@10141
   260
    by (simp only: group_right_inverse)
wenzelm@10141
   261
  also have "... = y"
wenzelm@10141
   262
    by (simp only: group_left_one)
wenzelm@10141
   263
  finally show ?thesis .
wenzelm@10141
   264
qed
wenzelm@10141
   265
wenzelm@10141
   266
end