Re: [isabelle] antiquotation for the current goal



On Fri, 23 Aug 2013, Ondřej Kunčar wrote:

Dear Isabelle Users,
for debugging purposes I would like to have an antiquotation that would give me a current goal as a term. For example:

lemma "A ∧ B"
apply (rule conjI)

ML_prf{*
@{goal} (* would output val it = Const ("HOL.Trueprop", "bool ⇒ prop") $ Free ("A", "bool"): term *)
*}

I found that there is @{Isar.goal} but that gives me only an error message "No goal present". I also tried some ML like "Toplevel.proof_of (Toplevel.toplevel)" but that gives me a similar result "exception UNDEF raised (line 168 of "Isar/toplevel.ML")".

Is there a way how to have such an antiquotation?

Basically all Isabelle/ML antiquotations are documented in the "implementation" manual -- if something important is missing just keep me informed.

For @{Isar.goal} see http://isabelle.in.tum.de/dist/Isabelle2013/doc/implementation.pdf page 112:

  @{text "@{Isar.goal}"} refers to the regular goal state (if
  available) of the current proof state managed by the Isar toplevel
  --- as abstract value.

  This only works for diagnostic ML commands, such as @{command
  ML_val} or @{command ML_command}.

There are also a few examples with @{Isar.goal} in the same manual.


	Makarius


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