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

Question

我想在 Isabelle/HOL 中创建一个带有 quotient_type 的商类型，我将在其中留下 "non-constructed" 非空集 S 和等价关系 ≡。我的目标是导出通用属性 w.r.t。 S 和 ≡ 在商提升集 S/≡ 上。这样，Isabelle/HOL 接受 dependent types 会很有趣……但我被告知这是不可能的。

因此，我尝试了这个

(* 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... *)

这是形式化吗，好像有两个问题

我不认为这是定义任意集合 最干净 的方法 S 因为我不能将其指定为非空...
我无法使用 definition 或 fun 命令定义任意等价关系 equiv，因为它们只允许我定义 "constructive-strongly normalizing-inductive" 定义...然而，我想说我只是有一些函数 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内的商理论，我建议你不要使用类型，而是使用普通集合。有商运算符 op // 和理论中的一些定理 Equiv_Relations 这是库的一部分。

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

Create a quotient-lifted type with polymorphism over working set and equivalence relation in Isabelle/HOL

set

higher-order-functions

isabelle

theorem-proving

isar