# HG changeset patch
# User wenzelm
# Date 928607325 -7200
# Node ID 687ddcad858139ee00507ead0bc6071f11a2e509
# Parent  9cf9c17d9e35aa3a2dd71cc550612cf20dd1be1e
proper calculation;

diff -r 9cf9c17d9e35 -r 687ddcad8581 src/HOL/Isar_examples/Group.thy
--- 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)";
     by (simp add: left_unit);
-
-  note calculation = facts;
-  let "_ = ..." = ??facts;
-
-  have "... = (one * x) * inverse x";
+  also; have "... = (one * x) * inv x";
+    by (simp add: assoc);
+  also; have "... = inv (inv x) * inv x * x * inv x";
+    by (simp add: left_inverse);
+  also; have "... = inv (inv x) * (inv x * x) * inv x";
+    by (simp add: assoc);
+  also; have "... = inv (inv x) * one * inv x";
+    by (simp add: left_inverse);
+  also; have "... = inv (inv x) * (one * inv x)";
     by (simp add: assoc);
+  also; have "... = inv (inv x) * inv x";
+    by (simp add: left_unit);
+  also; have "... = one";
+    by (simp add: left_inverse);
+  finally; show ??thesis; .;
+qed;
 
-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
-
-  have "... = inverse (inverse x) * inverse x * x * inverse x";
-    by (simp add: left_inverse);
+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)";
+    by (simp add: left_inverse);
+  also; have "... = x * inv x * x";
     by (simp add: assoc);
+  also; have "... = one * x";
+    by (simp add: right_inverse);
+  also; have "... = x";
+    by (simp add: left_unit);
+  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)";
     by (simp add: left_inverse);
 
-  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";
     by (simp add: assoc);
 
-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
-
-  have "... = inverse (inverse x) * inverse x";
-    by (simp add: left_unit);
-
-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
-
-  have "... = one";
-    by (simp add: left_inverse);
-
-  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)";
-    by (simp add: left_inverse);
-
-  note calculation = facts;
-  let "_ = ..." = ??facts;
-
-  have "... = x * inverse x * x";
-    by (simp add: assoc);
-
-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
+  note calculation = trans[APP calculation facts]
+    -- {* general calculational step: compose with transitivity rule *};
 
   have "... = one * x";
     by (simp add: right_inverse);
 
-  note calculation = trans[APP calculation facts];
-  let "_ = ..." = ??facts;
+  note calculation = trans[APP calculation facts]
+    -- {* general calculational step: compose with transitivity rule *};
 
   have "... = x";
     by (simp add: left_unit);
 
-  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;