equal
deleted
inserted
replaced
1857 lemma card_Diff_singleton: |
1857 lemma card_Diff_singleton: |
1858 "finite A ==> x: A ==> card (A - {x}) = card A - 1" |
1858 "finite A ==> x: A ==> card (A - {x}) = card A - 1" |
1859 by (simp add: card_Suc_Diff1 [symmetric]) |
1859 by (simp add: card_Suc_Diff1 [symmetric]) |
1860 |
1860 |
1861 lemma card_Diff_singleton_if: |
1861 lemma card_Diff_singleton_if: |
1862 "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)" |
1862 "finite A ==> card (A - {x}) = (if x : A then card A - 1 else card A)" |
1863 by (simp add: card_Diff_singleton) |
1863 by (simp add: card_Diff_singleton) |
1864 |
1864 |
1865 lemma card_Diff_insert[simp]: |
1865 lemma card_Diff_insert[simp]: |
1866 assumes "finite A" and "a:A" and "a ~: B" |
1866 assumes "finite A" and "a:A" and "a ~: B" |
1867 shows "card(A - insert a B) = card(A - B) - 1" |
1867 shows "card(A - insert a B) = card(A - B) - 1" |