Email Gateway (Oct 18 2022 at 10:42): Email Gateway (Oct 18 2022 at 10:42):From: Johannes Neubrand <neubrand@in.tum.de>
Hi all,
I'm trying to call an Isar method entirely from ML. Does anyone have
pointers to looking up the method in ML and giving it Isabelle/HOL terms
as arguments (that would usually be passed in in parentheses such as in
(measure "my_term_here"))?
I'd like to avoid rebuilding the method in ML and continue using the
present Eisbach definition for readability.
The cookbook seems not to cover this topic. I'd be glad if someone could
link me to a theory where this is accomplished.
Thanks,
Johannes
Email Gateway (Oct 18 2022 at 12:06):From: Makarius <makarius@sketis.net>
On 18/10/2022 12:42, Johannes Neubrand wrote:
Hi all,
I'm trying to call an Isar method entirely from ML. Does anyone have pointers
to looking up the method in ML and giving it Isabelle/HOL terms as arguments
(that would usually be passed in in parentheses such as in(measure "my_term_here"))?
The proper way is to use the ML type tactic directly, together with its many
combinators (tacticals).
The result can be easily integrated into the Isar proof language via the proof
method "tactic" (for experimentation) or the command 'method_setup' (for
production quality). See also the "isar-ref" and "implementation" manual,
which contains general explanations and tiny examples.
The remaining exercise is to look at the real Isabelle sources, and learn
which applications/examples are good and which are bad, outdated etc.
Sometimes, tool authors have forgotten to expose proper ML interfaces to their
proof methods: this is an error, and needs to be sorted out in the tool
implementation.
I'd like to avoid rebuilding the method in ML and continue using the present
Eisbach definition for readability.
Readability is relative to what the reader knows. After learning about ML type
tactic, that is readable, robust, maintainable.
Embedded "scripts" are not: there is a whole lot of extra complexity to make
something like Eisbach work most of the time (but not always).
The cookbook seems not to cover this topic. I'd be glad if someone could link
me to a theory where this is accomplished.
The cookbook is unofficial "fan fiction", and not the first place to look.
Makarius
Email Gateway (Oct 23 2022 at 20:20):From: Yutaka Nagashima <united.reasoning@gmail.com>
Hi Johannes,
As Makarius wrote, using the corresponding ML tactic directly is usually a
good idea.
But for some reason I had to make a "tactic" out of a string such as "auto
simp: my_lemma" sometimes.
So, I wrote this function:
https://github.com/data61/PSL/blob/a6f2de70be57339ba9c9f89ddf6409a453398037/SeLFiE/Util.ML#L1198
Note that here I am not using the word "tactic" accurately.
That is, tactics in Isabelle are functions takes a value of type Thm.thm
and returns a lazy sequence of thms (thm seq),
but my "tactic"s are functions, each of which takes a value of type
Proof.state and returns a lazy sequence of Proof.states.
It allows us to do something like "Repeat (Hammer)".
Regards,
Yutaka
Email Gateway (Oct 24 2022 at 07:16):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Note that here I am not using the word "tactic" accurately.
and if an actual tactic is needed, I found this function in my code:
(I wrote it quite a while ago, so I cannot say much about the pros and
cons of it. I think one disadvantage is definitely that it reparses the
method on each invocation when you have it in some loop. But it may be a
starting point for experiments.)
Best wishes,
Dominique.
Email Gateway (Jan 18 2023 at 16:15):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
I just ran into the same question. Here's a simple working example:
theory Scratch
imports
Main
"HOL-Eisbach.Eisbach"
begin
method my_simp = simp
ML‹
fun my_simp_tac ctxt =
Method_Closure.apply_method @{context} @{method "my_simp"} [] [] []
ctxt []
|> Context_Tactic.NO_CONTEXT_TACTIC @{context}
›
lemma "(1 :: nat) + 1 = 2"
by (tactic ‹my_simp_tac @{context}›)
end
From: Rafal Kolanski <xs@xaph.net>
Not sure how useful you'll find it, but you can build up a stack of
these, i.e. if you have a method that takes another method as an
argument, you can invoke it with one of these, e.g.
val solves_wpsimp =
let
fun wpsimp st = Method_Closure.apply_method st @{method wpsimp} [] [] [] st
fun solves_wpsimp_tac st = Method_Closure.apply_method st @{method solves} [] [] [wpsimp] st
in solves_wpsimp_tac end
If you have a tac but need to give it to a method:
fun rtac st = METHOD (HEADGOAL o Method.rule_tac st [thm]);
fun mr_sh_tac st = Method_Closure.apply_method st @{method monadic_rewrite_solve_head}
[] [] [rtac] st;
As you already indicated, if you have a method but need a tac,
NO_CONTEXT_TACTIC seems the way to go.
Raf.
Last updated: Apr 26 2024 at 20:16 UTC