# [isabelle] Sum of list elements

Hello,

`I am having a problem on the exercise 1.8 Sum of list elements, tail
``recursively at http://isabelle.in.tum.de/exercises/
`I have the same functions as in the solution :
primrec ListSum :: "nat list \<Rightarrow> nat" where
"ListSum [] = 0"
| "ListSum (n#ns) = n + (ListSum ns)"

`primrec ListSumTAux :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
``where
` "ListSumTAux [] n = n"
| "ListSumTAux (x#xs) n = ListSumTAux xs (x + n)"
definition ListSumT :: "nat list \<Rightarrow> nat" where
"ListSumT xs \<equiv> ListSumTAux xs 0"
(* I tried to prove the following lemma, but couldn't. *)

`lemma switch_ListSumTAux: "\<forall>x y. (x + ListSumTAux xs y) =
``ListSumTAux xs (x+y)"
`apply (induct_tac xs)
apply auto
done

`(* So I looked in the solution and found that if you try to prove it
``the other way around it works... *)
`

`lemma switch_ListSumTAux: "\<forall>x y. ListSumTAux xs (x+y) = (x +
``ListSumTAux xs y)"
`apply (induct_tac xs)
apply auto
done
Does anyone know why ?
Thank you for your help, best regards
Etienne

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