prove_monotonicity_hyps : thm -> thm
- SYNOPSIS
-
Attempt to prove monotonicity hypotheses of theorem automatically.
- DESCRIPTION
-
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.
- COMMENTS
-
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,
prove_inductive_relations_exist.