*To*: Ondřej Kunčar <kuncar at in.tum.de>*Subject*: Re: [isabelle] Matching done by the transfer method*From*: Daniel Raggi <danielraggi at gmail.com>*Date*: Fri, 22 Mar 2013 13:12:31 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAFzz2xSB3CBkSRs17hM+KyP5HRQieGR48vPDSHPMiidX6Bpk4w@mail.gmail.com>*References*: <CAFzz2xSBsndQV1M2n-8e9KdqjdJTK298UTZDmDnysa+0ss-Xqg@mail.gmail.com> <514C49BB.30102@in.tum.de> <CAFzz2xTVpwMp-hTFdCD-GPkJKcns_+T5w7yco49FrVSHAW=-UA@mail.gmail.com> <CAFzz2xSB3CBkSRs17hM+KyP5HRQieGR48vPDSHPMiidX6Bpk4w@mail.gmail.com>

No, actually my example is wrong... it does reduce "P (4+3)" to "Q N". Then it is more puzzling than I thought, because it is specific to the forall. On 22 March 2013 13:07, Daniel Raggi <danielraggi at gmail.com> wrote: > ok, so I made a simpler example to clarify stuff. Suppose you have this > transfer rules: > "BN N (4+3)" > "(BN ===> op <->) Q P" > (where N and Q are some constants we previously defined) > > and this goal: > "P (4+3)" > > One would think that the transfer method would reduce the goal to "Q N", > but it doesn't, because I think it would rather find transfer rules for 4, > 3 and +, not the whole term. > > Daniel > > > > On 22 March 2013 12:38, Daniel Raggi <danielraggi at gmail.com> wrote: > >> On 03/22/2013 12:20 PM, Daniel Raggi wrote: >> >>> Suppose I have a transfer rule of the form: >>> "((R ===> op =) ===> op =) All (λ Q. ∀ x>0. Q x)" >> >> >> Ok, sorry I wrote this. I meant BN instead of R. >> >> >> >>> Well, this suggests that you need a rule of this form: >>> "((BN ===> op =) ===> op =) <something> All" >>> >>> but your rule is >>> "((R ===> op =) ===> op =) All <something>" >>> >>> >> The problem is that if you define a rule like >> "((BN ===> op =) ===> op =) All <something>" >> with <something> being composite (say it is "s t"), the rule will be >> completely useless because the transfer method, when applied to a goal, >> will search for matches only for the symbols in the goal, i.e., it will >> search for a match >> "(<transfer stuff here>) <something> s" >> and another match >> "(<transfer stuff here>) <something> t" >> >> Even when the goal contains expression "s t" explicitly, a rule of the >> form >> "(<transfer stuff here>) <something> (s t)" >> will not be used. >> >> In the case I'm working one wouldn't be able to find a rule of the form >> "((BN ===> op =) ===> op =) <something> All" >> because BN is not right-total. That's why I am bounding it. >> >> I have looked at Transfer_Int_Nat.thy. The difference from my example and >> that example is that, there, things are being transferred from Int to Nat, >> so every All in a goal is translated to a bounded forall. That same example >> wouldn't work the other way around if we had a bounded forall in a goal (of >> Int) and tried to reduce it to an All (of Nat). >> >> I hope I'm not being too unclear... >> >> Daniel >> > >

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