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