Email Gateway (Aug 18 2022 at 18:59): Email Gateway (Aug 18 2022 at 18:59):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Hello,
I was hoping that someone of you could give me a little help with tactics.
I try to rewrite an apply-style proof into a tactic, for future
automization.
my goal:
rewrite apply(rule_tac x="A" in exI) as a tactic
my attempt:
val tac = let x = @{term "A"} in rtac @{thm exI} 1 end
my problem:
the bound variable x is represented in another way, i.e. I'm substituting
nothing with the let-in command.
my questions:
1) could somebody tell me, how it will work
2) how can i display the internal representation of a theorem (on ML-level,
so that i can see which term instead of x i need to substitute)
thanks in advance
Nils
Email Gateway (Aug 18 2022 at 18:59):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
i forgot "val" in my attempt
val tac = let val x = @{term "A"} in rtac @{thm exI} 1 end
Email Gateway (Aug 18 2022 at 18:59):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
this helped. thank you.
Email Gateway (Aug 18 2022 at 18:59):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hello Nils,
I suggest you have a look at the tactics in subgoal.ML.
Subgoal.FOCUS and friends should be helpful for your quest.
Maybe the Isabelle Programming Tutorial (Cookbook) also tells you a
little bit about those functions.
Lukas
Email Gateway (Aug 18 2022 at 18:59):From: Jeremy Dawson <jlcaadawson@netspeed.com.au>
Nils,
For this you want res_inst_tac, described in the Reference manual.
Eg (res_inst_tac [("x", "A")] exI 1)
For your second question (not needed to answer the first) the ML
function prop_of gives the content of a theorem as a term, which (by
default) gets printed out in all its detail.
Jeremy
Email Gateway (Aug 18 2022 at 19:04):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Thank you.
i will give the terms a try.
Email Gateway (Aug 18 2022 at 19:08):From: Makarius <makarius@sketis.net>
Appendix C of the "isar-ref" manual explains the correspondence of ML
tactic expressions and Isar proof methods a little. It was originally
written to help converting old ML proof scripts, which are now obsolete
and hardly ever encountered in recent years, but it also helps in the
other direction.
The "implementation" manual explains further things about rules and
tactics from the bottom up. The important FOCUS combinator has already
been mentioned -- it is based on Isar structuring principles in ML, and is
able to get rid of most res_inst_tac applications in practice. For plain
thm instantiation you mainly use Thm.instantiate, despite various later
attempts (mostly outdated now) to produce more convenient alternatives.
Makarius
Email Gateway (Aug 18 2022 at 19:08):From: Makarius <makarius@sketis.net>
This probably refers to Isabelle2005, which was the last version with all the
old things from Isabelle98 etc. still present. The "Reference manual" is called
"Old Reference manual" for quite some years already, and it explicitly says in
current Isabelle2011-1:
Note: this document is part of the earlier Isabelle
documentation and is mostly outdated. Fully obsolete parts of the
original text have already been removed. The remaining material
covers some aspects that did not make it into the newer manuals yet.
The "newer manuals" refers mainly to the "Isabelle/Isar Reference Manual and
"Isabelle/Isar Implementation Manual".
Makarius
Email Gateway (Aug 18 2022 at 19:08):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Makarius wrote:
Yes, I observe that now res_inst_tac requires a proof context argument,
and some other changes as well.
Makarius is right in guessing that I'm referring to Isabelle2005 - it
was when I started to convert all my proofs from Isabelle 2005 to 2007 I
seemed to be spending a lot of time on it when I would rather be doing
useful work.
I gather things have got worse since then, in terms of
incompatibilities between versions of Isabelle and therefore the
prospects of users making use of other users' work
Jeremy
Email Gateway (Aug 18 2022 at 19:10):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
I did forget to reply.
it helped. with the name i found the tactic and its syntax. the right way
to use it is
res_inst_tac @{context} [ ( (x,0) , "A" ) ] exI 1
which was convenient for me, as i don't have a term, but a string, which is
easier to manipulate, if you're not yet on good terms with terms.
Nils
Email Gateway (Aug 18 2022 at 19:10):From: Makarius <makarius@sketis.net>
On Thu, 16 Feb 2012, Nils Jähnig wrote:
I did forget to reply.
it helped. with the name i found the tactic and its syntax. the right way
to use it isres_inst_tac @{context} [ ( (x,0) , "A" ) ] exI 1
Is this going to be a generally abstracted tactic or proof method? If so,
the compile-time @{context} needs to be passed as runtime parameter,
typically as ctxt : Proof.context. You get the runtime value via the
normal method_setup syntax wrapping.
The static @{context} only makes sense for one-shot applications as in the
proof method called "tactic", or certain ML commands in Isar.
which was convenient for me, as i don't have a term, but a string, which
is easier to manipulate, if you're not yet on good terms with terms.
Again, it depends on the situation. Little can be done reliably with
strings: accepting them from the end-user and passing them to certain
other ML operations that expect such source input.
Composing "terms" in concrete syntax representation in general tactics
breaks very quickly. Moreover, if the official source position markup is
preserved, as is done by default by Args.term parsers etc. for Isar
methods, any attempt to paste together such formal source will be rejected
quickly. This is good because it makes such accidents immediately clear.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC