Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] antiquotation for the current goal

Email Gateway (Aug 19 2022 at 11:41):

From: Ondřej Kunčar <kuncar@in.tum.de>
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?

Thanks for your answers.

Best,
Ondrej

Email Gateway (Aug 19 2022 at 11:42):

From: Makarius <makarius@sketis.net>
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

Email Gateway (Aug 19 2022 at 11:42):

From: Ondřej Kunčar <kuncar@in.tum.de>

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't fit 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
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?
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.

Best,
Ondrej

Email Gateway (Aug 19 2022 at 11:42):

From: Makarius <makarius@sketis.net>
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't
fit 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 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.

Makarius

Last updated: Apr 25 2024 at 16:19 UTC