Dear friends, how do you usually express the largest integer or natural number that subjects to some condition?

With `GREATEST x. P`

; so you write, for example, `GREATEST n :: nat. n < 1000`

.

It should work with all types that are instances of `ord`

. I used it for relations, which are only partially ordered.

There's also `Sup`

and `Max`

and `arg_max`

. I would typically use `Max`

I think, but `GREATEST`

also works of course.

`arg_max`

unfortunately has a lot of missing lemmas so it is of limited use.

For what it's worth, I have (more or less copied) the lemmas in `Lattices-Big.thy`

for `arg_max`

(and primarily `arg_max_on`

) which are there for `arg_min`

(resp. `arg_min_on`

) here.

Last updated: Dec 07 2023 at 12:30 UTC