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.