# HG changeset patch # User wenzelm # Date 1307375474 -7200 # Node ID 34ed34804d90ea033fc755d946d6f7cdeee6b507 # Parent ac4094f30a44676b01205bab04e288928ac14420 removed obsolete material (superseded by implementation manual); diff -r ac4094f30a44 -r 34ed34804d90 doc-src/Ref/theories.tex --- 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|)} diff -r ac4094f30a44 -r 34ed34804d90 doc-src/Ref/thm.tex --- 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.