src/HOL/Isar_examples/Group.thy
author wenzelm
Wed Sep 01 21:35:20 1999 +0200 (1999-09-01)
changeset 7433 27887c52b9c8
parent 7356 1714c91b8729
child 7480 0a0e0dbe1269
permissions -rw-r--r--
"this";
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@6763
     6
theory Group = Main:;
wenzelm@6763
     7
wenzelm@6793
     8
title {* Basic group theory *};
wenzelm@6763
     9
wenzelm@6784
    10
section {* Groups *}; 
wenzelm@6784
    11
wenzelm@6784
    12
text {*
wenzelm@6793
    13
 We define an axiomatic type class of general groups over signature
wenzelm@6784
    14
 (op *, one, inv).
wenzelm@6784
    15
*};
wenzelm@6763
    16
wenzelm@6763
    17
consts
wenzelm@6784
    18
  one :: "'a"
wenzelm@6784
    19
  inv :: "'a => 'a";
wenzelm@6763
    20
wenzelm@6763
    21
axclass
wenzelm@6763
    22
  group < times
wenzelm@6793
    23
  group_assoc:         "(x * y) * z = x * (y * z)"
wenzelm@6793
    24
  group_left_unit:     "one * x = x"
wenzelm@6793
    25
  group_left_inverse:  "inv x * x = one";
wenzelm@6763
    26
wenzelm@6784
    27
text {*
wenzelm@6793
    28
 The group axioms only state the properties of left unit and inverse,
wenzelm@6793
    29
 the right versions are derivable as follows.  The calculational proof
wenzelm@6793
    30
 style below closely follows typical presentations given in any basic
wenzelm@6793
    31
 course on algebra.
wenzelm@6784
    32
*};
wenzelm@6763
    33
wenzelm@6793
    34
theorem group_right_inverse: "x * inv x = (one::'a::group)";
wenzelm@7133
    35
proof -;
wenzelm@6784
    36
  have "x * inv x = one * (x * inv x)";
wenzelm@6908
    37
    by (simp only: group_left_unit);
wenzelm@6784
    38
  also; have "... = (one * x) * inv x";
wenzelm@6908
    39
    by (simp only: group_assoc);
wenzelm@6784
    40
  also; have "... = inv (inv x) * inv x * x * inv x";
wenzelm@6908
    41
    by (simp only: group_left_inverse);
wenzelm@6784
    42
  also; have "... = inv (inv x) * (inv x * x) * inv x";
wenzelm@6908
    43
    by (simp only: group_assoc);
wenzelm@6784
    44
  also; have "... = inv (inv x) * one * inv x";
wenzelm@6908
    45
    by (simp only: group_left_inverse);
wenzelm@6784
    46
  also; have "... = inv (inv x) * (one * inv x)";
wenzelm@6908
    47
    by (simp only: group_assoc);
wenzelm@6784
    48
  also; have "... = inv (inv x) * inv x";
wenzelm@6908
    49
    by (simp only: group_left_unit);
wenzelm@6784
    50
  also; have "... = one";
wenzelm@6908
    51
    by (simp only: group_left_inverse);
wenzelm@6784
    52
  finally; show ??thesis; .;
wenzelm@6784
    53
qed;
wenzelm@6763
    54
wenzelm@6784
    55
text {*
wenzelm@6793
    56
 With group_right_inverse already at our disposal, group_right_unit is
wenzelm@6793
    57
 now obtained much easier as follows.
wenzelm@6784
    58
*};
wenzelm@6763
    59
wenzelm@6793
    60
theorem group_right_unit: "x * one = (x::'a::group)";
wenzelm@7133
    61
proof -;
wenzelm@6784
    62
  have "x * one = x * (inv x * x)";
wenzelm@6908
    63
    by (simp only: group_left_inverse);
wenzelm@6784
    64
  also; have "... = x * inv x * x";
wenzelm@6908
    65
    by (simp only: group_assoc);
wenzelm@6784
    66
  also; have "... = one * x";
wenzelm@6908
    67
    by (simp only: group_right_inverse);
wenzelm@6784
    68
  also; have "... = x";
wenzelm@6908
    69
    by (simp only: group_left_unit);
wenzelm@6784
    70
  finally; show ??thesis; .;
wenzelm@6784
    71
qed;
wenzelm@6763
    72
wenzelm@6784
    73
text {*
wenzelm@6793
    74
 There are only two Isar language elements for calculational proofs:
wenzelm@6793
    75
 'also' for initial or intermediate calculational steps, and 'finally'
wenzelm@6793
    76
 for building the result of a calculation.  These constructs are not
wenzelm@6793
    77
 hardwired into Isabelle/Isar, but defined on top of the basic Isar/VM
wenzelm@6793
    78
 interpreter.  Expanding the 'also' or 'finally' derived language
wenzelm@6793
    79
 elements, calculations may be simulated as demonstrated below.
wenzelm@6784
    80
wenzelm@6793
    81
 Note that "..." is just a special term binding that happens to be
wenzelm@6793
    82
 bound automatically to the argument of the last fact established by
wenzelm@6793
    83
 assume or any local goal.  In contrast to ??thesis, "..." is bound
wenzelm@6793
    84
 after the proof is finished.
wenzelm@6784
    85
*};
wenzelm@6784
    86
wenzelm@6793
    87
theorem "x * one = (x::'a::group)";
wenzelm@7133
    88
proof -;
wenzelm@6784
    89
  have "x * one = x * (inv x * x)";
wenzelm@6908
    90
    by (simp only: group_left_inverse);
wenzelm@6763
    91
wenzelm@7433
    92
  note calculation = this
wenzelm@6793
    93
    -- {* first calculational step: init calculation register *};
wenzelm@6763
    94
wenzelm@6784
    95
  have "... = x * inv x * x";
wenzelm@6908
    96
    by (simp only: group_assoc);
wenzelm@6763
    97
wenzelm@7433
    98
  note calculation = trans [OF calculation this]
wenzelm@6784
    99
    -- {* general calculational step: compose with transitivity rule *};
wenzelm@6763
   100
wenzelm@6763
   101
  have "... = one * x";
wenzelm@6908
   102
    by (simp only: group_right_inverse);
wenzelm@6763
   103
wenzelm@7433
   104
  note calculation = trans [OF calculation this]
wenzelm@6784
   105
    -- {* general calculational step: compose with transitivity rule *};
wenzelm@6763
   106
wenzelm@6763
   107
  have "... = x";
wenzelm@6908
   108
    by (simp only: group_left_unit);
wenzelm@6763
   109
wenzelm@7433
   110
  note calculation = trans [OF calculation this]
wenzelm@6784
   111
    -- {* final calculational step: compose with transitivity rule ... *};
wenzelm@6784
   112
  from calculation
wenzelm@6784
   113
    -- {* ... and pick up final result *};
wenzelm@6763
   114
wenzelm@6763
   115
  show ??thesis; .;
wenzelm@6763
   116
qed;
wenzelm@6763
   117
wenzelm@6763
   118
wenzelm@6793
   119
section {* Groups and monoids *};
wenzelm@6793
   120
wenzelm@6793
   121
text {*
wenzelm@6793
   122
  Monoids are usually defined like this.
wenzelm@6793
   123
*};
wenzelm@6793
   124
wenzelm@6793
   125
axclass monoid < times
wenzelm@6793
   126
  monoid_assoc:       "(x * y) * z = x * (y * z)"
wenzelm@6793
   127
  monoid_left_unit:   "one * x = x"
wenzelm@6793
   128
  monoid_right_unit:  "x * one = x";
wenzelm@6793
   129
wenzelm@6793
   130
text {*
wenzelm@7005
   131
 Groups are *not* yet monoids directly from the definition.  For
wenzelm@6793
   132
 monoids, right_unit had to be included as an axiom, but for groups
wenzelm@6793
   133
 both right_unit and right_inverse are derivable from the other
wenzelm@6793
   134
 axioms.  With group_right_unit derived as a theorem of group theory
wenzelm@6793
   135
 (see above), we may still instantiate group < monoid properly as
wenzelm@6793
   136
 follows.
wenzelm@6793
   137
*};
wenzelm@6793
   138
wenzelm@6793
   139
instance group < monoid;
wenzelm@7356
   140
  by (intro_classes,
wenzelm@6793
   141
       rule group_assoc,
wenzelm@6793
   142
       rule group_left_unit,
wenzelm@6793
   143
       rule group_right_unit);
wenzelm@6793
   144
wenzelm@6793
   145
wenzelm@6763
   146
end;