src/HOL/Library/Cardinality.thy
changeset 69663 41ff40bf1530
parent 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/Cardinality.thy	Mon Jan 14 18:35:03 2019 +0000
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Tue Jan 15 21:31:20 2019 +0100
     1.3 @@ -153,6 +153,19 @@
     1.4  lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)"
     1.5    by (simp add: less_Suc_eq_le [symmetric])
     1.6  
     1.7 +
     1.8 +class CARD_1 =
     1.9 +  assumes CARD_1: "CARD ('a) = 1"
    1.10 +begin
    1.11 +
    1.12 +subclass finite
    1.13 +proof
    1.14 +  from CARD_1 show "finite (UNIV :: 'a set)"
    1.15 +    by (auto intro!: card_ge_0_finite)
    1.16 +qed
    1.17 +
    1.18 +end
    1.19 +
    1.20  text \<open>Class for cardinality "at least 2"\<close>
    1.21  
    1.22  class card2 = finite +