[isabelle] Using implications

Hello list,

I'm still picking up Isabelle and thought I might try out some of the axioms
posted here earlier (which seemed to be consistent). I've made some
amendments just for experimenting. Assume we have:

S :: "real set" and
foo :: "real => real" and
bar :: "real => real" and
bax :: "real => real" and
c :: real
where ax1: "ALL f g. (ALL x y. x > c & y > c <-> f x = g y) --> f = g"
and ax2: "ALL a b. bax a > c & bax b > c <-> foo (bax a) = bar (bax b)"

lemma "foo = bar"
using ax1 ax2
apply auto

How come "x" and "y" can't be instantiated to "bax a" and "bax b", resp.? If
ax2 was:

ax2: "ALL a b. a > c & b > c <-> foo (a) = bar (b)"

then that works fine.

Any help will be much appreciated!


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