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

Tobias Nipkow nipkow at in.tum.de
Tue May 17 13:55:12 CEST 2022

```
On 16/05/2022 17:02, Martin Desharnais wrote:
> 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.

I wonder if it should also go into Orderings.thy, just to keep the two versions
closer together? Or does Orderings.thy not work because it does not include
Fun.thy and thus misses some necessary material (eg Sets)?

Tobias

> 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)"
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220517/831b00a6/attachment.bin>
```