*To*: Ondřej Kunčar <kuncar at in.tum.de>*Subject*: Re: [isabelle] antiquotation for the current goal*From*: Makarius <makarius at sketis.net>*Date*: Mon, 26 Aug 2013 12:28:48 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <521B2A53.40107@in.tum.de>*References*: <52177A72.6050400@in.tum.de> <alpine.LNX.2.00.1308261129100.26473@macbroy21.informatik.tu-muenchen.de> <521B2A53.40107@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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

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}.That's great that the antiquotation works. Unfortunately, it still doesn'tfit into my use case.My use case is the following: lemma "bla" apply sth ML_prf{* 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 thevariable "rules" outside of the ML block.

Is there any deep reason why @{Isar.goal} can be used only inside ofML_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 inIsabelle. It's basically about moving parts of F from "apply (tactic {*F *})" to a ML_prf block as much as possible and inspecting intermediateresults in the Output window. This gives me more flexibility thancluttering F with print statements and inspecting the printed stuff.

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) *})

Makarius

**References**:**[isabelle] antiquotation for the current goal***From:*Ondřej Kunčar

**Re: [isabelle] antiquotation for the current goal***From:*Makarius

**Re: [isabelle] antiquotation for the current goal***From:*Ondřej Kunčar

- Previous by Date: Re: [isabelle] Which parser to use for theorems in a toplevel-command?
- Next by Date: [isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy
- Previous by Thread: Re: [isabelle] antiquotation for the current goal
- Next by Thread: [isabelle] Which parser to use for theorems in a toplevel-command?
- Cl-isabelle-users August 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list