# HG changeset patch
# User nipkow
# Date 1646728539 -3600
# Node ID 810d16927cdc575d0f0230cb158bf689de64e77e
# Parent  83197a0ac6df75cabb1c8d45090db5adad802663# Parent  21b2e37e03007caa90ee85ebb2ad9d5b46df0635
merged

diff -r 83197a0ac6df -r 810d16927cdc src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 07 21:16:12 2022 +0100
+++ b/src/HOL/List.thy	Tue Mar 08 09:35:39 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)