Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Missing lemma in `List` theory

view this post on Zulip Email Gateway (Oct 05 2022 at 01:35):

From: Javier Diaz <cl-isabelle-users@lists.cam.ac.uk>
Hi everyone,

I think it would be useful to add the following lemma to the List theory:

lemma count_append: "count_list (xs @ ys) z = count_list xs z + count_list
ys z"
by (induct xs) simp_all

Best regards,
Javier

view this post on Zulip Email Gateway (Oct 05 2022 at 06:09):

From: Tobias Nipkow <nipkow@in.tum.de>
The lemma is there already:

lemma count_list_append[simp]: "count_list (xs @ ys) x = count_list xs x +
count_list ys x"
by (induction xs) simp_all

Tobias
smime.p7s

Last updated: Apr 26 2024 at 16:20 UTC