在没有局部假设的情况下证明 Isar 中的定理

Question

陈述 n+0 = n 很容易证明：

theorem add_0: "n+0 = (n::nat)"
  apply(simp)
  done

然而，在尝试将其转换为 Isar 时，我注意到它似乎不需要任何假设。所以在这次尝试中：

theorem add_0: "n+0 = (n::nat)"
proof -
  thus "True" by simp
qed

它失败了，因为有“No current facts available”。第二次尝试也失败了：

theorem add_0: "n+0 = (n::nat)"
proof -
  from add_0 show "True" by simp
qed

这次出现错误“Failed to refine any pending goal”。

是否可以证明 Isar 中不需要 assume 子句的命题？如果是，那又如何？

Answer 1

thus "True"有两个问题

正如您所指出的，您开始的证明状态没有任何假设，因此证明状态中没有事实。缩写 thus 扩展为 then show，因为我们的证明状态中没有事实，所以使用 then 没有意义，因此我们应该将其替换为 show。
show "True" 是说我们要证明 "True" 而不是我们要证明定理的目标。我们可以使用示意图变量?thesis来引用定理的原始论文。错误Failed to refine any pending goal只是说如果我们要证明True是真的，那将无助于解决我们论文的目标。

所以我们可以使用以下模式用 Isar 证明来证明我们的原始定理。

theorem add_0: "n+0 = (n::nat)"
proof -
  show ?thesis by simp
qed

Proving theorem in Isar with no local assumptions