# 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 \ A \ length xs = n}" (is "finite (?S n)") +proof(induct n) + case 0 show ?case by simp +next + case (Suc n) + have "?S (Suc n) = (\x\A. (\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 \ A \ length xs \ n}" + (is "finite ?S") +proof- + have "?S = (\n\{0..n}. {xs. set xs \ A \ 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)