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.