如何定义一个抽象的collection数据类型？

Question

我的理论里有4种collection。对于每个 collection 类型，我定义了 count 和 for_all 操作：

theory MyCollections
  imports Main
    "~~/src/HOL/Library/Dlist"
    "~~/src/HOL/Library/Multiset"
begin

typedef 'a mybag = "UNIV :: 'a multiset set" .. (* not unique, not ordered *)
typedef 'a myseq = "UNIV :: 'a list set" ..     (* not unique, ordered *)
typedef 'a myset = "UNIV :: 'a set set" ..      (* unique, not ordered *)
typedef 'a myord = "UNIV :: 'a dlist set" ..    (* unique, ordered *)

setup_lifting type_definition_mybag
setup_lifting type_definition_myseq
setup_lifting type_definition_myset
setup_lifting type_definition_myord

lift_definition mybag_count :: "'a mybag ⇒ 'a ⇒ nat" is "Multiset.count" .
lift_definition myseq_count :: "'a myseq ⇒ 'a ⇒ nat" is "count_list" .
lift_definition myset_count :: "'a myset ⇒ 'a ⇒ nat" is "(λxs x. if x ∈ xs then 1 else 0)" .
lift_definition myord_count :: "'a myord ⇒ 'a ⇒ nat" is "(λxs x. if Dlist.member xs x then 1 else 0)" .

lift_definition mybag_for_all :: "'a mybag ⇒ ('a ⇒ bool) ⇒ bool" is "Multiset.Ball" .
lift_definition myseq_for_all :: "'a myseq ⇒ ('a ⇒ bool) ⇒ bool" is "(λxs f. list_all f xs)" .
lift_definition myset_for_all :: "'a myset ⇒ ('a ⇒ bool) ⇒ bool" is "Ball" .
lift_definition myord_for_all :: "'a myord ⇒ ('a ⇒ bool) ⇒ bool" is "(λxs f. list_all f (list_of_dlist xs))" .

我需要为这些 collection 类型定义多态操作（includes 和 includes_all）：

lift_definition mybag_includes :: "'a mybag ⇒ 'a ⇒ bool" is
  "(λxs x. mybag_count xs x > 0)" .

lift_definition myseq_includes :: "'a myseq ⇒ 'a ⇒ bool" is
  "(λxs x. myseq_count xs x > 0)" .

lift_definition myset_includes :: "'a myset ⇒ 'a ⇒ bool" is
  "(λxs x. myset_count xs x > 0)" .

lift_definition myord_includes :: "'a myord ⇒ 'a ⇒ bool" is
  "(λxs x. myord_count xs x > 0)" .


lift_definition mybag_mybag_includes_all :: "'a mybag ⇒ 'a mybag ⇒ bool" is
  "(λxs ys. mybag_for_all ys (mybag_includes xs))" .

lift_definition mybag_myseq_includes_all :: "'a mybag ⇒ 'a myseq ⇒ bool" is
  "(λxs ys. myseq_for_all ys (mybag_includes xs))" .

(* ... and 14 more similar operations for other type combinations *)

部分测试用例：

value "mybag_myseq_includes_all (Abs_mybag {#1::nat,2,4,5,3,4#}) (Abs_myseq [1::nat,2])"
value "mybag_myseq_includes_all (Abs_mybag {#1::nat,2,4,5,3,4#}) (Abs_myseq [1::nat,7])"

问题是这些操作在结构上是相同的，我不想重复它们。我尝试定义一个抽象 collection 类型：

typedecl 'a mycol
consts
  mycol_count :: "'a mycol ⇒ 'a ⇒ nat"
  mycol_for_all :: "'a mycol ⇒ ('a ⇒ bool) ⇒ bool"

definition mycol_includes :: "'a mycol ⇒ 'a ⇒ bool" where
  "mycol_includes xs x ≡ mycol_count xs x > 0"

definition mycol_includes_all :: "'a mycol ⇒ 'a mycol ⇒ bool" where
  "mycol_includes_all xs ys ≡ mycol_for_all xs (mycol_includes ys)"

但我不知道如何从抽象类型中派生出具体的 collection 类型：

typedef 'a mybag = "{xs :: 'a mycol. ???}" ..
typedef 'a myseq = "{xs :: 'a mycol. ???}" ..
typedef 'a myset = "{xs :: 'a mycol. ???}" ..
typedef 'a myord = "{xs :: 'a mycol. ???}" ..

Answer 1

一旦将抽象集合类型公理化，就无法再在逻辑中对其进行细化。因此，建议的方法不起作用。但是，如果您将容器类型保留为抽象（作为类型变量），那么这是可能的。我建议使用语言环境来做到这一点：

locale container =
  fixes count :: "'container => 'a => nat"
  and for_all :: "'container => ('a => bool) => bool"
begin

definition "includes" where "includes C x <--> count C x > 0"
definition includes_all where "includes_all C C' <--> for_all C (includes C')"

end

然后，您可以像往常一样定义不同的集合类型，并通过语言环境解释获取常用操作。例如，

interpretation mybag: container mybag_count mybag_forall .

生成缩写 mybag.includes 和 mybag.includes_all。此外，所有在语言环境 container 中证明的定理也专门针对 mybag 并以 mybag.

为前缀

如何定义一个抽象的collection数据类型？

How to define an abstract collection data type?

isabelle