author wenzelm Sat, 05 Jun 1999 21:43:02 +0200 changeset 6793 88aba7f486cb parent 6792 c68035d06cce child 6794 ac367328b875
groups as monoids; tuned;
```--- a/src/HOL/Isar_examples/Group.thy	Sat Jun 05 21:38:30 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy	Sat Jun 05 21:43:02 1999 +0200
@@ -5,12 +5,12 @@

theory Group = Main:;

-title {* Basic group theory -- demonstrating calculational proofs *};
+title {* Basic group theory *};

section {* Groups *};

text {*
- We define an axiomatic type class of general groupes over signature
+ We define an axiomatic type class of general groups over signature
(op *, one, inv).
*};

@@ -20,95 +20,92 @@

axclass
group < times
-  assoc:         "(x * y) * z = x * (y * z)"
-  left_unit:     "one * x = x"
-  left_inverse:  "inv x * x = one";
+  group_assoc:         "(x * y) * z = x * (y * z)"
+  group_left_unit:     "one * x = x"
+  group_left_inverse:  "inv x * x = one";

text {*
- The group axioms only state the properties of left unit and inverse, the
- right versions are derivable as follows.  The calculational proof style below
- closely follows a typical presentation given in any basic course on
- algebra.
+ The group axioms only state the properties of left unit and inverse,
+ the right versions are derivable as follows.  The calculational proof
+ style below closely follows typical presentations given in any basic
+ course on algebra.
*};

-theorem right_inverse: "x * inv x = (one::'a::group)";
+theorem group_right_inverse: "x * inv x = (one::'a::group)";
proof same;
have "x * inv x = one * (x * inv x)";
-    by (simp add: left_unit);
+    by (simp add: group_left_unit);
also; have "... = (one * x) * inv x";
-    by (simp add: assoc);
+    by (simp add: group_assoc);
also; have "... = inv (inv x) * inv x * x * inv x";
-    by (simp add: left_inverse);
+    by (simp add: group_left_inverse);
also; have "... = inv (inv x) * (inv x * x) * inv x";
-    by (simp add: assoc);
+    by (simp add: group_assoc);
also; have "... = inv (inv x) * one * inv x";
-    by (simp add: left_inverse);
+    by (simp add: group_left_inverse);
also; have "... = inv (inv x) * (one * inv x)";
-    by (simp add: assoc);
+    by (simp add: group_assoc);
also; have "... = inv (inv x) * inv x";
-    by (simp add: left_unit);
+    by (simp add: group_left_unit);
also; have "... = one";
-    by (simp add: left_inverse);
+    by (simp add: group_left_inverse);
finally; show ??thesis; .;
qed;

text {*
-  With right_inverse already at our disposel, right_unit is now
-  obtained much simpler.
+ With group_right_inverse already at our disposal, group_right_unit is
+ now obtained much easier as follows.
*};

-theorem right_unit: "x * one = (x::'a::group)";
+theorem group_right_unit: "x * one = (x::'a::group)";
proof same;
have "x * one = x * (inv x * x)";
-    by (simp add: left_inverse);
+    by (simp add: group_left_inverse);
also; have "... = x * inv x * x";
-    by (simp add: assoc);
+    by (simp add: group_assoc);
also; have "... = one * x";
-    by (simp add: right_inverse);
+    by (simp add: group_right_inverse);
also; have "... = x";
-    by (simp add: left_unit);
+    by (simp add: group_left_unit);
finally; show ??thesis; .;
qed;

text {*
- There are only two language elements 'also' (for initial or
- intermediate calculational steps), and 'finally' (for picking up the
- result of a calculation).  These constructs are not hardwired into
- Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
+ There are only two Isar language elements for calculational proofs:
+ 'also' for initial or intermediate calculational steps, and 'finally'
+ for building the result of a calculation.  These constructs are not
+ hardwired into Isabelle/Isar, but defined on top of the basic Isar/VM
+ interpreter.  Expanding the 'also' or 'finally' derived language
+ elements, calculations may be simulated as demonstrated below.

- Without referring to 'also' or 'finally', calculations may be
- simulated as follows.  This can be also understood as an expansion of these
- two derived language elements.
-
- Also note that "..." is just a special term binding that happens to
- be bound automatically to the argument of the last fact established by
- assume or any local goal.  Unlike ??thesis, "..." is bound after the
- proof is finished.
+ Note that "..." is just a special term binding that happens to be
+ bound automatically to the argument of the last fact established by
+ assume or any local goal.  In contrast to ??thesis, "..." is bound
+ after the proof is finished.
*};

-theorem right_unit': "x * one = (x::'a::group)";
+theorem "x * one = (x::'a::group)";
proof same;
-
have "x * one = x * (inv x * x)";
-    by (simp add: left_inverse);
+    by (simp add: group_left_inverse);

note calculation = facts
-    -- {* first calculational step: init register *};
+    -- {* first calculational step: init calculation register *};

have "... = x * inv x * x";
-    by (simp add: assoc);
+    by (simp add: group_assoc);

note calculation = trans[APP calculation facts]
-- {* general calculational step: compose with transitivity rule *};

have "... = one * x";
-    by (simp add: right_inverse);
+    by (simp add: group_right_inverse);

note calculation = trans[APP calculation facts]
-- {* general calculational step: compose with transitivity rule *};

have "... = x";
-    by (simp add: left_unit);
+    by (simp add: group_left_unit);

note calculation = trans[APP calculation facts]
-- {* final calculational step: compose with transitivity rule ... *};
@@ -116,8 +113,34 @@
-- {* ... and pick up final result *};

show ??thesis; .;
-
qed;

+section {* Groups and monoids *};
+
+text {*
+  Monoids are usually defined like this.
+*};
+
+axclass monoid < times
+  monoid_assoc:       "(x * y) * z = x * (y * z)"
+  monoid_left_unit:   "one * x = x"
+  monoid_right_unit:  "x * one = x";
+
+text {*
+ Groups are *not* yet monoids directly from the definition .  For
+ monoids, right_unit had to be included as an axiom, but for groups
+ both right_unit and right_inverse are derivable from the other
+ axioms.  With group_right_unit derived as a theorem of group theory
+ (see above), we may still instantiate group < monoid properly as
+ follows.
+*};
+
+instance group < monoid;
+  by (expand_classes,
+       rule group_assoc,
+       rule group_left_unit,
+       rule group_right_unit);
+
+
end;```