*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Quotients of nominal types*From*: Aleks Kissinger <aleks0 at gmail.com>*Date*: Wed, 7 Aug 2013 11:58:18 +0100

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

**Follow-Ups**:**Re: [isabelle] Quotients of nominal types***From:*Christian Urban

- Previous by Date: Re: [isabelle] Replacing COMP
- Next by Date: Re: [isabelle] "show" taking very long with goals with many hypothesis
- Previous by Thread: Re: [isabelle] Questions about theories distributed with Isabelle
- Next by Thread: Re: [isabelle] Quotients of nominal types
- Cl-isabelle-users August 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list