为什么不能在Isabelle中简化Σ{0} = 0以使它们相等？

Question

[我正在阅读第5章（Isar），并尝试为"Σ{0..n::nat} = n*(n+1) div 2"做结构归纳证明，但失败了：

lemma "Σ{0..n::nat} = n*(n+1) div 2" 
proof (induction n)
  show "Σ{0..0::nat} = 0*(0+1) div 2" by simp
next
  fix n 
  assume "Σ {0..n} = n * (n + 1) div 2"
  thus "Σ {0..Suc n} = Suc n * (Suc n + 1) div 2" by simp
qed

它说：

show Σ {0..0} = 0 * (0 + 1) div 2 
Successful attempt to solve goal by exported rule:
  Σ {0..0} = 0 * (0 + 1) div 2 
proof (state)
this:
  Σ {0..0} = 0 * (0 + 1) div 2

goal (1 subgoal):
 1. ⋀n. Σ {0..n} = n * (n + 1) div 2 ⟹ Σ {0..Suc n} = Suc n * (Suc n + 1) div 2 
Failed to finish proof⌂:
goal (1 subgoal):
 1. Σ {0} = 0

我不知道为什么。大锤也没有解决。我确实尝试过blast，auto等，但我知道它们会失败，因为大锤曾向我建议过这些，但值得尝试吗？

我尝试过应用样式以查看发生了什么：

lemma "Σ{0..n::nat} = n*(n+1) div 2"
  apply (induction n)
   apply simp
apply simp

相同错误：

proof (prove)
goal (2 subgoals):
 1. Σ {0} = 0
 2. ⋀n. Σ {0..n} = n * (n + 1) div 2 ⟹ Σ {0..Suc n} = Suc n * (Suc n + 1) div 2 
Failed to apply proof method⌂:
goal (2 subgoals):
 1. Σ {0} = 0
 2. ⋀n. Σ {0..n} = n * (n + 1) div 2 ⟹ Σ {0..Suc n} = Suc n * (Suc n + 1) div 2

为什么这不起作用？我的Isabelle安装有问题吗？

[我还在没有任何内容的文件上尝试过证明，但它也失败了，所以它不是我以前的任何定义（我认为可能性很大）。

Answer 1

似乎在右下角可以手动插入符号的位置不是一个好主意。它插入了符号sigma而不是Sum。我通过执行\<Sum>来修复它（实际上我是使用Tab自动完成的）。证明现在可以使用：

lemma "∑{0..n::nat} = n*(n+1) div 2"
  apply (induction n)
   apply simp
  by simp