[isabelle] Writing a specific rule_tac application on ML level
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
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:
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? 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).
2. "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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and