Email Gateway (May 20 2022 at 20:25): Email Gateway (May 20 2022 at 20:25):From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s
Email Gateway (May 20 2022 at 20:35):From: Tobias Nipkow <nipkow@in.tum.de>
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,
Martinsubsubsection ‹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
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Email Gateway (May 20 2022 at 20:35):From: Peter Lammich <lammich@in.tum.de>
There is already Complete_Partial_Order.monotone, which you get via
HOL.Main.
Is that what you are looking for?
Email Gateway (May 20 2022 at 20:40):From: Martin Desharnais <martin.desharnais@posteo.de>
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
OpenPGP_signature
Email Gateway (May 20 2022 at 20:45):From: Lawrence Paulson <lp15@cam.ac.uk>
I certainly can’t object, if there’s nothing comparable there already.
We are in fact faced with the Herculean task of seeing whether we can generalise the Analysis library away from type classes.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (May 23 2022 at 11:20):From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s
Last updated: Dec 21 2024 at 16:20 UTC