isabelle - 如何在 Isabelle 中定义偏函数？

Question

我尝试使用 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 })"

它们都不起作用。我想我的尝试存在概念和语法问题，这些问题是什么？

Answer 1

您的定义有两个问题:

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

2. 类型 nat 的构造函数是Suc和0 ，不是Succ和Zero 。这就是为什么您的 case 表达式生成错误 Succ和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