# HG changeset patch
# User nipkow
# Date 1244755468 -7200
# Node ID 4e36f2f17c636479f821dc772d3ced5dbdf465f5
# Parent  ac0badf13d934c29b17766681f3851afd8b0963d
two finiteness lemmas by Robert Himmelmann

diff -r ac0badf13d93 -r 4e36f2f17c63 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 11 14:25:58 2009 +0200
+++ b/src/HOL/List.thy	Thu Jun 11 23:24:28 2009 +0200
@@ -2931,7 +2931,7 @@
 done
 
 
-subsubsection {* Infiniteness *}
+subsubsection {* (In)finiteness *}
 
 lemma finite_maxlen:
   "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
@@ -2944,6 +2944,27 @@
   thus ?case ..
 qed
 
+lemma finite_lists_length_eq:
+assumes "finite A"
+shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")
+proof(induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
+    by (auto simp:length_Suc_conv)
+  then show ?case using `finite A`
+    by (auto intro: finite_imageI Suc) (* FIXME metis? *)
+qed
+
+lemma finite_lists_length_le:
+  assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
+ (is "finite ?S")
+proof-
+  have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
+  thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
+qed
+
 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
 apply(rule notI)
 apply(drule finite_maxlen)