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

Thanks again, Ondrej. 

I have one further question on this topic, which can be summarised as "How can I make the transfer method work properly inside a context?".

In more detail: suppose I'm working inside a context that gives me the assumption "P f" for some fixed f. I write a lemma involving f, and begin the proof by applying the transfer method. The transfer method *generalises* f, and thus loses the fact that P holds for it. 

I find that I can survive, just about, by inserting "P f" *before* applying the transfer method. But this feels rather unscalable.

All of this is explained in further detail in the following theory file.

Best wishes,


theory Scratch imports

locale always_true =
  fixes f :: "'a ⇒ bool"
  assumes always_true: "f x = True"
begin end

typedef 'a fset = "{A :: 'a set . finite A }"
by (rule exI[of _ "{}"], auto)

setup_lifting type_definition_fset

  fset_member :: "'a ⇒ 'a fset ⇒ bool" (infix "|∈|" 50)
is "op ∈" by simp

context always_true begin

lemma "a |∈| A ⟹ f a"
apply transfer

lemma "a |∈| A ⟹ f a"
apply (insert always_true)
apply transfer
apply auto




On 24 Jan 2013, at 13:51, Ondřej Kunčar wrote:

> 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.