added lemma
authornipkow
Thu, 26 Oct 2023 20:41:42 +0200
changeset 78833 98e164c3059f
parent 78832 c62003e05e46
child 78834 35b2282fbc77
added lemma
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)