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.