[isabelle-dev] Missing generic predication for monotone function

[Martin Desharnais]

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"
   by (simp add: mono_wrt_on_def)

lemma mono_wrtI:
   "(⋀x y. R x y ⟹ R (f x) (f y)) ⟹ mono_wrt f R"
   by (simp add: mono_wrt_onI)

lemma mono_wrt_onD: "mono_wrt_on f R A ⟹ x ∈ A ⟹ y ∈ A ⟹ R x y ⟹ R (f x) 
(f y)"
   by (simp add: mono_wrt_on_def)

lemma mono_wrtD: "mono_wrt f R ⟹ R x y ⟹ R (f x) (f y)"
   by (simp add: mono_wrt_onD)
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0x58AE985FE188789A.asc
Type: application/pgp-keys
Size: 3139 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220516/cad35790/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 840 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220516/cad35790/attachment.sig>