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