Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Combining BNF and Quotient

Email Gateway (Aug 19 2022 at 10:39):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,

I am trying to convert the Coinductive entry in the AFP to use the new
BNF package for the type definitions. So far, the type the type ('a, 'b)
tlist has been defined as a quotient of ('a llist * 'b), where 'a llist
has been constructed directly in a coinductive style. Most definitions
and lemmas about tllist are simply lifted versions of their 'a llist
counterparts.

Now, I am wondering whether it is sensible to convert this to BNF or
whether I should better stick to the current setup. Or can I have it
both ways? Can I define tllist with the BNF package and then setup the
quotient package manually (similar to what setup_lifting does for
typedefs)? Or can I define the type via quotient_type and then declare
to the BNF package that tllist is actually

codata ('a, b) tllist = TNil 'b | TCons 'a "('a, b') tllist"

(this would be similar to rep_datatype)? How could I achieve this? Is
there some documentation or example around?

Thanks in advance for any suggestions,
Andreas

Email Gateway (Aug 19 2022 at 10:39):

From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Andreas,

You can setup the Lifting package manually even for quotient types.
Again by setup_lifting by providing the Quotient theorem (and optionally
reflp theorem). See the documentation in The Isabelle/Isar Reference
Manual. An example is in Word.thy. The command setup_lifting is not only
for typedefs.

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.

Ondrej

Email Gateway (Aug 19 2022 at 10:39):

From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,

If you go for the "quotient -> BNF" direction, there are a couple of things you can do.

1. The "wrap_data" command derives all the characteristic lemmas that are common for datatypes and codatatypes. It is somewhat similar to "rep_datatype" but not quite, because it has nothing to do with (co)induction and (co)recursion, only constructors, discriminators, and selectors. Here's an example of its use

   wrap_data [Nil, Cons] list_case [] [[], [hd, tl]] [[hd: undefined, tl: Nil]]
   apply -
   apply (erule list.exhaust, assumption)
   apply (rule list.inject)
   apply (rule list.distinct)
   apply (rule list.cases)+
   done

   print_theorems

Here "Nil", "Cons", and "list_case" must already exist, whereas "hd" and "tl" are defined by the command. The syntax is

wrap_data <constructors> <case> <discriminator names> <selector names> <default values>

(see "bnf_wrap.ML" for details). With a bit of ML, you could export the properties of codatatypes and their (co)iterators/recursors under the familiar names given by "codata". Ideally, we would rename "wrap_data" to, say, "wrap_pre_data" and provide additionally "wrap_data" and "wrap_codata" to finish the job. Perhaps you could help us design good interfaces for this pair, since you apparently would need "wrap_codata".

2. If you want to do (co)recursion through one of the "tllist" type arguments, you will need to register the type as a BNF. For this there currently is only one way, namely "bnf_def", which you already used before for the "option" type IIRC.

I hope this helps.

Cheers,

Jasmin

Email Gateway (Aug 19 2022 at 10:39):

From: Makarius <makarius@sketis.net>
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.

Makarius

Email Gateway (Aug 19 2022 at 10:39):

From: Ondřej Kunčar <kuncar@in.tum.de>
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. When Lifting and Transfer
subsume the Quotient package completely, the Quotient package will be
probably outdated and eventually removed. Only the quotient_type command
will be preserved. It's on my todo list but not really on the top
because there are more important things to be done.

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.

Ondrej

Email Gateway (Aug 19 2022 at 10:40):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Ondřej and Jasmin,

thanks for the feedback.

Email Gateway (Aug 19 2022 at 10:40):

From: Makarius <makarius@sketis.net>
On Thu, 7 Mar 2013, Cezary Kaliszyk wrote:

On Thu, Mar 7, 2013 at 2:12 PM, Ondřej Kunčar <kuncar@in.tum.de> 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.

Makarius

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.

Makarius

Last updated: Apr 25 2024 at 16:19 UTC