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.