Single-Step Decomposition

The decomposition  tactics invoke the primitive so-called introduction and elimination rules  of Nuprl's logic. We prefer the use of the word decomposition because it suggests in most cases the effect of the rules when they are applied.

D c

Decompose the outermost connective of clause c.
indexD c Usually D unfolds all top level abstractions and applies the appropriate primitive decomposition rule. D can take several optional arguments:
• A `universe` argument, usually applied using the At tactical.
• A `t1` argument for a term. This argument is for instance necessary when decomposing a hypothesis with a universal quantifier outermost, or decomposing the conclusion with an existential quantifier outermost. For example: With `a' (D 0).
• `v1` and `v2` arguments for new variable names. These are useful for some hypothesis decompositions if one is not satisfied with the system supplied variable names. For example, New [`x';`y'] (D 3).
• An `n` argument to select a subterm. This is necessary when applying D to a disjunct in the conclusion. For example, Sel 1 (D 0).
D is somewhat intelligent with instances of set and squash terms.

ID c

Intuitionistically decompose  clause c.  This behaves as D does, except that when decomposing a function, a universal quantifier, or an implication, in a hypothesis, the original hypothesis is left intact rather than thinned.

MemCD

  MemCD

Decomposes terms which are the immediate subterms of an membership term in the conclusion. Labels subgoal corresponding to subterm n with label subterm and number n. Other subgoals are labelled wf. For primitive terms MemCD uses the appropriate primitive rule. For abstractions, MemCD tries to use an appropriate well-formedness lemma. The lemma for term a t with opid opid should have name opid_wf   and should be a simple universal formula with consequent . The subterms of t usually should be all variables. Constants are acceptable as subterms too. If more than one lemma is needed, the lemmas should be distinguished by suffices to the opid_wf root. MemCD attempts to use lemmas in the reverse of the order in which they occur in the library. If the concl is where a is an instance of t and A doesn't match any of the T of the lemmas, then MemCD tries matching a against t of the last lemma. If this succeeds and generates some substitution , MemCD produces a subgoal and tries to use the Inclusion tactic to prove it.

An example application of the MemCD tactic is

EqCD

EqCD   is like MemCD except that it works on the immediate subterms of equality terms rather than membership terms and the subgoals generated are equality terms rather than membership terms. Equalities don't have to be reflexive. EqCD is good for congruence reasoning and is used extensively by the rewrite package.

EqHD i

Decompose terms which are immediate subterms of equality hypotheses. Works when the type is a product or function type.

Like EqHD but works on the immediate subterms of membership terms.

EqTypeCD

Decompose just the type subterm of a conclusion equality term. Only works when the type is a set type or is an abstraction that eventually unfolds to a set type.

As EqTypeCD but works on membership terms.

Decompose just the type subterm of a hypothesis equality term. Only works when the type is a set type or is an abstraction that eventually unfolds to a set type.

As EqTypeHD  but works on membership terms.