*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Matching done by the transfer method*From*: Ondřej Kunčar <kuncar at in.tum.de>*Date*: Fri, 22 Mar 2013 15:11:29 +0100*In-reply-to*: <CAFzz2xRPrxXux4452fewzhLPYhX3fb5S8iGAqu9KSwDm=Hc7gg@mail.gmail.com>*References*: <CAFzz2xSBsndQV1M2n-8e9KdqjdJTK298UTZDmDnysa+0ss-Xqg@mail.gmail.com> <514C49BB.30102@in.tum.de> <CAFzz2xTVpwMp-hTFdCD-GPkJKcns_+T5w7yco49FrVSHAW=-UA@mail.gmail.com> <514C6030.8000809@in.tum.de> <CAFzz2xRPrxXux4452fewzhLPYhX3fb5S8iGAqu9KSwDm=Hc7gg@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/17.0 Thunderbird/17.0

On 03/22/2013 03:02 PM, Daniel Raggi wrote:

As far as I know, that works. If you have a transfer rule "R f (g h)" andyour goal contains "g h", that term is transferred to f. If your rule is, let's say, "R f (%P. g P)" and your goal contains g R, this is not magically transferred to "f R". Because in order to transfer g, a rule "R ? g" is expected. But concerning your example with quantifiers, I think you can use Ball constant instead "((R ===> op =) ===> op =) All (Ball {0..})", similarly to HOL/ex/Transfer_Int_Nat.thy.Yes, Ball works, and some composite expressions work. But suppose we have the transfer rules "(BN ===> op ⟷) T P" "((BN ===> op ⟷) ===> op ⟷) All (λ Q. (∀ x>0. Q x))" and goal "(λ Q. (∀ x>0. Q x)) (λx. P x)" (note that this is exactly the same as "∀ x>0. P x"). The transfer rules match the goal perfectly, but when "(λ Q. (∀ x>0. Q x)) (λx. P x)" is parsed by Isabelle it states the goal as "∀ x>0. P x" and apparently the transfer method tries to find a match for that expression, and not the more "internal" one. Thanks for your help. I'll stop repeating myself now. Daniel

Ondrej

**Follow-Ups**:**Re: [isabelle] Matching done by the transfer method***From:*Daniel Raggi

**References**:**[isabelle] Matching done by the transfer method***From:*Daniel Raggi

**Re: [isabelle] Matching done by the transfer method***From:*Ondřej Kunčar

**Re: [isabelle] Matching done by the transfer method***From:*Daniel Raggi

**Re: [isabelle] Matching done by the transfer method***From:*Ondřej Kunčar

**Re: [isabelle] Matching done by the transfer method***From:*Daniel Raggi

- Previous by Date: Re: [isabelle] Matching done by the transfer method
- Next by Date: Re: [isabelle] Matching done by the transfer method
- Previous by Thread: Re: [isabelle] Matching done by the transfer method
- Next by Thread: Re: [isabelle] Matching done by the transfer method
- Cl-isabelle-users March 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