[isabelle] Quotient Type Definition: Map and Relator

[Tjark Weber]

Dear quotient type experts,

When defining

quotient_type 'a Q = "'a T" / "R" <proof>

for some existing type T and an equivalence relation R, I see two
warnings:

No map function defined for T. This will cause problems later on.

Generation of a parametrized correspondence relation failed.
Reason: No relator for the type "T" found.

What are the problems that these warnings allude to, and how can I
provide a map function and a relator to avoid them?

I have been browsing the documentation and examples, but with limited
insight so far.

Best,
Tjark

[Andreas Lochbihler]

Dear Tjark,

These warnings stem from the lifting package, which quotient_type calls internally such
that lift_definition can be used. The documentation of the lifting package (Isar-Ref,
chapter 12.3) explains what form the map function and the relator should have. The
problems are that transfer and lifting might not work as expected.

For (co)datatypes T without dead type variables, the datatype packages already installs a
map function and the relator. Apparently, your type does not fall into this category, so
you have to define your own map function. It is important that the map function has a
function argument for each argument of T and the relator one relation for each. That is
why you cannot use the map function and the relator from datatypes with dead type variables.

Hope this helps,
Andreas

[Ondřej Kunčar]

Hi Tjark,
you can happily ignore the warning about the map function. This is
relevant only if you use the "old" Quotient package for constant
definitions and proving and Lifting/Transfer.

Concerning the other warning. You can be fine if you don't want do
lifting/transferring that would change 'a in your type 'a Q. Nesting is
an example when this can happen: 'a Q Q => 'a T T.

If you want to support/use this, you have to provide some semantic
information for 'a T (a relator is a part of this). Just look at
HOL/Lifting_Set.thy where such a thing is provided for the type 'a set
and follow analogously. As Andreas already mentioned, this is not
necessary if 'a T is a datatype without "dead" variables.

Hope this helps,
Ondrej

[Ondřej Kunčar]

Sorry for a typo. The second sentence should be:

This is relevant only if you use the "old" Quotient package for constant

definitions and proving and *NOT* Lifting/Transfer.