isabelle - 在 Isabelle 中将集合转换为列表

Question

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

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

"'a set => 'a list"

我该如何定义？

Answer 1

通过搜索 "'a set" "'a list"在我偶然发现的 Isabelle/jEdit 查询面板的 Find Constants 选项卡中

sorted_list_of_set :: "'a set ⇒ 'a list"

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

This function maps (finite) linearly ordered sets to sorted lists. Warning: in most cases it is not a good idea to convert from sets to lists but one should convert in the other direction (via @{const set}).