Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Monotonicity rules for function application

Email Gateway (Aug 22 2022 at 13:00):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Last updated: Apr 20 2024 at 04:19 UTC