[isabelle] HOLCF Finite Sets


I'm trying to devise a HOLCF cpo for finite sets, which I intend to use as
part of a larger domain type via indirect recursion. One way of doing this
would seem to be by creating a cpo of totally ordered slists, e.g.

cpodef (open) 'a fset = "{l. ordslist l}"

And then build all the standard set stuff on top of this. Ordlist is an
inductive predicate requiring a strict ordering on the elements. The main
advantage of this definition is that it is flat, and therefore easier to
use. The big problem with this definition is that it can't easily be used
recursively as it depends on the fset's parameter being in linorder, which
of course it isn't when creating the domain.

I'm wondering though if I'm missing a trick and if there's a simpler way of
doing it than this? Obviously sets in HOL can be be made finite either
through the finite predicate or by using the FSet quotient type, but I
don't see an obvious way that either of them can be carried over into a
domain, particularly whilst retaining flatness.

I also saw that instances of countable are made an instance of domain under
lift. Since finite sets of countables are again countable, could I make use
of this somehow? Although again this may be difficult because of indirect

Alternatively has this already been done, and I just haven't searched

Many thanks,

- Simon

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.