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
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:
assumes Pf: "\<exists>x. P(f x)"
shows "\<exists>y. P y"
from Pf obtain x where "P(f x)" ..
thus "\<exists>y. P y" ..
What might that look like in ML?
This archive was generated by a fusion of
Pipermail (Mailman edition) and