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.
Any 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)
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
