Re: [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)
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:
1. 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" *)
fix x y z
show "P x y z" <proof>
but the inner tactic (the rule application) does not have to solve the goal.
2. Manually lift some_theorem into your "goal context" using
Thm.lift_rule. Then, the schematic variables become parameterized over
the goal parameters (i.e. they are now of function type). You can then
instantiate them as you need. To apply the rule, you would then use
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?
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and