[isabelle-dev] Missing generic predication for monotone function

[Tobias Nipkow]

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 
about it every time would be an advantage ;-)

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 
> "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
> 
> _______________________________________________
> 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>