--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Sat Feb 15 21:15:03 2020 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Feb 16 18:01:03 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>
--- a/src/HOL/Finite_Set.thy Sat Feb 15 21:15:03 2020 +0100
+++ b/src/HOL/Finite_Set.thy Sun Feb 16 18:01:03 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)
--- a/src/HOL/Library/Ramsey.thy Sat Feb 15 21:15:03 2020 +0100
+++ b/src/HOL/Library/Ramsey.thy Sun Feb 16 18:01:03 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)
--- a/src/HOL/Set_Interval.thy Sat Feb 15 21:15:03 2020 +0100
+++ b/src/HOL/Set_Interval.thy Sun Feb 16 18:01:03 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