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.