*To*: Cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Writing a specific rule_tac application on ML level*From*: Sylvia Gruener <sylvia.gruener at googlemail.com>*Date*: Wed, 20 Oct 2010 16:51:32 +0200

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

**Follow-Ups**:**Re: [isabelle] Writing a specific rule_tac application on ML level***From:*Alexander Krauss

- Previous by Date: [isabelle] Minor type-setting mistake in http://isabelle.in.tum.de/dist/Isabelle/doc/sugar.pdf
- Next by Date: Re: [isabelle] Minor type-setting mistake in http://isabelle.in.tum.de/dist/Isabelle/doc/sugar.pdf
- Previous by Thread: Re: [isabelle] Minor type-setting mistake in http://isabelle.in.tum.de/dist/Isabelle/doc/sugar.pdf
- Next by Thread: Re: [isabelle] Writing a specific rule_tac application on ML level
- Cl-isabelle-users October 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list