[isabelle-dev] Missing generic predication for monotone function

[Peter Lammich]

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
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev