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