# HG changeset patch
# User nipkow
# Date 1747936783 -7200
# Node ID c833618d80eb167d25a0ef1caeec7b76c4435ee2
# Parent  8a02dd7fcb5d03668dd2cc8719dafb9baa34689a
added lemmas

diff -r 8a02dd7fcb5d -r c833618d80eb src/HOL/Groups_List.thy
--- 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)
diff -r 8a02dd7fcb5d -r c833618d80eb src/HOL/List.thy
--- 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 []"