Qiyuan Xu (Jan 19 2023 at 08:13): Qiyuan Xu (Jan 19 2023 at 08:13):Dear friends, how do you usually express the largest integer or natural number that subjects to some condition?
Wolfgang Jeltsch (Jan 19 2023 at 12:28):With GREATEST x. P; so you write, for example, GREATEST n :: nat. n < 1000.
Wolfgang Jeltsch (Jan 19 2023 at 12:30):It should work with all types that are instances of ord. I used it for relations, which are only partially ordered.
Manuel Eberl (Jan 19 2023 at 22:17):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.
Christoph Madlener (Jan 20 2023 at 11:20):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: Nov 04 2025 at 16:27 UTC