48028
|
1 |
(* Author: Andreas Lochbihler, KIT *)
|
|
2 |
|
|
3 |
header {* A type class for computing the cardinality of a type's universe *}
|
|
4 |
|
|
5 |
theory Card_Univ imports Main begin
|
|
6 |
|
|
7 |
subsection {* A type class for computing the cardinality of a type's universe *}
|
|
8 |
|
|
9 |
class card_UNIV =
|
|
10 |
fixes card_UNIV :: "'a itself \<Rightarrow> nat"
|
|
11 |
assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
|
|
12 |
begin
|
|
13 |
|
|
14 |
lemma card_UNIV_neq_0_finite_UNIV:
|
|
15 |
"card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
|
|
16 |
by(simp add: card_UNIV card_eq_0_iff)
|
|
17 |
|
|
18 |
lemma card_UNIV_ge_0_finite_UNIV:
|
|
19 |
"card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
|
|
20 |
by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
|
|
21 |
|
|
22 |
lemma card_UNIV_eq_0_infinite_UNIV:
|
|
23 |
"card_UNIV x = 0 \<longleftrightarrow> \<not> finite (UNIV :: 'a set)"
|
|
24 |
by(simp add: card_UNIV card_eq_0_iff)
|
|
25 |
|
|
26 |
definition is_list_UNIV :: "'a list \<Rightarrow> bool"
|
|
27 |
where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
|
|
28 |
|
|
29 |
lemma is_list_UNIV_iff:
|
|
30 |
fixes xs :: "'a list"
|
|
31 |
shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
|
|
32 |
proof
|
|
33 |
assume "is_list_UNIV xs"
|
|
34 |
hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
|
|
35 |
unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
|
|
36 |
from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
|
|
37 |
have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
|
|
38 |
also note set_remdups
|
|
39 |
finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
|
|
40 |
next
|
|
41 |
assume xs: "set xs = UNIV"
|
|
42 |
from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
|
|
43 |
hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
|
|
44 |
moreover have "size (remdups xs) = card (set (remdups xs))"
|
|
45 |
by(subst distinct_card) auto
|
|
46 |
ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
|
|
47 |
qed
|
|
48 |
|
|
49 |
lemma card_UNIV_eq_0_is_list_UNIV_False:
|
|
50 |
assumes cU0: "card_UNIV x = 0"
|
|
51 |
shows "is_list_UNIV = (\<lambda>xs. False)"
|
|
52 |
proof(rule ext)
|
|
53 |
fix xs :: "'a list"
|
|
54 |
from cU0 have "\<not> finite (UNIV :: 'a set)"
|
|
55 |
by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
|
|
56 |
moreover have "finite (set xs)" by(rule finite_set)
|
|
57 |
ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
|
|
58 |
thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
|
|
59 |
qed
|
|
60 |
|
|
61 |
end
|
|
62 |
|
|
63 |
subsection {* Instantiations for @{text "card_UNIV"} *}
|
|
64 |
|
|
65 |
subsubsection {* @{typ "nat"} *}
|
|
66 |
|
|
67 |
instantiation nat :: card_UNIV begin
|
|
68 |
|
|
69 |
definition card_UNIV_nat_def:
|
|
70 |
"card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
|
|
71 |
|
|
72 |
instance proof
|
|
73 |
fix x :: "nat itself"
|
|
74 |
show "card_UNIV x = card (UNIV :: nat set)"
|
|
75 |
unfolding card_UNIV_nat_def by simp
|
|
76 |
qed
|
|
77 |
|
|
78 |
end
|
|
79 |
|
|
80 |
subsubsection {* @{typ "int"} *}
|
|
81 |
|
|
82 |
instantiation int :: card_UNIV begin
|
|
83 |
|
|
84 |
definition card_UNIV_int_def:
|
|
85 |
"card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
|
|
86 |
|
|
87 |
instance proof
|
|
88 |
fix x :: "int itself"
|
|
89 |
show "card_UNIV x = card (UNIV :: int set)"
|
|
90 |
unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int)
|
|
91 |
qed
|
|
92 |
|
|
93 |
end
|
|
94 |
|
|
95 |
subsubsection {* @{typ "'a list"} *}
|
|
96 |
|
|
97 |
instantiation list :: (type) card_UNIV begin
|
|
98 |
|
|
99 |
definition card_UNIV_list_def:
|
|
100 |
"card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
|
|
101 |
|
|
102 |
instance proof
|
|
103 |
fix x :: "'a list itself"
|
|
104 |
show "card_UNIV x = card (UNIV :: 'a list set)"
|
|
105 |
unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
|
|
106 |
qed
|
|
107 |
|
|
108 |
end
|
|
109 |
|
|
110 |
subsubsection {* @{typ "unit"} *}
|
|
111 |
|
|
112 |
lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
|
|
113 |
unfolding UNIV_unit by simp
|
|
114 |
|
|
115 |
instantiation unit :: card_UNIV begin
|
|
116 |
|
|
117 |
definition card_UNIV_unit_def:
|
|
118 |
"card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
|
|
119 |
|
|
120 |
instance proof
|
|
121 |
fix x :: "unit itself"
|
|
122 |
show "card_UNIV x = card (UNIV :: unit set)"
|
|
123 |
by(simp add: card_UNIV_unit_def card_UNIV_unit)
|
|
124 |
qed
|
|
125 |
|
|
126 |
end
|
|
127 |
|
|
128 |
subsubsection {* @{typ "bool"} *}
|
|
129 |
|
|
130 |
lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
|
|
131 |
unfolding UNIV_bool by simp
|
|
132 |
|
|
133 |
instantiation bool :: card_UNIV begin
|
|
134 |
|
|
135 |
definition card_UNIV_bool_def:
|
|
136 |
"card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
|
|
137 |
|
|
138 |
instance proof
|
|
139 |
fix x :: "bool itself"
|
|
140 |
show "card_UNIV x = card (UNIV :: bool set)"
|
|
141 |
by(simp add: card_UNIV_bool_def card_UNIV_bool)
|
|
142 |
qed
|
|
143 |
|
|
144 |
end
|
|
145 |
|
|
146 |
subsubsection {* @{typ "char"} *}
|
|
147 |
|
|
148 |
lemma card_UNIV_char: "card (UNIV :: char set) = 256"
|
|
149 |
proof -
|
|
150 |
from enum_distinct
|
|
151 |
have "card (set (Enum.enum :: char list)) = length (Enum.enum :: char list)"
|
|
152 |
by (rule distinct_card)
|
|
153 |
also have "set Enum.enum = (UNIV :: char set)" by (auto intro: in_enum)
|
|
154 |
also note enum_chars
|
|
155 |
finally show ?thesis by (simp add: chars_def)
|
|
156 |
qed
|
|
157 |
|
|
158 |
instantiation char :: card_UNIV begin
|
|
159 |
|
|
160 |
definition card_UNIV_char_def:
|
|
161 |
"card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
|
|
162 |
|
|
163 |
instance proof
|
|
164 |
fix x :: "char itself"
|
|
165 |
show "card_UNIV x = card (UNIV :: char set)"
|
|
166 |
by(simp add: card_UNIV_char_def card_UNIV_char)
|
|
167 |
qed
|
|
168 |
|
|
169 |
end
|
|
170 |
|
|
171 |
subsubsection {* @{typ "'a \<times> 'b"} *}
|
|
172 |
|
|
173 |
instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
|
|
174 |
|
|
175 |
definition card_UNIV_product_def:
|
|
176 |
"card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
|
|
177 |
|
|
178 |
instance proof
|
|
179 |
fix x :: "('a \<times> 'b) itself"
|
|
180 |
show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
|
|
181 |
by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
|
|
182 |
qed
|
|
183 |
|
|
184 |
end
|
|
185 |
|
|
186 |
subsubsection {* @{typ "'a + 'b"} *}
|
|
187 |
|
|
188 |
instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
|
|
189 |
|
|
190 |
definition card_UNIV_sum_def:
|
|
191 |
"card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
|
|
192 |
in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
|
|
193 |
|
|
194 |
instance proof
|
|
195 |
fix x :: "('a + 'b) itself"
|
|
196 |
show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
|
|
197 |
by (auto simp add: card_UNIV_sum_def card_UNIV card_eq_0_iff UNIV_Plus_UNIV[symmetric] finite_Plus_iff Let_def card_Plus simp del: UNIV_Plus_UNIV dest!: card_ge_0_finite)
|
|
198 |
qed
|
|
199 |
|
|
200 |
end
|
|
201 |
|
|
202 |
subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
|
|
203 |
|
|
204 |
instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
|
|
205 |
|
|
206 |
definition card_UNIV_fun_def:
|
|
207 |
"card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
|
|
208 |
in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
|
|
209 |
|
|
210 |
instance proof
|
|
211 |
fix x :: "('a \<Rightarrow> 'b) itself"
|
|
212 |
|
|
213 |
{ assume "0 < card (UNIV :: 'a set)"
|
|
214 |
and "0 < card (UNIV :: 'b set)"
|
|
215 |
hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
|
|
216 |
by(simp_all only: card_ge_0_finite)
|
|
217 |
from finite_distinct_list[OF finb] obtain bs
|
|
218 |
where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
|
|
219 |
from finite_distinct_list[OF fina] obtain as
|
|
220 |
where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
|
|
221 |
have cb: "card (UNIV :: 'b set) = length bs"
|
|
222 |
unfolding bs[symmetric] distinct_card[OF distb] ..
|
|
223 |
have ca: "card (UNIV :: 'a set) = length as"
|
|
224 |
unfolding as[symmetric] distinct_card[OF dista] ..
|
|
225 |
let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
|
|
226 |
have "UNIV = set ?xs"
|
|
227 |
proof(rule UNIV_eq_I)
|
|
228 |
fix f :: "'a \<Rightarrow> 'b"
|
|
229 |
from as have "f = the \<circ> map_of (zip as (map f as))"
|
|
230 |
by(auto simp add: map_of_zip_map intro: ext)
|
|
231 |
thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
|
|
232 |
qed
|
|
233 |
moreover have "distinct ?xs" unfolding distinct_map
|
|
234 |
proof(intro conjI distinct_n_lists distb inj_onI)
|
|
235 |
fix xs ys :: "'b list"
|
|
236 |
assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
|
|
237 |
and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
|
|
238 |
and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
|
|
239 |
from xs ys have [simp]: "length xs = length as" "length ys = length as"
|
|
240 |
by(simp_all add: length_n_lists_elem)
|
|
241 |
have "map_of (zip as xs) = map_of (zip as ys)"
|
|
242 |
proof
|
|
243 |
fix x
|
|
244 |
from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y"
|
|
245 |
by(simp_all add: map_of_zip_is_Some[symmetric])
|
|
246 |
with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
|
|
247 |
by(auto dest: fun_cong[where x=x])
|
|
248 |
qed
|
|
249 |
with dista show "xs = ys" by(simp add: map_of_zip_inject)
|
|
250 |
qed
|
|
251 |
hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
|
|
252 |
moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
|
|
253 |
ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
|
|
254 |
using cb ca by simp }
|
|
255 |
moreover {
|
|
256 |
assume cb: "card (UNIV :: 'b set) = Suc 0"
|
|
257 |
then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
|
|
258 |
have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
|
|
259 |
proof(rule UNIV_eq_I)
|
|
260 |
fix x :: "'a \<Rightarrow> 'b"
|
|
261 |
{ fix y
|
|
262 |
have "x y \<in> UNIV" ..
|
|
263 |
hence "x y = b" unfolding b by simp }
|
|
264 |
thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
|
|
265 |
qed
|
|
266 |
have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
|
|
267 |
ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
|
|
268 |
unfolding card_UNIV_fun_def card_UNIV Let_def
|
|
269 |
by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
|
|
270 |
qed
|
|
271 |
|
|
272 |
end
|
|
273 |
|
|
274 |
subsubsection {* @{typ "'a option"} *}
|
|
275 |
|
|
276 |
instantiation option :: (card_UNIV) card_UNIV
|
|
277 |
begin
|
|
278 |
|
|
279 |
definition card_UNIV_option_def:
|
|
280 |
"card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
|
|
281 |
in if c \<noteq> 0 then Suc c else 0)"
|
|
282 |
|
|
283 |
instance proof
|
|
284 |
fix x :: "'a option itself"
|
|
285 |
show "card_UNIV x = card (UNIV :: 'a option set)"
|
|
286 |
unfolding UNIV_option_conv
|
|
287 |
by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
|
|
288 |
(subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
|
|
289 |
qed
|
|
290 |
|
|
291 |
end
|
|
292 |
|
|
293 |
end |