updated documentation of sort hypotheses;
authorwenzelm
Thu Jun 13 17:40:58 2013 +0200 (2013-06-13)
changeset 524061e57c3c4e05c
parent 52405 3dd63180cdbf
child 52407 e4662afb3483
updated documentation of sort hypotheses;
src/Doc/IsarImplementation/Logic.thy
src/Doc/Ref/document/thm.tex
src/HOL/Tools/reflection.ML
     1.1 --- a/src/Doc/IsarImplementation/Logic.thy	Fri Jun 21 16:21:33 2013 -0700
     1.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Thu Jun 13 17:40:58 2013 +0200
     1.3 @@ -932,6 +932,72 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsection {* Sort hypotheses *}
     1.8 +
     1.9 +text {* Type variables are decorated with sorts, as explained in
    1.10 +  \secref{sec:types}.  This constrains type instantiation to certain
    1.11 +  ranges of types: variable @{text "\<alpha>\<^sub>s"} may only be assigned to types
    1.12 +  @{text "\<tau>"} that belong to sort @{text "s"}.  Within the logic, sort
    1.13 +  constraints act like implicit preconditions on the result @{text
    1.14 +  "\<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
    1.15 +  "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} cover the propositions @{text "\<Gamma>"}, @{text "\<phi>"}, as
    1.16 +  well as the proof of @{text "\<Gamma> \<turnstile> \<phi>"}.
    1.17 +
    1.18 +  These \emph{sort hypothesis} of a theorem are passed monotonically
    1.19 +  through further derivations.  They are redundant, as long as the
    1.20 +  statement of a theorem still contains the type variables that are
    1.21 +  accounted here.  The logical significance of sort hypotheses is
    1.22 +  limited to the boundary case where type variables disappear from the
    1.23 +  proposition, e.g.\ @{text "\<lparr>\<alpha>\<^sub>s : s\<rparr> \<turnstile> \<phi>"}.  Since such dangling type
    1.24 +  variables can be renamed arbitrarily without changing the
    1.25 +  proposition @{text "\<phi>"}, the inference kernel maintains sort
    1.26 +  hypotheses in anonymous form @{text "s \<turnstile> \<phi>"}.
    1.27 +
    1.28 +  In most practical situations, such extra sort hypotheses may be
    1.29 +  stripped in a final bookkeeping step, e.g.\ at the end of a proof:
    1.30 +  they are typically left over from intermediate reasoning with type
    1.31 +  classes that can be satisfied by some concrete type @{text "\<tau>"} of
    1.32 +  sort @{text "s"} to replace the hypothetical type variable @{text
    1.33 +  "\<alpha>\<^sub>s"}.  *}
    1.34 +
    1.35 +text %mlref {*
    1.36 +  \begin{mldecls}
    1.37 +  @{index_ML Thm.extra_shyps: "thm -> sort list"} \\
    1.38 +  @{index_ML Thm.strip_shyps: "thm -> thm"} \\
    1.39 +  \end{mldecls}
    1.40 +
    1.41 +  \begin{description}
    1.42 +
    1.43 +  \item @{ML Thm.extra_shyps}~@{text "thm"} determines the extraneous
    1.44 +  sort hypotheses of the given theorem, i.e.\ the sorts that are not
    1.45 +  present within type variables of the statement.
    1.46 +
    1.47 +  \item @{ML Thm.strip_shyps}~@{text "thm"} removes any extraneous
    1.48 +  sort hypotheses that can be witnessed from the type signature.
    1.49 +
    1.50 +  \end{description}
    1.51 +*}
    1.52 +
    1.53 +text %mlex {* The following artificial example demonstrates the
    1.54 +  derivation of @{prop False} with a pending sort hypothesis involving
    1.55 +  a logically empty sort.  *}
    1.56 +
    1.57 +class empty =
    1.58 +  assumes bad: "\<And>(x::'a) y. x \<noteq> y"
    1.59 +
    1.60 +theorem (in empty) false: False
    1.61 +  using bad by blast
    1.62 +
    1.63 +ML {*
    1.64 +  @{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])
    1.65 +*}
    1.66 +
    1.67 +text {* Thanks to the inference kernel managing sort hypothesis
    1.68 +  according to their logical significance, this example is merely an
    1.69 +  instance of \emph{ex falso quodlibet consequitur} --- not a collapse
    1.70 +  of the logical framework! *}
    1.71 +
    1.72 +
    1.73  section {* Object-level rules \label{sec:obj-rules} *}
    1.74  
    1.75  text {*
     2.1 --- a/src/Doc/Ref/document/thm.tex	Fri Jun 21 16:21:33 2013 -0700
     2.2 +++ b/src/Doc/Ref/document/thm.tex	Thu Jun 13 17:40:58 2013 +0200
     2.3 @@ -1,51 +1,6 @@
     2.4  
     2.5  \chapter{Theorems and Forward Proof}
     2.6  
     2.7 -\section{*Sort hypotheses} \label{sec:sort-hyps}
     2.8 -
     2.9 -\begin{ttbox} 
    2.10 -strip_shyps         : thm -> thm
    2.11 -strip_shyps_warning : thm -> thm
    2.12 -\end{ttbox}
    2.13 -
    2.14 -Isabelle's type variables are decorated with sorts, constraining them to
    2.15 -certain ranges of types.  This has little impact when sorts only serve for
    2.16 -syntactic classification of types --- for example, FOL distinguishes between
    2.17 -terms and other types.  But when type classes are introduced through axioms,
    2.18 -this may result in some sorts becoming {\em empty\/}: where one cannot exhibit
    2.19 -a type belonging to it because certain sets of axioms are unsatisfiable.
    2.20 -
    2.21 -If a theorem contains a type variable that is constrained by an empty
    2.22 -sort, then that theorem has no instances.  It is basically an instance
    2.23 -of {\em ex falso quodlibet}.  But what if it is used to prove another
    2.24 -theorem that no longer involves that sort?  The latter theorem holds
    2.25 -only if under an additional non-emptiness assumption.
    2.26 -
    2.27 -Therefore, Isabelle's theorems carry around sort hypotheses.  The {\tt
    2.28 -shyps} field is a list of sorts occurring in type variables in the current
    2.29 -{\tt prop} and {\tt hyps} fields.  It may also includes sorts used in the
    2.30 -theorem's proof that no longer appear in the {\tt prop} or {\tt hyps}
    2.31 -fields --- so-called {\em dangling\/} sort constraints.  These are the
    2.32 -critical ones, asserting non-emptiness of the corresponding sorts.
    2.33 - 
    2.34 -Isabelle automatically removes extraneous sorts from the {\tt shyps} field at
    2.35 -the end of a proof, provided that non-emptiness can be established by looking
    2.36 -at the theorem's signature: from the {\tt classes} and {\tt arities}
    2.37 -information.  This operation is performed by \texttt{strip_shyps} and
    2.38 -\texttt{strip_shyps_warning}.
    2.39 -
    2.40 -\begin{ttdescription}
    2.41 -  
    2.42 -\item[\ttindexbold{strip_shyps} $thm$] removes any extraneous sort hypotheses
    2.43 -  that can be witnessed from the type signature.
    2.44 -  
    2.45 -\item[\ttindexbold{strip_shyps_warning}] is like \texttt{strip_shyps}, but
    2.46 -  issues a warning message of any pending sort hypotheses that do not have a
    2.47 -  (syntactic) witness.
    2.48 -
    2.49 -\end{ttdescription}
    2.50 -
    2.51 -
    2.52  \section{Proof terms}\label{sec:proofObjects}
    2.53  \index{proof terms|(} Isabelle can record the full meta-level proof of each
    2.54  theorem.  The proof term contains all logical inferences in detail.