[isabelle] Obtain.result



First, thank you for the replies to "Structured induction with custom
tactics". FOCUS and SUBPROOF does indeed seem to be more or less what we
were looking for. We may have read over that particular part of the
programming tutorial a bit too lightly. At the time, we were also using
a slightly older Isabelle version without FOCUS.

Anyway. This time I have a somewhat more specific question. How do we
use Obtain.result?

For some proofs, we often need to fix variables using the Isar obtain
command. Obtain.result would seem to be the corresponding ML function,
but we have so far been unable to figure out how to use it properly. And
we may possibly be on the wrong track again.

An example may be best at this stage, so let us take a simple one from
the Isar tutorial:

lemma
  assumes Pf: "\<exists>x. P(f x)"
  shows "\<exists>y. P y"
using assms
proof -
  from Pf obtain x where "P(f x)" ..
  thus "\<exists>y. P y" ..
qed

What might that look like in ML?

Regards,
Palle Raabjerg





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