# Re: [isabelle] Matching done by the transfer method

```On 03/22/2013 01:38 PM, Daniel Raggi 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.
```
```
My point was about the order of the transfer rule, not about the relation.
```
But I was too hasty. I thought you tried to use BN :: int => nat => bool, but your relation is really BN :: nat => int => bool.
```
```
```
Well, this suggests that you need a rule of this form:
"((BN ===> op =) ===> op =) <something> All"

"((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"
```
```
```
As far as I know, that works. If you have a transfer rule "R f (g h)" and your 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.

Hope this helps.

Ondrej

```

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