[isabelle] a simplifier subtlety



Hi,

theory Dummy
imports Main

begin

lemma "? { 0..n::nat} = n*(n+1) div 2" (is "?P n")
proof (induction n)
  show "?P 0" by simp
next
  fix n assume "?P n"
  from this show "?P (Suc n)" by simp
qed

verifies the formula for this sum as expected, especially the simplifier solves the ”?P 0” case:

                ?{0..0} = 0 * (0 + 1) div 2

However, when I pose that lemma directly, the simplifier cannot prove it:

lemma "?{0..0} = 0 * (0 + 1) div 2"
apply simp

results in

?{0..0} = 0 * 1 div 2

What is the difference between the two case?

- Gergely



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.