# Re: [isabelle] Sum of list elements

On 12.04.2012 10:04, Etienne Mabille wrote:

primrec ListSumTAux :: "nat list \<Rightarrow> nat \<Rightarrow> nat" where
"ListSumTAux [] n = n"
| "ListSumTAux (x#xs) n = ListSumTAux xs (x + n)"

[...]

(* 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

Basically, you are left to show
∀x y. ListSumTAux list (x + (a + y)) = ListSumTAux list (a + (x + y))

`here. This is trivial, if "x + (a + y)" and "a + (x + y)" can be
``rewritten to the same normal form. You can do this by adding ac_simps
``(AC = associativity, commutativity) to the simpset:
`
apply (auto simp: ac_simps)
> done

`ac_simps (and its companions algebra_simps and field_simps) are very
``useful for normalizing arithmetic goals.
`

(* 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)

`To find out, how the simplifier solves this goal, it is useful to enable
``the simplifier trace:
`
apply simp (* discharge the first goal *)
using [[simp_trace]]
apply simp

`As this lemma is stated the other way round, also the induction
``hypothesis is the other way round, and the simplifier moves additions to
``the outside and you get an intermediate goal of the form:
`
∀x y. a + (x + ListSumTAux list y) = x + (a + ListSumTAux list y)

`For goals with arithmetic operations on the toplevel, the simplifier has
``a number of specialized simplification procedures (simprocs), which try
``to remove operands which occur on both sides:
`

` [1] Procedure "Numeral_Simprocs.nateq_cancel_numerals" produced
``rewrite rule:
`` a + (x + ListSumTAux list y) = x + (a + ListSumTAux list y) ≡ x +
``ListSumTAux list y = x + ListSumTAux list y
`

`(from the trace). Hence there is no need to explicitly add ac_simps to
``the simpset.
`
-- Lars

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