irule_atTactic.irule_at : match_position -> thm -> tacticApplies an implicational theorem backwards in a particular position in the goal
A call to irule_at pos th, with th an
“implicational” theorem of general form ∀xs... P ⇒ Q, will
attempt to find an instance of term Q at position
pos within the current goal, and replace it with an
appropriately instantiated version of P. (It is possible
for P to be empty, in which case the term is effectively
replaced by truth.) The possible positions encoded by pos
are all “positive”, meaning that this process is sound (it may
nonetheless turn a provable goal into an unprovable one).
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.
Fails if the position parameter fails to specify a term, or if that
term does not unify with the implicational theorem’s conclusion. A
position may fail to specify a term in mulitple ways depending on the
form of the position. A position of form Pos f will fail if
the function f fails when applied to the goal’s conjuncts.
(Note that there is no failure if f returns a term that is
not actually a conjunct; if this term unifies, this will simply result
in new conjuncts appearing in the goal without any old conjuncts being
removed.)
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.
Solving a goal outright:
?- ∃x. x ≤ 3
============== irule_at (Pos hd) (DECIDE “y ≤ y”)Refining a goal under an existential prefix (the theorem
RTC_SUBSET states that
∀x y. R x y ⇒ RTC R x 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 zInstantiating existential variables (with LESS_MONO
stating that m < n ⇒ SUC m < SUC n):
?- ∃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) zThe underlying operation is resolution, where one resolvent is always
the conclusion of th, and the other is the conjunct from
the goal selected by the position parameter. The goal is viewed as a
literal clause by negating it (via the action of
goal_assum).