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

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

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

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

Martin,

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

Tobias

smime.p7s

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: Mar 04 2024 at 10:08 UTC