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

Tobias Nipkow nipkow at in.tum.de
Mon May 23 13:20:06 CEST 2022

```I still prefer this argument order:

mono_wrt_on :: "('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ 'a set ⇒ ('a ⇒ 'b) ⇒ bool"

In the end, it is an attempt at a consistent order where the `actual' argument
comes last. True, inj_on departs from this schema, possibly because "inj_on f A"
seems to read a bit better.

Not sure if a good argument can be made either way, but not having to worry

Tobias

On 23/05/2022 11:17, Martin Desharnais wrote:
> Hello,
>
> I searched the Isabelle distribution and AFP and found many similar definitions.
>
> Isabelle/HOL
> Orderings.mono :: "('a::order ⇒ 'b::order) ⇒ bool"
> Fun.mono_on :: "'a::order set ⇒ ('a::order ⇒ 'b::order) ⇒ bool"
> Complete_Partial_Order.monotone :: "('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒
> 'b) ⇒ bool"
>
> AFP/Complete_Non_Orders
> Binary_Relations.monotone_on :: "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒
> ('a ⇒ 'b) ⇒ bool"
>
> AFP/KBPs
> ODList.mono_on :: "('a::order ⇒ 'b::order) ⇒ 'a::order set ⇒ bool"
>
> AFP/List-Infinite
> SetInterval2.mono_on :: "('a::order ⇒ 'b::order) ⇒ 'a::order set ⇒ bool"
>
> AFP/Stable_Matching
> Basis.mono_on :: "'a::order set ⇒ ('a::order ⇒ 'b::order) ⇒ bool"
>
> It also has been brought to my attention that a "_on" predicate with a
> restricting set is necessary in some cases, e.g. inj_on, but not in others, e.g.
> mono_on, as one could define a new relation/order defined only on desired
> elements. Nonetheless, the proliferation of "_on" predicates seems to indicate
> that this interface is preferred. We should decide what we want for the Isabelle
> distribution:
>
> i) Strive for minimalism and offer an "_on" version only when necessary.
> ii) Strive for ease of use systematically offer an "_on" version, the normal
> version would be "_on UNIV".
>
> If i) then we can close this conversation and I will use
> Complete_Partial_Order.monotone. If ii) we could use the name "monotone_on" as
>
> Another remarks is that the distribution appears inconsistent on whether to put
> the restricting set as first argument, e.g.,
>
> Relation.total_on :: "'a set ⇒ ('a × 'a) set ⇒ bool"
> Relation.total :: "('a × 'a) set ⇒ bool"
>
> or as last argument, e.g.,
>
> Fun.inj_on :: "('a ⇒ 'b) ⇒ 'a set ⇒ bool"
> Fun.inj :: "('a ⇒ 'b) ⇒ bool".
>
> Tobias expressed preference for the first argument. Can we agree on that?
>
> Regards,
> Martin
>
> _______________________________________________
> 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/20220523/1f3aa7c5/attachment.bin>
```