Isabelle中函数n阶导数的表示方法及相关实现咨询

刚接触Isabelle的求导操作，想知道有没有表示函数$f$的$n$阶导数$f^{(n)}(x)$的方法，纠结是用类似(f has_derivative f') (at x)的语法，还是借助DERIV、deriv算子？

附上Derivative.thy中的相关定义与引理：

definition✐‹tag important› deriv :: "('a ⇒ 'a::real_normed_field) ⇒ 'a ⇒ 'a" where
"deriv f x ≡ SOME D. DERIV f x :> D"

lemma DERIV_imp_deriv: "DERIV f x :> f' ⟹ deriv f x = f'"
unfolding deriv_def by (metis some_equality DERIV_unique)

另外，has_derivative的定义位于Deriv.thy中。我倾向于使用has_derivative，但缺乏充分依据，也不清楚是否存在n阶导数的通用定义。若自行定义，希望语法类似：(f has_nth_derivative n [lambda表达式表示n阶导数]) (at x)。

核心解答 #

1. 标准库中的n阶导数支持 #

Isabelle标准库已内置n阶导数的定义，核心是iterated_deriv算子：

• iterated_deriv n f 直接表示函数$f$的$n$阶导函数
• 结合语境可以用(iterated_deriv n f has_derivative f'') (at x)这类形式，标准库中也有iterated_has_derivative相关引理用于证明衔接。

2. 三种求导语法的区别 #

• DERIV f x :> D: 底层谓词，直接断言$f$在$x$处的导数为$D$，偏向基础逻辑证明场景。
• deriv f x: 通过SOME算子封装的函数，直接返回$f$在$x$处的导数值（若存在），适合直接引用或计算导数值。
• (f has_derivative f') (at x): 高层封装语法，本质是对DERIV的可读性包装，用于断言导数关系，在日常证明中更常用，你的倾向是合理的。

3. 自定义n阶导数语法的实现 #

如果要实现你预期的has_nth_derivative语法，可以参考以下两种方式：

(* 基于iterated_deriv的直接定义 *)
definition has_nth_derivative :: "('a ⇒ 'b::real_normed_field) ⇒ nat ⇒ ('a ⇒ 'b) ⇒ 'a filter ⇒ bool" where
  "has_nth_derivative f n f' F ≡ (iterated_deriv n f has_derivative f') F"

(* 递归式定义，更贴合直观逻辑 *)
primrec has_nth_derivative :: "('a ⇒ 'b::real_normed_field) ⇒ nat ⇒ ('a ⇒ 'b) ⇒ 'a filter ⇒ bool" where
  "has_nth_derivative f 0 f' F ≡ (f has_derivative f') F" |
  "has_nth_derivative f (Suc n) f' F ≡ (∃g. has_nth_derivative f n g F ∧ (g has_derivative f') F)"

定义完成后，就能使用(f has_nth_derivative n (λx. ...)) (at x)的形式来断言n阶导数关系。

内容的提问来源于stack exchange，提问作者Squirtle