[isabelle-dev] Missing generic predication for monotone function

[Martin Desharnais]

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 "monotone" already exists.

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
-------------- 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/20220523/5b60a049/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/20220523/5b60a049/attachment.sig>