Email Gateway (Aug 19 2022 at 09:59): 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.
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.
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
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: Nov 21 2024 at 12:39 UTC