伊莎贝尔中的应用和Isar风格的等价性

Question

应用样式与Isar校对是否相等？这是我想了一段时间的问题。当然，Isar校对的可读性、可维护性和编写(?)但我的问题是，你能否证明这两种风格完全相同。

举个例子，我目前正在研究一个我需要离开的证据：

apply(simp split: prod.splits) 
using some_lemma by fastforce

在apply和Isar样式中，这些命令的等效形式是什么？事实上，我对Isar风格更感兴趣，因为我被告知混合风格是不好的。

Answer 1

与之相当的国际会计准则的风格是：

have "P"
  using some_lemma by fastforce
then have "Q"
  by (simp split: prod.splits)

其中"P“表示第一个apply之后的中间目标状态。

一般来说，任何可以证明的东西都可以在Isar和apply风格中证明；两者都有各自的优点和缺点。

我个人使用的风格是我试图在外部构建我的证明:外部(比如归纳) Isar，如果有必要的话，用apply构建内部(比如简化、低级的东西)。

总的来说，我建议您尽可能多地呆在Isar中。