The
simplest example of interest here is the natural numbers, which can be
defined (in HOL) as the smallest set of individuals which includes zero
(the individual which is not in the range of the one-one function whose
existence is asserted by the usual axiom of infinity) and is closed
under the successor function (which is that same one-one function).
We
can think of this as forming the natural numbers by starting with some
set ({0}) and then adding the additional values following some
prescription until no more can be added.
Because we are always adding values, the operation on the
set-of-values-so-far is monotonic.
If the closure is supplied in a suitable manner then a completely
general proof of monotonicity will suffice.
There
is a little difficulty in doing this automatically because the
operators under which closure is wanted (counting the starting points
as 0-ary operators) will be of diverse types.
We
keep the constructor exactly as it is required on the representation
type.
This is combined with an "immediate content" function on the domain of
the constructor to give a relation which indicates which values are
immediate constituents of a constructed value, and then we close up the
empty set on the principle of adding a constructed value whenever its
immediate constituents are available.
In
addition to the constructor function and the content information we
want to allow some constraint on values which are acceptable for the
construction so that it need not be defined over the entire
representation type.
In fact this can be coded into the content function by making it
reflexive for values which we wish to exclude from the domain.
Actually its type doesn't allow reflexive, but mapping these to the
universe of the representation type will do the trick.
© 
_conv"] "fixp"; 
'b SET) 
f
monotonic f 
y 
f(x) 
{X | f X 
{X | X 
); 
{X|h X 
B 
THEN REPEAT strip_tac); 
h g 
('a 
s
{t | 