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;
```