1\section{Theories} 2\label{theories} 3 4The result of a session with the \HOL{} system is an object called a 5{\it theory\/}. This object is closely related to what a logician 6would call a theory, but there are some differences arising from the 7needs of mechanical proof. A \HOL{} theory, like a logician's theory, 8contains sets of types, constants, definitions and axioms. In 9addition, however, a \HOL{} theory contains an explicit list of 10theorems that have been proved from the axioms and definitions. 11Logicians normally do not need to distinguish theorems that have 12actually been proved from those that could be proved, hence they do 13not normally consider sets of proven theorems as part of a theory; 14rather, they take the theorems of a theory to be the (often infinite) 15set of all consequences of the axioms and definitions. Another 16difference between logicians' theories and \HOL{} theories is that, for 17logicians, theories are relatively static objects, but in \HOL{} they 18can be thought of as potentially extendable. For example, the \HOL\ 19system provides tools for adding to theories and combining theories. 20A typical interaction with \HOL{} consists in combining some existing 21theories, making some definitions, proving some theorems and then 22saving the resulting new theory. 23 24The purpose of the \HOL{} system is to provide tools to enable 25well-formed theories to be constructed. All the theorems of such 26theories are logical consequences of the definitions and axioms of the 27theory. The \HOL{} system ensures that only well-formed theories can 28be constructed by allowing theorems to be created by {\it formal 29 proof\/} only. 30 31A theory is represented in the \HOL{} system as a collection of SML 32object files, called theory files. Each file has a name of the form 33$name$\ml{Theory.}$ext$, where $name$ is a string supplied by the 34user, and $ext$ is one of \ml{sig}, \ml{sml}, \ml{ui}, \ml{uo}. 35 36Theory files are structured hierarchically to represent sequences of 37extensions of an initial theory called \ml{scratch}. Each theory file 38making up a theory records some types, constants, axioms and theorems, 39together with pointers to other theory files called its {\it 40 parents\/}. This collection of reachable files is called the {\it 41 ancestry\/} of the theory file. Axioms, definitions and theorems are 42named in the \HOL{} system by two strings: the name of the theory file 43where they are stored, together with a name within that file supplied 44by the user. Specifically, axioms, definitions and theorems are named 45by a pair of strings $\langle thy,name\rangle$ where $thy$ is the name 46of the theory current when the item was declared and $name$ is a 47specific name supplied by the user (see the functions \ml{new\_axiom}, 48\ml{new\_definition} \etc\ below). 49 50A typical piece of work with the \HOL{} system consists in a number of 51sessions. A theorem-proving session consists of interactions with the 52system through its ``command-line interface''. At the same time, it's 53important that the commands the user enters are saved in some sort of 54file (presumably through an editor) so that these commands can be 55replayed later. For the first sessions of theory development, each 56time \HOL{} is started, the saved commands from previous sessions will 57need to be re-entered into the system. This can be done with 58cut-and-paste functionality, or the \ml{use} command (which takes a 59file-name and reads it for input). 60 61Eventually (possibly even after the very first session; this is a 62matter of taste), the theory under development will be in a 63sufficiently polished state that the user will want to save it to a 64``script'' file and compile it. This process is described further in 65the examples below, but produces a theory file that can be loaded in 66the same way as the system's built-in theories. 67 68There is always a {\it current theory\/}, whose name is given by the 69function \ml{current\_theory}. This function maps the unit value, 70written `\ml{()}' in \ML, to a string giving the name of the current 71theory. Thus the \ML{} expression \ml{current\_theory ()} evaluates to 72a string giving the name of the current theory. Initially \HOL{} has 73its current theory called \ml{scratch}. In the examples so far, there 74hasn't been a call to \ml{new\_theory}, so the current theory is still 75``scratch''. 76 77\begin{session}\begin{verbatim} 78- current_theory(); 79> val it = "scratch" : string 80- 81\end{verbatim}\end{session} 82 83 Executing \ml{new\_theory`$thy$`} creates a new theory called 84 $thy$. The remaining example sessions will demonstrate the 85 construction of a theory of prime numbers. 86 87\begin{session}\begin{verbatim} 88- new_theory "primes"; 89> val it = () : unit 90\end{verbatim}\end{session} 91 92\noindent 93This starts a theory called \ml{primes}, which is to be made into a 94theory containing definitions and theorems about the prime numbers. 95This will be developed further in chapter~\ref{euclid} to include 96Euclid's proof that there are an infinite number of primes. 97 98Because we loaded \ml{arithmeticTheory} and \ml{pairTheory} to begin, 99both of these theories are part of our new theory's ancestry. In 100fact, there are a number of other ancestor theories that these two 101depend on in turn. 102 103%%% Local Variables: 104%%% mode: latex 105%%% TeX-master: "tutorial" 106%%% End: 107