如何在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