{0,1} 作为 Isabelle 中的函数类型

Question

我正在尝试编写一个带有第二个参数的函数，该参数可以是 0 或 1：

typedef f_2 = "{0::nat,1}"

function proj_add :: "(real × real) × f_2 ⇒ (real × real) × f_2 ⇒ (real × real) × f_2" where
  "proj_add ((x1,y1),l) ((x2,y2),j) = ((add (x1,y1) (x2,y2)), (l+j) mod 2)" 
    if "delta x1 y1 x2 y2 ≠ 0"
| "proj_add ((x1,y1),l) ((x2,y2),j) = ((ext_add (x1,y1) (x2,y2)), (l+j) mod 2)" 
    if "delta' x1 y1 x2 y2 ≠ 0"

如果我直接写 {0::nat,1} 我会得到错误 inner syntax error.

如果我写 f_2 我会收到错误未定义类型名称 f_2。

用伊莎贝尔写这个定义的正确方法是什么？

Answer 1

理论HOL-Library.Bit中有类型bit，有0和1两个元素。这包含使 0 和 1 符号适用于 bit 所需的所有设置，包括模式匹配。

{0,1} 作为 Isabelle 中的函数类型

{0,1} as function type in Isabelle

isabelle