[isabelle-dev] Missing generic predication for monotone function

[Tobias Nipkow]

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
-------------- 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/a18f5899/attachment.bin>