503 moreover with Cons.hyps have "P xs" . 
503 moreover with Cons.hyps have "P xs" . 
504 ultimately show ?thesis by (rule cons) 
504 ultimately show ?thesis by (rule cons) 
505 qed 
505 qed 
506 qed 
506 qed 
507 
507 

508 lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X" 

509 by (auto intro!: inj_onI) 
508 
510 
509 subsubsection {* @{const length} *} 
511 subsubsection {* @{const length} *} 
510 
512 
511 text {* 
513 text {* 
512 Needs to come before @{text "@"} because of theorem @{text 
514 Needs to come before @{text "@"} because of theorem @{text 
3707 then obtain n where "\<forall>s\<in>M. length s < n" by blast 
3709 then obtain n where "\<forall>s\<in>M. length s < n" by blast 
3708 hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto 
3710 hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto 
3709 thus ?case .. 
3711 thus ?case .. 
3710 qed 
3712 qed 
3711 
3713 
3712 lemma finite_lists_length_eq: 
3714 lemma lists_length_Suc_eq: 
3713 assumes "finite A" 
3715 "{xs. set xs \<subseteq> A \<and> length xs = Suc n} = 
3714 shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)") 
3716 (\<lambda>(xs, n). n#xs) ` ({xs. set xs \<subseteq> A \<and> length xs = n} \<times> A)" 
3715 proof(induct n) 
3717 by (auto simp: length_Suc_conv) 
3716 case 0 show ?case by simp 
3718 
3717 next 
3719 lemma 
3718 case (Suc n) 
3720 assumes "finite A" 
3719 have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)" 
3721 shows finite_lists_length_eq: "finite {xs. set xs \<subseteq> A \<and> length xs = n}" 
3720 by (auto simp:length_Suc_conv) 
3722 and card_lists_length_eq: "card {xs. set xs \<subseteq> A \<and> length xs = n} = (card A)^n" 
3721 then show ?case using `finite A` 
3723 using `finite A` 
3722 by (auto intro: Suc) (* FIXME metis? *) 
3724 by (induct n) 
3723 qed 
3725 (auto simp: card_image inj_split_Cons lists_length_Suc_eq cong: conj_cong) 
3724 
3726 
3725 lemma finite_lists_length_le: 
3727 lemma finite_lists_length_le: 
3726 assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}" 
3728 assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}" 
3727 (is "finite ?S") 
3729 (is "finite ?S") 
3728 proof 
3730 proof 
3729 have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto 
3731 have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto 
3730 thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`]) 
3732 thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`]) 

3733 qed 

3734 

3735 lemma card_lists_length_le: 

3736 assumes "finite A" shows "card {xs. set xs \<subseteq> A \<and> length xs \<le> n} = (\<Sum>i\<le>n. card A^i)" 

3737 proof  

3738 have "(\<Sum>i\<le>n. card A^i) = card (\<Union>i\<le>n. {xs. set xs \<subseteq> A \<and> length xs = i})" 

3739 using `finite A` 

3740 by (subst card_UN_disjoint) 

3741 (auto simp add: card_lists_length_eq finite_lists_length_eq) 

3742 also have "(\<Union>i\<le>n. {xs. set xs \<subseteq> A \<and> length xs = i}) = {xs. set xs \<subseteq> A \<and> length xs \<le> n}" 

3743 by auto 

3744 finally show ?thesis by simp 
3731 qed 
3745 qed 
3732 
3746 
3733 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)" 
3747 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)" 
3734 apply(rule notI) 
3748 apply(rule notI) 
3735 apply(drule finite_maxlen) 
3749 apply(drule finite_maxlen) 