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



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
> 






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