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