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
OpenPGP_0x58AE985FE188789A.asc
Description: OpenPGP public key
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
