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