Max of set in Isabelle

Question

How can I find the maximum element in a set of numbers (nat) in Isabelle. The max function doesn't work, as it is only defined to take the maximum of two elements. I have an idea of how I could implement it using a reduce like function, but I don't know how to pick one random element from a set.

Answer 1

The function you are looking for is called Max. If you are looking for basic constants the guide What's in Main from the official Isabelle documentation is often useful. There is also the find_consts command which can be used to search for functions by type.

Answer 2

If you follow the definition of Max to theory Big_Operators in the main HOL library, you will see that it is defined like this:

Max = fold1 max

The combinator fold1 is your "reduce like function" that works on finite sets. See also theory Finite_Set and its locale folding for the mathematical background that is required here to fold over arbitrary sets, instead of concrete lists.