*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: Re: [isabelle] setup_lifting - "no relator for the type" warning*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 24 Jan 2013 16:47:56 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <88D07BAD-56FA-4CF2-ACB2-AFEFAB0DCF33@cam.ac.uk>*References*: <05E79377-A812-465B-BE5F-CF93440F92BF@cam.ac.uk> <51001172.5060105@in.tum.de> <E5403A88-1C00-4113-8254-F5DB2BA5900A@cam.ac.uk> <51012E5A.3040606@in.tum.de> <88D07BAD-56FA-4CF2-ACB2-AFEFAB0DCF33@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130106 Thunderbird/17.0.2

Hi John,

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

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

**Re: [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

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

- Previous by Date: Re: [isabelle] setup_lifting - "no relator for the type" warning
- 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