Re: [isabelle] Combining BNF and Quotient

On Thu, 7 Mar 2013, Cezary Kaliszyk wrote:

On Thu, Mar 7, 2013 at 2:12 PM, Ondřej Kunčar <kuncar at> wrote:
On 03/07/2013 12:58 PM, Makarius wrote:
On Thu, 7 Mar 2013, Ondřej Kunčar wrote:

If you mean the Quotient package by Kaliszyk, Urban, I think you would
have to go to the ML level (which doesn't exist, I know ;)) to setup
the package manually.

Can some of the quotient guys please clarify the situation.

How many quotient packages are there at the moment in Isabelle? Are
there plans to converge them, and remove old stuff?

I know that this is a lot of extra work, but this is how we usually
managed to keep things going (and moving forward) over so many years.


There is one Quotient package and there is Lifting and Transfer, which
almost subsume the functionality of the Quotient package regarding defining
new constants and transferring goals.
As far as I know, the only place where some extra features of the Quotient
package (that are not covered by Lifting and Transfer) are used is Nominal2.

Right, at some point we tried to define a simple nominal datatype
using Lifting/Transfer in Nominal2, but it cannot transfer all the
theorems that Quotient can.

For example the exhausts theorems for many datatypes fail to transfer
with the Transfer package. It is possible to reprove them using the
theorems that Transfer is able to use, but the purpose of the Quotient
package is automating such tasks...

I do not know if the issue would be the same for the co-datatypes.

Thanks, this sheds more light on the situation. It also helps Isabelle users to keep an overview.

Concerning Nomimal2, someone was asking about it on the Nominal mailing list recently: to include some Isabelle application in AFP that depends on Nomimal2, it has to be available in some official manner. AFP already has a "temporary" copy of Nominal2 now, but what is its relation to the main Nominal2 repository, and its relation to Nominal1 that is part of Isabelle2013 (and earlier)?

As for the differences between Quotient and Lifting+Transfer, apart
from missing regulatization (the above), Quotient has been designed to
be used not only interactively, but also from the ML level.

Proper Isabelle/ML interfaces are indeed very important for *any* package. It is the first thing a tool author should do, before adding some conrete syntax icing on the cake (for end-users who won't build their own tools on top of other tools).

Generally, I hope that the misleading terminology of Isabelle "ML level" and "Scala layer" (which was introduced myself) will eventually disappear. It is just Isabelle/ML, Isabelle/Scala, Isabelle/Isar, Isabelle/Pure, Isabelle/HOL, Isabelle/.... Many aspects of a system, and many of them cannot be assigned to a "level" or "layer" at all, because they are intertwined.

The term "ML level" is particularly bad, because it sounds like something alien and inaccessible at the bottom of the pit. If that were the case, the Prover IDE would not provide so much support for editing Isabelle/ML as part of regular theory sources.


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