Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] New lemmas about count_list

Email Gateway (Feb 28 2022 at 14:36):

From: Martin Desharnais <martin.desharnais@posteo.de>
Dear Isabelle developers,

I just needed a few simple lemmas about the count_list function and
suggest adding them directly to HOL.List. A quick search on
https://search.isabelle.in.tum.de revealed that some of them were
duplicated in some AFP entries.

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

See Groebner_Macaulay.Dube_Prelims.count_list_append,
List_Update.TS.count_append,
Signature_Groebner.Prelims.count_list_append, and
Buildings.Prelim.count_list_append.

lemma count_list_eq_zero_conv: "count_list xs x = 0 ⟷ x ∉ set xs"
by (induction xs) simp_all

See Groebner_Macaulay.Dube_Prelims.count_list_eq_0_iff,
HOL.list.count_notin, and List_Update.TS.count_notin2.

lemma distinct_iff_count_list: "distinct xs ⟷ (∀x. count_list xs x = 0 ∨
count_list xs x = 1)"
by (induction xs) (auto simp add: count_list_eq_zero_conv)

See Buildings.Prelim.distinct_count_list.

lemma count_list_filter:
"P x ⟹ count_list (filter P xs) x = count_list xs x"
"¬ P x ⟹ count_list (filter P xs) x = 0"
by (induction xs) simp_all

Would it make sense to include them in the distribution?

Regards,
Martin
OpenPGP_0x58AE985FE188789A.asc
OpenPGP_signature

Email Gateway (Mar 01 2022 at 13:58):

From: Tobias Nipkow <nipkow@in.tum.de>
Dear Martin,

In List.thy it says

text ‹In the context of multisets, ‹count_list› is equivalent to
\<^term>‹count ∘ mset› and it it advisable to use the latter.›

Thus I would rather not create a growing count_list library, if it can be
avoided. Could you try to use the above hint and go via multisets? (I may add
one or two of your lemmas anyway, as a compromise)

Tobias
smime.p7s

Email Gateway (Mar 04 2022 at 08:38):

From: Martin Desharnais <martin.desharnais@posteo.de>
Dear Tobias,

thanks for looking into it.

I will try to replace all my usages of count_list by "count ∘ mset" and
see how things turn out.

Cheers,
Martin
OpenPGP_0x58AE985FE188789A.asc
OpenPGP_signature

Email Gateway (Mar 08 2022 at 15:53):

From: Tobias Nipkow <nipkow@in.tum.de>
Martin,

I have compromised and have added some of the lemmas to the distribution.

Tobias
smime.p7s

Email Gateway (Mar 10 2022 at 19:08):

From: Martin Desharnais <martin.desharnais@posteo.de>
Hi Tobias,

I have compromised and have added some of the lemmas to the distribution.

Thank you.

Regars,
Martin
OpenPGP_0x58AE985FE188789A.asc
OpenPGP_signature

Last updated: Dec 07 2024 at 16:22 UTC