summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 13 Jun 2013 17:40:58 +0200 | |

changeset 52406 | 1e57c3c4e05c |

parent 52405 | 3dd63180cdbf |

child 52407 | e4662afb3483 |

updated documentation of sort hypotheses;

--- 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 {*

--- 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.