irule_at : match_position -> thm -> tactic
The possible positions encoded by parameter pos view the goal as if it is of form ?ys. c1 ∧ ... ∧ cn, where the existential prefix ys may be empty, and where there may only be one conjunct. If pos encodes the choice of conjunct cj, then irule_at pos will instantiate type variables and term variables from xs in th, and variables from ys in the goal so as to make cj unify with Q. The conjunct cj will then be replaced with the correspondingly instantiated P, which may itself be multiple conjunctions. While the goal may lose variables from ys because they have been instantiated, it may also acquire new variables from xs; these will be added to the goal’s existential prefix.
The new goal will be assembled to put new conjuncts first, followed by conjuncts from the original goal in their original order (these conjuncts may still be different if existential variables from ys have been instantiated). If two conjuncts become the same because of variable instantiation, only one will be present in the resulting goal. There is some effort made to keep variables from the existential prefix with the same names, but some renaming may occur, and the new goal’s existential variables will be ordered arbitrarily. If the new goal has no conjuncts, then the tactic has proved the original.
There are four possible forms for the pos parameter. If it is of form Pos f, f will be a function of type term list -> term, and this function will be passed the list of conjuncts. The returned term should be one of those conjuncts. Typical values for this function are hd, last and el i, for positive integers i. If the pos parameter is of form Pat q, the quotation q will be parsed in the context of the goal (honouring the goal’s free variables), generating a set of possible terms (multiple terms are possible because of ambiguities caused by overloading) that are then viewed as patterns against which the conjuncts of the goal are matched. The first conjunct that matches the earliest pattern in the sequence of possible parses, and which unifies with th’s conclusion, is used.
The pattern form Concl is used to indicate that the entire goal (including its existential prefix) should be viewed as the desired target for th. This results in a call to irule th being made.
Finally, the pattern form Any is used to have the tactic search for any conjunct that matches the conclusion (as with a pattern of ‘_:bool’), and if no conjunct unifies with th’s conclusion, to then try to call irule th, as is done with the Concl pattern form.
A position of form Pat q can fail if no conjunct of the goal matches any of the terms parsed to by q. The other position forms always return at least one term to be considered. Failure after this point will only follow if none of these terms unifies with the implicational theorem’s conclusion.
?- ∃x. x ≤ 3 ============== irule_at (Pos hd) (DECIDE “y ≤ y”)
?- ∃x y z. P x ∧ RTC R x (f y) ∧ Q y z ======================================== irule_at Any RTC_SUBSET ?- ∃z y0 x. R x (f y0) ∧ P x ∧ Q y0 z
?- ∃x y z. P x ∧ SUC x < y ∧ Q y z ====================================== irule_at Any LESS_MONO ?- ∃z n m. m < n ∧ P m ∧ Q (SUC n) z