[isabelle-dev] Missing generic predication for monotone function

[Lawrence Paulson]

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

> On 16 May 2022, at 16:02, Martin Desharnais <martin.desharnais at posteo.de> 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.
> 
> 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>_______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev