Re: [isabelle] Fwd: Max of set in Isabelle

Do you need it to be computable?
Otherwise just use choice: SOME x. x ∈ S ∧ ∀y. y ∈ S ⇒ y ≤ x
This may already be defined in some library.

On Sun, Jan 20, 2013 at 6:05 AM, Konstantin Weitz <weitzkon at> wrote:

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.