[isabelle-dev] New lemmas about count_list

[Tobias Nipkow]

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

On 28/02/2022 15:36, Martin Desharnais wrote:
> 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220301/23eedbcd/attachment.bin>