Identity function used to force a hypothesis

`rewrite`, `linear`, `type-prescription`, `definition`, `meta` (actually in that case, the result of
evaluating the hypothesis metafunction call), and `forward-chaining`.

When a hypothesis of a conditional rule (of one of the classes listed
above) has the form

Note that the only time that ACL2 gives special treatment to calls of

(implies (implies (and ... (force HYP) ...) concl) G)

then the rewriter will not give any special treatment to `(force
HYP)`. Instead, it will first rewrite `(force HYP)`.

Forcing is generally used on hypotheses that are always expected to be
true, as is commonly the case for guards of functions. All the power
of the theorem prover is brought to bear on a forced hypothesis and no
backtracking is possible. Forced goals can be attacked immediately (see immediate-force-modep) or in a subsequent forcing round (see forcing-round). Also see case-split for a related utility. If the
`executable-counterpart` of the function

It sometimes happens that a conditional rule is not applied because some
hypothesis, `corollary` field of the `rule-classes` entry, a hypothesis can be forced without changing the statement
of the theorem from which the rule is derived.

Technically,

Since a forced hypothesis must be provable whenever the rule is otherwise applicable, forcing should be used only on hypotheses that are expected always to be true.

A particularly common situation in which some hypotheses should be forced is in ``most general'' type-prescription lemmas. If a single lemma describes the ``expected'' type of a function, for all ``expected'' arguments, then it is probably a good idea to force the hypotheses of the lemma. Thus, every time a term involving the function arises, the term will be given the expected type and its arguments will be required to be of the expected type. In applying this advice it might be wise to avoid forcing those hypotheses that are in fact just type predicates on the arguments, since the routine that applies type-prescription lemmas has fairly thorough knowledge of the types of all terms.

`consp`?'' ``does this expression produce some kind of ACL2 number,
e.g., an `integerp`, a `rationalp`, or a `complex-rationalp`?'' etc. It is driven by type-prescription rules.
To relieve the hypotheses of such rules, the type system recursively invokes
itself. This can be done for any hypothesis, whether it is ``type-like'' or
not, since any proposition, `consp` then
does

The ACL2 rewriter uses the type reasoning system as a subsystem. It is therefore possible that the type system will force a hypothesis that the rewriter could establish. Before a forced hypothesis is reported out of the rewriter, we try to establish it by rewriting.

This makes the following surprising behavior possible: A type-prescription rule fails to apply because some true hypothesis is not
being relieved. The user changes the rule so as to **force** the
hypothesis. The system then applies the rule but reports no forcing. How can
this happen? The type system ``punted'' the forced hypothesis to the
rewriter, which established it.

The discussion above may give the impression that a forcing round only takes place because of a failure to relieve a forced hypothesis. A notable exception, however, is due to linear-arithmetic. Consider the following example:

(implies (not (equal 0 x)) (or (< 0 x) (< x 0)))

This is not a theorem; in particular, it fails when `pso`,
you'll see the following.

But forced simplification reduces this to T, using the :executable- counterpart of FORCE and linear arithmetic.

Thus, no specific rule created this forcing round (see also forcing-round). Rather, ACL2 was able to prove the goal using linear
arithmetic, but it needed to force the assumption that

[1]Goal, below, will focus on (ACL2-NUMBERP X), which was forced in Goal' by the linearization of (EQUAL 0 X).

Finally, we should mention that the rewriter is never willing to force when
there is an `if` term present in the goal being simplified. Since
`and` terms and `or` terms are merely abbreviations for `if`
terms, they also prevent forcing. Note that `if` terms are ultimately
eliminated using the ordinary flow of the proof (but see set-case-split-limitations), allowing

**Function: **

(defun force (x) (declare (xargs :guard t)) x)

- Forcing-round
- A section of a proof dealing with forced assumptions
- Failed-forcing
- How to deal with a proof failure in a forcing round
- Immediate-force-modep
- When the executable-counterpart is enabled, forced hypotheses are attacked immediately
- Disable-forcing
- To disallow forced case-splits
- Enable-forcing
- To allow forced case splits
- Disable-immediate-force-modep
- forced hypotheses are not attacked immediately
- Enable-immediate-force-modep
- forced hypotheses are attacked immediately