[isabelle-dev] Missing generic predication for monotone function

[YAMADA, Akihisa]

Hello,

we have the predicate as "monotone_on" in this AFP entry:

https://www.isa-afp.org/browser_info/current/AFP/Complete_Non_Orders/Binary_Relations.html#Binary_Relations.monotone_on|const

Best,
Akihisa


On 5/18/2022 12:15 AM, Tobias Nipkow wrote:
> 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
> 
> On 17/05/2022 16:16, Peter Lammich wrote:
>> 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev