isabelle - 如何定义带有约束的数据类型？

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"

是否可以组合数据类型和谓词？我尝试过使用 inducing_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)

使用这种新创建的类型最好通过 lift-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)

我希望这会有所帮助。