伊莎贝尔被以前的引理搞糊涂了?

我在做具体语义书的练习2.5时发现了一些奇怪的东西。基本上,我们必须证明著名的高斯公式的和n整数。这是我的代码:

fun sum_upto :: "nat ⇒ nat" where
"sum_upto 0 = 0" |
"sum_upto (Suc n) = (Suc n) + (sum_upto n)"

lemma gauss: "sum_upto n = (n * (n + 1)) div 2"
apply(induction n)
apply(auto)
done 

至少我从练习2.3中删除了以前的引理:

fun double :: "nat ⇒ nat" where
"double 0 = 0" |
"double (Suc n) = add (double n) 2"

lemma double_succ [simp]: "Suc (Suc (m)) = add m 2"
apply(induction m)
apply(auto)
done

lemma double_add: "double m = add m m"
apply(induction m)
apply(auto)
done

所以这里添加是一个用户定义的函数。我已经找到了其他的解决方案,我对double的定义被替换为 Suc(Suc (double n)) 在这种情况下,下一个引理是不必要的,高斯中的错误消失了。

然而,我有兴趣知道为什么会发生这种情况,因为原则上这两个问题都不使用任何公共结构。