Re: [isabelle] transfer / lifting / quotient - questions



Hi Salomon.

On 06/23/2014 02:41 PM, Salomon Sickert wrote:

datatype tree = leaf "nat"
               | node "tree" "tree"

(*
   Question 1:

   If I try to generalize nat to 'a, I get the following error from the
quotient_type command:

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

   Looking at the quotient examples didn't help me to figure out, what
to prove or define to fix this.
   What do I have to do? Or can I simply ignore it?
*)

First of all, it's not an error but a warning. You can ignore it if you don't want to nest your types during lifting (and transfer), for example, when you don't want to work with "'a tree tree". If you want to work with such types (or want to remove the warning for esthetic reasons), then you have to provide a certain structure to your type. See for example HOL/Lifting_Option: in the most general case, you need all the corresponding theorems from the section "Relator and predicator properties" and "Quotient theorem for the Lifting package".

Note that in the coming release - Isabelle 2014 (released hopefully this summer) - all these theorems are proved (and registred) automatically if you define your type with datatype_new.

The other two question don't have probably much to do with Lifting and
Transfer. Mayber more knowledgeable experts can comment on them.

Best,
Ondrej Kuncar




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