Re: [isabelle] antiquotation for the current goal

On Mon, 26 Aug 2013, Ondřej Kunčar wrote:

For @{Isar.goal} see page

   @{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}.

That's great that the antiquotation works. Unfortunately, it still doesn't fit into my use case.

My use case is the following:
lemma "bla"
apply sth
 val goal = @{Isar.goal}
 val rules = do_sth_complicated goal
apply (tactic {* rtac rules 1 *})

If I am allowed to use @{Isar.goal} only inside of ML_val, I cannot see the variable "rules" outside of the ML block.

Is there any deep reason why @{Isar.goal} can be used only inside of ML_val and not in ML_prf?

Yes, according to the way the various Isabelle contexts and states work.

Allowing @{Isar.goal} inside of ML_prf would help me to do debugging in Isabelle. It's basically about moving parts of F from "apply (tactic {* F *})" to a ML_prf block as much as possible and inspecting intermediate results in the Output window. This gives me more flexibility than cluttering F with print statements and inspecting the printed stuff.

You can either put everything you need into the 'ML_val', i.e. apply the tactic yourself and inspect the outcome, or into the "tactic" expression. The latter is just normal Isabelle/ML and may consist of arbitrary complex let expressions etc. Here are examples for both -- just printing the goal again:

lemma A

  ML_val {*
    val st = #goal @{Isar.goal};
    writeln (Proof_Display.string_of_goal @{context} st);

  apply (tactic {* fn st =>
    (writeln (@{make_string} st); Seq.single st) *})

Note that "st" of type thm is the canonical way to refer to tactical goal states in ML, according to Larry Paulson.


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