首先，您对limit的定义是错误的。您混合了一些量词顺序。这是我的写法：

definition limit :: "(nat ⇒ rat) ⇒ rat ⇒ bool"
  where "limit sequence l = (∀ε>0. ∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε)"

然后这就是如何证明您想要的东西：

lemma limit_simple: "limit (λ(x::nat). 1 / of_nat x) 0"
  unfolding limit_def
proof (intro allI impI)
  fix ε :: rat assume "ε > 0"
  obtain d_rat::rat where d_rat: "1 / ε < d_rat" using linordered_field_no_ub by auto
  define d where "d = nat (⌊d_rat⌋ + 1)"

  have "d_rat ≤ of_nat d"
    unfolding d_def by linarith

  from ‹ε > 0› have "0 < 1 / ε" by simp
  also have "1 / ε < d_rat" by fact
  also have "d_rat ≤ of_nat d" by fact
  finally have "d > 0" by simp

  have "d_rat > 0" using ‹1 / ε > 0› and d_rat by linarith

  have "∀e≥d. ¦1 / of_nat e - 0¦ ≤ ε"
  proof (intro allI impI)
    fix e :: nat
    assume "d ≤ e"
    have "¦1 / rat_of_nat e - 0¦ = 1 / rat_of_nat e" by simp
    have "d_rat ≤ rat_of_nat e"
      using ‹d ≤ e› and ‹d_rat ≤ of_nat d› by simp
    hence "1 / rat_of_nat e ≤ 1 / d_rat"
      using ‹d ≤ e› and ‹d > 0› and ‹d_rat > 0›
      by (intro divide_left_mono) auto
    also have "1 / d_rat < ε"
      using ‹ε > 0› and ‹d_rat > 0› and d_rat by (auto simp: field_simps)
    finally show "¦1 / rat_of_nat e - 0¦ ≤ ε" by simp
  qed
  thus "∃d. ∀e≥d. ¦1 / of_nat e - 0¦ ≤ ε"
    by auto
qed

对于实数而不是有理数，证明看起来基本上是相同的。当然，它可以自动化得更多（好吧，如果导入Isabelle的分析库，它可以一步一步自动证明整个过程）。

在“现实世界”伊莎贝尔（Isabelle）中，限制用 filters 表示，并且周围有一个大型图书馆。这使上述证明的陈述变得乏味。

更新：回应您的评论：是的，这有点冗长。在惯用的Isabelle中，我将这样写证明：

lemma A: "filterlim (λn. 1 / real n) (nhds 0) sequentially"
proof
  fix ε :: real assume "ε > 0"
  have "∀⇩F n in sequentially. n > nat ⌈1 / ε⌉"
    by (rule eventually_gt_at_top)
  hence "∀⇩F n in sequentially. real n > 1 / ε"
    by eventually_elim (use ‹ε > 0› in linarith)
  moreover have "∀⇩F n in sequentially. n > 0"
    by (rule eventually_gt_at_top)
  ultimately show "∀⇩F n in sequentially. dist (1 / real n) 0 < ε"
    by eventually_elim (use ‹ε > 0› in ‹auto simp: field_simps›)
qed

这种过滤器的概念和一个拥有“最终”属性的属性（这就是∀⇩F语法的含义）。

更好的是，您可以对上述证明进行更多的模块化，首先显示对于真实的x，x→∞的1 / x趋于0，然后表明对于自然real n，n趋于实∞，然后n趋于∞，然后简单地将这两个语句组合在一起：

lemma B: "filterlim (λx::real. 1 / x) (nhds 0) at_top"
proof
  fix ε :: real assume "ε > 0"
  have "∀⇩F x in at_top. x > 1 / ε"
    by (rule eventually_gt_at_top)
  thus "∀⇩F (x::real) in at_top. dist (1 / x) 0 < ε"
    using eventually_gt_at_top[of 0]
    by eventually_elim (use ‹ε > 0› in ‹auto simp: field_simps›)
qed

lemma C: "filterlim real at_top sequentially"
  unfolding filterlim_at_top
proof
  fix C :: real
  have "∀⇩F n in sequentially. n ≥ nat ⌈C⌉"
    by (rule eventually_ge_at_top)
  thus "∀⇩F n in sequentially. C ≤ real n"
    by eventually_elim linarith
qed

lemma D: "filterlim (λn. 1 / real n) (nhds 0) sequentially"
  by (rule filterlim_compose[OF B C])

或者，当然，您可以简单地导入HOL-Real_Asymp.Real_Asymp，然后使用by real_asymp自动完成所有这些操作。 ;）

您真的不应该根据从头开始做所有事情的难度来判断一个系统，尤其是当已经有一种惯用的方式来做这些事情并且您正在积极地做些不同的事情时。标准库及其习语是系统的重要组成部分。

在证明助手中难以模仿笔式推理，尤其是在诸如“渐近”之类的许多事物“显而易见”的领域。幸运的是，有了一个好的库，确实可以实现这种推理的某种近似。当然，您可以 进行明确的ε-δ推理，但这只会使您的生活更加困难。当我开始在Isabelle中使用限制时，我犯了同样的错误（因为ε-δ是处理我知道的限制的唯一正式方法，但我并不了解所有那些花哨的过滤器内容），但是当我开始了解过滤器时而且，事情变得更加清晰，轻松和自然。

我认为这里的许多困难都来自nat和rat之间的所有转换。在有理上证明等效函数的极限比较容易：

definition limit_r :: "(rat ⇒ rat) ⇒ rat ⇒ bool"
  where "limit_r sequence l = (∀ε>0. ∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε)"

lemma limit_simple_r: "limit_r (λx. 1 / x) 0"
 unfolding limit_r_def
proof (intro allI impI)
  fix ε :: rat assume "ε > 0"

  hence "¦1 / (1/ε) - 0¦ ≤ ε"
    by auto

  hence "∀e≥(1/ε). ¦1 / e - 0¦ ≤ ε"
    using `ε > 0` by (auto simp add: divide_le_eq order_trans )

  thus "∃d. ∀e≥d. ¦1 / e - 0¦ ≤ ε"
    by blast
qed

然后可以将结果转回序列：

definition limit :: "(nat ⇒ rat) ⇒ rat ⇒ bool"
  where "limit sequence l = (∀ε>0. ∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε)"

lemma to_rat_limit:
  assumes a1: "limit_r sequence_r l"
    and a2: "⋀n. sequence n = sequence_r (of_nat n)"
  shows "limit sequence l"
  unfolding limit_def proof (intro allI impI)
  fix ε :: rat
  assume "0 < ε"

  from assms obtain d where "∀e≥d. ¦sequence_r e - l¦ ≤ ε"
    using ‹0 < ε› using limit_r_def by blast  

  hence "¦sequence e - l¦ ≤ ε" if "e ≥ nat ⌈d⌉" for e
    using that a2 by (auto,meson of_nat_ceiling of_nat_mono order_trans)

  thus "∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε"
    by blast
qed


lemma limit_simple: "limit (λ(x::nat). 1 / of_nat x) 0"
  using limit_simple_r to_rat_limit by auto