I am currently working on my first formalization of a paper in Isabelle. But I am not sure how I can model the following terms as a datatype within Isabelle. The terms are basically an extended version of how terms look in lambda calculus. So we have abstraction and application. There are also some operators but I now how to model them.

The point where I get stuck is that everything is in the context of a complete lattice. So we consider some complete lattice M and then a set of functions on that lattice. And each of those functions would be allowed as a term too.

I would add a `Lattice_Operation f`

constructor where `f`

is any function with the correct type. Then I would define a predicate stating that the term is well founded iff `f`

is in the set of functions on the lattice.

If your functions have many different types, this is going to be ugly however. Or it will not work if you have infinitely many types.

Last updated: Aug 13 2022 at 05:18 UTC