equal
deleted
inserted
replaced
151 unfolding neq0_conv [symmetric] by simp |
151 unfolding neq0_conv [symmetric] by simp |
152 |
152 |
153 lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)" |
153 lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)" |
154 by (simp add: less_Suc_eq_le [symmetric]) |
154 by (simp add: less_Suc_eq_le [symmetric]) |
155 |
155 |
|
156 |
|
157 class CARD_1 = |
|
158 assumes CARD_1: "CARD ('a) = 1" |
|
159 begin |
|
160 |
|
161 subclass finite |
|
162 proof |
|
163 from CARD_1 show "finite (UNIV :: 'a set)" |
|
164 by (auto intro!: card_ge_0_finite) |
|
165 qed |
|
166 |
|
167 end |
|
168 |
156 text \<open>Class for cardinality "at least 2"\<close> |
169 text \<open>Class for cardinality "at least 2"\<close> |
157 |
170 |
158 class card2 = finite + |
171 class card2 = finite + |
159 assumes two_le_card: "2 \<le> CARD('a)" |
172 assumes two_le_card: "2 \<le> CARD('a)" |
160 |
173 |