[isabelle] Writing a specific rule_tac application on ML level



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: 
 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,
Sylvia




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.