# HG changeset patch
# User paulson
# Date 843750919 -7200
# Node ID 6db93e6f1b1114bf51876d0b33b766d0524273ed
# Parent  79c86b966257d1567f83e10d779d37065369ada1
Documented sort hypotheses and improved discussion of derivations

diff -r 79c86b966257 -r 6db93e6f1b11 doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Thu Sep 26 17:14:02 1996 +0200
+++ b/doc-src/Ref/thm.tex	Thu Sep 26 17:15:19 1996 +0200
@@ -213,8 +213,8 @@
 stamps_of_thy : thm -> string ref list
 theory_of_thm : thm -> theory
 dest_state    : thm*int -> (term*term)list*term list*term*term
-rep_thm       : thm -> \{prop: term, hyps: term list, 
-                        maxidx: int, der: deriv, sign: Sign.sg\}
+rep_thm       : thm -> \{prop: term, hyps: term list, der: deriv, 
+                        maxidx: int, sign: Sign.sg, shyps: sort list\}
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{concl_of} $thm$] 
@@ -241,11 +241,43 @@
 list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
 (this will be an implication if there are more than $i$ subgoals).
 
-\item[\ttindexbold{rep_thm} $thm$] 
-decomposes $thm$ as a record containing the statement of~$thm$, its list of
-meta-assumptions, the maximum subscript of its unknowns, and its signature.
+\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record containing the
+  statement of~$thm$ ({\tt prop}), its list of meta-assumptions ({\tt hyps}),
+  its derivation ({\tt der}), a bound on the maximum subscript of its
+  unknowns ({\tt maxidx}), and its signature ({\tt sign}).  The {\tt shyps}
+  field is discussed below.
+\end{ttdescription}
+
+
+\subsection{*Sort hypotheses} 
+\index{sort hypotheses}
+\begin{ttbox} 
+force_strip_shyps : bool ref \hfill{\bf initially true}
+\end{ttbox}
+
+\begin{ttdescription}
+\item[\ttindexbold{force_strip_shyps}]
+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.
+
+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.
+
 
 \subsection{Tracing flags for unification}
 \index{tracing!of unification}
@@ -734,5 +766,12 @@
   operations on rules (such as rewriting) are left as-is.  
 \end{ttdescription}
 
+Functions {\tt Deriv.linear} and {\tt Deriv.tree} omit the proof of any named
+theorems (constructor {\tt Theorem}) they encounter in a derivation.  Applying
+them directly to the derivation of a named theorem is therefore pointless.
+Use {\tt Deriv.drop} with argument~1 to skip over the initial {\tt Theorem}
+constructor.
+
+
 \index{proof objects|)}
 \index{theorems|)}