src/HOL/List.thy
changeset 45714 ad4242285560
parent 45607 16b4f5774621
child 45789 36ea69266e61
     1.1 --- a/src/HOL/List.thy	Thu Dec 01 15:41:48 2011 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Dec 01 15:41:58 2011 +0100
     1.3 @@ -505,6 +505,8 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
     1.8 +  by (auto intro!: inj_onI)
     1.9  
    1.10  subsubsection {* @{const length} *}
    1.11  
    1.12 @@ -3709,18 +3711,18 @@
    1.13    thus ?case ..
    1.14  qed
    1.15  
    1.16 -lemma finite_lists_length_eq:
    1.17 -assumes "finite A"
    1.18 -shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")
    1.19 -proof(induct n)
    1.20 -  case 0 show ?case by simp
    1.21 -next
    1.22 -  case (Suc n)
    1.23 -  have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
    1.24 -    by (auto simp:length_Suc_conv)
    1.25 -  then show ?case using `finite A`
    1.26 -    by (auto intro: Suc) (* FIXME metis? *)
    1.27 -qed
    1.28 +lemma lists_length_Suc_eq:
    1.29 +  "{xs. set xs \<subseteq> A \<and> length xs = Suc n} =
    1.30 +    (\<lambda>(xs, n). n#xs) ` ({xs. set xs \<subseteq> A \<and> length xs = n} \<times> A)"
    1.31 +  by (auto simp: length_Suc_conv)
    1.32 +
    1.33 +lemma
    1.34 +  assumes "finite A"
    1.35 +  shows finite_lists_length_eq: "finite {xs. set xs \<subseteq> A \<and> length xs = n}"
    1.36 +  and card_lists_length_eq: "card {xs. set xs \<subseteq> A \<and> length xs = n} = (card A)^n"
    1.37 +  using `finite A`
    1.38 +  by (induct n)
    1.39 +     (auto simp: card_image inj_split_Cons lists_length_Suc_eq cong: conj_cong)
    1.40  
    1.41  lemma finite_lists_length_le:
    1.42    assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
    1.43 @@ -3730,6 +3732,18 @@
    1.44    thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
    1.45  qed
    1.46  
    1.47 +lemma card_lists_length_le:
    1.48 +  assumes "finite A" shows "card {xs. set xs \<subseteq> A \<and> length xs \<le> n} = (\<Sum>i\<le>n. card A^i)"
    1.49 +proof -
    1.50 +  have "(\<Sum>i\<le>n. card A^i) = card (\<Union>i\<le>n. {xs. set xs \<subseteq> A \<and> length xs = i})"
    1.51 +    using `finite A`
    1.52 +    by (subst card_UN_disjoint)
    1.53 +       (auto simp add: card_lists_length_eq finite_lists_length_eq)
    1.54 +  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}"
    1.55 +    by auto
    1.56 +  finally show ?thesis by simp
    1.57 +qed
    1.58 +
    1.59  lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
    1.60  apply(rule notI)
    1.61  apply(drule finite_maxlen)