CODEWITHSUNDEEP
isabelle
Konstantin Weitz
Konstantin Weitz

Reputation: 6422

Max of set in Isabelle

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.

Upvotes: 5

Views: 1237

Answers (2)

Makarius
Makarius

Reputation: 2224

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.

Upvotes: 4

Lars Noschinski
Lars Noschinski

Reputation: 3667

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.

Upvotes: 7

Related Questions