在 Isabelle 中将集合转换为列表

Question

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

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

"'a set => 'a list"

我该如何定义它？

Answer 1

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

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

来自理论List。但是，此常量要求 'a 在 class 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}).

Answer 2

您可以从

开始

definition set_to_list :: "'a set ⇒ 'a list"
  where "set_to_list s = (SOME l. set l = s)"

然后证明

lemma  set_set_to_list:
   "finite s ⟹ set (set_to_list s) = s"
unfolding set_to_list_def by (metis (mono_tags) finite_list some_eq_ex)

在 Isabelle 中将集合转换为列表

Converting a set to a list in Isabelle

isabelle