Re: [isabelle] Matching done by the transfer method

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.


On 22 March 2013 12:38, Daniel Raggi <danielraggi at> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.