Email Gateway (Aug 07 2020 at 13:16): Email Gateway (Aug 07 2020 at 13:16):From: Mario Carneiro <di.gama@gmail.com>
Is it possible to access the current proof state (of type "state" or
"goal") from an ML or ML_val block? For example:
theory Scratch
imports Pure
begin
lemma ex:
assumes "PROP P ⟹ PROP Q" and "PROP P"
shows "PROP Q"
ML_val‹
Isar_Cmd.ml_diag true ‹goal› (* returns a transition -> transition but I'm
not sure how to apply it to the current proof context *)
›
Mario
Email Gateway (Aug 07 2020 at 15:39):From: Makarius <makarius@sketis.net>
Like this:
val ctxt = @{context};
See also the various explanations and examples in the "implementation" manual.
You can forget about command transitions like Isar_Cmd.ml_diag: that is only
relevant for composing new command transactions, when defining outer syntax
commands.
Makarius
Email Gateway (Aug 07 2020 at 16:26):From: Mario Carneiro <di.gama@gmail.com>
I was aware of the @{context} command, but it seems like this only gives
you the "Proof.context" type. Is there a way to get a "state" or "goal" out
of that, as if I was in an Isar tactic? For example, in that context I
believe there should be some goal state theorem saying that ([PROP P ⟹ PROP
Q; PROP P] ⟹ PROP Q) ⟹ ?thesis or something to that effect, where Isar
commands modify the left hand side of this implication. How do I access
this theorem from the current context?
Mario
Email Gateway (Aug 07 2020 at 17:04):From: Makarius <makarius@sketis.net>
On 07/08/2020 18:26, Mario Carneiro wrote:
I was aware of the @{context} command, but it seems like this only gives
you the "Proof.context" type.
This thing is called "ML antiquotation", not command. You can figure out the
formal kind (and name) of everything by C-hover in the Prover IDE.
Is there a way to get a "state" or "goal" out> of that, as if I was in an
Isar tactic? For example, in that context I
believe there should be some goal state theorem saying that ([PROP P ⟹ PROP
Q; PROP P] ⟹ PROP Q) ⟹ ?thesis or something to that effect, where Isar
commands modify the left hand side of this implication. How do I access
this theorem from the current context?
Goal refinement operations are called "proof method" or just "method" in Isar,
not "tactic" --- that is a more low-level concept, before the emergence of
structured reasoning in Isar.
An Isar command like 'apply' takes a proof method as argument, and modifies
the proof state in the manner of goal-directed reasoning, as you have sketched
above.
You can experiment with the mechanics of it, by using the 'ML_val' command
together with antiquotation @{Isar.goal} (or @{Isar.state} if you really want
to have the full "toplevel" state in your hand).
You can read more on it and try it interactively as follows:
isabelle jedit src/Doc/Implementation/Isar.thy
The PDF version of this material is available as "implementation" entry in the
Documentation panel of Isabelle/jEdit, or via "isabelle doc implementation".
Makarius
Last updated: Jan 04 2025 at 20:18 UTC