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,
john

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.

Ondrej





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