# 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

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.