42 by simp |
42 by simp |
43 |
43 |
44 lemma card_bit1 [simp]: "CARD('a bit1) = Suc (2 * CARD('a::finite))" |
44 lemma card_bit1 [simp]: "CARD('a bit1) = Suc (2 * CARD('a::finite))" |
45 unfolding type_definition.card [OF type_definition_bit1] |
45 unfolding type_definition.card [OF type_definition_bit1] |
46 by simp |
46 by simp |
|
47 |
|
48 subsection \<open>@{typ num1}\<close> |
47 |
49 |
48 instance num1 :: finite |
50 instance num1 :: finite |
49 proof |
51 proof |
50 show "finite (UNIV::num1 set)" |
52 show "finite (UNIV::num1 set)" |
51 unfolding type_definition.univ [OF type_definition_num1] |
53 unfolding type_definition.univ [OF type_definition_num1] |
59 proof |
61 proof |
60 show "CARD(num1) = 1" by auto |
62 show "CARD(num1) = 1" by auto |
61 qed |
63 qed |
62 |
64 |
63 end |
65 end |
|
66 |
|
67 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True" |
|
68 by (induct x, induct y) simp |
|
69 |
|
70 instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}" |
|
71 begin |
|
72 |
|
73 instance |
|
74 by standard (simp_all add: num1_eq_iff) |
|
75 |
|
76 end |
|
77 |
|
78 lemma num1_eqI: |
|
79 fixes a::num1 shows "a = b" |
|
80 by(simp add: num1_eq_iff) |
|
81 |
|
82 lemma num1_eq1 [simp]: |
|
83 fixes a::num1 shows "a = 1" |
|
84 by (rule num1_eqI) |
|
85 |
|
86 lemma forall_1[simp]: "(\<forall>i::num1. P i) \<longleftrightarrow> P 1" |
|
87 by (metis (full_types) num1_eq_iff) |
|
88 |
|
89 lemma ex_1[simp]: "(\<exists>x::num1. P x) \<longleftrightarrow> P 1" |
|
90 by auto (metis (full_types) num1_eq_iff) |
|
91 |
|
92 instantiation num1 :: linorder begin |
|
93 definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b" |
|
94 definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b" |
|
95 instance |
|
96 by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI) |
|
97 end |
|
98 |
|
99 instance num1 :: wellorder |
|
100 by intro_classes (auto simp: less_eq_num1_def less_num1_def) |
|
101 |
64 |
102 |
65 instance bit0 :: (finite) card2 |
103 instance bit0 :: (finite) card2 |
66 proof |
104 proof |
67 show "finite (UNIV::'a bit0 set)" |
105 show "finite (UNIV::'a bit0 set)" |
68 unfolding type_definition.univ [OF type_definition_bit0] |
106 unfolding type_definition.univ [OF type_definition_bit0] |
193 text \<open> |
231 text \<open> |
194 Unfortunately \<open>ring_1\<close> instance is not possible for |
232 Unfortunately \<open>ring_1\<close> instance is not possible for |
195 \<^typ>\<open>num1\<close>, since 0 and 1 are not distinct. |
233 \<^typ>\<open>num1\<close>, since 0 and 1 are not distinct. |
196 \<close> |
234 \<close> |
197 |
235 |
198 instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}" |
|
199 begin |
|
200 |
|
201 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True" |
|
202 by (induct x, induct y) simp |
|
203 |
|
204 instance |
|
205 by standard (simp_all add: num1_eq_iff) |
|
206 |
|
207 end |
|
208 |
|
209 instantiation |
236 instantiation |
210 bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}" |
237 bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}" |
211 begin |
238 begin |
212 |
239 |
213 definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where |
240 definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where |
358 definition "enum_class.enum = [1 :: num1]" |
385 definition "enum_class.enum = [1 :: num1]" |
359 definition "enum_class.enum_all P = P (1 :: num1)" |
386 definition "enum_class.enum_all P = P (1 :: num1)" |
360 definition "enum_class.enum_ex P = P (1 :: num1)" |
387 definition "enum_class.enum_ex P = P (1 :: num1)" |
361 instance |
388 instance |
362 by intro_classes |
389 by intro_classes |
363 (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def, |
390 (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def) |
364 (metis (full_types) num1_eq_iff)+) |
|
365 end |
391 end |
366 |
392 |
367 instantiation num0 and num1 :: card_UNIV begin |
393 instantiation num0 and num1 :: card_UNIV begin |
368 definition "finite_UNIV = Phantom(num0) False" |
394 definition "finite_UNIV = Phantom(num0) False" |
369 definition "card_UNIV = Phantom(num0) 0" |
395 definition "card_UNIV = Phantom(num0) 0" |