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.
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.