author wenzelm Sat, 05 Jun 1999 20:28:45 +0200 changeset 6784 687ddcad8581 parent 6783 9cf9c17d9e35 child 6785 10b77354862b
proper calculation;
```--- a/src/HOL/Isar_examples/Group.thy	Sat Jun 05 20:27:53 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy	Sat Jun 05 20:28:45 1999 +0200
@@ -1,114 +1,122 @@
(*  Title:      HOL/Isar_examples/Group.thy
ID:         \$Id\$
Author:     Markus Wenzel, TU Muenchen
-
-Some bits of group theory.  Demonstrate calculational proofs.
*)

theory Group = Main:;

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

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

consts
-  inv :: "'a => 'a"
-  one :: "'a";
+  one :: "'a"
+  inv :: "'a => 'a";

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

-subsection {* some basic theorems of group theory *};
-
-text {* We simulate *};
+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.
+*};

-theorem right_inverse: "x * inverse x = (one::'a::group)";
+theorem right_inverse: "x * inv x = (one::'a::group)";
proof same;
-  have "x * inverse x = one * (x * inverse x)";
+  have "x * inv x = one * (x * inv x)";
-
-  note calculation = facts;
-  let "_ = ..." = ??facts;
-
-  have "... = (one * x) * inverse x";
+  also; have "... = (one * x) * inv x";
+  also; have "... = inv (inv x) * inv x * x * inv x";
+  also; have "... = inv (inv x) * (inv x * x) * inv x";
+  also; have "... = inv (inv x) * one * inv x";
+  also; have "... = inv (inv x) * (one * inv x)";
+  also; have "... = inv (inv x) * inv x";
+  also; have "... = one";
+  finally; show ??thesis; .;
+qed;

-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
-
-  have "... = inverse (inverse x) * inverse x * x * inverse x";
+text {*
+  With right_inverse already at our disposel, right_unit is now
+  obtained much simpler.
+*};

-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
-
-  have "... = inverse (inverse x) * (inverse x * x) * inverse x";
+theorem right_unit: "x * one = (x::'a::group)";
+proof same;
+  have "x * one = x * (inv x * x)";
+  also; have "... = x * inv x * x";
+  also; have "... = one * x";
+  also; have "... = x";
+  finally; show ??thesis; .;
+qed;

-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
+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.
+
+ 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.

-  have "... = inverse (inverse x) * one * inverse x";
+ 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.
+*};
+
+theorem right_unit': "x * one = (x::'a::group)";
+proof same;
+
+  have "x * one = x * (inv x * x)";

-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
+  note calculation = facts
+    -- {* first calculational step: init register *};

-  have "... = inverse (inverse x) * (one * inverse x)";
+  have "... = x * inv x * x";

-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
-
-  have "... = inverse (inverse x) * inverse x";
-
-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
-
-  have "... = one";
-
-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
-  from calculation;
-
-  show ??thesis; .;
-qed;
-
-
-theorem right_inverse: "x * one = (x::'a::group)";
-proof same;
-
-  have "x * one = x * (inverse x * x)";
-
-  note calculation = facts;
-  let "_ = ..." = ??facts;
-
-  have "... = x * inverse x * x";
-
-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
+  note calculation = trans[APP calculation facts]
+    -- {* general calculational step: compose with transitivity rule *};

have "... = one * x";

-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
+  note calculation = trans[APP calculation facts]
+    -- {* general calculational step: compose with transitivity rule *};

have "... = x";

-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
-  from calculation;
+  note calculation = trans[APP calculation facts]
+    -- {* final calculational step: compose with transitivity rule ... *};
+  from calculation
+    -- {* ... and pick up final result *};

show ??thesis; .;
+
qed;

```