【发布时间】：2013-01-03 12:44:22
【问题描述】：
如何在 Isabelle 的一组数字 (nat) 中找到最大元素。 max 函数不起作用，因为它只定义为取两个元素中的最大值。我知道如何使用类似 reduce 的函数来实现它，但我不知道如何从集合中选择一个随机元素。
【问题讨论】：
-
如果你真的想了解列表，使用集合非常麻烦，而且通常会使证明时间更长。
【发布时间】：2013-01-03 12:44:22
【问题描述】：
您要查找的函数名为Max。如果您正在寻找基本常量，Isabelle 官方文档中的指南 What's in Main 通常很有用。还有find_consts命令，可用于按类型搜索函数。
【讨论】：
-
补充一点：Isabelle/jEdit 的查询面板也可以搜索常量（参见 Isabelle/jEdit 手册中的3.4.2, p.30）。如果您知道可以调用函数的名称（或其中的一部分），可以编写
name: <name-or-part-of-name>来搜索匹配的常量。小警告：搜索仅限于导入的理论。在这种情况下，您必须导入理论Lattices_Big（它似乎被传递地包含在Main中）。
如果你在主HOL库中按照Max到理论Big_Operators的定义，你会看到它是这样定义的：
Max = fold1 max
组合器fold1 是您的“类约归函数”，适用于有限集。
另请参阅理论Finite_Set 及其语言环境folding，了解此处折叠任意集合而不是具体列表所需的数学背景。
【讨论】：