[isabelle] Matching done by the transfer method



Suppose I have a transfer rule of the form:
"((R ===> op =) ===> op =) All (λ Q. ∀ x>0. Q x)"

and a goal of the form:
"∀ x>0. P x"

I would expect the transfer method to find the transfer rule as a match for
the goal  provided that we have a match for P). However, what I get is:
goal (3 subgoals):
 1. ?a10 (λx. ?ab10 0 x ⟶ P1 x)          (* here P1 is the match for P *)
 2. Transfer.Rel ((BN ===> op =) ===> op =) ?a10 All
 3. Transfer.Rel (op = ===> BN ===> op =) ?ab10 op <

which suggests that the method is not looking for any `complex' matches,
but just searching for simpler matches. Is this a limitation of the
transfer method, or am I missing something? Should I have to create a
definition for "λ Q. ∀ x>0. Q x" (or whichever  constraint I suggest as a
transfer target).

Daniel



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