author | wenzelm |

Thu Jun 13 17:40:58 2013 +0200 (2013-06-13) | |

changeset 52406 | 1e57c3c4e05c |

parent 52405 | 3dd63180cdbf |

child 52407 | e4662afb3483 |

updated documentation of sort hypotheses;

src/Doc/IsarImplementation/Logic.thy | file | annotate | diff | revisions | |

src/Doc/Ref/document/thm.tex | file | annotate | diff | revisions | |

src/HOL/Tools/reflection.ML | file | annotate | diff | revisions |

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.