Tactic.irule

STRUCTURE

SYNOPSIS

Applies an implicational theorem backwards in a particular position in the goal

DESCRIPTION

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.

FAILURE

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.

EXAMPLE

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 z

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

COMMENTS

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

SEEALSO

irule, MATCH_MP_TAC