--- a/src/HOL/List.thy Thu Oct 26 17:53:22 2023 +0200
+++ b/src/HOL/List.thy Thu Oct 26 20:41:42 2023 +0200
@@ -5325,6 +5325,14 @@
subsubsection \<open>(In)finiteness\<close>
+lemma finite_list_length: "finite {xs::('a::finite) list. length xs = n}"
+proof(induction n)
+ case (Suc n)
+ have "{xs::'a list. length xs = Suc n} = (\<Union>x. (#) x ` {xs. length xs = n})"
+ by (auto simp: length_Suc_conv)
+ then show ?case using Suc by simp
+qed simp
+
lemma finite_maxlen:
"finite (M::'a list set) \<Longrightarrow> \<exists>n. \<forall>s\<in>M. size s < n"
proof (induct rule: finite.induct)