# [isabelle] "PROOF FAILED for depth4"

Hi,
I'm experimenting with a simple proof, but I keep getting an error saying
"PROOF FAILED for depth 4". Here's my theory:
consts
s :: real
f :: real
F :: "real => real"
Y :: "real => real"
Z :: "real => real"
axioms
ax1 : "F t = Y t + Z t"
ax2 : "Y s = -1"
ax3 : "Z s = 1"
lemma funczero: "EX func t. func t = 0"
using ax1 ax2 ax3
by auto
I suspect providing ax1 ax2 ax3 and using auto is not sufficient to prove
the lemma. However, if I do:
lemma te_zero: "EX func t. func t = 0"
proof
show "F s = 0"
I get an error saying:
*** Local statement will fail to refine any pending goal
*** Failed attempt to solve goal by exported rule:
*** F s = 0
*** At command "show".
Isn't "F s = 0" a witness for the existential statement?
Thanks
Steve

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