如何定义抽象集合数据类型？

Question

在我的理论中有 4 种集合。对于我定义的每个集合类型 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))" .

我需要为这些集合类型定义多态操作（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])"

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

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)"

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

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 为前缀。