Re: [isabelle] Writing a specific rule_tac application on ML level



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 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)

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" *)
  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.

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,
Alex






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