在Isabelle/HOL中创建一个具有工作集多态性和等价关系的商提升类型

Question

我想在Isabelle/HOL中创建一个具有quotient_type的商类型，其中我将保留"非构造"的非空集S和等价关系≡。我的目标是在商提升集S/≡上导出关于S和≡的一般性质。通过这种方式，Isabelle/HOL接受依赖类型会很有趣。。。但我被告知这是不可能的。

因此，我尝试了这个

(* 1. Defining an arbitrary set and its associated type *)
consts S :: "'a set"
typedef ('a) inst = "{ x :: 'a. ¬ S = ({} :: 'a set) ⟶ x ∈ S}" by(auto)
(* 2. Defining the equivalence relation *)
definition equiv :: "'a ⇒ 'a ⇒ bool" where
  "equiv x y = undefined"
  (* here needs a property of equivalence relationship... *)
(* 3. Defining the quotiented set *)
quotient_type ('a) quotiented_set = "('a inst × 'a inst)" / "equiv"
(* Hence, impossible end proof here... *)

这种形式化，似乎有两个问题

1. 我不认为这是定义任意集S的最干净的方法，因为我不能将其指定为非空
2. 我不能用definition或fun命令定义任意的等价关系equiv，因为它们只允许我定义"构造性强规范化归纳"定义。。。然而，我想说，我只是有一些函数equiv，它满足等价性质（自反性、对称性、传递性）

你知道吗？谢谢

Answer 1

HOL类型不能依赖于值。因此，如果要使用quotient_type为任意非空集S和等价关系equiv定义商类型，则任意部分必须停留在元级别。因此，S和equiv可以是公理化的，也可以是定义的，这样你就可以说服自己，你真的抓住了想要的任意概念。

如果你将S和equiv公理化，那么你自己有责任确保这些公理与HOL的其他公理一致。您可以像在中那样使用命令axiomatization来执行此操作

axiomatization S :: "'a set" where S_not_empty: "S ≠ {}"

对于Isabelle/HOL，S是一个固定常数，你只知道它不是空的。你永远无法实例化S，因为任意性只存在于Isabelle/HOL的集合论解释中。

如果你不想添加新的公理，你可以使用specification代替：

consts S :: "'a set"
specification (S) S_not_empty: "S ≠ {}" by auto

使用specification，你必须证明你的公理是一致的，所以这里没有危险。然而，S不再是绝对任意的，因为它是根据选择算子Eps定义的，这可以从生成定理S_def中看出。

如果你真的想研究Isabelle/HOL中的商理论，我建议你不要使用类型，而是使用普通集合。商算子CCD_ 27和理论CCD_。