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_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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
