summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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