interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$.  We

 interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$.  We

 extend \texttt{Arith} as follows:

 extend \texttt{Arith} as follows:

 \begin{ttbox}

 \begin{ttbox}

 NatSum = Arith +

 NatSum = Arith +

 consts sum     :: [nat=>nat, nat] => nat

 consts sum     :: [nat=>nat, nat] => nat

   "sum f 0 = 0"

   "sum f 0 = 0"

   "sum f (Suc n) = f(n) + sum f n"

   "sum f (Suc n) = f(n) + sum f n"

 end

 end

 \end{ttbox}

 \end{ttbox}

 The \texttt{primrec} declaration automatically adds rewrite rules for

 The \texttt{primrec} declaration automatically adds rewrite rules for