# HG changeset patch
# User noschinl
# Date 1324302068 -3600
# Node ID 6f08f8fe9752a4aee279743d1707679af681bab5
# Parent  99cf6e4708164887986746153517e48b2a95dc03
add lemmas

diff -r 99cf6e470816 -r 6f08f8fe9752 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Dec 19 14:41:08 2011 +0100
+++ b/src/HOL/List.thy	Mon Dec 19 14:41:08 2011 +0100
@@ -3807,6 +3807,39 @@
   finally show ?thesis by simp
 qed
 
+lemma card_lists_distinct_length_eq:
+  assumes "k < card A"
+  shows "card {xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A} = \<Prod>{card A - k + 1 .. card A}"
+using assms
+proof (induct k)
+  case 0
+  then have "{xs. length xs = 0 \<and> distinct xs \<and> set xs \<subseteq> A} = {[]}" by auto
+  then show ?case by simp
+next
+  case (Suc k)
+  let "?k_list" = "\<lambda>k xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A"
+  have inj_Cons: "\<And>A. inj_on (\<lambda>(xs, n). n # xs) A"  by (rule inj_onI) auto
+
+  from Suc have "k < card A" by simp
+  moreover have "finite A" using assms by (simp add: card_ge_0_finite)
+  moreover have "finite {xs. ?k_list k xs}"
+    using finite_lists_length_eq[OF `finite A`, of k]
+    by - (rule finite_subset, auto)
+  moreover have "\<And>i j. i \<noteq> j \<longrightarrow> {i} \<times> (A - set i) \<inter> {j} \<times> (A - set j) = {}"
+    by auto
+  moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
+    by (simp add: card_Diff_subset distinct_card)
+  moreover have "{xs. ?k_list (Suc k) xs} =
+      (\<lambda>(xs, n). n#xs) ` \<Union>(\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs}"
+    by (auto simp: length_Suc_conv)
+  moreover
+  have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
+  then have "(card A - k) * \<Prod>{Suc (card A - k)..card A} = \<Prod>{Suc (card A - Suc k)..card A}"
+    by (subst setprod_insert[symmetric]) (simp add: atLeastAtMost_insertL)+
+  ultimately show ?case
+    by (simp add: card_image inj_Cons card_UN_disjoint Suc.hyps algebra_simps)
+qed
+
 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
 apply(rule notI)
 apply(drule finite_maxlen)
diff -r 99cf6e470816 -r 6f08f8fe9752 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Dec 19 14:41:08 2011 +0100
+++ b/src/HOL/SetInterval.thy	Mon Dec 19 14:41:08 2011 +0100
@@ -477,6 +477,9 @@
 lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
 by (auto simp add: atLeastAtMost_def)
 
+lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}"
+by auto
+
 text {* The analogous result is useful on @{typ int}: *}
 (* here, because we don't have an own int section *)
 lemma atLeastAtMostPlus1_int_conv: