Re: [isabelle] setup_lifting - "no relator for the type" warning

On 01/24/2013 12:05 PM, John Wickerson wrote:
Thanks Ondrej.

Continuing my attempt to make a typedef for finite sets, I've managed to lift definitions like "union" from sets to finite sets. I'm now trying to lift "big union" from sets of sets to finite sets of finite sets, but this turns out to be less trivial. Could somebody kindly advise on how to do this proof?

Below is my complete .thy file.

Thanks very much,

You might want to take a look to ~~/src/HOL/Quotient_Examples/Lift_DList and ~~/src/HOL/Quotient_Examples/Lift_FSet.

You can find two operations using nested types there
concat :: "'a dlist dlist => 'a dlist (it uses typedef)
fconcat :: "'a fset fset => 'a fset" (it uses quotient)
and also corresponding proofs.

I think the example with 'a dlist is more suitable for what you are doing in your formalization because 'a dlist is defined as a typedef.


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