--- a/doc-src/Ref/theories.tex Sun Jun 05 22:09:04 2011 +0200
+++ b/doc-src/Ref/theories.tex Mon Jun 06 17:51:14 2011 +0200
@@ -21,68 +21,12 @@
\end{ttdescription}
-\section{Terms}\label{sec:terms}
-\index{terms|bold}
-Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
-with six constructors:
-\begin{ttbox}
-type indexname = string * int;
-infix 9 $;
-datatype term = Const of string * typ
- | Free of string * typ
- | Var of indexname * typ
- | Bound of int
- | Abs of string * typ * term
- | op $ of term * term;
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{Const} ($a$, $T$)] \index{constants|bold}
- is the \textbf{constant} with name~$a$ and type~$T$. Constants include
- connectives like $\land$ and $\forall$ as well as constants like~0
- and~$Suc$. Other constants may be required to define a logic's concrete
- syntax.
-
-\item[\ttindexbold{Free} ($a$, $T$)] \index{variables!free|bold}
- is the \textbf{free variable} with name~$a$ and type~$T$.
-
-\item[\ttindexbold{Var} ($v$, $T$)] \index{unknowns|bold}
- is the \textbf{scheme variable} with indexname~$v$ and type~$T$. An
- \mltydx{indexname} is a string paired with a non-negative index, or
- subscript; a term's scheme variables can be systematically renamed by
- incrementing their subscripts. Scheme variables are essentially free
- variables, but may be instantiated during unification.
-
-\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
- is the \textbf{bound variable} with de Bruijn index~$i$, which counts the
- number of lambdas, starting from zero, between a variable's occurrence
- and its binding. The representation prevents capture of variables. For
- more information see de Bruijn \cite{debruijn72} or
- Paulson~\cite[page~376]{paulson-ml2}.
-
-\item[\ttindexbold{Abs} ($a$, $T$, $u$)]
- \index{lambda abs@$\lambda$-abstractions|bold}
- is the $\lambda$-\textbf{abstraction} with body~$u$, and whose bound
- variable has name~$a$ and type~$T$. The name is used only for parsing
- and printing; it has no logical significance.
-
-\item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
-is the \textbf{application} of~$t$ to~$u$.
-\end{ttdescription}
-Application is written as an infix operator to aid readability. Here is an
-\ML\ pattern to recognize FOL formulae of the form~$A\imp B$, binding the
-subformulae to~$A$ and~$B$:
-\begin{ttbox}
-Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
-\end{ttbox}
-
-
\section{*Variable binding}
\begin{ttbox}
loose_bnos : term -> int list
incr_boundvars : int -> term -> term
abstract_over : term*term -> term
variant_abs : string * typ * term -> string * term
-aconv : term * term -> bool\hfill\textbf{infix}
\end{ttbox}
These functions are all concerned with the de Bruijn representation of
bound variables.
@@ -112,172 +56,8 @@
of~$a$ chosen to be distinct from all constants and from all variables
free in~$u$.
-\item[$t$ \ttindexbold{aconv} $u$]
- tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
- to renaming of bound variables.
-\begin{itemize}
- \item
- Two constants, \texttt{Free}s, or \texttt{Var}s are \(\alpha\)-convertible
- if their names and types are equal.
- (Variables having the same name but different types are thus distinct.
- This confusing situation should be avoided!)
- \item
- Two bound variables are \(\alpha\)-convertible
- if they have the same number.
- \item
- Two abstractions are \(\alpha\)-convertible
- if their bodies are, and their bound variables have the same type.
- \item
- Two applications are \(\alpha\)-convertible
- if the corresponding subterms are.
-\end{itemize}
-
\end{ttdescription}
-\section{Certified terms}\index{terms!certified|bold}\index{signatures}
-A term $t$ can be \textbf{certified} under a signature to ensure that every type
-in~$t$ is well-formed and every constant in~$t$ is a type instance of a
-constant declared in the signature. The term must be well-typed and its use
-of bound variables must be well-formed. Meta-rules such as \texttt{forall_elim}
-take certified terms as arguments.
-
-Certified terms belong to the abstract type \mltydx{cterm}.
-Elements of the type can only be created through the certification process.
-In case of error, Isabelle raises exception~\ttindex{TERM}\@.
-
-\subsection{Printing terms}
-\index{terms!printing of}
-\begin{ttbox}
- string_of_cterm : cterm -> string
-Sign.string_of_term : Sign.sg -> term -> string
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{string_of_cterm} $ct$]
-displays $ct$ as a string.
-
-\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
-displays $t$ as a string, using the syntax of~$sign$.
-\end{ttdescription}
-
-\subsection{Making and inspecting certified terms}
-\begin{ttbox}
-cterm_of : Sign.sg -> term -> cterm
-read_cterm : Sign.sg -> string * typ -> cterm
-cert_axm : Sign.sg -> string * term -> string * term
-read_axm : Sign.sg -> string * string -> string * term
-rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
-Sign.certify_term : Sign.sg -> term -> term * typ * int
-\end{ttbox}
-\begin{ttdescription}
-
-\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies
- $t$ with respect to signature~$sign$.
-
-\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] reads the string~$s$
- using the syntax of~$sign$, creating a certified term. The term is
- checked to have type~$T$; this type also tells the parser what kind
- of phrase to parse.
-
-\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] certifies $t$ with
- respect to $sign$ as a meta-proposition and converts all exceptions
- to an error, including the final message
-\begin{ttbox}
-The error(s) above occurred in axiom "\(name\)"
-\end{ttbox}
-
-\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] similar to {\tt
- cert_axm}, but first reads the string $s$ using the syntax of
- $sign$.
-
-\item[\ttindexbold{rep_cterm} $ct$] decomposes $ct$ as a record
- containing its type, the term itself, its signature, and the maximum
- subscript of its unknowns. The type and maximum subscript are
- computed during certification.
-
-\item[\ttindexbold{Sign.certify_term}] is a more primitive version of
- \texttt{cterm_of}, returning the internal representation instead of
- an abstract \texttt{cterm}.
-
-\end{ttdescription}
-
-
-\section{Types}\index{types|bold}
-Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
-three constructor functions. These correspond to type constructors, free
-type variables and schematic type variables. Types are classified by sorts,
-which are lists of classes (representing an intersection). A class is
-represented by a string.
-\begin{ttbox}
-type class = string;
-type sort = class list;
-
-datatype typ = Type of string * typ list
- | TFree of string * sort
- | TVar of indexname * sort;
-
-infixr 5 -->;
-fun S --> T = Type ("fun", [S, T]);
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructors|bold}
- applies the \textbf{type constructor} named~$a$ to the type operand list~$Ts$.
- Type constructors include~\tydx{fun}, the binary function space
- constructor, as well as nullary type constructors such as~\tydx{prop}.
- Other type constructors may be introduced. In expressions, but not in
- patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
- types.
-
-\item[\ttindexbold{TFree} ($a$, $s$)] \index{type variables|bold}
- is the \textbf{type variable} with name~$a$ and sort~$s$.
-
-\item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknowns|bold}
- is the \textbf{type unknown} with indexname~$v$ and sort~$s$.
- Type unknowns are essentially free type variables, but may be
- instantiated during unification.
-\end{ttdescription}
-
-
-\section{Certified types}
-\index{types!certified|bold}
-Certified types, which are analogous to certified terms, have type
-\ttindexbold{ctyp}.
-
-\subsection{Printing types}
-\index{types!printing of}
-\begin{ttbox}
- string_of_ctyp : ctyp -> string
-Sign.string_of_typ : Sign.sg -> typ -> string
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{string_of_ctyp} $cT$]
-displays $cT$ as a string.
-
-\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
-displays $T$ as a string, using the syntax of~$sign$.
-\end{ttdescription}
-
-
-\subsection{Making and inspecting certified types}
-\begin{ttbox}
-ctyp_of : Sign.sg -> typ -> ctyp
-rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
-Sign.certify_typ : Sign.sg -> typ -> typ
-\end{ttbox}
-\begin{ttdescription}
-
-\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies
- $T$ with respect to signature~$sign$.
-
-\item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record
- containing the type itself and its signature.
-
-\item[\ttindexbold{Sign.certify_typ}] is a more primitive version of
- \texttt{ctyp_of}, returning the internal representation instead of
- an abstract \texttt{ctyp}.
-
-\end{ttdescription}
-
-
\index{theories|)}
--- a/doc-src/Ref/thm.tex Sun Jun 05 22:09:04 2011 +0200
+++ b/doc-src/Ref/thm.tex Mon Jun 06 17:51:14 2011 +0200
@@ -3,58 +3,13 @@
\index{theorems|(}
Theorems, which represent the axioms, theorems and rules of
-object-logics, have type \mltydx{thm}. This chapter begins by
-describing operations that print theorems and that join them in
-forward proof. Most theorem operations are intended for advanced
-applications, such as programming new proof procedures. Many of these
-operations refer to signatures, certified terms and certified types,
-which have the \ML{} types {\tt Sign.sg}, {\tt cterm} and {\tt ctyp}
-and are discussed in Chapter~\ref{theories}. Beginning users should
-ignore such complexities --- and skip all but the first section of
-this chapter.
+object-logics, have type \mltydx{thm}. This chapter describes
+operations that join theorems in forward proof. Most theorem
+operations are intended for advanced applications, such as programming
+new proof procedures.
\section{Basic operations on theorems}
-\subsection{Pretty-printing a theorem}
-\index{theorems!printing of}
-\begin{ttbox}
-prth : thm -> thm
-prths : thm list -> thm list
-prthq : thm Seq.seq -> thm Seq.seq
-print_thm : thm -> unit
-print_goals : int -> thm -> unit
-string_of_thm : thm -> string
-\end{ttbox}
-The first three commands are for interactive use. They are identity
-functions that display, then return, their argument. The \ML{} identifier
-{\tt it} will refer to the value just displayed.
-
-The others are for use in programs. Functions with result type {\tt unit}
-are convenient for imperative programming.
-
-\begin{ttdescription}
-\item[\ttindexbold{prth} {\it thm}]
-prints {\it thm\/} at the terminal.
-
-\item[\ttindexbold{prths} {\it thms}]
-prints {\it thms}, a list of theorems.
-
-\item[\ttindexbold{prthq} {\it thmq}]
-prints {\it thmq}, a sequence of theorems. It is useful for inspecting
-the output of a tactic.
-
-\item[\ttindexbold{print_thm} {\it thm}]
-prints {\it thm\/} at the terminal.
-
-\item[\ttindexbold{print_goals} {\it limit\/} {\it thm}]
-prints {\it thm\/} in goal style, with the premises as subgoals. It prints
-at most {\it limit\/} subgoals. The subgoal module calls {\tt print_goals}
-to display proof states.
-
-\item[\ttindexbold{string_of_thm} {\it thm}]
-converts {\it thm\/} to a string.
-\end{ttdescription}
-
\subsection{Forward proof: joining rules by resolution}
\index{theorems!joining by resolution}
@@ -371,123 +326,6 @@
\section{*Primitive meta-level inference rules}
\index{meta-rules|(}
-These implement the meta-logic in the style of the {\sc lcf} system,
-as functions from theorems to theorems. They are, rarely, useful for
-deriving results in the pure theory. Mainly, they are included for
-completeness, and most users should not bother with them. The
-meta-rules raise exception \xdx{THM} to signal malformed premises,
-incompatible signatures and similar errors.
-
-\index{meta-assumptions}
-The meta-logic uses natural deduction. Each theorem may depend on
-meta-level assumptions. Certain rules, such as $({\Imp}I)$,
-discharge assumptions; in most other rules, the conclusion depends on all
-of the assumptions of the premises. Formally, the system works with
-assertions of the form
-\[ \phi \quad [\phi@1,\ldots,\phi@n], \]
-where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions. This can be
-also read as a single conclusion sequent $\phi@1,\ldots,\phi@n \vdash
-\phi$. Do not confuse meta-level assumptions with the object-level
-assumptions in a subgoal, which are represented in the meta-logic
-using~$\Imp$.
-
-Each theorem has a signature. Certified terms have a signature. When a
-rule takes several premises and certified terms, it merges the signatures
-to make a signature for the conclusion. This fails if the signatures are
-incompatible.
-
-\medskip
-
-The following presentation of primitive rules ignores sort
-hypotheses\index{sort hypotheses} (see also \S\ref{sec:sort-hyps}). These are
-handled transparently by the logic implementation.
-
-\bigskip
-
-\index{meta-implication}
-The \textbf{implication} rules are $({\Imp}I)$
-and $({\Imp}E)$:
-\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad
- \infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi} \]
-
-\index{meta-equality}
-Equality of truth values means logical equivalence:
-\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi &
- \psi\Imp\phi}
- \qquad
- \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \]
-
-The \textbf{equality} rules are reflexivity, symmetry, and transitivity:
-\[ {a\equiv a}\,(refl) \qquad
- \infer[(sym)]{b\equiv a}{a\equiv b} \qquad
- \infer[(trans)]{a\equiv c}{a\equiv b & b\equiv c} \]
-
-\index{lambda calc@$\lambda$-calculus}
-The $\lambda$-conversions are $\alpha$-conversion, $\beta$-conversion, and
-extensionality:\footnote{$\alpha$-conversion holds if $y$ is not free
-in~$a$; $(ext)$ holds if $x$ is not free in the assumptions, $f$, or~$g$.}
-\[ {(\lambda x.a) \equiv (\lambda y.a[y/x])} \qquad
- {((\lambda x.a)(b)) \equiv a[b/x]} \qquad
- \infer[(ext)]{f\equiv g}{f(x) \equiv g(x)} \]
-
-The \textbf{abstraction} and \textbf{combination} rules let conversions be
-applied to subterms:\footnote{Abstraction holds if $x$ is not free in the
-assumptions.}
-\[ \infer[(abs)]{(\lambda x.a) \equiv (\lambda x.b)}{a\equiv b} \qquad
- \infer[(comb)]{f(a)\equiv g(b)}{f\equiv g & a\equiv b} \]
-
-\index{meta-quantifiers}
-The \textbf{universal quantification} rules are $(\Forall I)$ and $(\Forall
-E)$:\footnote{$(\Forall I)$ holds if $x$ is not free in the assumptions.}
-\[ \infer[(\Forall I)]{\Forall x.\phi}{\phi} \qquad
- \infer[(\Forall E)]{\phi[b/x]}{\Forall x.\phi} \]
-
-
-\subsection{Assumption rule}
-\index{meta-assumptions}
-\begin{ttbox}
-assume: cterm -> thm
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{assume} $ct$]
-makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$.
-The rule checks that $ct$ has type $prop$ and contains no unknowns, which
-are not allowed in assumptions.
-\end{ttdescription}
-
-\subsection{Implication rules}
-\index{meta-implication}
-\begin{ttbox}
-implies_intr : cterm -> thm -> thm
-implies_intr_list : cterm list -> thm -> thm
-implies_intr_hyps : thm -> thm
-implies_elim : thm -> thm -> thm
-implies_elim_list : thm -> thm list -> thm
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{implies_intr} $ct$ $thm$]
-is $({\Imp}I)$, where $ct$ is the assumption to discharge, say~$\phi$. It
-maps the premise~$\psi$ to the conclusion $\phi\Imp\psi$, removing all
-occurrences of~$\phi$ from the assumptions. The rule checks that $ct$ has
-type $prop$.
-
-\item[\ttindexbold{implies_intr_list} $cts$ $thm$]
-applies $({\Imp}I)$ repeatedly, on every element of the list~$cts$.
-
-\item[\ttindexbold{implies_intr_hyps} $thm$]
-applies $({\Imp}I)$ to discharge all the hypotheses (assumptions) of~$thm$.
-It maps the premise $\phi \; [\phi@1,\ldots,\phi@n]$ to the conclusion
-$\List{\phi@1,\ldots,\phi@n}\Imp\phi$.
-
-\item[\ttindexbold{implies_elim} $thm@1$ $thm@2$]
-applies $({\Imp}E)$ to $thm@1$ and~$thm@2$. It maps the premises $\phi\Imp
-\psi$ and $\phi$ to the conclusion~$\psi$.
-
-\item[\ttindexbold{implies_elim_list} $thm$ $thms$]
-applies $({\Imp}E)$ repeatedly to $thm$, using each element of~$thms$ in
-turn. It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and
-$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$.
-\end{ttdescription}
\subsection{Logical equivalence rules}
\index{meta-equality}
@@ -561,97 +399,6 @@
\end{ttdescription}
-\subsection{Forall introduction rules}
-\index{meta-quantifiers}
-\begin{ttbox}
-forall_intr : cterm -> thm -> thm
-forall_intr_list : cterm list -> thm -> thm
-forall_intr_frees : thm -> thm
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{forall_intr} $x$ $thm$]
-applies $({\Forall}I)$, abstracting over all occurrences (if any!) of~$x$.
-The rule maps the premise $\phi$ to the conclusion $\Forall x.\phi$.
-Parameter~$x$ is supplied as a cterm. It may be an unknown or a free
-variable (provided it does not occur in the assumptions).
-
-\item[\ttindexbold{forall_intr_list} $xs$ $thm$]
-applies $({\Forall}I)$ repeatedly, on every element of the list~$xs$.
-
-\item[\ttindexbold{forall_intr_frees} $thm$]
-applies $({\Forall}I)$ repeatedly, generalizing over all the free variables
-of the premise.
-\end{ttdescription}
-
-
-\subsection{Forall elimination rules}
-\begin{ttbox}
-forall_elim : cterm -> thm -> thm
-forall_elim_list : cterm list -> thm -> thm
-forall_elim_var : int -> thm -> thm
-forall_elim_vars : int -> thm -> thm
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{forall_elim} $ct$ $thm$]
-applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
-$\phi[ct/x]$. The rule checks that $ct$ and $x$ have the same type.
-
-\item[\ttindexbold{forall_elim_list} $cts$ $thm$]
-applies $({\Forall}E)$ repeatedly, on every element of the list~$cts$.
-
-\item[\ttindexbold{forall_elim_var} $k$ $thm$]
-applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
-$\phi[\Var{x@k}/x]$. Thus, it replaces the outermost $\Forall$-bound
-variable by an unknown having subscript~$k$.
-
-\item[\ttindexbold{forall_elim_vars} $k$ $thm$]
-applies {\tt forall_elim_var}~$k$ repeatedly until the theorem no longer has
-the form $\Forall x.\phi$.
-\end{ttdescription}
-
-
-\subsection{Instantiation of unknowns}
-\index{instantiation}
-\begin{alltt}\footnotesize
-instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list -> thm -> thm
-\end{alltt}
-There are two versions of this rule. The primitive one is
-\ttindexbold{Thm.instantiate}, which merely performs the instantiation and can
-produce a conclusion not in normal form. A derived version is
-\ttindexbold{Drule.instantiate}, which normalizes its conclusion.
-
-\begin{ttdescription}
-\item[\ttindexbold{instantiate} ($tyinsts$,$insts$) $thm$]
-simultaneously substitutes types for type unknowns (the
-$tyinsts$) and terms for term unknowns (the $insts$). Instantiations are
-given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the
-same type as $v$) or a type (of the same sort as~$v$). All the unknowns
-must be distinct.
-
-In some cases, \ttindex{instantiate'} (see \S\ref{sec:instantiate})
-provides a more convenient interface to this rule.
-\end{ttdescription}
-
-
-
-
-\subsection{Freezing/thawing type unknowns}
-\index{type unknowns!freezing/thawing of}
-\begin{ttbox}
-freezeT: thm -> thm
-varifyT: thm -> thm
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{freezeT} $thm$]
-converts all the type unknowns in $thm$ to free type variables.
-
-\item[\ttindexbold{varifyT} $thm$]
-converts all the free type variables in $thm$ to type unknowns.
-\end{ttdescription}
-
-
\section{Derived rules for goal-directed proof}
Most of these rules have the sole purpose of implementing particular
tactics. There are few occasions for applying them directly to a theorem.