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_allSee 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_allSee 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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
