Martin, I have compromised and have added some of the lemmas to the distribution.
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
