在 Isabelle 中使用泛型定义

Question

我正在处理限制，我无法证明以下内容

definition func :: "real ⇒ real"
where "func = real"

lemma "(λh. (func (x+h))) -- 0 --> (func (x))"
unfolding func_def
apply (auto intro!: tendsto_eq_intros)

但是，如果我将 func 的定义替换为

definition func :: "real ⇒ real"
where "func x = x"

引理解决了。

在使用泛型定义时如何解决这个引理？

Answer 1

我相信，这里的问题是函数real 仅具有通用（重载）语法，即real :: 'a => real，但不一定为所有可能的类型定义'a。使用 find_theorems 时很容易看到这一点：在 real :: nat => real 上搜索引理时，您会得到很多结果，而搜索 real :: real => real 不会给您一个结果。

find_theorems "real :: real => real"
find_theorems "real :: nat => real"

因此，您甚至无法证明像func x = x 这样的简单引理，因为没有指定real :: real => real 确实是恒等函数。