doc-src/Ref/theories.tex

merged

\chapter{Theories, Terms and Types} \label{theories}
\index{theories|(}

\section{The theory loader}\label{sec:more-theories}
\index{theories!reading}\index{files!reading}

Isabelle's theory loader manages dependencies of the internal graph of theory
nodes (the \emph{theory database}) and the external view of the file system.

\medskip Theory and {\ML} files are located by skimming through the
directories listed in Isabelle's internal load path, which merely contains the
current directory ``\texttt{.}'' by default.  The load path may be accessed by
the following operations.

\begin{ttbox}
show_path: unit -> string list
add_path: string -> unit
del_path: string -> unit
reset_path: unit -> unit
with_path: string -> ('a -> 'b) -> 'a -> 'b
no_document: ('a -> 'b) -> 'a -> 'b
\end{ttbox}

\begin{ttdescription}
\item[\ttindexbold{show_path}();] displays the load path components in
  canonical string representation (which is always according to Unix rules).
  
\item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning
  of the load path.
  
\item[\ttindexbold{del_path} "$dir$";] removes any occurrences of component
  $dir$ from the load path.
  
\item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}''
  (current directory) only.
  
\item[\ttindexbold{with_path} "$dir$" $f$ $x$;] temporarily adds component
  $dir$ to the beginning of the load path while executing $(f~x)$.
  
\item[\ttindexbold{no_document} $f$ $x$;] temporarily disables {\LaTeX}
  document generation while executing $(f~x)$.

\end{ttdescription}

Furthermore, in operations referring indirectly to some file (e.g.\ 
\texttt{use_dir}) the argument may be prefixed by a directory that will be
temporarily appended to the load path, too.


\section{Basic operations on theories}\label{BasicOperationsOnTheories}

\subsection{*Theory inclusion}
\begin{ttbox}
transfer    : theory -> thm -> thm
\end{ttbox}

Transferring theorems to super theories has no logical significance,
but may affect some operations in subtle ways (e.g.\ implicit merges
of signatures when applying rules, or pretty printing of theorems).

\begin{ttdescription}

\item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to
  theory $thy$, provided the latter includes the theory of $thm$.
  
\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.
\begin{ttdescription}
\item[\ttindexbold{loose_bnos} $t$]
  returns the list of all dangling bound variable references.  In
  particular, \texttt{Bound~0} is loose unless it is enclosed in an
  abstraction.  Similarly \texttt{Bound~1} is loose unless it is enclosed in
  at least two abstractions; if enclosed in just one, the list will contain
  the number 0.  A well-formed term does not contain any loose variables.

\item[\ttindexbold{incr_boundvars} $j$]
  increases a term's dangling bound variables by the offset~$j$.  This is
  required when moving a subterm into a context where it is enclosed by a
  different number of abstractions.  Bound variables with a matching
  abstraction are unaffected.

\item[\ttindexbold{abstract_over} $(v,t)$]
  forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
  It replaces every occurrence of \(v\) by a \texttt{Bound} variable with the
  correct index.

\item[\ttindexbold{variant_abs} $(a,T,u)$]
  substitutes into $u$, which should be the body of an abstraction.
  It replaces each occurrence of the outermost bound variable by a free
  variable.  The free variable has type~$T$ and its name is a variant
  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|)}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "ref"
%%% End: