equal
deleted
inserted
replaced
1927 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert) |
1927 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert) |
1928 |
1928 |
1929 lemma card_insert_le: "finite A ==> card A <= card (insert x A)" |
1929 lemma card_insert_le: "finite A ==> card A <= card (insert x A)" |
1930 by (simp add: card_insert_if) |
1930 by (simp add: card_insert_if) |
1931 |
1931 |
|
1932 lemma card_Collect_less_nat[simp]: "card{i::nat. i < n} = n" |
|
1933 by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq) |
|
1934 |
|
1935 lemma card_Collect_le_nat[simp]: "card{i::nat. i <= n} = n+1" |
|
1936 using card_Collect_less_nat[of "Suc n"] by(simp add: less_Suc_eq_le) |
|
1937 |
1932 lemma card_mono: |
1938 lemma card_mono: |
1933 assumes "finite B" and "A \<subseteq> B" |
1939 assumes "finite B" and "A \<subseteq> B" |
1934 shows "card A \<le> card B" |
1940 shows "card A \<le> card B" |
1935 proof - |
1941 proof - |
1936 from assms have "finite A" by (auto intro: finite_subset) |
1942 from assms have "finite A" by (auto intro: finite_subset) |
2249 apply (simp add: card_image Pow_insert) |
2255 apply (simp add: card_image Pow_insert) |
2250 apply (unfold inj_on_def) |
2256 apply (unfold inj_on_def) |
2251 apply (blast elim!: equalityE) |
2257 apply (blast elim!: equalityE) |
2252 done |
2258 done |
2253 |
2259 |
2254 text {* Relates to equivalence classes. Based on a theorem of F. Kammüller. *} |
2260 text {* Relates to equivalence classes. Based on a theorem of F. Kamm\"uller. *} |
2255 |
2261 |
2256 lemma dvd_partition: |
2262 lemma dvd_partition: |
2257 "finite (Union C) ==> |
2263 "finite (Union C) ==> |
2258 ALL c : C. k dvd card c ==> |
2264 ALL c : C. k dvd card c ==> |
2259 (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==> |
2265 (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==> |