doc-src/Ref/theories.tex

Mirabelle: command-line action options may either be key=value or just key

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