Stream: General

Topic: Missing lemma in `List`

Javier Diaz (Oct 05 2022 at 01:24):

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

Mathias Fleury (Oct 05 2022 at 05:15):

Use multisets instead of lists count (mset xs) z

Javier Diaz (Oct 05 2022 at 14:10):

Thanks, @Mathias Fleury, for your answer. That definitely is a workaround, however the List theory already includes a count_list function which avoids the overhead of creating a temporary multiset out of a list. There are some basic lemmas about count_list already, but surprisingly there is no lemma relating count_list and @ in the style of Multiset.count_union. That's why I think adding a count_append lemma as above is a good idea.

Lukas Stevens (Oct 05 2022 at 14:15):

This is already part of List.thy in the development version of Isabelle.

Lukas Stevens (Oct 05 2022 at 14:15):

It was added back in March.

Lukas Stevens (Oct 05 2022 at 14:16):

The next release will be soon so you can just add the lemma temporarily to your theory and then remove it when upgrading to the new version.

Last updated: Apr 26 2024 at 20:16 UTC