isabelle - Isar 虚拟机输出中的深度指的是什么？

Question

这是一个证明：

theory Example

imports Main

begin

datatype natural = Zero | Succ natural

lemma "⋀ n. n = Succ m ⟹ n ≠ Zero"
proof -
 fix n
 assume "n = Succ m" 
 from this show "n ≠ Zero" by (metis natural.distinct(2))
qed

end

在整个证明过程中该depth值为 0，但之后

show "n ≠ Zero"

它变为

proof (prove): depth 1

这里是什么depth意思？进行证明时是否重要？

Answer 1

简而言之，它指的是当前的证明嵌套级别。在您的情况下，它是 1，因为show在证明中打开了一个新证明。

回答你的第二个问题：不，这根本不重要。有些人用它来衡量一个证明的复杂程度，但对于系统来说，它没有任何区别。