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 <[email protected]> > 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 > [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
