Что делает глубина в выводе Isar Virtual Machine?

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 открывает новое доказательство внутри доказательства.

Чтобы ответить на второй вопрос: Нет, это не важно. Некоторые люди используют его для измерения того, насколько сложным является доказательство, но для системы это не имеет значения.