# HG changeset patch
# User nipkow
# Date 1736311093 -3600
# Node ID 2f70c60cdbb2c20f3bdca6099a0cfd4dc6ce2765
# Parent  fac2045e61d576f2dce41716c9dbdf9b7d626e5a# Parent  9714d5b221e2d5017625269b1624a16dde0ec141
merged

diff -r fac2045e61d5 -r 2f70c60cdbb2 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jan 07 22:07:46 2025 +0100
+++ b/src/HOL/List.thy	Wed Jan 08 05:38:13 2025 +0100
@@ -4416,6 +4416,43 @@
     by (auto simp: sum.If_cases simp flip: diff_eq)
 qed simp
 
+lemma count_list_Suc_split_first:
+  assumes "count_list xs x = Suc n"
+  shows "\<exists> pref rest. xs = pref @ x # rest \<and> x \<notin> set pref \<and> count_list rest x = n"
+proof -
+  let ?pref = "takeWhile (\<lambda>u. u \<noteq> x) xs"
+  let ?rest = "drop (length ?pref) xs"
+  have "x \<in> set xs" using assms count_notin by fastforce
+  hence rest: "?rest \<noteq> [] \<and> hd ?rest = x"
+    by (metis (mono_tags, lifting) append_Nil2 dropWhile_eq_drop hd_dropWhile
+        takeWhile_dropWhile_id takeWhile_eq_all_conv)
+  have 1: "x \<notin> set ?pref" by (metis (full_types) set_takeWhileD)
+  have 2: "xs = ?pref @ x # tl ?rest"
+    by (metis rest append_eq_conv_conj hd_Cons_tl takeWhile_eq_take)
+  have "count_list (tl ?rest) x = n"using [[metis_suggest_of]]
+    using assms rest 1 2 count_notin count_list_append[of ?pref "x # tl ?rest" x] by simp
+  with 1 2 show ?thesis by blast
+qed
+
+lemma split_list_cycles:
+  "\<exists>pref xss. xs = pref @ concat xss \<and> x \<notin> set pref \<and> (\<forall>ys \<in> set xss. \<exists>zs. ys = x # zs)"
+proof (induction "count_list xs x" arbitrary: xs)
+  case 0
+  show ?case using 0[symmetric] concat.simps(1) count_list_0_iff by fastforce
+next
+  case (Suc n)
+  from Suc.hyps(2) obtain pref rest where
+    *: "xs = pref @ x # rest" "x \<notin> set pref" "count_list rest x = n"
+    by (metis count_list_Suc_split_first)
+  from Suc.hyps(1)[OF *(3)[symmetric]] obtain pref1 xss where
+    **: "rest = pref1 @ concat xss" "x \<notin> set pref1" "\<forall>ys\<in>set xss. \<exists>zs. ys = x # zs"
+    by blast
+  let ?xss = "(x # pref1) # xss"
+  have "xs = pref @ concat ?xss \<and> x \<notin> set pref \<and> (\<forall>ys \<in> set ?xss. \<exists>zs. ys = x # zs)"
+    using *(1,2) ** by auto
+  thus ?case by blast
+qed
+
 
 subsubsection \<open>\<^const>\<open>List.extract\<close>\<close>