[isabelle] "PROOF FAILED for depth4"


I'm experimenting with a simple proof, but I keep getting an error saying
"PROOF FAILED for depth 4". Here's my theory:

s :: real
f :: real
F :: "real => real"
Y :: "real => real"
Z :: "real => real"

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"
  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?


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