src/HOL/Isar_examples/Group.thy
 changeset 7982 d534b897ce39 parent 7968 964b65b4e433 child 8910 981ac87f905c
     1.1 --- a/src/HOL/Isar_examples/Group.thy	Sat Oct 30 20:13:16 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/Group.thy	Sat Oct 30 20:20:48 1999 +0200
1.3 @@ -53,8 +53,9 @@
1.4  qed;
1.5
1.6  text {*
1.7 - With \name{group-right-inverse} already at our disposal,
1.8 - \name{group-right-unit} is now obtained much easier.
1.9 + With \name{group-right-inverse} already available,
1.10 + \name{group-right-unit}\label{thm:group-right-unit} is now
1.11 + established much easier.
1.12  *};
1.13
1.14  theorem group_right_unit: "x * one = (x::'a::group)";
1.15 @@ -75,14 +76,14 @@
1.16   presentations given in any introductory course on algebra.  The basic
1.17   technique is to form a transitive chain of equations, which in turn
1.18   are established by simplifying with appropriate rules.  The low-level
1.19 - logical parts of equational reasoning are left implicit.
1.20 + logical details of equational reasoning are left implicit.
1.21
1.22 - Note that $\dots$'' is just a special term variable that happens to
1.23 - be bound automatically to the argument\footnote{The argument of a
1.24 - curried infix expression happens to be its right-hand side.} of the
1.25 - last fact achieved by any local assumption or proven statement.  In
1.26 - contrast to $\var{thesis}$, the $\dots$'' variable is bound
1.27 - \emph{after} the proof is finished.
1.28 + Note that $\dots$'' is just a special term variable that is bound
1.29 + automatically to the argument\footnote{The argument of a curried
1.30 + infix expression happens to be its right-hand side.} of the last fact
1.31 + achieved by any local assumption or proven statement.  In contrast to
1.32 + $\var{thesis}$, the $\dots$'' variable is bound \emph{after} the
1.33 + proof is finished, though.
1.34
1.35   There are only two separate Isar language elements for calculational
1.36   proofs: \isakeyword{also}'' for initial or intermediate
1.37 @@ -90,8 +91,8 @@
1.38   result of a calculation.  These constructs are not hardwired into
1.39   Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
1.40   Expanding the \isakeyword{also} and \isakeyword{finally} derived
1.41 - language elements, calculations may be simulated as demonstrated
1.42 - below.
1.43 + language elements, calculations may be simulated by hand as
1.44 + demonstrated below.
1.45  *};
1.46
1.47  theorem "x * one = (x::'a::group)";
1.48 @@ -128,10 +129,10 @@
1.49  text {*
1.50   Note that this scheme of calculations is not restricted to plain
1.51   transitivity.  Rules like anti-symmetry, or even forward and backward
1.52 - substitution work as well.  For the actual \isacommand{also} and
1.53 - \isacommand{finally} commands, Isabelle/Isar maintains separate
1.54 - context information of transitivity'' rules.  Rule selection takes
1.55 - place automatically by higher-order unification.
1.56 + substitution work as well.  For the actual implementation of
1.57 + \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
1.58 + separate context information of transitivity'' rules.  Rule
1.59 + selection takes place automatically by higher-order unification.
1.60  *};
1.61
1.62
1.63 @@ -150,10 +151,11 @@
1.64  text {*
1.65   Groups are \emph{not} yet monoids directly from the definition.  For
1.66   monoids, \name{right-unit} had to be included as an axiom, but for
1.67 - groups both \name{right-unit} and \name{right-inverse} are
1.68 - derivable from the other axioms.  With \name{group-right-unit}
1.69 - derived as a theorem of group theory (see above), we may still
1.70 - instantiate $\idt{group} \subset \idt{monoid}$ properly as follows.
1.71 + groups both \name{right-unit} and \name{right-inverse} are derivable
1.72 + from the other axioms.  With \name{group-right-unit} derived as a
1.73 + theorem of group theory (see page~\pageref{thm:group-right-unit}), we
1.74 + may still instantiate $\idt{group} \subset \idt{monoid}$ properly as
1.75 + follows.
1.76  *};
1.77
1.78  instance group < monoid;
1.79 @@ -167,7 +169,7 @@
1.80   \isacommand{theorem}, setting up a goal that reflects the intended
1.81   class relation (or type constructor arity).  Thus any Isar proof
1.82   language element may be involved to establish this statement.  When
1.83 - concluding the proof, the result is transformed into the original
1.84 + concluding the proof, the result is transformed into the intended
1.85   type signature extension behind the scenes.
1.86  *};
1.87