add lemmas
authornoschinl
Mon Dec 19 14:41:08 2011 +0100 (2011-12-19)
changeset 459326f08f8fe9752
parent 45931 99cf6e470816
child 45933 ee70da42e08a
add lemmas
src/HOL/List.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/List.thy	Mon Dec 19 14:41:08 2011 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Dec 19 14:41:08 2011 +0100
     1.3 @@ -3807,6 +3807,39 @@
     1.4    finally show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +lemma card_lists_distinct_length_eq:
     1.8 +  assumes "k < card A"
     1.9 +  shows "card {xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A} = \<Prod>{card A - k + 1 .. card A}"
    1.10 +using assms
    1.11 +proof (induct k)
    1.12 +  case 0
    1.13 +  then have "{xs. length xs = 0 \<and> distinct xs \<and> set xs \<subseteq> A} = {[]}" by auto
    1.14 +  then show ?case by simp
    1.15 +next
    1.16 +  case (Suc k)
    1.17 +  let "?k_list" = "\<lambda>k xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A"
    1.18 +  have inj_Cons: "\<And>A. inj_on (\<lambda>(xs, n). n # xs) A"  by (rule inj_onI) auto
    1.19 +
    1.20 +  from Suc have "k < card A" by simp
    1.21 +  moreover have "finite A" using assms by (simp add: card_ge_0_finite)
    1.22 +  moreover have "finite {xs. ?k_list k xs}"
    1.23 +    using finite_lists_length_eq[OF `finite A`, of k]
    1.24 +    by - (rule finite_subset, auto)
    1.25 +  moreover have "\<And>i j. i \<noteq> j \<longrightarrow> {i} \<times> (A - set i) \<inter> {j} \<times> (A - set j) = {}"
    1.26 +    by auto
    1.27 +  moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
    1.28 +    by (simp add: card_Diff_subset distinct_card)
    1.29 +  moreover have "{xs. ?k_list (Suc k) xs} =
    1.30 +      (\<lambda>(xs, n). n#xs) ` \<Union>(\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs}"
    1.31 +    by (auto simp: length_Suc_conv)
    1.32 +  moreover
    1.33 +  have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
    1.34 +  then have "(card A - k) * \<Prod>{Suc (card A - k)..card A} = \<Prod>{Suc (card A - Suc k)..card A}"
    1.35 +    by (subst setprod_insert[symmetric]) (simp add: atLeastAtMost_insertL)+
    1.36 +  ultimately show ?case
    1.37 +    by (simp add: card_image inj_Cons card_UN_disjoint Suc.hyps algebra_simps)
    1.38 +qed
    1.39 +
    1.40  lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
    1.41  apply(rule notI)
    1.42  apply(drule finite_maxlen)
     2.1 --- a/src/HOL/SetInterval.thy	Mon Dec 19 14:41:08 2011 +0100
     2.2 +++ b/src/HOL/SetInterval.thy	Mon Dec 19 14:41:08 2011 +0100
     2.3 @@ -477,6 +477,9 @@
     2.4  lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
     2.5  by (auto simp add: atLeastAtMost_def)
     2.6  
     2.7 +lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}"
     2.8 +by auto
     2.9 +
    2.10  text {* The analogous result is useful on @{typ int}: *}
    2.11  (* here, because we don't have an own int section *)
    2.12  lemma atLeastAtMostPlus1_int_conv: