# [isabelle] Monotonicity rules for function application

Dear all,

`In the HOL library, many rules for reasoning about predicates which are closed under
``function composition (such as monotonicity, continuity and measurability) follow a common
``format:
`
1. There is a rule for the identity function: "P (%x. x)"

`2. All the rules for function constants F are lifted over function composition, i.e., we
``use the rule
` "P ?f ==> P (%x. F (?f x))"
rather than
"P F"

`This way, "P <some complicated expression>" can be proved by resolving with the rules if
``all the constituent parts satisfy P.
`

`For monotonicity rules as used by the partial_function package, there is one exception to
``this format, namely the rule call_mono:
`
monotone (fun_ord ?ord) ?ord (Îf. f ?t)

`Now, monotonicity proofs by resolution with the rules fail in my applications, because in
``my goal, I would need the lifted version of call_mono, namely
`
monotone ?orda (fun_ord ?ord) ?F â monotone ?orda ?ord (Îf. ?F x ?y) (***)
because my goal looks has the form
monotone (fun_ord ord) ord (%f. G f x)
for some HOL term G, which is monotone, too.

`My problem is that I don't know how to control resolution with (***). If I add (***) to
``the intro rules, then it also matches when there is no ?y that should be removed, i.e.,
``the HO unifier has the form ?F = (%x y. ?F' x). Is there anything in the ML library that
``would only yield unifiers which do not discard the second argument to ?F? Do you have any
``suggestions how to solve this problem?
`
Andreas

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*