如何在 Isabelle 中定义偏函数？

我尝试用以下方法定义偏函数partial_function关键词。它不起作用。这是最能表达直觉的：

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity Zero = Zero "
| "oddity (Succ (Succ n)) = n"

然后我尝试了以下操作：

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity arg = ( case arg of (Succ (Succ n)) => n
                          | Zero => Zero
                )"

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity (Succ(Succ n)) = n
   | oddity Zero = Zero"

partial_function (tailrec) oddity :: "nat => nat"
where
  "oddity n =
   (if n = Zero then Zero
    else if (n >= 2)
      then do { m ← oddity (n-2); m })"

他们都没有工作。我想我的尝试存在概念和句法问题，这些问题是什么？

您的定义有两个问题：

1. partial_function不支持左侧的模式匹配。这必须模仿case右边的表达式。

2. 类型的构造函数nat are Suc and 0, not Succ and Zero。这就是为什么您的 case 表达式会生成错误Succ and Zero不是数据类型构造函数，为什么parital_function抱怨说Zero是右侧的额外变量。

概括起来，主要做了以下工作：

partial_function (tailrec) oddity :: "nat => nat"
where "oddity arg = (case arg of (Suc (Suc n)) => n | 0 => 0 )"

您可以使用模式匹配来恢复简化规则simp_of_case转换自~~/src/HOL/Library/Simps_Case_Conv:

simps_of_case oddity_simps[simp]: oddity.simps

thm oddity_simps