choice - 伊莎贝尔集的最大值

Question

如何在 Isabelle 的一组数字 (nat) 中找到最大元素。max 函数不起作用，因为它只定义为取两个元素中的最大值。我知道如何使用类似 reduce 的函数来实现它，但我不知道如何从一组中选择一个随机元素。

Answer 1

您正在寻找的功能被称为Max。如果您正在寻找基本常量，Isabelle 官方文档中的What's in Main指南通常很有用。还有一个find_consts命令可用于按类型搜索功能。

Answer 2

如果您遵循主 HOL 库中Maxto theory的定义Big_Operators，您会看到它是这样定义的：

Max = fold1 max

组合fold1器是适用于有限集的“类约归函数”。另请参阅理论Finite_Set及其语言环境folding，了解此处折叠任意集合而不是具体列表所需的数学背景。