*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] setup_lifting - "no relator for the type" warning*From*: John Wickerson <jpw48 at cam.ac.uk>*Date*: Thu, 24 Jan 2013 12:05:13 +0100*In-reply-to*: <51001172.5060105@in.tum.de>*References*: <05E79377-A812-465B-BE5F-CF93440F92BF@cam.ac.uk> <51001172.5060105@in.tum.de>

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 ------8<-------- theory J_Finite_Set imports Main "~~/src/HOL/Library/Quotient_Set" begin typedef 'a fset = "{A :: 'a set . finite A }" by (rule exI[of _ "{}"], auto) setup_lifting type_definition_fset lift_definition union_fset :: "'a fset ⇒ 'a fset ⇒ 'a fset" is "union :: 'a set ⇒ 'a set ⇒ 'a set" by simp lift_definition Union_fset :: "('a fset) fset ⇒ 'a fset" is "Union :: 'a set set ⇒ 'a set" (* not worked out how to prove this yet *) sorry end ------8<-------- On 23 Jan 2013, at 17:36, Ondřej Kunčar wrote: > On 01/23/2013 05:24 PM, John Wickerson wrote: >> Dear Isabelle, >> >> My attempt to make a typedef for finite sets ... >> >>> typedef 'a fset = "{A :: 'a set . finite A }" >>> by (rule exI[of _ "{}"], auto) >>> >>> setup_lifting type_definition_fset >> >> >> ... results in the following warning message. >> >>> Generation of a parametrized correspondence relation failed. >>> Reason: No relator for the type "Set.set" found. >> >> Could somebody kindly tell me how I can address this? Thanks. >> >> john >> > > The relator for sets is defined in ~~/src/HOL/Library/Quotient_Set. Including this file should remove the warning. > > The warning is currently not really harmful because parametrized correspondence relations are not used in Isabelle2013. I didn't include other improvements of the Lifting package that depends on them to the coming release. Maybe in the next release this will come into play. > > Ondrej >

**Follow-Ups**:**Re: [isabelle] setup_lifting - "no relator for the type" warning***From:*Ondřej Kunčar

**References**:**[isabelle] setup_lifting - "no relator for the type" warning***From:*John Wickerson

**Re: [isabelle] setup_lifting - "no relator for the type" warning***From:*Ondřej Kunčar

- Previous by Date: Re: [isabelle] redirect tracing output to file in Jedit
- Next by Date: Re: [isabelle] setup_lifting - "no relator for the type" warning
- Previous by Thread: Re: [isabelle] setup_lifting - "no relator for the type" warning
- Next by Thread: Re: [isabelle] setup_lifting - "no relator for the type" warning
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list