[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.