-1

ここに証明があります：

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どういう意味ですか? 証明を行う際に重要なことはありますか?

4

1 に答える 1

0

In a nutshell, it refers to the current proof nesting level. In your case, it's 1, because show opens a new proof inside the proof.

To answer your second question: No, it's not important at all. Some people use it to measure how complicated a proof is, but to the system, it makes no difference.

于 2015-10-19T19:15:21.650 に答える