[isabelle-dev] Missing generic predication for monotone function

[Tobias Nipkow]

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
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220517/831b00a6/attachment.bin>