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