# Re: [isabelle] Obtain.result

On Thu, 18 Feb 2010, Palle Raabjerg wrote:

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?

`The following version tries to imitate what the system actually does --
``only concerning contexts, facts and goals, without Isar proof machinery
``getting in between.
`
ML {*
val cert = Thm.cterm_of @{theory};
val ctxt1 = @{context};
val (_, ctxt2) = ctxt1 |> Variable.add_fixes ["P", "f"];
val [A, C] = Syntax.read_props ctxt2 ["EX x. P (f x)", "EX y. P y"];
val ([a], ctxt3) = ctxt2
|> Variable.declare_term A
|> Variable.declare_term C
|> Assumption.add_assumes [cert A];
val ((xs, [b]), ctxt4) = ctxt3
|> Obtain.result (fn _ => etac @{thm exE} 1) [a];
val res = Goal.prove ctxt4 [] [] C (fn _ => rtac @{thm exI} 1 THEN rtac b 1);
val final_res = singleton (ProofContext.export ctxt4 ctxt1) res;
*}

`This may also serve as an example of operations from Chapter 4 in the Isar
``Implementation manual.
`

`When experimenting, you can often do it in a more light-weight fashion,
``e.g. using @{cprop "EX x. P (f x)"} the produce a certified proposition
``that will become the assumption later. Nonetheless, simultaneous reading
``of propositions as above affects type-inference -- a priori the "f" and
``"P" carry no type constraint. The fully official Variable.declare_term is
``required in production code to get implicit polymorphism of results right,
``among other things.
`
Makarius

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