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.