# 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"
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"

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