[isabelle] Monotonicity rules for function application
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
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))"
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and