# HG changeset patch
# User wenzelm
# Date 1371138058 -7200
# Node ID 1e57c3c4e05c9e9ad668ca007fcfd5a31b0f0c9f
# Parent  3dd63180cdbf51518e110b8550c44c468f48d21f
updated documentation of sort hypotheses;

diff -r 3dd63180cdbf -r 1e57c3c4e05c src/Doc/IsarImplementation/Logic.thy
--- a/src/Doc/IsarImplementation/Logic.thy	Fri Jun 21 16:21:33 2013 -0700
+++ b/src/Doc/IsarImplementation/Logic.thy	Thu Jun 13 17:40:58 2013 +0200
@@ -932,6 +932,72 @@
 *}
 
 
+subsection {* Sort hypotheses *}
+
+text {* Type variables are decorated with sorts, as explained in
+  \secref{sec:types}.  This constrains type instantiation to certain
+  ranges of types: variable @{text "\<alpha>\<^sub>s"} may only be assigned to types
+  @{text "\<tau>"} that belong to sort @{text "s"}.  Within the logic, sort
+  constraints act like implicit preconditions on the result @{text
+  "\<lparr>\<alpha>\<^sub>1 : s\<^sub>1\<rparr>, \<dots>, \<lparr>\<alpha>\<^sub>n : s\<^sub>n\<rparr>, \<Gamma> \<turnstile> \<phi>"} where the type variables @{text
+  "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} cover the propositions @{text "\<Gamma>"}, @{text "\<phi>"}, as
+  well as the proof of @{text "\<Gamma> \<turnstile> \<phi>"}.
+
+  These \emph{sort hypothesis} of a theorem are passed monotonically
+  through further derivations.  They are redundant, as long as the
+  statement of a theorem still contains the type variables that are
+  accounted here.  The logical significance of sort hypotheses is
+  limited to the boundary case where type variables disappear from the
+  proposition, e.g.\ @{text "\<lparr>\<alpha>\<^sub>s : s\<rparr> \<turnstile> \<phi>"}.  Since such dangling type
+  variables can be renamed arbitrarily without changing the
+  proposition @{text "\<phi>"}, the inference kernel maintains sort
+  hypotheses in anonymous form @{text "s \<turnstile> \<phi>"}.
+
+  In most practical situations, such extra sort hypotheses may be
+  stripped in a final bookkeeping step, e.g.\ at the end of a proof:
+  they are typically left over from intermediate reasoning with type
+  classes that can be satisfied by some concrete type @{text "\<tau>"} of
+  sort @{text "s"} to replace the hypothetical type variable @{text
+  "\<alpha>\<^sub>s"}.  *}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML Thm.extra_shyps: "thm -> sort list"} \\
+  @{index_ML Thm.strip_shyps: "thm -> thm"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML Thm.extra_shyps}~@{text "thm"} determines the extraneous
+  sort hypotheses of the given theorem, i.e.\ the sorts that are not
+  present within type variables of the statement.
+
+  \item @{ML Thm.strip_shyps}~@{text "thm"} removes any extraneous
+  sort hypotheses that can be witnessed from the type signature.
+
+  \end{description}
+*}
+
+text %mlex {* The following artificial example demonstrates the
+  derivation of @{prop False} with a pending sort hypothesis involving
+  a logically empty sort.  *}
+
+class empty =
+  assumes bad: "\<And>(x::'a) y. x \<noteq> y"
+
+theorem (in empty) false: False
+  using bad by blast
+
+ML {*
+  @{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])
+*}
+
+text {* Thanks to the inference kernel managing sort hypothesis
+  according to their logical significance, this example is merely an
+  instance of \emph{ex falso quodlibet consequitur} --- not a collapse
+  of the logical framework! *}
+
+
 section {* Object-level rules \label{sec:obj-rules} *}
 
 text {*
diff -r 3dd63180cdbf -r 1e57c3c4e05c src/Doc/Ref/document/thm.tex
--- a/src/Doc/Ref/document/thm.tex	Fri Jun 21 16:21:33 2013 -0700
+++ b/src/Doc/Ref/document/thm.tex	Thu Jun 13 17:40:58 2013 +0200
@@ -1,51 +1,6 @@
 
 \chapter{Theorems and Forward Proof}
 
-\section{*Sort hypotheses} \label{sec:sort-hyps}
-
-\begin{ttbox} 
-strip_shyps         : thm -> thm
-strip_shyps_warning : thm -> thm
-\end{ttbox}
-
-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 sets of axioms are unsatisfiable.
-
-If a theorem contains a type variable that is constrained by an empty
-sort, then that theorem has no instances.  It is basically an instance
-of {\em ex falso quodlibet}.  But what if it is used to prove another
-theorem that no longer involves that sort?  The latter theorem holds
-only if under an additional non-emptiness assumption.
-
-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 automatically removes extraneous sorts from the {\tt shyps} field at
-the end of a proof, provided that non-emptiness can be established by looking
-at the theorem's signature: from the {\tt classes} and {\tt arities}
-information.  This operation is performed by \texttt{strip_shyps} and
-\texttt{strip_shyps_warning}.
-
-\begin{ttdescription}
-  
-\item[\ttindexbold{strip_shyps} $thm$] removes any extraneous sort hypotheses
-  that can be witnessed from the type signature.
-  
-\item[\ttindexbold{strip_shyps_warning}] is like \texttt{strip_shyps}, but
-  issues a warning message of any pending sort hypotheses that do not have a
-  (syntactic) witness.
-
-\end{ttdescription}
-
-
 \section{Proof terms}\label{sec:proofObjects}
 \index{proof terms|(} Isabelle can record the full meta-level proof of each
 theorem.  The proof term contains all logical inferences in detail.
diff -r 3dd63180cdbf -r 1e57c3c4e05c src/HOL/Tools/reflection.ML