# [isabelle-dev] Missing generic predication for monotone function

Martin Desharnais martin.desharnais at posteo.de
Mon May 16 17:02:14 CEST 2022

```Dear Isabelle developers,

the theory Orderings.thy defines the "mono" predicate in the context of
the "order" type class. However, in some situations, one cannot use type
classes and must resort to an arbitrary ordering predicate. Some useful
characterizing predicates (e.g. reflp, transp, antisymp, inj) are
already available in HOL, but there is nothing for monotonicity.

I would like to introduce said missing predicate to, e.g., the Fun.thy
theory. A concrete suggestion is attached at the end of this email.

Any opinion on the matter?

Regards,
Martin

subsubsection ‹Monotonicity›

definition mono_wrt_on :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool"
where
"mono_wrt_on f R A ⟷ (∀x ∈ A. ∀y ∈ A. R x y ⟶ R (f x) (f y))"

abbreviation mono_wrt :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool" where
"mono_wrt f R ≡ mono_wrt_on f R UNIV"

lemma mono_wrt_onI:
"(⋀x y. x ∈ A ⟹ y ∈ A ⟹ R x y ⟹ R (f x) (f y)) ⟹ mono_wrt_on f R A"

lemma mono_wrtI:
"(⋀x y. R x y ⟹ R (f x) (f y)) ⟹ mono_wrt f R"

lemma mono_wrt_onD: "mono_wrt_on f R A ⟹ x ∈ A ⟹ y ∈ A ⟹ R x y ⟹ R (f x)
(f y)"

lemma mono_wrtD: "mono_wrt f R ⟹ R x y ⟹ R (f x) (f y)"
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0x58AE985FE188789A.asc
Type: application/pgp-keys
Size: 3139 bytes
Desc: OpenPGP public key