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

On 12.11.2012 20:21, Julian Brunner wrote:

Hello,
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?). There is a
``more useful error message when the last theorem of a {-}-block contains
``an obtained variable
`
{ obtain x where "x = Suc 0" by auto
then have "x > 0" by auto }
results in:
Result contains obtained parameters: x

`This is due to the same reason. When you use "fix" or "def" to define a
``variable, they either get just generalized (i.e. turned into schematics)
``(fix) or replaced by their right hand side (definitions)
`when a block is closed / a show is performed.
This cannot be done for obtained variables.

Of course I can work around this by invoking proof with the '-' method and
using automation to prove the existentially quantified statement using the
witness, but it'd be nicer if it'd work like this, I feel like this is just
a minor technical issue, but I couldn't figure out what's going on.

A good scheme for proving such things is
lemma "EX x. P x"
proof -
obtain x where <...>
<...>
have "P x" <...>
show ?thesis ..
qed
where .. is a shorthand for "by rule".
-- Lars

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