src/HOL/Isar_Examples/Group.thy
author haftmann
Tue Feb 23 10:11:15 2010 +0100 (2010-02-23)
changeset 35317 d57da4abb47d
parent 33026 8f35633c4922
child 37671 fa53d267dab3
permissions -rw-r--r--
dropped axclass; dropped Id
wenzelm@33026
     1
(*  Title:      HOL/Isar_Examples/Group.thy
wenzelm@6763
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6763
     3
*)
wenzelm@6763
     4
wenzelm@10007
     5
header {* Basic group theory *}
wenzelm@7748
     6
wenzelm@31758
     7
theory Group
wenzelm@31758
     8
imports Main
wenzelm@31758
     9
begin
wenzelm@6763
    10
wenzelm@10007
    11
subsection {* Groups and calculational reasoning *} 
wenzelm@6784
    12
wenzelm@6784
    13
text {*
wenzelm@7968
    14
 Groups over signature $({\times} :: \alpha \To \alpha \To \alpha,
wenzelm@10141
    15
 \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined
wenzelm@10141
    16
 as an axiomatic type class as follows.  Note that the parent class
wenzelm@7968
    17
 $\idt{times}$ is provided by the basic HOL theory.
wenzelm@10007
    18
*}
wenzelm@6763
    19
haftmann@35317
    20
notation Groups.one ("one")
wenzelm@6763
    21
haftmann@35317
    22
class group = times + one + inverse +
haftmann@35317
    23
  assumes group_assoc:         "(x * y) * z = x * (y * z)"
haftmann@35317
    24
  assumes group_left_one:      "one * x = x"
haftmann@35317
    25
  assumes group_left_inverse:  "inverse x * x = one"
wenzelm@6763
    26
wenzelm@6784
    27
text {*
wenzelm@10141
    28
 The group axioms only state the properties of left one and inverse,
wenzelm@7874
    29
 the right versions may be derived as follows.
wenzelm@10007
    30
*}
wenzelm@6763
    31
wenzelm@10141
    32
theorem group_right_inverse: "x * inverse x = (one::'a::group)"
wenzelm@10007
    33
proof -
wenzelm@10141
    34
  have "x * inverse x = one * (x * inverse x)"
wenzelm@10141
    35
    by (simp only: group_left_one)
wenzelm@10141
    36
  also have "... = one * x * inverse x"
wenzelm@10007
    37
    by (simp only: group_assoc)
wenzelm@10141
    38
  also have "... = inverse (inverse x) * inverse x * x * inverse x"
wenzelm@10007
    39
    by (simp only: group_left_inverse)
wenzelm@10141
    40
  also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
wenzelm@10007
    41
    by (simp only: group_assoc)
wenzelm@10141
    42
  also have "... = inverse (inverse x) * one * inverse x"
wenzelm@10007
    43
    by (simp only: group_left_inverse)
wenzelm@10141
    44
  also have "... = inverse (inverse x) * (one * inverse x)"
wenzelm@10007
    45
    by (simp only: group_assoc)
wenzelm@10141
    46
  also have "... = inverse (inverse x) * inverse x"
wenzelm@10141
    47
    by (simp only: group_left_one)
wenzelm@10007
    48
  also have "... = one"
wenzelm@10007
    49
    by (simp only: group_left_inverse)
wenzelm@10007
    50
  finally show ?thesis .
wenzelm@10007
    51
qed
wenzelm@6763
    52
wenzelm@6784
    53
text {*
wenzelm@7982
    54
 With \name{group-right-inverse} already available,
wenzelm@10141
    55
 \name{group-right-one}\label{thm:group-right-one} is now established
wenzelm@10141
    56
 much easier.
wenzelm@10007
    57
*}
wenzelm@6763
    58
wenzelm@10141
    59
theorem group_right_one: "x * one = (x::'a::group)"
wenzelm@10007
    60
proof -
wenzelm@10141
    61
  have "x * one = x * (inverse x * x)"
wenzelm@10007
    62
    by (simp only: group_left_inverse)
wenzelm@10141
    63
  also have "... = x * inverse x * x"
wenzelm@10007
    64
    by (simp only: group_assoc)
wenzelm@10007
    65
  also have "... = one * x"
wenzelm@10007
    66
    by (simp only: group_right_inverse)
wenzelm@10007
    67
  also have "... = x"
wenzelm@10141
    68
    by (simp only: group_left_one)
wenzelm@10007
    69
  finally show ?thesis .
wenzelm@10007
    70
qed
wenzelm@6763
    71
wenzelm@6784
    72
text {*
wenzelm@7874
    73
 \medskip The calculational proof style above follows typical
wenzelm@7874
    74
 presentations given in any introductory course on algebra.  The basic
wenzelm@7874
    75
 technique is to form a transitive chain of equations, which in turn
wenzelm@7874
    76
 are established by simplifying with appropriate rules.  The low-level
wenzelm@7982
    77
 logical details of equational reasoning are left implicit.
wenzelm@6784
    78
wenzelm@7982
    79
 Note that ``$\dots$'' is just a special term variable that is bound
wenzelm@7982
    80
 automatically to the argument\footnote{The argument of a curried
wenzelm@7982
    81
 infix expression happens to be its right-hand side.} of the last fact
wenzelm@7982
    82
 achieved by any local assumption or proven statement.  In contrast to
wenzelm@7982
    83
 $\var{thesis}$, the ``$\dots$'' variable is bound \emph{after} the
wenzelm@7982
    84
 proof is finished, though.
wenzelm@7874
    85
wenzelm@7874
    86
 There are only two separate Isar language elements for calculational
wenzelm@7874
    87
 proofs: ``\isakeyword{also}'' for initial or intermediate
wenzelm@7874
    88
 calculational steps, and ``\isakeyword{finally}'' for exhibiting the
wenzelm@7874
    89
 result of a calculation.  These constructs are not hardwired into
wenzelm@7874
    90
 Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
wenzelm@7874
    91
 Expanding the \isakeyword{also} and \isakeyword{finally} derived
wenzelm@7982
    92
 language elements, calculations may be simulated by hand as
wenzelm@7982
    93
 demonstrated below.
wenzelm@10007
    94
*}
wenzelm@6784
    95
wenzelm@10007
    96
theorem "x * one = (x::'a::group)"
wenzelm@10007
    97
proof -
wenzelm@10141
    98
  have "x * one = x * (inverse x * x)"
wenzelm@10007
    99
    by (simp only: group_left_inverse)
wenzelm@6763
   100
wenzelm@7433
   101
  note calculation = this
wenzelm@10007
   102
    -- {* first calculational step: init calculation register *}
wenzelm@6763
   103
wenzelm@10141
   104
  have "... = x * inverse x * x"
wenzelm@10007
   105
    by (simp only: group_assoc)
wenzelm@6763
   106
wenzelm@7433
   107
  note calculation = trans [OF calculation this]
wenzelm@10007
   108
    -- {* general calculational step: compose with transitivity rule *}
wenzelm@6763
   109
wenzelm@10007
   110
  have "... = one * x"
wenzelm@10007
   111
    by (simp only: group_right_inverse)
wenzelm@6763
   112
wenzelm@7433
   113
  note calculation = trans [OF calculation this]
wenzelm@10007
   114
    -- {* general calculational step: compose with transitivity rule *}
wenzelm@6763
   115
wenzelm@10007
   116
  have "... = x"
wenzelm@10141
   117
    by (simp only: group_left_one)
wenzelm@6763
   118
wenzelm@7433
   119
  note calculation = trans [OF calculation this]
wenzelm@10007
   120
    -- {* final calculational step: compose with transitivity rule ... *}
wenzelm@6784
   121
  from calculation
wenzelm@10007
   122
    -- {* ... and pick up the final result *}
wenzelm@6763
   123
wenzelm@10007
   124
  show ?thesis .
wenzelm@10007
   125
qed
wenzelm@6763
   126
wenzelm@7874
   127
text {*
wenzelm@7874
   128
 Note that this scheme of calculations is not restricted to plain
wenzelm@7874
   129
 transitivity.  Rules like anti-symmetry, or even forward and backward
wenzelm@7982
   130
 substitution work as well.  For the actual implementation of
wenzelm@7982
   131
 \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
wenzelm@7982
   132
 separate context information of ``transitivity'' rules.  Rule
wenzelm@7982
   133
 selection takes place automatically by higher-order unification.
wenzelm@10007
   134
*}
wenzelm@7874
   135
wenzelm@6763
   136
wenzelm@10007
   137
subsection {* Groups as monoids *}
wenzelm@6793
   138
wenzelm@6793
   139
text {*
wenzelm@7874
   140
 Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,
wenzelm@7874
   141
 \idt{one} :: \alpha)$ are defined like this.
wenzelm@10007
   142
*}
wenzelm@6793
   143
haftmann@35317
   144
class monoid = times + one +
haftmann@35317
   145
  assumes monoid_assoc:       "(x * y) * z = x * (y * z)"
haftmann@35317
   146
  assumes monoid_left_one:   "one * x = x"
haftmann@35317
   147
  assumes monoid_right_one:  "x * one = x"
wenzelm@6793
   148
wenzelm@6793
   149
text {*
wenzelm@7748
   150
 Groups are \emph{not} yet monoids directly from the definition.  For
wenzelm@10141
   151
 monoids, \name{right-one} had to be included as an axiom, but for
wenzelm@10141
   152
 groups both \name{right-one} and \name{right-inverse} are derivable
wenzelm@10141
   153
 from the other axioms.  With \name{group-right-one} derived as a
wenzelm@10141
   154
 theorem of group theory (see page~\pageref{thm:group-right-one}), we
wenzelm@10141
   155
 may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly
wenzelm@10141
   156
 as follows.
wenzelm@10007
   157
*}
wenzelm@6793
   158
wenzelm@10007
   159
instance group < monoid
wenzelm@7356
   160
  by (intro_classes,
wenzelm@6793
   161
       rule group_assoc,
wenzelm@10141
   162
       rule group_left_one,
wenzelm@10141
   163
       rule group_right_one)
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@7982
   170
 concluding the proof, the result is transformed into the intended
wenzelm@7874
   171
 type signature extension behind the scenes.
wenzelm@10007
   172
*}
wenzelm@7874
   173
wenzelm@10141
   174
subsection {* More theorems of group theory *}
wenzelm@10141
   175
wenzelm@10141
   176
text {*
wenzelm@10141
   177
 The one element is already uniquely determined by preserving an
wenzelm@10141
   178
 \emph{arbitrary} group element.
wenzelm@10141
   179
*}
wenzelm@10141
   180
wenzelm@10141
   181
theorem group_one_equality: "e * x = x ==> one = (e::'a::group)"
wenzelm@10141
   182
proof -
wenzelm@10141
   183
  assume eq: "e * x = x"
wenzelm@10141
   184
  have "one = x * inverse x"
wenzelm@10141
   185
    by (simp only: group_right_inverse)
wenzelm@10141
   186
  also have "... = (e * x) * inverse x"
wenzelm@10141
   187
    by (simp only: eq)
wenzelm@10141
   188
  also have "... = e * (x * inverse x)"
wenzelm@10141
   189
    by (simp only: group_assoc)
wenzelm@10141
   190
  also have "... = e * one"
wenzelm@10141
   191
    by (simp only: group_right_inverse)
wenzelm@10141
   192
  also have "... = e"
wenzelm@10141
   193
    by (simp only: group_right_one)
wenzelm@10141
   194
  finally show ?thesis .
wenzelm@10141
   195
qed
wenzelm@10141
   196
wenzelm@10141
   197
text {*
wenzelm@10141
   198
 Likewise, the inverse is already determined by the cancel property.
wenzelm@10141
   199
*}
wenzelm@10141
   200
wenzelm@10141
   201
theorem group_inverse_equality:
wenzelm@10141
   202
  "x' * x = one ==> inverse x = (x'::'a::group)"
wenzelm@10141
   203
proof -
wenzelm@10141
   204
  assume eq: "x' * x = one"
wenzelm@10141
   205
  have "inverse x = one * inverse x"
wenzelm@10141
   206
    by (simp only: group_left_one)
wenzelm@10141
   207
  also have "... = (x' * x) * inverse x"
wenzelm@10141
   208
    by (simp only: eq)
wenzelm@10141
   209
  also have "... = x' * (x * inverse x)"
wenzelm@10141
   210
    by (simp only: group_assoc)
wenzelm@10141
   211
  also have "... = x' * one"
wenzelm@10141
   212
    by (simp only: group_right_inverse)
wenzelm@10141
   213
  also have "... = x'"
wenzelm@10141
   214
    by (simp only: group_right_one)
wenzelm@10141
   215
  finally show ?thesis .
wenzelm@10141
   216
qed
wenzelm@10141
   217
wenzelm@10141
   218
text {*
wenzelm@10141
   219
 The inverse operation has some further characteristic properties.
wenzelm@10141
   220
*}
wenzelm@10141
   221
wenzelm@10141
   222
theorem group_inverse_times:
wenzelm@10141
   223
  "inverse (x * y) = inverse y * inverse (x::'a::group)"
wenzelm@10141
   224
proof (rule group_inverse_equality)
wenzelm@10141
   225
  show "(inverse y * inverse x) * (x * y) = one"
wenzelm@10141
   226
  proof -
wenzelm@10141
   227
    have "(inverse y * inverse x) * (x * y) =
wenzelm@10141
   228
        (inverse y * (inverse x * x)) * y"
wenzelm@10141
   229
      by (simp only: group_assoc)
wenzelm@10141
   230
    also have "... = (inverse y * one) * y"
wenzelm@10141
   231
      by (simp only: group_left_inverse)
wenzelm@10141
   232
    also have "... = inverse y * y"
wenzelm@10141
   233
      by (simp only: group_right_one)
wenzelm@10141
   234
    also have "... = one"
wenzelm@10141
   235
      by (simp only: group_left_inverse)
wenzelm@10141
   236
    finally show ?thesis .
wenzelm@10141
   237
  qed
wenzelm@10141
   238
qed
wenzelm@10141
   239
wenzelm@10141
   240
theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)"
wenzelm@10141
   241
proof (rule group_inverse_equality)
wenzelm@10141
   242
  show "x * inverse x = one"
wenzelm@10141
   243
    by (simp only: group_right_inverse)
wenzelm@10141
   244
qed
wenzelm@10141
   245
wenzelm@10141
   246
theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)"
wenzelm@10141
   247
proof -
wenzelm@10141
   248
  assume eq: "inverse x = inverse y"
wenzelm@10141
   249
  have "x = x * one"
wenzelm@10141
   250
    by (simp only: group_right_one)
wenzelm@10141
   251
  also have "... = x * (inverse y * y)"
wenzelm@10141
   252
    by (simp only: group_left_inverse)
wenzelm@10141
   253
  also have "... = x * (inverse x * y)"
wenzelm@10141
   254
    by (simp only: eq)
wenzelm@10141
   255
  also have "... = (x * inverse x) * y"
wenzelm@10141
   256
    by (simp only: group_assoc)
wenzelm@10141
   257
  also have "... = one * y"
wenzelm@10141
   258
    by (simp only: group_right_inverse)
wenzelm@10141
   259
  also have "... = y"
wenzelm@10141
   260
    by (simp only: group_left_one)
wenzelm@10141
   261
  finally show ?thesis .
wenzelm@10141
   262
qed
wenzelm@10141
   263
wenzelm@10141
   264
end