Email Gateway (Aug 18 2022 at 11:12): Email Gateway (Aug 18 2022 at 11:12):From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi
I'm trying to write some tacticals, and want to be able to translate
the line
apply (drule_tac x=A in spec)
so that I can put it in my tactical. I tried
dtac spec 1
but this does not allow me to instantiate with a term I supply. I've
looked through the Isabelle manual and cannot find anything. Is this
possible? And, if so, can someone tell me how to do it, please?
Thanks
Peter
Email Gateway (Aug 18 2022 at 11:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Peter,
Perhaps Drule.instantiate or Drule.instantiate' provide what you need.
Hope this helps
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 11:12):From: Clemens Ballarin <ballarin@in.tum.de>
Peter,
Use res_inst_tac, or rather dres_inst_tac.
Clemens
Email Gateway (Aug 18 2022 at 11:18):From: Makarius <makarius@sketis.net>
The family of proof methods called "rule_tac", "erule_tac", "drule_tac"
etc. works by reading given terms within the joint context of a given rule
and corresponding sub-goal (potentially with locally bound goal parameters
by the !! quantifier). This very delicate operation has traditionally
been performed by dres_inst_tac etc. as defined in src/Pure/tactic.ML (the
old "Isabelle Reference Manual" also says a few words about these
tactics).
Unfortunately, these tactics are ignorant of the real proof context, only
taking the background theory into account. The corresponding Isar methods
"drule_tac" etc. use a different implementation along similar lines. See
src/Pure/rule_insts.ML which is still only half-way towards a proper Isar
implementation of this idea, and awaits another major cleanup. When this
happens eventually (really soon now), there will be just one version of
dres_inst_tac etc. taking an explicit Proof.context, and probably also
explicit pre-terms instead of strings. The details are still in flux.
Anyway, what is your conrete application? It might be easier to avoid
instantiation tactics altogether, and merely instantiate the rule
beforehand, independently of the goal.
Makarius
Last updated: May 03 2024 at 08:18 UTC