# HG changeset patch
# User nipkow
# Date 1581883888 -3600
# Node ID efcd6742ea9c908b05ffa4d06ea973b7fe4c7caa
# Parent  404624eb3a22936f25e3e2d59bfe7d989b3316f4# Parent  3cf130a896a393540a445c9f64d9ce02423fbc2c
merged

diff -r 404624eb3a22 -r efcd6742ea9c src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Feb 16 20:07:28 2020 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Feb 16 21:11:28 2020 +0100
@@ -851,9 +851,6 @@
     by simp
 qed
 
-lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y))"
-  by (auto simp: card_Suc_eq eval_nat_numeral)
-
 lemma ksimplex_replace_2:
   assumes s: "ksimplex p n s" and "a \<in> s" and "n \<noteq> 0"
     and lb: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> 0"
@@ -1231,7 +1228,7 @@
       done
   qed
   then show ?thesis
-    using s \<open>a \<in> s\<close> by (simp add: card_2_exists Ex1_def) metis
+    using s \<open>a \<in> s\<close> by (simp add: card_2_iff' Ex1_def) metis
 qed
 
 text \<open>Hence another step towards concreteness.\<close>
diff -r 404624eb3a22 -r efcd6742ea9c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Feb 16 20:07:28 2020 +0100
+++ b/src/HOL/Finite_Set.thy	Sun Feb 16 21:11:28 2020 +0100
@@ -1785,11 +1785,6 @@
   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)
diff -r 404624eb3a22 -r efcd6742ea9c src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Sun Feb 16 20:07:28 2020 +0100
+++ b/src/HOL/Library/Ramsey.thy	Sun Feb 16 21:11:28 2020 +0100
@@ -19,8 +19,7 @@
   by (auto simp: nsets_def)
 
 lemma nsets_2_eq: "nsets A 2 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. {{x, y}})"
-  unfolding numeral_2_eq_2
-  by (auto simp: nsets_def  elim!: card_2_doubletonE)
+by (auto simp: nsets_def card_2_iff)
 
 lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)"
   apply (simp add: binomial_def nsets_def)
diff -r 404624eb3a22 -r efcd6742ea9c src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sun Feb 16 20:07:28 2020 +0100
+++ b/src/HOL/Set_Interval.thy	Sun Feb 16 21:11:28 2020 +0100
@@ -15,6 +15,13 @@
 imports Divides
 begin
 
+(* Belongs in Finite_Set but 2 is not available there *)
+lemma card_2_iff: "card S = 2 \<longleftrightarrow> (\<exists>x y. S = {x,y} \<and> x \<noteq> y)"
+by (auto simp: card_Suc_eq numeral_eq_Suc)
+
+lemma card_2_iff': "card S = 2 \<longleftrightarrow> (\<exists>x\<in>S. \<exists>y\<in>S. x \<noteq> y \<and> (\<forall>z\<in>S. z = x \<or> z = y))"
+by (auto simp: card_Suc_eq numeral_eq_Suc)
+
 context ord
 begin