[isabelle] Quotients of nominal types



Hi all,

This is mainly a question for the nominal folks, but I figured other
people might have some good suggestions as well. I'm looking to
formalise a nominal algebraic theory in Isabelle, which consists
(essentially) of a binder and an associative/commutative
multiplication operation. The types of theorems I want to prove
initially are things of the form "s = t", where s and t are elements
of such a nominal algebra A, presented by generators and relations.

So, there seem to be a handful of choices available for doing this, so
I'm trying to get an idea of what approach will yield the nicest
proofs, with the least overhead/faff. The two ideas I had in mind
were:

1. Forming a nominal_datatype and taking a quotient. This seems like
the obvious choice, but I have a few questions about it. Firstly, in
Nominal2, a nominal_datatype is already a quotient. Is this
quotient-of-a-quotient setup going to be a pain? If not, what things
need to be lifted to the quotient type in order to keep working modulo
alpha-equivalence as automatic as possible?

2. Forming the nominal_datatype, then defining a new equivalence
relation ~~ with the axioms of the algebra, along with any relations
between generators. Prove theorems of the form "s ~~ t". Essentially,
the the first half of the construction in #1, but don't bother with a
quotient type. This seems to come with its own set of problems. For
instance, things like "s ~~ t ==> P s ==> P t" would need to be
assumed for particular P, rather than being an axiom of HOL (as is the
case with "=").

3. Treating A as a "theory" rather than a presentation of a particular
algebra. That is, form a locale where the term formers are assumed as
functions, then assume relevant equalities, including equivariance
properties for the term formers. I think the latter should be tagged
[eqvt] so the nominal code knows it can apply them to try and
alpha-unify terms in various places. The main downside here is you
don't get all the nice scaffolding that is laid down by
nominal_datatype, but by having the correct assumptions/theorems in
context, a term built from these assumed functions could, at least in
theory, be handled in much the same way (though clearly things like
injectivity of constructors gets lost, once non-trivial equations are
assumed).

I'm pretty new to Isabelle, and especially Nominal/Nominal2. Any input
and pointers to relevant docs or examples would be much appreciated.


Many thanks,

Aleks




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