# 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.*