isabelle - c^n 的极限（¦c¦<1）为0（伊莎贝尔）

Question

有谁知道显示规则

"¦c¦<1 ==> (λn. c^n) ---> 0"

在现实中？

我使用“查询”面板找到了以下规则：

Limits.LIMSEQ_rabs_realpow_zero2: ¦?c¦ < 1 ⟹ op ^ ?c ---> 0
Limits.LIMSEQ_rabs_realpow_zero: ¦?c¦ < 1 ⟹ op ^ ¦?c¦ ---> 0
Limits.LIMSEQ_realpow_zero: 0 ≤ ?x ⟹ ?x < 1 ⟹ op ^ ?x ---> 0

虽然我有点困惑是什么op意思。

Answer 1

您要证明的引理正是LIMSEQ_rabs_realpow_zero2. 因此，您可以用 证明您的目标apply (rule LIMSEQ_rabs_realpow_zero2)。

例如尝试term "λx y. x + y"或term "λx. 1 + x"在伊莎贝尔。输出将分别为op +和op + 1。

Theop ^只是 的简写λx y. x ^ y。一般来说，op在 Isabelle 中，是用于将二元中缀运算符转换为具有两个参数的函数的语法（有点像 ML）。