# [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.