Email Gateway (Aug 18 2022 at 19:32): Email Gateway (Aug 18 2022 at 19:32):From: Etienne Mabille <Etienne.Mabille@onera.fr>
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
Email Gateway (Aug 18 2022 at 19:32):From: Lars Noschinski <noschinl@in.tum.de>
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
Last updated: Apr 24 2024 at 20:16 UTC