Documented sort hypotheses and improved discussion of derivations
Thu, 26 Sep 1996 17:15:19 +0200
changeset 2040 6db93e6f1b11
parent 2039 79c86b966257
child 2041 a3262b93c1d2
Documented sort hypotheses and improved discussion of derivations
--- 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:\}
+rep_thm       : thm -> \{prop: term, hyps: term list, der: deriv, 
+                        maxidx: int, sign:, shyps: sort list\}
 \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.
+\subsection{*Sort hypotheses} 
+\index{sort hypotheses}
+force_strip_shyps : bool ref \hfill{\bf initially true}
+causes sort hypotheses to be deleted, printing a warning.
+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.  
+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}
 \index{proof objects|)}