\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.

 See \S\ref{sec:intro-theories} for its most basic commands, such as

 \texttt{use_thy}.  There are a few more operations available.

 \begin{ttbox}

 use_thy_only    : string -> unit

 update_thy_only : string -> unit

 touch_thy       : string -> unit

 remove_thy      : string -> unit

 delete_tmpfiles : bool ref \hfill\textbf{initially true}

 \end{ttbox}

 \begin{ttdescription}

 \item[\ttindexbold{use_thy_only} "$name$";] is similar to \texttt{use_thy},

   but processes the actual theory file $name$\texttt{.thy} only, ignoring

   $name$\texttt{.ML}.  This might be useful in replaying proof scripts by hand

   from the very beginning, starting with the fresh theory.

 \item[\ttindexbold{update_thy_only} "$name$";] is similar to

   \texttt{update_thy}, but processes the actual theory file

   $name$\texttt{.thy} only, ignoring $name$\texttt{.ML}.

 \item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the

   internal graph as outdated.  While the theory remains usable, subsequent

   operations such as \texttt{use_thy} may cause a reload.

 \item[\ttindexbold{remove_thy} "$name$";] deletes theory node $name$,

   including \emph{all} of its descendants.  Beware!  This is a quick way to

   dispose a large number of theories at once.  Note that {\ML} bindings to

   theorems etc.\ of removed theories may still persist.

 \end{ttdescription}

 \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}

 subthy      : theory * theory -> bool

 eq_thy      : theory * theory -> bool

 transfer    : theory -> thm -> thm

 transfer_sg : Sign.sg -> thm -> thm

 \end{ttbox}

 Inclusion and equality of theories is determined by unique

 identification stamps that are created when declaring new components.

 Theorems contain a reference to the theory (actually to its signature)

 they have been derived in.  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{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$

   is included in $thy@2$ wrt.\ identification stamps.

 \item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$

   is exactly the same as $thy@2$.

 \item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to

   theory $thy$, provided the latter includes the theory of $thm$.

 \item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to

   \texttt{transfer}, but identifies the super theory via its

   signature.

 \end{ttdescription}

 \subsection{*Primitive theories}

 \begin{ttbox}

 ProtoPure.thy  : theory

 Pure.thy       : theory

 CPure.thy      : theory

 \end{ttbox}

 \begin{description}

 \item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},

   \ttindexbold{CPure.thy}] contain the syntax and signature of the

   meta-logic.  There are basically no axioms: meta-level inferences

   are carried out by \ML\ functions.  \texttt{Pure} and \texttt{CPure}

   just differ in their concrete syntax of prefix function application:

   $t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in

   \texttt{CPure}.  \texttt{ProtoPure} is their common parent,

   containing no syntax for printing prefix applications at all!

 %% FIXME

 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends

 %  the theory $thy$ with new types, constants, etc.  $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

 %extend_theory  : theory -> string -> \(\cdots\) -> theory

 %\begin{ttbox}

 %Attempt to merge different versions of theory: \(T\)

 %\end{ttbox}

 \end{description}

 %% FIXME

 %\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}

 \subsection{Inspecting a theory}\label{sec:inspct-thy}

 \index{theories!inspecting|bold}

 \begin{ttbox}

 print_syntax        : theory -> unit

 print_theory        : theory -> unit

 parents_of          : theory -> theory list

 ancestors_of        : theory -> theory list

 sign_of             : theory -> Sign.sg

 Sign.stamp_names_of : Sign.sg -> string list

 \end{ttbox}

 These provide means of viewing a theory's components.

 \begin{ttdescription}

 \item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$

   (grammar, macros, translation functions etc., see

   page~\pageref{pg:print_syn} for more details).

 \item[\ttindexbold{print_theory} $thy$] prints the logical parts of

   $thy$, excluding the syntax.

 \item[\ttindexbold{parents_of} $thy$] returns the direct ancestors

   of~$thy$.

 \item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$

   (not including $thy$ itself).

 \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.

 \item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures}

   returns the names of the identification \rmindex{stamps} of ax

   signature.  These coincide with the names of its full ancestry

   including that of $sg$ itself.

 \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: