--- a/src/HOL/Groups_List.thy Wed May 21 20:44:12 2025 +0200
+++ b/src/HOL/Groups_List.thy Thu May 22 19:59:43 2025 +0200
@@ -147,6 +147,9 @@
lemma sum_list_of_int: "sum_list (map of_int xs) = of_int (sum_list xs)"
by (induction xs) auto
+lemma count_list_concat: "count_list (concat xss) x = sum_list (map (\<lambda>xs. count_list xs x) xss)"
+by(induction xss) auto
+
lemma (in comm_monoid_add) sum_list_map_remove1:
"x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))"
by (induct xs) (auto simp add: ac_simps)
--- a/src/HOL/List.thy Wed May 21 20:44:12 2025 +0200
+++ b/src/HOL/List.thy Thu May 22 19:59:43 2025 +0200
@@ -3769,6 +3769,9 @@
case False with d show ?thesis by auto
qed
+lemma distinct_concat_rev[simp]: "distinct (concat (rev xs)) = distinct (concat xs)"
+by (induction xs) auto
+
lemma distinct_concat:
"\<lbrakk> distinct xs;
\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys;
@@ -4285,6 +4288,7 @@
qed
qed
+
subsection \<open>@{const distinct_adj}\<close>
lemma distinct_adj_Nil [simp]: "distinct_adj []"