prove_monotonicity_hyps : thm -> thm
Attempt to prove monotonicity hypotheses of theorem automatically.
Given a theorem A |- t, the rule prove_monotonicity_hyps attempts to prove
and remove all hypotheses that are not equations, by breaking them down and
repeatedly using MONO_TAC. Any that are equations or are not automatically
provable will be left as they are.
- FAILURE CONDITIONS
Never fails but may have no effect.
Normally, this kind of reasoning is automated by the inductive definitions
package, so explicit use of this tactic is rare.
- SEE ALSO
MONO_TAC, monotonicity_theorems, new_inductive_definition,