author paulson Mon, 30 Sep 1996 11:04:14 +0200 changeset 2044 e8d52d05530a parent 2043 8de7a0ab463b child 2045 ae1030e66745
Improved discussion of shyps thanks to Markus Wenzel
 doc-src/Ref/thm.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/thm.tex	Mon Sep 30 10:59:47 1996 +0200
+++ b/doc-src/Ref/thm.tex	Mon Sep 30 11:04:14 1996 +0200
@@ -260,23 +260,30 @@
causes sort hypotheses to be deleted, printing a warning.
\end{ttdescription}

-A sort is {\em empty\/} if there are no types having that sort.  If a theorem
-contain a type variable whose sort is empty, then that theorem has no
-instances.  In effect, it asserts nothing.  But what if it is used to prove
-another theorem that no longer involves that sort?  The latter theorem holds
-only if the sort is non-empty.
+Isabelle's type variables are decorated with sorts, constraining them to
+certain ranges of types.  This has little impact when sorts only serve for
+syntactic classification of types --- for example, FOL distinguishes between
+terms and other types.  But when type classes are introduced through axioms,
+this may result in some sorts becoming {\em empty\/}: where one cannot exhibit
+a type belonging to it because certain axioms are unsatisfiable.
+
+If a theorem contain a type variable whose sort is empty, then that theorem
+has no instances.  In effect, it asserts nothing.  But what if it is used to
+prove another theorem that no longer involves that sort?  The latter theorem
+holds only if the sort is non-empty.

-Theorems are therefore subject to sort hypotheses, which express that certain
-sorts are non-empty.  The {\tt shyps} field is a list of sorts occurring in
-type variables.  The list includes all sorts from the current theorem (the
-{\tt prop} and {\tt hyps} fields).  It also includes sorts used in the
-theorem's proof --- so-called {\em dangling\/} sort constraints.  These are
-the critical ones that must be non-empty in order for the proof to be valid.
-
-Isabelle removes sorts from the {\tt shyps} field whenever
-non-emptiness holds.  Because its current implementation is highly incomplete,
-the flag shown above is available.  Setting it to true (the default) allows
-existing proofs to run.
+Therefore, Isabelle's theorems carry around sort hypotheses. The {\tt
+shyps} field is a list of sorts occurring in type variables in the current
+{\tt prop} and {\tt hyps} fields.  It may also includes sorts used in the
+theorem's proof that no longer appear in the {\tt prop} or {\tt hyps}
+fields --- so-called {\em dangling\/} sort constraints. These are the
+critical ones, asserting non-emptiness of the corresponding sorts.
+
+Isabelle tries to remove extraneous sorts from the {\tt shyps} field whenever
+non-emptiness can be established by looking at the theorem's signature: from
+the {\tt arities} information, etc.  Because its current implementation is
+highly incomplete, the flag shown above is available.  Setting it to true (the
+default) allows existing proofs to run.

\subsection{Tracing flags for unification}