如何定义具有约束的数据类型？

Question

例如我需要为列表对定义一个数据类型，它们必须具有相同的长度：

type_synonym list2 = "nat list × nat list"

definition good_list :: "list2" where
  "good_list ≡ ([1,2],[3,4])"

definition bad_list :: "list2" where
  "bad_list ≡ ([1,2],[3,4,5])"

我可以定义一个单独的谓词，它检查一对列表是否正确：

definition list2_is_good :: "list2 ⇒ bool" where
  "list2_is_good x ≡ length (fst x) = length (snd x)"

value "list2_is_good good_list"
value "list2_is_good bad_list"

是否可以将数据类型和谓词结合起来？我尝试过使用 inductive_set，但我不知道如何使用它：

inductive_set ind_list2 :: "(nat list × nat list) set" where
  "length (fst x) = length (snd x) ⟹
   x ∈ ind_list2"

Answer 1

您可以通过 typedef 创建一个受某些谓词约束的新类型，尽管结果将只是 type 而不是 datatype。

typedef good_lists2 = "{xy :: list2. list2_is_good xy}" 
  by (intro exI[of _ "([],[])"], auto simp: list2_is_good_def)

使用这种新创建的类型最好通过 lifting-package 来完成。

setup_lifting type_definition_good_lists2

现在对于这个新提升类型的每个操作 good_lists2，你首先有从原始类型 list2 中解除操作。例如，下面我们定义了一个提取函数和一个 Cons 函数。在后者中，您已经证明新生成的对确实满足不变量。

lift_definition get_lists :: "good_lists2 ⇒ list2" is "λ x. x" .

lift_definition Cons_good_lists2 :: "nat ⇒ nat ⇒ good_lists2 ⇒ good_lists2" 
  is "λ x y (xs,ys). (x # xs, y # ys)" 
  by (auto simp: list2_is_good_def)

当然你也可以访问不变量提升型。

lemma get_lists: "get_lists xy = (x,y) ⟹ length x = length y" 
  by (transfer, auto simp: list2_is_good_def)

希望对您有所帮助。

Answer 2

René 的回答是您所要求的答案，但为了完整起见，我想补充两点：

首先，在这里说明一个显而易见的事实：如果您只使用成对的列表而不是成对的列表，这似乎会容易得多。您提出的新类型显然与成对列表同构。那你就不用再引入额外的类型了。

此外，更笼统地说，仅仅因为您可以在 Isabelle 中引入具有类型定义的新类型来捕获某些不变量并不意味着这始终是最好的主意。单独携带不变量可能更容易。这在很大程度上取决于这些不变量的外观以及您实际对该类型的值进行的操作。在许多情况下，我会争辩说，用于设置新类型（特别是 class 实例化，如果需要的话）和在基本类型和新类型之间转换的额外样板不值得你从抽象中获得任何好处它。

我认为，一个很好的启发式方法是问问自己，您要引入的类型是否更像是您在某个特定位置需要的“一次性”东西 – 然后不要为其引入新类型——或者它是否是你可以证明很好的一般事实并引入一个很好的抽象理论的东西——然后为它引入一个新类型。后者分布的好例子是多重集、有限集和概率质量函数。

如何定义具有约束的数据类型？

How to define a data type with constraints?

isabelle