author nipkow Sun, 16 Feb 2020 21:11:28 +0100 changeset 71662 efcd6742ea9c parent 71661 404624eb3a22 (current diff) parent 71659 3cf130a896a3 (diff) child 71663 fb08117a106b child 71669 d6e139438e4a
merged
```--- 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>```
```--- 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)```
```--- 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)"
```--- 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
```