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



Hi John,

With the option fixing, you can tell transfer not to generalize certain variables:

apply(transfer fixing: f)

Hope this helps,
Andreas

On 01/24/2013 04:31 PM, John Wickerson wrote:
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,
John

---------8<----------

theory Scratch imports
   Main
   "~~/src/HOL/Library/Quotient_Set"
begin

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

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

context always_true begin

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

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

end

end

---------8<----------


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.