[isabelle] Higher-order matching


I have a rather trivial problem with higher-order matching. Suppose I have:

FuncA :: "X_Int => X_Int"
FuncB :: "X_Int => X_Int"

ax1 [rule_format] :
"ALL x y. FuncA(x) <' FuncB(y)"

declare ax1 [simp]

theorem test1:
"ALL x y. FuncA(x) <' FuncB(y)"
using ax1
by (auto)

The proof succeeds since it's simply applying ax1.

What about if I want to prove the following:

theorem test2:
"ALL x y.
EX f.
f(x) <' FuncB(y)"
using ax1
by (auto)

It fails. Am I missing a lemma? If so, what lemma am I missing? Can ax1 not be applied in the same way as in test1?

Any help will be appreciated.


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