Re: [isabelle] Combining BNF and Quotient



Hi Ondřej and Jasmin,

thanks for the feedback.

On 07/03/13 09:31, Ondřej Kunčar wrote:> On 03/07/2013 08:32 AM,
> 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.

I think I will go that route, then. Proving a quotient theorems seems less work than proving the necessary theorems for the BNF package.

> 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.

So far, Coinductive used this very Quotient package, but I guess I can transfer everything to the lifting/transfer package, as the BNF package already constructs the type.

Best,
Andreas





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