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)?
Tobias
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)
_______________________________________________
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
