Re: [isabelle] Quotient Type Definition: Map and Relator



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

On 19/03/15 14:34, Tjark Weber wrote:
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







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