无局部假设下的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是没有意义的，所以我们应该用then代替它，意思是我们想证明"True"，而我们想证明定理的目的。我们可以用示意图变量?thesis来参考定理的原著。错误Failed to refine any pending goal只是说，如果我们要证明True是真的，这无助于解决我们论文的目标。

因此，我们可以用一个Isar证明来证明我们原来的定理，用下面的模式。

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