18 lemma nsets_mono: "A \<subseteq> B \<Longrightarrow> nsets A n \<subseteq> nsets B n" |
18 lemma nsets_mono: "A \<subseteq> B \<Longrightarrow> nsets A n \<subseteq> nsets B n" |
19 by (auto simp: nsets_def) |
19 by (auto simp: nsets_def) |
20 |
20 |
21 lemma nsets_2_eq: "nsets A 2 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. {{x, y}})" |
21 lemma nsets_2_eq: "nsets A 2 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. {{x, y}})" |
22 by (auto simp: nsets_def card_2_iff) |
22 by (auto simp: nsets_def card_2_iff) |
|
23 |
|
24 lemma nsets_doubleton_2_eq [simp]: "[{x, y}]\<^bsup>2\<^esup> = (if x=y then {} else {{x, y}})" |
|
25 by (auto simp: nsets_2_eq) |
|
26 |
|
27 lemma doubleton_in_nsets_2 [simp]: "{x,y} \<in> [A]\<^bsup>2\<^esup> \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> x \<noteq> y" |
|
28 by (auto simp: nsets_2_eq Set.doubleton_eq_iff) |
23 |
29 |
24 lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)" |
30 lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)" |
25 apply (simp add: binomial_def nsets_def) |
31 apply (simp add: binomial_def nsets_def) |
26 by (meson subset_eq_atLeast0_lessThan_finite) |
32 by (meson subset_eq_atLeast0_lessThan_finite) |
27 |
33 |
39 show "{N. N \<subseteq> A \<and> finite N \<and> card N = r} = {}" |
45 show "{N. N \<subseteq> A \<and> finite N \<and> card N = r} = {}" |
40 if "finite A \<and> card A < r" |
46 if "finite A \<and> card A < r" |
41 using that card_mono leD by auto |
47 using that card_mono leD by auto |
42 qed |
48 qed |
43 |
49 |
44 lemma nsets_eq_empty: "n < r \<Longrightarrow> nsets {..<n} r = {}" |
50 lemma nsets_eq_empty: "\<lbrakk>finite A; card A < r\<rbrakk> \<Longrightarrow> nsets A r = {}" |
45 by (simp add: nsets_eq_empty_iff) |
51 by (simp add: nsets_eq_empty_iff) |
46 |
52 |
47 lemma nsets_empty_iff: "nsets {} r = (if r=0 then {{}} else {})" |
53 lemma nsets_empty_iff: "nsets {} r = (if r=0 then {{}} else {})" |
48 by (auto simp: nsets_def) |
54 by (auto simp: nsets_def) |
49 |
55 |
75 using assms |
81 using assms |
76 apply (auto simp: nsets_def bij_betw_def image_iff card_image inj_on_subset) |
82 apply (auto simp: nsets_def bij_betw_def image_iff card_image inj_on_subset) |
77 by (metis card_image inj_on_finite order_refl subset_image_inj) |
83 by (metis card_image inj_on_finite order_refl subset_image_inj) |
78 with assms show ?thesis |
84 with assms show ?thesis |
79 by (auto simp: bij_betw_def inj_on_nsets) |
85 by (auto simp: bij_betw_def inj_on_nsets) |
|
86 qed |
|
87 |
|
88 lemma nset_image_obtains: |
|
89 assumes "X \<in> [f`A]\<^bsup>k\<^esup>" "inj_on f A" |
|
90 obtains Y where "Y \<in> [A]\<^bsup>k\<^esup>" "X = f ` Y" |
|
91 using assms |
|
92 apply (clarsimp simp add: nsets_def subset_image_iff) |
|
93 by (metis card_image finite_imageD inj_on_subset) |
|
94 |
|
95 lemma nsets_image_funcset: |
|
96 assumes "g \<in> S \<rightarrow> T" and "inj_on g S" |
|
97 shows "(\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> [T]\<^bsup>k\<^esup>" |
|
98 using assms |
|
99 by (fastforce simp add: nsets_def card_image inj_on_subset subset_iff simp flip: image_subset_iff_funcset) |
|
100 |
|
101 lemma nsets_compose_image_funcset: |
|
102 assumes f: "f \<in> [T]\<^bsup>k\<^esup> \<rightarrow> D" and "g \<in> S \<rightarrow> T" and "inj_on g S" |
|
103 shows "f \<circ> (\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> D" |
|
104 proof - |
|
105 have "(\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> [T]\<^bsup>k\<^esup>" |
|
106 using assms by (simp add: nsets_image_funcset) |
|
107 then show ?thesis |
|
108 using f by fastforce |
80 qed |
109 qed |
81 |
110 |
82 subsubsection \<open>Partition predicates\<close> |
111 subsubsection \<open>Partition predicates\<close> |
83 |
112 |
84 definition partn :: "'a set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'b set \<Rightarrow> bool" |
113 definition partn :: "'a set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'b set \<Rightarrow> bool" |