Email Gateway (Aug 22 2022 at 14:03): Email Gateway (Aug 22 2022 at 14:03):From: Lawrence Paulson <lp15@cam.ac.uk>
Could you please be more specific? That sounds pretty much like what auto/force/blast do anyway if you use intro/elim/dest without the (!) modifier.
Larry Paulson
Email Gateway (Aug 22 2022 at 14:03):From: Joachim Breitner <joachim@cis.upenn.edu>
Dear Larry,
precisely – but auto (AFAIK) can only invoke _rules_, not _methods_. I
want it to invoke a (custom eisbach-defined) method in this way.
The introduction rule in my example requires picking a “sufficiently
fresh” variable, by specifying a set of variables to avoid. Such an
intro rule does not work well with "auto", as it would leave a
schematic variable around.
But almost always, this set of variables can be calculated from the
context, i.e. the current goal statement. I (more or less) have a
method that does that, and I want auto to try that.
Thanks,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 14:03):From: Joachim Breitner <breitner@kit.edu>
Dear Larry,
indeed, that seems to be the right way into the machinery!
I have something that seems to work, but raises a few questions about
Isabelle/ML-level programming.
Here is my code so far:
theory Auto_Method
imports
Main
"~~/src/HOL/Eisbach/Eisbach"
keywords "auto_method" :: thy_decl
begin
ML ‹
fun auto_method method_text = (fn ctxt =>
ctxt addSbefore ("TODO", fn ctxt => fn _ =>
let val method = Method.evaluate method_text ctxt
in Method.NO_CONTEXT_TACTIC ctxt (method [])
end
));
fun auto_method_cmd method_text lthy =
let (* val ctxt = Local_Theory.target_of lthy
val method = Method.evaluate method_text ctxt *)
in Local_Theory.background_theory (map_theory_claset (auto_method method_text)) lthy
end;
Outer_Syntax.local_theory @{command_keyword "auto_method"}
"adds a method invocation to the classical reasoner"
(Method.parse >> (fn (method_text, _) => auto_method_cmd method_text))
›
And this actually works:
consts P :: bool
consts Q :: bool
lemma H1: "P ⟹ Q" and H2: P sorry
method Q_method methods m = (match conclusion in "Q" ⇒ ‹rule H1; m›)
auto_method (Q_method ‹rule H2›)
lemma Q by auto
So far so good. But I noticed that if I make a mistake in auto_method,
i.e. by writing
auto_method (Q_method ‹rule does_not_exist›)
then the error about does_not_exist is raised in the application of
auto, _not_ the invocation of auto_method, where it should be.
I concluded that this is due to the executing Method.evaluate in the
context of the wrapper invocation, not in the context of the
local_theory command. When I try doing it there (see the commented-out-
code) I get the proper error message. But actually using the wrapper
causes the error message
exception CONTEXT
("Cannot transfer: not a super theory", [], [], ["Q ⟹ (Q)"],
What am I doing wrong?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 14:03):From: Lawrence Paulson <lp15@cam.ac.uk>
Possibly you could accomplish what you want using a “wrapper”. Unfortunately, they are very obscure. See The Isabelle/Isar Reference Manual, section 9.4.7, Modifying the search step.
Larry Paulson
Email Gateway (Aug 22 2022 at 14:09):From: Joachim Breitner <joachim@cis.upenn.edu>
Dear list,
I’m current in the process of following a Coq course using Isabelle
(more as a Fingerübung), and there I see some nice use of tactics, such
as:
- If you find a goal of this shape,
- invoke that particular rule
- with an instantiation calculated from the current goal state.
In this case, the instantiation includes a set of names to avoid. I
have posed my question about that part at
http://stackoverflow.com/q/39280314/946226
(and now there is an Eisbach tag), but I am also wondering:
How do I best integrate this into an (otherwise) nicely automated proof
using our beloved auto?
Conceptually, to me, the custom method is just a smart version of an
introduction rule. But clearly I cannot just give a method as an
argument to auto’s "intro:".
Is there any other way to tell auto: „When you try introduction rules,
well, also try running this given method?“
If not, should there be such a way?
Greetings,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 14:11):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Joachim,
I don't know the details of what you are trying to do. Maybe it could be
tackled by a simproc (which basically also says, do something special on
goals of a specific shape)?
cheers
chris
Email Gateway (Aug 22 2022 at 14:12):From: Joachim Breitner <joachim@cis.upenn.edu>
Dear Chris,
For an example, see
https://github.com/nomeata/cis670-16fa/blob/926a15752522836620dde10076132879aa83b2a3/isa/Ch4.thy#L366-L382
(this file has no dependencies outside of HOL and HOL/Library)
In essence, I want to replace
apply(induction "[x \<leadsto> u] e" arbitrary: x e rule: lc.induct)
apply(auto elim!: subst.elims[OF sym])
apply(lc_let_with_find_fresh; auto)
done
with "by (induction ...) (auto ...)".
Quite possible that simprocs are the way to go, although judging from
the name, they are not: It is not (safe) simplification that I want to
instrument, but rather the part of auto that does proof search, i.e.
undoes a rule application if it turned out that it did not lead
anywhere.
Greetings,
Joachim
signature.asc
Last updated: Apr 18 2024 at 01:05 UTC