# HG changeset patch
# User nipkow
# Date 1698345702 -7200
# Node ID 98e164c3059f6aef0f2a6f439204ad576b6effd4
# Parent  c62003e05e468f48a995ca1da200e68ecf874532
added lemma

diff -r c62003e05e46 -r 98e164c3059f src/HOL/List.thy
--- 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)