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