--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/theories.tex Wed Nov 10 05:00:57 1993 +0100
@@ -0,0 +1,445 @@
+%% $Id$
+\chapter{Theories, Terms and Types} \label{theories}
+\index{theories|(}\index{signatures|bold}
+\index{reading!axioms|see{{\tt extend_theory} and {\tt assume_ax}}}
+Theories organize the syntax, declarations and axioms of a mathematical
+development. They are built, starting from the Pure theory, by extending
+and merging existing theories. They have the \ML{} type \ttindex{theory}.
+Theory operations signal errors by raising exception \ttindex{THEORY},
+returning a message and a list of theories.
+
+Signatures, which contain information about sorts, types, constants and
+syntax, have the \ML{} type~\ttindexbold{Sign.sg}. For identification,
+each signature carries a unique list of {\bf stamps}, which are~\ML{}
+references (to strings). The strings serve as human-readable names; the
+references serve as unique identifiers. Each primitive signature has a
+single stamp. When two signatures are merged, their lists of stamps are
+also merged. Every theory carries a unique signature.
+
+Terms and types are the underlying representation of logical syntax. Their
+\ML{} definitions are irrelevant to naive Isabelle users. Programmers who wish
+to extend Isabelle may need to know such details, say to code a tactic that
+looks for subgoals of a particular form. Terms and types may be
+`certified' to be well-formed with respect to a given signature.
+
+\section{Defining Theories}
+\label{DefiningTheories}
+
+Theories can be defined either using concrete syntax or by calling certain
+\ML-functions (see \S\ref{BuildingATheory}). Figure~\ref{TheorySyntax}
+presents the concrete syntax for theories. This grammar employs the
+following conventions:
+\begin{itemize}
+\item Identifiers such as $theoryDef$ denote nonterminal symbols.
+\item Text in {\tt typewriter font} denotes terminal symbols.
+\item \ldots{} indicates repetition of a phrase.
+\item A vertical bar~($|$) separates alternative phrases.
+\item Square [brackets] enclose optional phrases.
+\item $id$ stands for an Isabelle identifier.
+\item $string$ stands for an ML string, with its quotation marks.
+\item $k$ stands for a natural number.
+\item $text$ stands for arbitrary ML text.
+\end{itemize}
+
+\begin{figure}[hp]
+\begin{center}
+\begin{tabular}{rclc}
+$theoryDef$ &=& $id$ {\tt=} $id@1$ {\tt+} \dots {\tt+} $id@n$
+ [{\tt+} $extension$]\\\\
+$extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$]
+ [$rules$] {\tt end} [$ml$]\\\\
+$classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\
+$class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\
+$default$ &=& \ttindex{default} $sort$ \\\\
+$sort$ &=& $id$ ~~$|$~~ {\tt\{} $id@1${\tt,} \dots{\tt,} $id@n$ {\tt\}} \\\\
+$name$ &=& $id$ ~~$|$~~ $string$ \\\\
+$types$ &=& \ttindex{types} $typeDecl$ \dots $typeDecl$ \\\\
+$typeDecl$ &=& $name${\tt,} \dots{\tt,} $name$ $k$
+ [{\tt(} $infix$ {\tt)}] \\\\
+$infix$ &=& \ttindex{infixl} $k$ ~~$|$~~ \ttindex{infixr} $k$ \\\\
+$arities$ &=& \ttindex{arities} $arityDecl$ \dots $arityDecl$ \\\\
+$arityDecl$ &=& $name${\tt,} \dots{\tt,} $name$ {\tt::} $arity$ \\\\
+$arity$ &=& [{\tt(} $sort${\tt,} \dots{\tt,} $sort$ {\tt)}] $id$ \\\\
+$consts$ &=& \ttindex{consts} $constDecl$ \dots $constDecl$ \\\\
+$constDecl$ &=& $name@1${\tt,} \dots{\tt,} $name@n$ {\tt::} $string$
+ [{\tt(} $mixfix$ {\tt)}] \\\\
+$mixfix$ &=& $string$
+ [ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\
+ &$|$& $infix$ \\
+ &$|$& \ttindex{binder} $string$ $k$\\\\
+$rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\
+$rule$ &=& $id$ $string$ \\\\
+$ml$ &=& \ttindex{ML} $text$
+\end{tabular}
+\end{center}
+\caption{Theory Syntax}
+\label{TheorySyntax}
+\end{figure}
+
+The different parts of a theory definition are interpreted as follows:
+\begin{description}
+\item[$theoryDef$] A theory has a name $id$ and is an extension of the union
+ of existing theories $id@1$ \dots $id@n$ with new classes, types,
+ constants, syntax and axioms. The basic theory, which contains only the
+ meta-logic, is called {\tt Pure}.
+\item[$class$] The new class $id$ is declared as a subclass of existing
+ classes $id@1$ \dots $id@n$. This rules out cyclic class structures.
+ Isabelle automatically computes the transitive closure of subclass
+ hierarchies. Hence it is not necessary to declare $c@1 < c@3$ in addition
+ to $c@1 < c@2$ and $c@2 < c@3$.
+\item[$default$] introduces $sort$ as the new default sort for type
+ variables. Unconstrained type variables in an input string are
+ automatically constrained by $sort$; this does not apply to type variables
+ created internally during type inference. If omitted,
+ the default sort is the same as in the parent theory.
+\item[$sort$] is a finite set $id@1$ \dots $id@n$ of classes; a single class
+ $id$ abbreviates the singleton set {\tt\{}$id${\tt\}}.
+\item[$name$] is either an alphanumeric identifier or an arbitrary string.
+\item[$typeDecl$] Each $name$ is declared as a new type constructor with
+ $k$ arguments. Only binary type constructors can have infix status and
+ symbolic names ($string$).
+\item[$infix$] declares a type or constant to be an infix operator of
+ precedence $k$ associating to the left ({\tt infixl}) or right ({\tt
+ infixr}).
+\item[$arityDecl$] Each existing type constructor $name@1$ \dots $name@n$
+ is given the additional arity $arity$.
+\item[$constDecl$] The new constants $name@1$ \dots $name@n$ are declared to
+ be of type $string$. For display purposes they can be annotated with
+ $mixfix$ declarations.
+\item[$mixfix$] $string$ is a mixfix template of the form {\tt"}\dots{\tt\_}
+ \dots{\tt\_} \dots{\tt"} where the $i$-th underscore indicates the position
+ where the $i$-th argument should go, $k@i$ is the minimum precedence of
+ the $i$-th argument, and $k$ the precedence of the construct. The list
+ \hbox{\tt[$k@1$, \dots, $k@n$]} is optional.
+
+ Binary constants can be given infix status.
+
+ A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
+ binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
+ like $f(F)$; $p$ is the precedence of the construct.
+\item[$rule$] A rule consists of a name $id$ and a formula $string$. Rule
+ names must be distinct.
+\item[$ml$] This final part of a theory consists of ML code,
+ typically for parse and print translations.
+\end{description}
+The $mixfix$ and $ml$ sections are explained in more detail in the {\it
+Defining Logics} chapter of the {\it Logics} manual.
+
+\begin{ttbox}
+use_thy: string -> unit
+\end{ttbox}
+Each theory definition must reside in a separate file. Let the file {\it
+ tf}{\tt.thy} contain the definition of a theory called $TF$ with rules named
+$r@1$ \dots $r@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it tf\/}{\tt"} reads
+file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file {\tt.}{\it
+ tf}{\tt.thy.ML}, and reads the latter file. This declares an {\ML}
+structure~$TF$ containing a component {\tt thy} for the new theory
+and components $r@1$ \dots $r@n$ for the rules; it also contains the
+definitions of the {\tt ML} section if any. Then {\tt use_thy}
+reads the file {\it tf}{\tt.ML}, if it exists; this file normally contains
+proofs involving the new theory.
+
+
+\section{Basic operations on theories}
+\subsection{Extracting an axiom from a theory}
+\index{theories!extracting axioms|bold}\index{axioms}
+\begin{ttbox}
+get_axiom: theory -> string -> thm
+assume_ax: theory -> string -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{get_axiom} $thy$ $name$]
+returns an axiom with the given $name$ from $thy$, raising exception
+\ttindex{THEORY} if none exists. Merging theories can cause several axioms
+to have the same name; {\tt get_axiom} returns an arbitrary one.
+
+\item[\ttindexbold{assume_ax} $thy$ $formula$]
+reads the {\it formula} using the syntax of $thy$, following the same
+conventions as axioms in a theory definition. You can thus pretend that
+{\it formula} is an axiom; in fact, {\tt assume_ax} returns an assumption.
+You can use the resulting theorem like an axiom. Note that
+\ttindex{result} complains about additional assumptions, but
+\ttindex{uresult} does not.
+
+For example, if {\it formula} is
+\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form
+\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]}
+\end{description}
+
+\subsection{Building a theory}
+\label{BuildingATheory}
+\index{theories!constructing|bold}
+\begin{ttbox}
+pure_thy: theory
+merge_theories: theory * theory -> theory
+extend_theory: theory -> string
+ -> (class * class list) list
+ * sort
+ * (string list * int)list
+ * (string list * (sort list * class))list
+ * (string list * string)list * sext option
+ -> (string*string)list -> theory
+\end{ttbox}
+Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is
+a synonym for \hbox{\tt class list}.
+\begin{description}
+\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
+ of the meta-logic. There are no axioms: meta-level inferences are carried
+ out by \ML\ functions.
+\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
+ theories $thy@1$ and $thy@2$. The resulting theory contains all types,
+ constants and axioms of the constituent theories; its default sort is the
+ union of the default sorts of the constituent theories.
+\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
+ ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
+\hfill\break %%% include if line is just too short
+is the \ML-equivalent of the following theory definition:
+\begin{ttbox}
+\(T\) = \(thy\) +
+classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
+ \dots
+default {\(d@1,\dots,d@r\)}
+types \(tycon@1\),\dots,\(tycon@i\) \(n\)
+ \dots
+arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
+ \dots
+consts \(b@1\),\dots,\(b@k\) :: \(\tau\)
+ \dots
+rules \(name\) \(rule\)
+ \dots
+end
+\end{ttbox}
+where
+\begin{tabular}[t]{l@{~=~}l}
+$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
+$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
+$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
+$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
+\\
+$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
+$rules$ & \tt[("$name$",$rule$),\dots]
+\end{tabular}
+
+If theories are defined as in \S\ref{DefiningTheories}, new syntax is added
+as mixfix annotations to constants. Using {\tt extend_theory}, new syntax can
+be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}. The
+latter case is not documented.
+
+$T$ identifies the theory internally. When a theory is redeclared, say to
+change an incorrect axiom, bindings to the old axiom may persist. Isabelle
+ensures that the old and new theories are not involved in the same proof.
+Attempting to combine different theories having the same name $T$ yields the
+fatal error
+\begin{center} \tt
+Attempt to merge different versions of theory: $T$
+\end{center}
+\end{description}
+
+
+\subsection{Inspecting a theory}
+\index{theories!inspecting|bold}
+\begin{ttbox}
+print_theory : theory -> unit
+axioms_of : theory -> (string*thm)list
+parents_of : theory -> theory list
+sign_of : theory -> Sign.sg
+stamps_of_thy : theory -> string ref list
+\end{ttbox}
+These provide a simple means of viewing a theory's components.
+Unfortunately, there is no direct connection between a theorem and its
+theory.
+\begin{description}
+\item[\ttindexbold{print_theory} {\it thy}]
+prints the theory {\it thy\/} at the terminal as a set of identifiers.
+
+\item[\ttindexbold{axioms_of} $thy$]
+returns the axioms of~$thy$ and its ancestors.
+
+\item[\ttindexbold{parents_of} $thy$]
+returns the parents of~$thy$. This list contains zero, one or two
+elements, depending upon whether $thy$ is {\tt pure_thy},
+\hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}.
+
+\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
+returns the stamps of the signature associated with~$thy$.
+
+\item[\ttindexbold{sign_of} $thy$]
+returns the signature associated with~$thy$. It is useful with functions
+like {\tt read_instantiate_sg}, which take a signature as an argument.
+\end{description}
+
+
+\section{Terms}
+\index{terms|bold}
+Terms belong to the \ML{} type \ttindexbold{term}, which is a concrete datatype
+with six constructors: there are six kinds of term.
+\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{description}
+\item[\ttindexbold{Const}($a$, $T$)]
+is the {\bf constant} with name~$a$ and type~$T$. Constants include
+connectives like $\land$ and $\forall$ (logical constants), as well as
+constants like~0 and~$Suc$. Other constants may be required to define the
+concrete syntax of a logic.
+
+\item[\ttindexbold{Free}($a$, $T$)]
+is the {\bf free variable} with name~$a$ and type~$T$.
+
+\item[\ttindexbold{Var}($v$, $T$)]
+is the {\bf scheme variable} with indexname~$v$ and type~$T$. An
+\ttindexbold{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$]
+is the {\bf 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~336]{paulson91}.
+
+\item[\ttindexbold{Abs}($a$, $T$, $u$)]
+is the {\bf 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[\tt $t$ \$ $u$] \index{$@{\tt\$}|bold}
+is the {\bf application} of~$t$ to~$u$.
+\end{description}
+Application is written as an infix operator in order to aid readability.
+For example, here is an \ML{} pattern to recognize first-order formula of
+the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
+\begin{ttbox}
+Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
+\end{ttbox}
+
+
+\section{Certified terms}
+\index{terms!certified|bold}\index{signatures}
+A term $t$ can be {\bf certified} under a signature to ensure that every
+type in~$t$ is declared in the signature and every constant in~$t$ is
+declared as a constant of the same type in the signature. It must be
+well-typed and must not have any `loose' bound variable
+references.\footnote{This concerns the internal representation of variable
+binding using de Bruijn indexes.} Meta-rules such as {\tt forall_elim} take
+certified terms as arguments.
+
+Certified terms belong to the abstract type \ttindexbold{Sign.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{printing!terms|bold}
+\begin{ttbox}
+Sign.string_of_cterm : Sign.cterm -> string
+Sign.string_of_term : Sign.sg -> term -> string
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{Sign.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{description}
+
+\subsection{Making and inspecting certified terms}
+\begin{ttbox}
+Sign.cterm_of : Sign.sg -> term -> Sign.cterm
+Sign.read_cterm : Sign.sg -> string * typ -> Sign.cterm
+Sign.rep_cterm : Sign.cterm -> \{T:typ, t:term,
+ sign: Sign.sg, maxidx:int\}
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{Sign.cterm_of} $sign$ $t$] \index{signatures}
+certifies $t$ with respect to signature~$sign$.
+
+\item[\ttindexbold{Sign.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{Sign.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.
+\end{description}
+
+
+\section{Types}
+\index{types|bold}
+Types belong to the \ML{} type \ttindexbold{typ}, which is a concrete
+datatype with three constructors. Types are classified by sorts, which are
+lists of classes. 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{description}
+\item[\ttindexbold{Type}($a$, $Ts$)]
+applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
+Type constructors include~\ttindexbold{fun}, the binary function space
+constructor, as well as nullary type constructors such
+as~\ttindexbold{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$)]
+is the {\bf free type variable} with name~$a$ and sort~$s$.
+
+\item[\ttindexbold{TVar}($v$, $s$)]
+is the {\bf scheme type variable} with indexname~$v$ and sort~$s$. Scheme
+type variables are essentially free type variables, but may be instantiated
+during unification.
+\end{description}
+
+
+\section{Certified types}
+\index{types!certified|bold}
+Certified types, which are analogous to certified terms, have type
+\ttindexbold{Sign.ctyp}.
+
+\subsection{Printing types}
+\index{printing!types|bold}
+\begin{ttbox}
+Sign.string_of_ctyp : Sign.ctyp -> string
+Sign.string_of_typ : Sign.sg -> typ -> string
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{Sign.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{description}
+
+
+\subsection{Making and inspecting certified types}
+\begin{ttbox}
+Sign.ctyp_of : Sign.sg -> typ -> Sign.ctyp
+Sign.rep_ctyp : Sign.ctyp -> \{T: typ, sign: Sign.sg\}
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{Sign.ctyp_of} $sign$ $T$] \index{signatures}
+certifies $T$ with respect to signature~$sign$.
+
+\item[\ttindexbold{Sign.rep_ctyp} $cT$]
+decomposes $cT$ as a record containing the type itself and its signature.
+\end{description}
+
+\index{theories|)}