author nipkow Wed, 16 Jan 2019 05:26:46 +0100 changeset 69664 839ebe61786f parent 69662 fd86ed39aea4 (current diff) parent 69663 41ff40bf1530 (diff) child 69665 60110f6d0b4e
merged
```--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Tue Jan 15 20:03:53 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 05:26:46 2019 +0100
@@ -873,16 +873,6 @@
fixes a::num1 shows "a = 1"
by (rule num1_eqI)

-instantiation num1 :: cart_one
-begin
-
-instance
-proof
-  show "CARD(1) = Suc 0" by auto
-qed
-
-end
-
instantiation num1 :: linorder begin
definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b"
definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b"```
```--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Tue Jan 15 20:03:53 2019 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Jan 16 05:26:46 2019 +0100
@@ -259,32 +259,20 @@

text\<open>The ordering on one-dimensional vectors is linear.\<close>

-class cart_one =
-  assumes UNIV_one: "card (UNIV :: 'a set) = Suc 0"
-begin
-
-subclass finite
-proof
-  from UNIV_one show "finite (UNIV :: 'a set)"
-    by (auto intro!: card_ge_0_finite)
-qed
-
-end
-
instance vec:: (order, finite) order
by standard (auto simp: less_eq_vec_def less_vec_def vec_eq_iff
intro: order.trans order.antisym order.strict_implies_order)

-instance vec :: (linorder, cart_one) linorder
+instance vec :: (linorder, CARD_1) linorder
proof
obtain a :: 'b where all: "\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a"
proof -
-    have "card (UNIV :: 'b set) = Suc 0" by (rule UNIV_one)
+    have "CARD ('b) = 1" by (rule CARD_1)
then obtain b :: 'b where "UNIV = {b}" by (auto iff: card_Suc_eq)
then have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P b" by auto
then show thesis by (auto intro: that)
qed
-  fix x y :: "'a^'b::cart_one"
+  fix x y :: "'a^'b::CARD_1"
note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps
show "x \<le> y \<or> y \<le> x" by auto
qed```
```--- a/src/HOL/Library/Cardinality.thy	Tue Jan 15 20:03:53 2019 +0100
+++ b/src/HOL/Library/Cardinality.thy	Wed Jan 16 05:26:46 2019 +0100
@@ -153,6 +153,19 @@
lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)"

+
+class CARD_1 =
+  assumes CARD_1: "CARD ('a) = 1"
+begin
+
+subclass finite
+proof
+  from CARD_1 show "finite (UNIV :: 'a set)"
+    by (auto intro!: card_ge_0_finite)
+qed
+
+end
+
text \<open>Class for cardinality "at least 2"\<close>

class card2 = finite + ```
```--- a/src/HOL/Library/Numeral_Type.thy	Tue Jan 15 20:03:53 2019 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Jan 16 05:26:46 2019 +0100
@@ -52,6 +52,16 @@
using finite by (rule finite_imageI)
qed

+instantiation num1 :: CARD_1
+begin
+
+instance
+proof
+  show "CARD(num1) = 1" by auto
+qed
+
+end
+
instance bit0 :: (finite) card2
proof
show "finite (UNIV::'a bit0 set)"```