# HG changeset patch
# User nipkow
# Date 1646663333 -3600
# Node ID 21b2e37e03007caa90ee85ebb2ad9d5b46df0635
# Parent  d647f6b74744510d4cf3d62807a34522f5bad374
more count_list lemmas

diff -r d647f6b74744 -r 21b2e37e0300 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 07 12:40:36 2022 +0100
+++ b/src/HOL/List.thy	Mon Mar 07 15:28:53 2022 +0100
@@ -4277,6 +4277,8 @@
 
 subsubsection \<open>\<^const>\<open>count_list\<close>\<close>
 
+text \<open>This library is intentionally minimal. See the remark about multisets at the point above where @{const count_list} is defined.\<close>
+
 lemma count_list_append[simp]: "count_list (xs @ ys) x = count_list xs x + count_list ys x"
 by (induction xs) simp_all
 
@@ -4289,10 +4291,16 @@
 lemma count_le_length: "count_list xs x \<le> length xs"
 by (induction xs) auto
 
+lemma count_list_map_ge: "count_list xs x \<le> count_list (map f xs) (f x)"
+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 count_list_rev[simp]: "count_list (rev xs) x = count_list xs x"
+by (induction xs) auto
+
 lemma sum_count_set:
   "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> sum (count_list xs) X = length xs"
 proof (induction xs arbitrary: X)