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_OrdersBinary_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
OpenPGP_0x58AE985FE188789A.asc
Description: OpenPGP public key
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
