*To*: Aleks Kissinger <aleks0 at gmail.com>*Subject*: Re: [isabelle] Quotients of nominal types*From*: Christian Urban <christian.urban at kcl.ac.uk>*Date*: Mon, 12 Aug 2013 08:38:42 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*References*: <CAJGV=ubzhS4=8M1M7hrNVmEVpZg+aEqHokY7yrAdPaT=52EBwg@mail.gmail.com>*Reply-to*: christian.urban at kcl.ac.uk

Hi Alex, On Wednesday, August 7, 2013 at 11:58:18 (+0100), Aleks Kissinger wrote: > > 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? There should be no problem with using quotients of nominal datatypes. One problem however is that you would have to list/transfer by hand theorems from the "nominal quotient" to your quotient. This is easy if the theorems are relatively small, but if you have induction rules with many constructors, then they are big beasts. You would need to state them explicitly for your quotient and then use the lift/transfer machinery to prove them. There is no way, I think, to lift/transfer theorems by names (on the non-ML-level). So this can be quite a bit of work, depending on how large your nominal datatype is. > 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 "="). Since your equivalence relation is "only" about an associative and commutative multiplication operation, this might be the easiest solution with the least "start-up" costs. The reasoning about a concrete alpha-equivalence relation is a pain, because one always has to rename. The reasoning about your equivalence relation might be much less painful. Though, I would prove that properties are preserved under the equivalence relation, not just assume this. > 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). In my opinion you would need to state things in even more concrete detail than with the first or second solution. Maybe an expert in locales can chip in and give an opinion whether this can be made to work smoothly. Hope this helps, Christian

**Follow-Ups**:**Re: [isabelle] Quotients of nominal types***From:*Dmitriy Traytel

**Re: [isabelle] Quotients of nominal types***From:*Makarius

**References**:**[isabelle] Quotients of nominal types***From:*Aleks Kissinger

- Previous by Date: [isabelle] This is a Theorem (a song)
- Next by Date: Re: [isabelle] Quotients of nominal types
- Previous by Thread: [isabelle] Quotients of nominal types
- 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