--- a/src/HOL/Finite_Set.thy Mon Dec 09 11:17:34 2019 +0100
+++ b/src/HOL/Finite_Set.thy Mon Dec 09 15:36:51 2019 +0000
@@ -319,7 +319,7 @@
next
case insert
then show ?case
- by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast
+ by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast
qed
lemma all_subset_image: "(\<forall>B. B \<subseteq> f ` A \<longrightarrow> P B) \<longleftrightarrow> (\<forall>B. B \<subseteq> A \<longrightarrow> P(f ` B))"
@@ -1785,10 +1785,18 @@
obtains x where "A = {x}"
using assms by (auto simp: card_Suc_eq)
+lemma card_2_doubletonE:
+ assumes "card A = Suc (Suc 0)"
+ obtains x y where "A = {x,y}" "x\<noteq>y"
+ using assms by (blast dest: card_eq_SucD)
+
lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1"
unfolding is_singleton_def
by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)
+lemma card_1_singleton_iff: "card A = Suc 0 \<longleftrightarrow> (\<exists>x. A = {x})"
+ by (simp add: card_Suc_eq)
+
lemma card_le_Suc0_iff_eq:
assumes "finite A"
shows "card A \<le> Suc 0 \<longleftrightarrow> (\<forall>a1 \<in> A. \<forall>a2 \<in> A. a1 = a2)" (is "?C = ?A")