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



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".

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

This example results in "Local statement will fail to refine any pending
goal" in line 4 of the proof. Furthermore, replacing line 3 with

def x == "0 :: nat"

makes everything work just fine. This is a minimal example built from a
bigger proof where the witness used for proving the existential statement
was an expression containing variables that originated in an obtain
statement. From what I've observed so far, it appears that whenever
variables from an obtain statement are part of the witness, the show
statement fails. I've used [[show_types]] to confirm that the types aren't
part of the issue, both x and 0 are of type nat. Also, the output doesn't
give me the usual "Failed attempt to solve goal by exported rule" line
stating why the show statement failed, as is the case with assume
statements that don't match any assumption in the goal.

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.

I think I've also run into a similar problem that didn't involve obtain
statements but I can't find the theory where that happened right now, maybe
I'll post again if I run into that issue once more. For now, I'd be happy
with figuring this one out.

Cheers,
 Julian




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