48 by (simp_all add: enum_all expand_fun_eq le_fun_def less_fun_def order_less_le) |
52 by (simp_all add: enum_all expand_fun_eq le_fun_def less_fun_def order_less_le) |
49 |
53 |
50 |
54 |
51 subsection {* Default instances *} |
55 subsection {* Default instances *} |
52 |
56 |
|
57 primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where |
|
58 "n_lists 0 xs = [[]]" |
|
59 | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))" |
|
60 |
|
61 lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])" |
|
62 by (induct n) simp_all |
|
63 |
|
64 lemma length_n_lists: "length (n_lists n xs) = length xs ^ n" |
|
65 by (induct n) (auto simp add: length_concat map_compose [symmetric] o_def listsum_triv) |
|
66 |
|
67 lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n" |
|
68 by (induct n arbitrary: ys) auto |
|
69 |
|
70 lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}" |
|
71 proof (rule set_ext) |
|
72 fix ys :: "'a list" |
|
73 show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}" |
|
74 proof - |
|
75 have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n" |
|
76 by (induct n arbitrary: ys) auto |
|
77 moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs" |
|
78 by (induct n arbitrary: ys) auto |
|
79 moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)" |
|
80 by (induct ys) auto |
|
81 ultimately show ?thesis by auto |
|
82 qed |
|
83 qed |
|
84 |
|
85 lemma distinct_n_lists: |
|
86 assumes "distinct xs" |
|
87 shows "distinct (n_lists n xs)" |
|
88 proof (rule card_distinct) |
|
89 from assms have card_length: "card (set xs) = length xs" by (rule distinct_card) |
|
90 have "card (set (n_lists n xs)) = card (set xs) ^ n" |
|
91 proof (induct n) |
|
92 case 0 then show ?case by simp |
|
93 next |
|
94 case (Suc n) |
|
95 moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs) |
|
96 = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))" |
|
97 by (rule card_UN_disjoint) auto |
|
98 moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)" |
|
99 by (rule card_image) (simp add: inj_on_def) |
|
100 ultimately show ?case by auto |
|
101 qed |
|
102 also have "\<dots> = length xs ^ n" by (simp add: card_length) |
|
103 finally show "card (set (n_lists n xs)) = length (n_lists n xs)" |
|
104 by (simp add: length_n_lists) |
|
105 qed |
|
106 |
|
107 lemma map_of_zip_map: |
|
108 fixes f :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>enum" |
|
109 shows "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)" |
|
110 by (induct xs) (simp_all add: expand_fun_eq) |
|
111 |
|
112 lemma map_of_zip_enum_is_Some: |
|
113 assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)" |
|
114 shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y" |
|
115 proof - |
|
116 from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow> |
|
117 (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)" |
|
118 by (auto intro!: map_of_zip_is_Some) |
|
119 then show ?thesis using enum_all by auto |
|
120 qed |
|
121 |
|
122 lemma map_of_zip_enum_inject: |
|
123 fixes xs ys :: "'b\<Colon>enum list" |
|
124 assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)" |
|
125 "length ys = length (enum \<Colon> 'a\<Colon>enum list)" |
|
126 and map_of: "the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys)" |
|
127 shows "xs = ys" |
|
128 proof - |
|
129 have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)" |
|
130 proof |
|
131 fix x :: 'a |
|
132 from length map_of_zip_enum_is_Some obtain y1 y2 |
|
133 where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1" |
|
134 and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast |
|
135 moreover from map_of have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)" |
|
136 by (auto dest: fun_cong) |
|
137 ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x" |
|
138 by simp |
|
139 qed |
|
140 with length enum_distinct show "xs = ys" by (rule map_of_zip_inject) |
|
141 qed |
|
142 |
|
143 instantiation "fun" :: (enum, enum) enum |
|
144 begin |
|
145 |
|
146 definition |
|
147 [code func del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)" |
|
148 |
|
149 instance proof |
|
150 show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)" |
|
151 proof (rule UNIV_eq_I) |
|
152 fix f :: "'a \<Rightarrow> 'b" |
|
153 have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))" |
|
154 by (auto simp add: map_of_zip_map expand_fun_eq) |
|
155 then show "f \<in> set enum" |
|
156 by (auto simp add: enum_fun_def set_n_lists) |
|
157 qed |
|
158 next |
|
159 from map_of_zip_enum_inject |
|
160 show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)" |
|
161 by (auto intro!: inj_onI simp add: enum_fun_def |
|
162 distinct_map distinct_n_lists enum_distinct set_n_lists enum_all) |
|
163 qed |
|
164 |
|
165 end |
|
166 |
|
167 lemma [code func]: |
|
168 "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>('a\<Colon>{enum, eq}) list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>{enum, eq} list)) enum)" |
|
169 unfolding enum_fun_def .. |
|
170 |
53 instantiation unit :: enum |
171 instantiation unit :: enum |
54 begin |
172 begin |
55 |
173 |
56 definition |
174 definition |
57 "enum = [()]" |
175 "enum = [()]" |
58 |
176 |
59 instance by default |
177 instance by default |
60 (simp add: enum_unit_def UNIV_unit) |
178 (simp_all add: enum_unit_def UNIV_unit) |
61 |
179 |
62 end |
180 end |
63 |
181 |
64 instantiation bool :: enum |
182 instantiation bool :: enum |
65 begin |
183 begin |
66 |
184 |
67 definition |
185 definition |
68 "enum = [False, True]" |
186 "enum = [False, True]" |
69 |
187 |
70 instance by default |
188 instance by default |
71 (simp add: enum_bool_def UNIV_bool) |
189 (simp_all add: enum_bool_def UNIV_bool) |
72 |
190 |
73 end |
191 end |
74 |
192 |
75 primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where |
193 primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where |
76 "product [] _ = []" |
194 "product [] _ = []" |
78 |
196 |
79 lemma product_list_set: |
197 lemma product_list_set: |
80 "set (product xs ys) = set xs \<times> set ys" |
198 "set (product xs ys) = set xs \<times> set ys" |
81 by (induct xs) auto |
199 by (induct xs) auto |
82 |
200 |
|
201 lemma distinct_product: |
|
202 assumes "distinct xs" and "distinct ys" |
|
203 shows "distinct (product xs ys)" |
|
204 using assms by (induct xs) |
|
205 (auto intro: inj_onI simp add: product_list_set distinct_map) |
|
206 |
83 instantiation * :: (enum, enum) enum |
207 instantiation * :: (enum, enum) enum |
84 begin |
208 begin |
85 |
209 |
86 definition |
210 definition |
87 "enum = product enum enum" |
211 "enum = product enum enum" |
88 |
212 |
89 instance by default |
213 instance by default |
90 (simp add: enum_prod_def product_list_set enum_all) |
214 (simp_all add: enum_prod_def product_list_set distinct_product enum_all enum_distinct) |
91 |
215 |
92 end |
216 end |
93 |
217 |
94 instantiation "+" :: (enum, enum) enum |
218 instantiation "+" :: (enum, enum) enum |
95 begin |
219 begin |
96 |
220 |
97 definition |
221 definition |
98 "enum = map Inl enum @ map Inr enum" |
222 "enum = map Inl enum @ map Inr enum" |
99 |
223 |
100 instance by default |
224 instance by default |
101 (auto simp add: enum_all enum_sum_def, case_tac x, auto) |
225 (auto simp add: enum_all enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct) |
102 |
226 |
103 end |
227 end |
104 |
228 |
105 primrec sublists :: "'a list \<Rightarrow> 'a list list" where |
229 primrec sublists :: "'a list \<Rightarrow> 'a list list" where |
106 "sublists [] = [[]]" |
230 "sublists [] = [[]]" |
107 | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" |
231 | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" |
108 |
232 |
|
233 lemma length_sublists: |
|
234 "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs" |
|
235 by (induct xs) (simp_all add: Let_def) |
|
236 |
109 lemma sublists_powset: |
237 lemma sublists_powset: |
110 "set (map set (sublists xs)) = Pow (set xs)" |
238 "set ` set (sublists xs) = Pow (set xs)" |
111 proof - |
239 proof - |
112 have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A" |
240 have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A" |
113 by (auto simp add: image_def) |
241 by (auto simp add: image_def) |
114 show ?thesis |
242 have "set (map set (sublists xs)) = Pow (set xs)" |
115 by (induct xs) |
243 by (induct xs) |
116 (simp_all add: aux Let_def Pow_insert Un_commute) |
244 (simp_all add: aux Let_def Pow_insert Un_commute) |
|
245 then show ?thesis by simp |
|
246 qed |
|
247 |
|
248 lemma distinct_set_sublists: |
|
249 assumes "distinct xs" |
|
250 shows "distinct (map set (sublists xs))" |
|
251 proof (rule card_distinct) |
|
252 have "finite (set xs)" by rule |
|
253 then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow) |
|
254 with assms distinct_card [of xs] |
|
255 have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp |
|
256 then show "card (set (map set (sublists xs))) = length (map set (sublists xs))" |
|
257 by (simp add: sublists_powset length_sublists) |
117 qed |
258 qed |
118 |
259 |
119 instantiation set :: (enum) enum |
260 instantiation set :: (enum) enum |
120 begin |
261 begin |
121 |
262 |
122 definition |
263 definition |
123 "enum = map set (sublists enum)" |
264 "enum = map set (sublists enum)" |
124 |
265 |
125 instance by default |
266 instance by default |
126 (simp add: enum_set_def sublists_powset enum_all del: set_map) |
267 (simp_all add: enum_set_def enum_all sublists_powset distinct_set_sublists enum_distinct) |
127 |
268 |
128 end |
269 end |
129 |
270 |
130 instantiation nibble :: enum |
271 instantiation nibble :: enum |
131 begin |
272 begin |
133 definition |
274 definition |
134 "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7, |
275 "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7, |
135 Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]" |
276 Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]" |
136 |
277 |
137 instance by default |
278 instance by default |
138 (simp add: enum_nibble_def UNIV_nibble) |
279 (simp_all add: enum_nibble_def UNIV_nibble) |
139 |
280 |
140 end |
281 end |
141 |
282 |
142 instantiation char :: enum |
283 instantiation char :: enum |
143 begin |
284 begin |
144 |
285 |
145 definition |
286 definition |
146 "enum = map (split Char) (product enum enum)" |
287 [code func del]: "enum = map (split Char) (product enum enum)" |
147 |
288 |
148 instance by default |
289 lemma enum_char [code func]: |
149 (auto intro: char.exhaust simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]) |
290 "enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2, |
150 |
291 Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5, |
151 end |
292 Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8, |
152 |
293 Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB, |
153 (*instantiation "fun" :: (enum, enum) enum |
294 Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE, |
154 begin |
295 Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1, |
155 |
296 Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4, |
156 |
297 Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7, |
157 definition |
298 Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA, |
158 "enum |
299 Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD, |
159 |
300 Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'', |
160 lemma inj_graph: "inj (%f. {(x, y). y = f x})" |
301 Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'', |
161 by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq) |
302 Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','', |
162 |
303 CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', |
163 instance "fun" :: (finite, finite) finite |
304 CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'', |
164 proof |
305 CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'', |
165 show "finite (UNIV :: ('a => 'b) set)" |
306 CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'', |
166 proof (rule finite_imageD) |
307 CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'', |
167 let ?graph = "%f::'a => 'b. {(x, y). y = f x}" |
308 CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'', |
168 show "finite (range ?graph)" by (rule finite) |
309 CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC, |
169 show "inj ?graph" by (rule inj_graph) |
310 CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'', |
170 qed |
311 CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'', |
171 qed*) |
312 CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'', |
172 |
313 CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'', |
173 end |
314 CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'', |
|
315 Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1, |
|
316 Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4, |
|
317 Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7, |
|
318 Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA, |
|
319 Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD, |
|
320 Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0, |
|
321 Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3, |
|
322 Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6, |
|
323 Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9, |
|
324 Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC, |
|
325 Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF, |
|
326 Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2, |
|
327 Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5, |
|
328 Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8, |
|
329 Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB, |
|
330 Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE, |
|
331 Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1, |
|
332 Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4, |
|
333 Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7, |
|
334 Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA, |
|
335 Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD, |
|
336 Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0, |
|
337 Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3, |
|
338 Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6, |
|
339 Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9, |
|
340 Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC, |
|
341 Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF, |
|
342 Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2, |
|
343 Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5, |
|
344 Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8, |
|
345 Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB, |
|
346 Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE, |
|
347 Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1, |
|
348 Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4, |
|
349 Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7, |
|
350 Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA, |
|
351 Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD, |
|
352 Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0, |
|
353 Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3, |
|
354 Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6, |
|
355 Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9, |
|
356 Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC, |
|
357 Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]" |
|
358 unfolding enum_char_def enum_nibble_def by simp |
|
359 |
|
360 instance by default |
|
361 (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric] |
|
362 distinct_map distinct_product enum_distinct) |
|
363 |
|
364 end |
|
365 |
|
366 end |