Max of set in Isabelle <p>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.</p>