Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails



On Tue, 13 Nov 2012, Lars Noschinski wrote:

On 12.11.2012 20:21, Julian Brunner wrote:

While using Isabelle, I keep running into the problem of not being able to prove existentially quantified statements using a witness with the show statement telling me that the "Local statement will fail to refine any pending goal".

This error message is not very helpful (and I seem to remember there once was a more useful one, mentioning obtained variables?).

It seems that I've destroyed that error messahe by accident in Jan-2009, but it is likely to work again in the coming release.


For instance:

theorem "EX x. x = (0 :: nat)"
proof
 obtain x where x_def: "x = (0 :: nat)" by simp
 show "x = 0" using x_def by simp
qed

BTW, a more compact way to write that wrong proof is this:

theorem "EX x. x = (0 :: nat)"
proof
  obtain x where "x = (0 :: nat)" by simp
  then show ?this .
qed

But that does not work for logical reasons, as has been pointed out before. You cannot apply an obtained result with parameters to the enclosing goal. This is also the deeper reason why there is 'have' for local results, and 'show' for local results that get exported into the enclosing goal context, but only 'obtain' and not 'obtain_show'.

(And you don't need to obtain local definitions in the first place, has has been said already.)


	Makarius





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