Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Max of set in Isabelle


view this post on Zulip Email Gateway (Aug 19 2022 at 09:59):

From: Konstantin Weitz <weitzkon@uw.edu>
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.

view this post on Zulip Email Gateway (Aug 19 2022 at 09:59):

From: Ramana Kumar <rk436@cam.ac.uk>
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.

view this post on Zulip Email Gateway (Aug 19 2022 at 09:59):

From: Peter Lammich <lammich@in.tum.de>
There's also a function Max:: 'a set => 'a

"Big_Operators.linorder_class.Max"
:: "'a\<Colon>Orderings.linorder Set.set \<Rightarrow> 'a
\<Colon>Orderings.linorder"

Peter

view this post on Zulip Email Gateway (Aug 19 2022 at 10:00):

From: Tobias Nipkow <nipkow@in.tum.de>
There is the prefined Max function in theory Big_Operators (which is part of
Main). It works for any linear order.

Tobias


Last updated: Mar 28 2024 at 16:17 UTC