# Re: [isabelle] "PROOF FAILED for depth4"

Hi Steve,

lemma te_zero: "EX func t. func t = 0"
proof
show "F s = 0"
*** Local statement will fail to refine any pending goal

`The implicit step at the "proof" command introduces one existential
``quantifier. Thus, in the body, you are expected to prove
``"EX t. ?func t = 0" which does not match what you have in your
``show-statement. When experimenting, you can look at the goal state to
``see what you are expected to prove at a given point.
`
Here are a few options that work:

`* Replace the implicit step with an explicit method, which does what you
``need:
`
lemma te_zero: "EX func t. func t = 0"
proof (intro exI)
show "F s = 0"
* Explicitly decompose the goal step by step (tedious):
lemma te_zero: "EX func t. func t = 0"
proof
show "EX t. F t = 0"
proof
show "F s = 0"
...
qed
qed
* Use an intermediate statement and let automation deal with quantifiers:
lemma te_zero: "EX func t. func t = 0"
proof -
have "F s = 0"
...
then show ?thesis by blast
qed
What you use depends on taste and the concrete problem.

`See also the Isar tutorial for Isar basics:
``http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf
`
Alex

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