为何无法在Isabelle中定义nat？代码报错求解决

Hey there! The error you're seeing boils down to a naming conflict between your custom nat type and the one built into Isabelle's Main library. Let me break it down simply:

When you write imports Main, you're pulling in Isabelle's standard library—which already includes a pre-defined nat type (with exactly the same 0 and Suc constructors you wrote!). By re-defining datatype nat = 0 | Suc nat yourself, you're forcing Isabelle to choose between two different entities both named nat.0, which triggers those "bad name binding" errors.

Here are two straightforward fixes: #

1. Drop the Main import (stick with your custom nat)

If you're working through the tutorial to learn how to define your own types, just remove imports Main so Isabelle only recognizes your nat definition:

theory BasicAdditionProof begin
datatype nat = 0 | Suc nat
fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 n = n" | "add (Suc m) n = Suc(add m n)"
lemma add_02: "add m 0 = m"
apply(induction m)
apply(auto)
done
end

2. Keep Main and use Isabelle's built-in nat

Isabelle's standard nat comes with a huge set of pre-proven theorems and utilities, so this is the better choice for most real-world work. Just delete your custom datatype nat line:

theory BasicAdditionProof imports Main begin
fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 n = n" | "add (Suc m) n = Suc(add m n)"
lemma add_02: "add m 0 = m"
apply(induction m)
apply(auto)
done
end

Either way, once the naming conflict is resolved, your proof for add_02 will run without errors.

内容的提问来源于stack exchange，提问作者Pro Q