如何在 Isabelle 的一组数字 (nat) 中找到最大元素。max 函数不起作用，因为它只定义为取两个元素中的最大值。我知道如何使用类似 reduce 的函数来实现它，但我不知道如何从一组中选择一个随机元素。
问问题
797 次
2 回答
7
您正在寻找的功能被称为Max。如果您正在寻找基本常量，Isabelle 官方文档中的What's in Main指南通常很有用。还有一个find_consts命令可用于按类型搜索功能。
于 2013-02-11T20:07:48.633 回答
4
如果您遵循主 HOL 库中Maxto theory的定义Big_Operators，您会看到它是这样定义的：
Max = fold1 max
组合fold1器是适用于有限集的“类约归函数”。另请参阅理论Finite_Set及其语言环境folding，了解此处折叠任意集合而不是具体列表所需的数学背景。
于 2013-03-02T17:26:02.783 回答