*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:07:26 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAFzz2xTVpwMp-hTFdCD-GPkJKcns_+T5w7yco49FrVSHAW=-UA@mail.gmail.com>*References*: <CAFzz2xSBsndQV1M2n-8e9KdqjdJTK298UTZDmDnysa+0ss-Xqg@mail.gmail.com> <514C49BB.30102@in.tum.de> <CAFzz2xTVpwMp-hTFdCD-GPkJKcns_+T5w7yco49FrVSHAW=-UA@mail.gmail.com>

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 >

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

- Previous by Date: [isabelle] Make quickcheck/nitpick/sledgehammer run in background in jEdit?
- 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