# HG changeset patch
# User bulwahn
# Date 1244760328 -7200
# Node ID 86eeb9b7a4ba604c555708dd7e986b7023b983f9
# Parent  ce3721fa1e17458feedac3ec44268e3fc7560737# Parent  4e36f2f17c636479f821dc772d3ced5dbdf465f5
merged

diff -r ce3721fa1e17 -r 86eeb9b7a4ba src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 11 23:13:02 2009 +0200
+++ b/src/HOL/List.thy	Fri Jun 12 00:45: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)