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