在 Isabelle 中将集合转换为列表

Question

如何在 Isabelle 中将集合转换为列表？

我对带有签名的函数定义感兴趣：

"'a set => 'a list"

我该如何定义这个？

Answer 1

通过在Isabelle/jEdit 的查询面板的“查找常量”"\'a set" "\'a list"选项卡中搜索，我偶然发现了

\n\n

sorted_list_of_set :: "\'a set \xe2\x87\x92 \'a list"\n

\n\n

从理论上来说List。然而，该常量需要\'a位于 class 中linorder，即，它仅适用于线性有序元素上的集合。此外，正如我的评论中提到的，它仅适用于有限集。定义正上方还有一个警告，sorted_list_of_set为了完整起见，我在此重复该警告：

\n\n

\n

此函数将（有限）线性排序集映射到排序列表。警告：在大多数情况下，从集合转换为列表并不是一个好主意，但应该向另一个方向转换（通过@{const set}）。

\n

\n