[isabelle-dev] New lemmas about count_list

[Martin Desharnais]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0x58AE985FE188789A.asc
Type: application/pgp-keys
Size: 3139 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220228/84687577/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 840 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220228/84687577/attachment.sig>