完善伊莎贝尔的定义

Question

我在Isabelle中有如下定义（详见here）：

definition gluing :: "(((real × real) × bit) × (real × real) × bit) set" where
  "gluing = {(((x0,y0),l),((x1,y1),j)). 
               ((x0,y0) ∈ e_circ ∧ (x1,y1) = τ (x0,y0) ∧ j = l+1) ∨
                (x0 = x1 ∧ y0 = y1 ∧ l = j)}"

现在，这种粘合应该定义集合上的等价关系：

e_aff × (range Bit)

所以我想细化类型：

(real × real) × bit

至此。如果我直接根据胶合的定义进行操作，我会得到：

Undefined type name: "e_aff"⌂

但是如果我改为尝试通过类型定义来实现：

typedef e_aff_t = "e_aff"

我得到：

Illegal variables in representing set: "d" The error(s) above occurred in typedef "e_aff_t"

我认为这来自e_aff的内部定义。

我该如何解决？

Answer 1

我将提供几点意见。如果这些还不够，请随时提出更多问题，我会尽力回复。

But if I instead try to do it through a type definition:

typedef e_aff_t = "e_aff"

I get:

Illegal variables in representing set: "d" The error(s) above occurred in typedef "e_aff_t"

发生这种情况是因为 e_aff 取决于固定变量。据我所知，目前这还没有被逻辑所接受（除了通过 Types-To-Sets 的 Local Typedef Rule 提供的有限支持外）： typedef α k = S 要求 S 是一个闭项，k 是一个 S 中的新类型构造函数和所有类型变量需要位于 α 中的变量。在您的情况下，S 不是封闭式术语。有许多有价值的资源对此进行了详细解释，其中许多在 Ondřej Kunčar 的博士论文中被引用。

可行的解决方案

考虑到我对您的应用程序的了解，可能的选项按照我个人偏好的顺序显示。但是，请记住，鉴于我自己有限的经验，这可能不是一个详尽的清单，而且我对您的最终目标知之甚少。

Set-based 商数

我认为表达 gluing 是 e_aff × UNIV::bit 上的等价关系的最简单方法是

definition qs where "qs = (e_aff × (range Bit)) // gluing"

lemma "equiv (e_aff × (range Bit)) gluing"
  sorry

完成此操作后，理论 Equiv_Relations（以及其他理论）提供了许多用于处理 set-based 商的有用定理。

Types-To-Sets

您还可以选择使用 Types-To-Sets 中的 Local Typedef 规则来创建基于固定变量的 quotient_type 上下文。但是，您仍然需要将 type-based 定理转换为 set-based 对应定理，然后才能在任何应用程序中使用它们（转换是自动进行的）。如果您有兴趣，我可以提供更多详细信息和示例。但是，我相信，对于您的应用程序，这并不比直接处理 set-based 定理更好。

quotient_type

如果出于任何原因，您仍然坚持使用 type-based 方法，那么，我想，您可以尝试以 e_aff 不依赖于 fixed 的方式重述理论变量。为此，您可以使用希尔伯特选择，例如definition c where "c = (SOME c::real. True)"，等等...但是，我认为这不是标准做法，因此会受到鼓励。

完善伊莎贝尔的定义

Refining a definition in Isabelle

isabelle