[isabelle] Proving equivalence



Hi all,

I'm having problem proving the following. Say I have:

axiomatization
foo :: "real => real => real" and
bar :: "real => real => real" and
bax :: "real => real => real"
where ax1: "ALL p r v e. (r = foo p e & v = bar p e) = (bax r e = v)"

lemma "ALL p r v e. bax r e = bar p e"
using ax1
by auto

The lemma can be proved. However, if I change the signature of bax to "real
=> real => real => real":

axiomatization
foo :: "real => real => real" and
bar :: "real => real => real" and
bax :: "real => real => real => real"
where ax2: "ALL q p r v e. (r = foo p e & v = bar p e) = (bax q r e = v)"

lemma "ALL q p r v e. bax q r e = bar p e"
using ax2
by auto

Auto can't find a proof. How come this is so difficult for auto? What is the
proper way to do this proof?

Thanks

Steve




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