Filter
Top Products
Chapter 11
Principles of definition
HOL’s basic principles of definition are often quite inconvenient to use. The function
new definition is extended quite soon to permit definitions of functions with the
arguments on the left, including pairs and tuples of arguments:
#let func = new_definition
‘func f x = f(x + 1) - 1‘;;
func : thm = |- !f x. func f x = f (x + 1) - 1
#let add3 = new_definition
‘add3(x,y,z) = x + y + z‘;;
add3 : thm = |- !x y z. add3 (x,y,z) = x + y + z
It’s often convenient to make definitions recursively. HOL has some limited sup-
port for so-called primitive recursive definitions, which we examine below. General
recursive functions can be defined using some of the theorems in the theory of well-
foundedness described below, but HOL Light doesn’t provide any handy functions
for doing it elegantly. So one can’t write down recursive functions with the abandon
that one can in ML. This is inevitable to some extent, since all HOL functions are
total and in general recursive definition schemes do not give well-defined or unique
total functions. For example f(n) = f(n) + 1 has no solution, and neither (at least
for functions N → N) does f(n) = f(n + 1) + 1, whereas f(n) = f(n − 1) + 1 has
many possible solutions.
11.1 Inductive definitions
What HOL does support in a more convenient way is the definition of inductive pred-
icates (or sets). Inductive definitions are very common in mathematics, especially
in the definition of formal languages used in mathematical logic and programming
language semantics. Camilleri and Melham (1992) give some illustrative examples.
Examples crop up in other parts of mathematics too, e.g. the definition of the Borel
hierarchy of subsets of R. A detailed discussion, from an advanced point of view, is
given by Aczel (1991).
Inductive definitions define a set S by means of a set of rules of the form ‘if
. .. then t ∈ S’, where the hypothesis of the rule may make assertions about mem-
bership in S. These rules are customarily written with a horizontal line separating
the hypotheses (if any) from the conclusion. For example, the set of even numbers
E might be defined as a subset of the reals by:
0 ∈ E
87