Email Gateway (Aug 18 2022 at 16:14): Email Gateway (Aug 18 2022 at 16:14):From: Sylvia Gruener <sylvia.gruener@googlemail.com>
Hello,
I would like to write a tactic which applies a theorem to the goal
(where it depends on the structure of the goal which theorem is
applied). Moreover, the tactic gets as argument a term with which the
free variable "ur" of the theorem should be instantiated before applying the theorem to the goal (each possible theorem contains a variable with this name). After deciding which theorem to apply, the tactic should behave exactly like applying rule_tac with the selected theorem and instantiating the variable "ur" with the given term.
On the Isabelle level, the rule_tac application would look like this:
apply (rule_tac ur="some_term" in some_theorem)
My question is: How can I write this rule_tac application on the
ML-Level?
I tried to do this rule_tac application by executing
(res_inst_tac ctxt [(("ur", 0), "some_term")] some_theorem 1)
in the ML code of the tactic, but I had two problems with this call, to
which I do not find a solution:
The name of the variable has to be given as indexname (a pair of a
string and an integer). What exactly does the integer stand for? I
tried several values, none of them (also not 0) yielded exactly the
behavior of rule_tac (because some variables inside the term are not
instantiated the way rule_tac would do it).
"some_term" is of type "term", but res_inst_tac needs of course a
parameter of type string. I defined my own syntax for my tactic using
the method_setup command, which parses the parameter as a term.
Is it possible to convert a term to a string of the format that
res_inst_tac is expecting? (The functions I tried only converted the
term structure to a string.)
Or is it possible to parse a string as argument instead of a term
when the tactic is applied on the Isabelle level?
Thank you very much,
Sylvia
Email Gateway (Aug 18 2022 at 16:15):From: Alexander Krauss <krauss@in.tum.de>
Hi Sylvia,
I would like to write a tactic which applies a theorem to the goal
(where it depends on the structure of the goal which theorem is
applied). Moreover, the tactic gets as argument a term with which the
free variable "ur" of the theorem should be instantiated before
applying the theorem to the goal (each possible theorem contains a
variable with this name). After deciding which theorem to apply, the
tactic should behave exactly like applying rule_tac with the selected
theorem and instantiating the variable "ur" with the given term.On the Isabelle level, the rule_tac application would look like this:
apply (rule_tac ur="some_term" in some_theorem)My question is: How can I write this rule_tac application on the
ML-Level?I tried to do this rule_tac application by executing
(res_inst_tac ctxt [(("ur", 0), "some_term")] some_theorem 1)
res_inst_tac is an old tactic designed for interactive use, which is why
it has "parsing built in". It is not really useful for writing other
tactics, due to the strings...
Unfortunately, there is no direct ML counterpart of rule_tac.
It is easy if your instantiation does not refer to goal parameters (that
is, variables that are !!-bound within the subgoal). Then you can first
instantiate the theorem (using Thm.instantiate, or one of its relatives
Drule.instantiate' and Drule.cterm_instantiate) and then apply it using
resolve_tac. What you are doing then roughly corresponds to
apply (rule some_theorem[where ur="some_term"]) .
If you do have to refer to goal parameters, then it is a bit more
difficult. I know of two approaches that work reasonably well:
Use Subgoal.FOCUS_PARAMS to turn your subgoal into a new goal in a
context where the parameters are turned to fixed variables. Then you can
instantiate and apply the rule as above. This roughly corresponds to
(* goal: "!!x y z. P x y z" *)
proof -
fix x y z
show "P x y z" <proof>
qed
but the inner tactic (the rule application) does not have to solve the goal.
in the ML code of the tactic, but I had two problems with this call,
to which I do not find a solution: 1. The name of the variable has to
be given as indexname (a pair of a string and an integer). What
exactly does the integer stand for?
Schematic variables have an indexname instead of just a name, which
allows for fast renaming. See Sect. 1.2.3 of the Implementation Manual.
[...]
Or is it possible to
parse a string as argument instead of a term when the tactic is
applied on the Isabelle level?
In principle you could do this and delegate the parsing to res_inst_tac,
but I would not recommend this as a general approach. In particular, you
could no longer inspect the term structure of some_term.
Hope this helps,
Alex
Email Gateway (Aug 18 2022 at 16:15):From: Jeremy Dawson <jlcaadawson@netspeed.com.au>
Sylvia,
Look at term_lift_inst_rule in tactic.ML, I've previously used it for (I
think) something like what you're trying to do
Jeremy
Email Gateway (Aug 18 2022 at 16:15):From: Alexander Krauss <krauss@in.tum.de>
Look at term_lift_inst_rule in tactic.ML, I've previously used it for (I
think) something like what you're trying to do
that function no longer exists:
http://isabelle.in.tum.de/repos/isabelle/rev/07a8904f8fcd
Alex
Email Gateway (Aug 18 2022 at 16:17):From: Makarius <makarius@sketis.net>
The question about term-based res_inst_tac is very old (maybe 15 years).
Various people had come up with private solutions to that. More recently,
with the almost accidental advent of FOCUS, it became suddenly clear that
the answer is there.
So only thing you can't do with FOCUS is instantiate schematic variables
in the goal, but these are very rare in (robust) proofs under ML program
control.
Makarius
Last updated: Apr 23 2024 at 20:15 UTC