Interesting. The generalization of the two would be something like
definition mono_wrt_on :: "('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ 'a set ⇒ ('a ⇒ 'b) ⇒ bool"
where "mono_wrt_on orda ordb A f ⟷ (∀x∈A.∀y∈A. orda x y ⟶ ordb (f x) (f y))" Possibly with the A first, to be able to recover "monotone" as "mono_wrt_on UNIV". And it should not be hidden in Complete_Partial_Order. I guess locales could also help. Tobias On 17/05/2022 16:16, Peter Lammich wrote:
There is already Complete_Partial_Order.monotone, which you get via HOL.Main. Is that what you are looking for? -- Peter On 17/05/2022 13:55, Tobias Nipkow wrote:On 16/05/2022 17:02, Martin Desharnais wrote:Dear Isabelle developers,the theory Orderings.thy defines the "mono" predicate in the context of the "order" type class. However, in some situations, one cannot use type classes and must resort to an arbitrary ordering predicate. Some useful characterizing predicates (e.g. reflp, transp, antisymp, inj) are already available in HOL, but there is nothing for monotonicity.I would like to introduce said missing predicate to, e.g., the Fun.thy theory. A concrete suggestion is attached at the end of this email.I wonder if it should also go into Orderings.thy, just to keep the two versions closer together? Or does Orderings.thy not work because it does not include Fun.thy and thus misses some necessary material (eg Sets)?TobiasAny opinion on the matter? Regards, Martin subsubsection ‹Monotonicity› definition mono_wrt_on :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where "mono_wrt_on f R A ⟷ (∀x ∈ A. ∀y ∈ A. R x y ⟶ R (f x) (f y))" abbreviation mono_wrt :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool" where "mono_wrt f R ≡ mono_wrt_on f R UNIV" lemma mono_wrt_onI: "(⋀x y. x ∈ A ⟹ y ∈ A ⟹ R x y ⟹ R (f x) (f y)) ⟹ mono_wrt_on f R A" by (simp add: mono_wrt_on_def) lemma mono_wrtI: "(⋀x y. R x y ⟹ R (f x) (f y)) ⟹ mono_wrt f R" by (simp add: mono_wrt_onI) lemma mono_wrt_onD: "mono_wrt_on f R A ⟹ x ∈ A ⟹ y ∈ A ⟹ R x y ⟹ R (f x) (f y)" by (simp add: mono_wrt_on_def) lemma mono_wrtD: "mono_wrt f R ⟹ R x y ⟹ R (f x) (f y)" by (simp add: mono_wrt_onD) _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev_______________________________________________ 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
