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