59 lemma nsets_zero [simp]: "nsets A 0 = {{}}" |
59 lemma nsets_zero [simp]: "nsets A 0 = {{}}" |
60 by (auto simp: nsets_def) |
60 by (auto simp: nsets_def) |
61 |
61 |
62 lemma nsets_one: "nsets A (Suc 0) = (\<lambda>x. {x}) ` A" |
62 lemma nsets_one: "nsets A (Suc 0) = (\<lambda>x. {x}) ` A" |
63 using card_eq_SucD by (force simp: nsets_def) |
63 using card_eq_SucD by (force simp: nsets_def) |
|
64 |
|
65 lemma inj_on_nsets: |
|
66 assumes "inj_on f A" |
|
67 shows "inj_on (\<lambda>X. f ` X) ([A]\<^bsup>n\<^esup>)" |
|
68 using assms unfolding nsets_def |
|
69 by (metis (no_types, lifting) inj_on_inverseI inv_into_image_cancel mem_Collect_eq) |
|
70 |
|
71 lemma bij_betw_nsets: |
|
72 assumes "bij_betw f A B" |
|
73 shows "bij_betw (\<lambda>X. f ` X) ([A]\<^bsup>n\<^esup>) ([B]\<^bsup>n\<^esup>)" |
|
74 proof - |
|
75 have "(`) f ` [A]\<^bsup>n\<^esup> = [f ` A]\<^bsup>n\<^esup>" |
|
76 using assms |
|
77 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) |
|
79 with assms show ?thesis |
|
80 by (auto simp: bij_betw_def inj_on_nsets) |
|
81 qed |
64 |
82 |
65 subsubsection \<open>Partition predicates\<close> |
83 subsubsection \<open>Partition predicates\<close> |
66 |
84 |
67 definition partn :: "'a set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'b set \<Rightarrow> bool" |
85 definition partn :: "'a set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'b set \<Rightarrow> bool" |
68 where "partn \<beta> \<alpha> \<gamma> \<delta> \<equiv> \<forall>f \<in> nsets \<beta> \<gamma> \<rightarrow> \<delta>. \<exists>H \<in> nsets \<beta> \<alpha>. \<exists>\<xi>\<in>\<delta>. f ` (nsets H \<gamma>) \<subseteq> {\<xi>}" |
86 where "partn \<beta> \<alpha> \<gamma> \<delta> \<equiv> \<forall>f \<in> nsets \<beta> \<gamma> \<rightarrow> \<delta>. \<exists>H \<in> nsets \<beta> \<alpha>. \<exists>\<xi>\<in>\<delta>. f ` (nsets H \<gamma>) \<subseteq> {\<xi>}" |