24 lemma nsets_doubleton_2_eq [simp]: "[{x, y}]\<^bsup>2\<^esup> = (if x=y then {} else {{x, y}})" |
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) |
25 by (auto simp: nsets_2_eq) |
26 |
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" |
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) |
28 by (auto simp: nsets_2_eq Set.doubleton_eq_iff) |
|
29 |
|
30 lemma nsets_3_eq: "nsets A 3 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. \<Union>z\<in>A - {x,y}. {{x,y,z}})" |
|
31 by (simp add: eval_nat_numeral nsets_def card_Suc_eq) blast |
|
32 |
|
33 lemma nsets_4_eq: "[A]\<^bsup>4\<^esup> = (\<Union>u\<in>A. \<Union>x\<in>A - {u}. \<Union>y\<in>A - {u,x}. \<Union>z\<in>A - {u,x,y}. {{u,x,y,z}})" |
|
34 (is "_ = ?rhs") |
|
35 proof |
|
36 show "[A]\<^bsup>4\<^esup> \<subseteq> ?rhs" |
|
37 by (clarsimp simp add: nsets_def eval_nat_numeral card_Suc_eq) blast |
|
38 show "?rhs \<subseteq> [A]\<^bsup>4\<^esup>" |
|
39 apply (clarsimp simp add: nsets_def eval_nat_numeral card_Suc_eq) |
|
40 by (metis insert_iff singletonD) |
|
41 qed |
|
42 |
|
43 lemma nsets_disjoint_2: |
|
44 "X \<inter> Y = {} \<Longrightarrow> [X \<union> Y]\<^bsup>2\<^esup> = [X]\<^bsup>2\<^esup> \<union> [Y]\<^bsup>2\<^esup> \<union> (\<Union>x\<in>X. \<Union>y\<in>Y. {{x,y}})" |
|
45 by (fastforce simp: nsets_2_eq Set.doubleton_eq_iff) |
|
46 |
|
47 lemma ordered_nsets_2_eq: |
|
48 fixes A :: "'a::linorder set" |
|
49 shows "nsets A 2 = {{x,y} | x y. x \<in> A \<and> y \<in> A \<and> x<y}" |
|
50 (is "_ = ?rhs") |
|
51 proof |
|
52 show "nsets A 2 \<subseteq> ?rhs" |
|
53 unfolding numeral_nat |
|
54 apply (clarsimp simp add: nsets_def card_Suc_eq Set.doubleton_eq_iff not_less) |
|
55 by (metis antisym) |
|
56 show "?rhs \<subseteq> nsets A 2" |
|
57 unfolding numeral_nat by (auto simp: nsets_def card_Suc_eq) |
|
58 qed |
|
59 |
|
60 lemma ordered_nsets_3_eq: |
|
61 fixes A :: "'a::linorder set" |
|
62 shows "nsets A 3 = {{x,y,z} | x y z. x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> x<y \<and> y<z}" |
|
63 (is "_ = ?rhs") |
|
64 proof |
|
65 show "nsets A 3 \<subseteq> ?rhs" |
|
66 apply (clarsimp simp add: nsets_def card_Suc_eq eval_nat_numeral) |
|
67 by (metis insert_commute linorder_cases) |
|
68 show "?rhs \<subseteq> nsets A 3" |
|
69 apply (clarsimp simp add: nsets_def card_Suc_eq eval_nat_numeral) |
|
70 by (metis empty_iff insert_iff not_less_iff_gr_or_eq) |
|
71 qed |
|
72 |
|
73 lemma ordered_nsets_4_eq: |
|
74 fixes A :: "'a::linorder set" |
|
75 shows "[A]\<^bsup>4\<^esup> = {U. \<exists>u x y z. U = {u,x,y,z} \<and> u \<in> A \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> u < x \<and> x < y \<and> y < z}" |
|
76 (is "_ = Collect ?RHS") |
|
77 proof - |
|
78 { fix U |
|
79 assume "U \<in> [A]\<^bsup>4\<^esup>" |
|
80 then obtain l where "strict_sorted l" "List.set l = U" "length l = 4" "U \<subseteq> A" |
|
81 by (simp add: nsets_def) (metis finite_set_strict_sorted) |
|
82 then have "?RHS U" |
|
83 unfolding numeral_nat length_Suc_conv by auto blast } |
|
84 moreover |
|
85 have "Collect ?RHS \<subseteq> [A]\<^bsup>4\<^esup>" |
|
86 apply (clarsimp simp add: nsets_def eval_nat_numeral) |
|
87 apply (subst card_insert_disjoint, auto)+ |
|
88 done |
|
89 ultimately show ?thesis |
|
90 by auto |
|
91 qed |
|
92 |
|
93 lemma ordered_nsets_5_eq: |
|
94 fixes A :: "'a::linorder set" |
|
95 shows "[A]\<^bsup>5\<^esup> = {U. \<exists>u v x y z. U = {u,v,x,y,z} \<and> u \<in> A \<and> v \<in> A \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> u < v \<and> v < x \<and> x < y \<and> y < z}" |
|
96 (is "_ = Collect ?RHS") |
|
97 proof - |
|
98 { fix U |
|
99 assume "U \<in> [A]\<^bsup>5\<^esup>" |
|
100 then obtain l where "strict_sorted l" "List.set l = U" "length l = 5" "U \<subseteq> A" |
|
101 apply (simp add: nsets_def) |
|
102 by (metis finite_set_strict_sorted) |
|
103 then have "?RHS U" |
|
104 unfolding numeral_nat length_Suc_conv by auto blast } |
|
105 moreover |
|
106 have "Collect ?RHS \<subseteq> [A]\<^bsup>5\<^esup>" |
|
107 apply (clarsimp simp add: nsets_def eval_nat_numeral) |
|
108 apply (subst card_insert_disjoint, auto)+ |
|
109 done |
|
110 ultimately show ?thesis |
|
111 by auto |
|
112 qed |
29 |
113 |
30 lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)" |
114 lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)" |
31 apply (simp add: binomial_def nsets_def) |
115 apply (simp add: binomial_def nsets_def) |
32 by (meson subset_eq_atLeast0_lessThan_finite) |
116 by (meson subset_eq_atLeast0_lessThan_finite) |
33 |
117 |