isabelle - 在 Isabelle 中定义有限集

Question

如何在 Isabelle 中定义常量集？例如像 {1,2,3}(给它一个更有趣的转折，1,2,3 是实数)，或 {x\in N: x < m}，其中 m 是某个固定数字 - 或者，也许更难，集合 {N,R,C}，其中 N 是自然数，R 是实数，C 是复数。

我想在所有情况下它都必须是这样的

definition a_set :: set
  where "a_set ⟷ ??? "

但是用正确的东西替换 ??? 的各种尝试都失败了。

不知何故，我找到的所有教程都在谈论在集合上定义函数 - 但我找不到像这样的简单示例来学习。

Answer 1

definition 命令定义了一个常量。它需要一个方程式，其符号在左侧定义，例如定义“x = 5”或定义“f = (λx.x + 1)”。为了提高可读性，函数参数可以出现在等式的左侧，例如f x = x + 1。

问题是您正在使用 ⟷(“当且仅当”运算符，即 bool 值相等)。当你有 bool 值时，最好使用它而不是简单地 = 因为它节省了括号:你可以写 'P x ⟷ x = 2 ∨ x = 5' 而不是 'P x = ( x = 2 ∨ x = 5)'。 (= 运算符比逻辑连接符 ∨ 和 ∧ 绑定(bind)得更牢固；另一方面，⟷，结合更弱)

⟷ 只是编写专用于 bool 值的 = 的另一种方式。这意味着如果您要定义不返回 bool 值的内容，⟷ 将不起作用。只需使用常规 =:

definition A :: "real set" where
  "A = {1, 2, 3}"

或者，对于您的另一个示例:

definition B :: "complex set set" where
  "B = {ℕ, ℝ, UNIV}"

请注意，HOL 是一个类型化逻辑；这意味着你不能只是做

definition a_set :: set

因为没有所有集合的类型。所有集合中只有一种类型，其元素具有特定类型，例如nat set 或 (real ⇒ real) set 或确实 nat set set。只是说 set 会给你一条错误消息“无法解析类型”，因为 set 是一个类型构造函数，它需要一个类型参数，而你却没有给它任何参数。

关于集合{ℕ, ℝ, ℂ}，这是我上面定义的常量B作为例子。 Isabelle 中没有 ℂ，因为那只是 UNIV::complex set。 (UNIV 是相关类型的所有值的集合)。请注意，这种情况下的 ℕ 和 ℝ 是自然数和实数的集合，作为复数的子集。