Filter
Top Products
1.2. GETTING STARTED 3
system works, or who want to build their own application-specific theorem proving
tools.
1.2 Getting started
After starting up CAML and loading HOL, the user is confronted with CAML
Light’s prompt (‘#’). CAML Light is expecting the user to type something in, and
it will then evaluate it and print the result. CAML will only act after the user
terminates the input with a double semicolon (‘;;’) and newline. For example, one
can use CAML like a pocket calculator:
#2 + 2;;
it : int = 4
The user enters the expression 2 + 2, and CAML evaluates it and prints the
answer, 4. It also prints out the type of the expression, namely int (short for
integer, i.e. whole number). We will explain CAML’s types in more detail later.
CAML also abbreviates the result by ‘it’, to save the user retyping. For example,
one can now do:
#it + 3;;
it : int = 7
Instead of using the default name it, which is overwritten every time a new
expression is evaluated, one can bind an expression to a name by using let. For
example, after the following interaction, x has the value 4, at least until another
‘let x = ...’ overwrites it.
#let x = 2 + 2;;
x : int = 4
The above was only intended as an introduction to interaction with CAML. We
are really interested in manipulating not numbers but logical entities like theorems.
In fact, there are three key logical notions in HOL Light, each with a corresponding
ML type: types (hol type), terms (term) and theorems (thm). HOL Light is, at
its core, a system for manipulating these objects. (Note the object-meta distinction
here: one has an ML (meta) type of data structures representing HOL (object)
types.)
A HOL term represents a mathematical assertion like x + 1 = y or just some
mathematical expression like x + 1. Every term has a type, indicating what sort of
mathematical entity it is, e.g. a boolean value (true or false), a real number, a set
of real functions etc. For example, x+ 1 has type num indicating that it is a natural
number, while x + 1 = y has type bool indicating that it is either true or false.
A HOL theorem simply asserts that some boolean-typed term is valid, or at least,
follows from a finite list of assumptions.
Terms and types are represented by ML data structures that we describe in
more detail below. However, it is tiresome to describe particular terms and types,
especially large ones, by creating such data structures explicitly. Instead, HOL
has parsers and printers that allow types and terms to be represented in something
closer to familiar mathematical notation, subject to the limitations of ASCII. Terms
are entered rather like strings, enclosed within backquotes:
#‘x + 1‘;;
it : term = ‘x + 1‘
#‘x + y <= z‘;;
it : term = ‘x + y <= z‘