如何中止伊莎贝尔的证明？

Question

我想知道是否有办法中止 Isabelle/jEdit 中的证明？

我搜索了“重置”、“中止”等命令，但没有找到。

我知道有Sorry。但我不确定是否有人使用 Sorry，手头的定理假定为真或被放弃。此外，Sorry 似乎在 apply..done 模式下不起作用。

目前，我把无法证明的定理注释掉了。但是注释或取消注释需要大量输入（（* *）中每个字符四个字符，这有点麻烦。

那么在 Isabelle 中是否有 standard/universal 中止证明的方法？

Answer 1

首先，命令是 sorry 并且它确实（但仅）适用于应用样式：

lemma 
  ‹False ∧ True›
  apply (rule conjI)
   apply auto
  sorry

关于实际问题，oops 中止证明，无论是否应用样式：

lemma 
  ‹False ∧ True›
proof -
  have True
    by auto
  oops

oops-ed 证明以后无法引用。

How to abort a proof in Isabelle?