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