*To*: Sylvia Gruener <sylvia.gruener at googlemail.com>*Subject*: Re: [isabelle] Writing a specific rule_tac application on ML level*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Sat, 23 Oct 2010 23:19:27 +0200*Cc*: Cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <C6F6742C-54AA-41B1-8BC8-62041C869C26@gmail.com>*References*: <C6F6742C-54AA-41B1-8BC8-62041C869C26@gmail.com>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

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 isapplied). Moreover, the tactic gets as argument a term with which thefree 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 theML-Level?I tried to do this rule_tac application by executing (res_inst_tac ctxt [(("ur", 0), "some_term")] some_theorem 1)

Unfortunately, there is no direct ML counterpart of rule_tac.

apply (rule some_theorem[where ur="some_term"]) .

(* 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.

some variant of compose_tac.

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?

[...]

Or is it possible to parse a string as argument instead of a term when the tactic is applied on the Isabelle level?

Hope this helps, Alex

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

**References**:**[isabelle] Writing a specific rule_tac application on ML level***From:*Sylvia Gruener

- Previous by Date: [isabelle] PostDoc and PhD Positions at Yale University
- Next by Date: Re: [isabelle] Writing a specific rule_tac application on ML level
- Previous by Thread: [isabelle] Writing a specific rule_tac application on ML level
- 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