# HG changeset patch
# User nipkow
# Date 1646601198 -3600
# Node ID 99b83e701c8ee26a53220026272103cc43fe2c6b
# Parent  6c4ec2a27ad6c0626bb0d1a8be277b3e592bc039
added count_list lemmas

diff -r 6c4ec2a27ad6 -r 99b83e701c8e src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Mar 06 17:53:14 2022 +0100
+++ b/src/HOL/List.thy	Sun Mar 06 22:13:18 2022 +0100
@@ -4277,12 +4277,22 @@
 
 subsubsection \<open>\<^const>\<open>count_list\<close>\<close>
 
+lemma count_list_append[simp]: "count_list (xs @ ys) x = count_list xs x + count_list ys x"
+by (induction xs) simp_all
+
+lemma count_list_0_iff: "count_list xs x = 0 \<longleftrightarrow> x \<notin> set xs"
+by (induction xs) simp_all
+
 lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> count_list xs x = 0"
-by (induction xs) auto
+by(simp add: count_list_0_iff)
 
 lemma count_le_length: "count_list xs x \<le> length xs"
 by (induction xs) auto
 
+lemma count_list_inj_map:
+  "\<lbrakk> inj_on f (set xs); x \<in> set xs \<rbrakk> \<Longrightarrow> count_list (map f xs) (f x) = count_list xs x"
+by (induction xs) (simp, fastforce)
+
 lemma sum_count_set:
   "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> sum (count_list xs) X = length xs"
 proof (induction xs arbitrary: X)