[isabelle] Using implications
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
How come "x" and "y" can't be instantiated to "bax a" and "bax b", resp.? If
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