70 |
69 |
71 section "length"; |
70 section "length"; |
72 |
71 |
73 Goal "length(xs@ys) = length(xs)+length(ys)"; |
72 Goal "length(xs@ys) = length(xs)+length(ys)"; |
74 by (induct_tac "xs" 1); |
73 by (induct_tac "xs" 1); |
75 by (ALLGOALS Asm_simp_tac); |
74 by (Auto_tac); |
76 qed"length_append"; |
75 qed"length_append"; |
77 Addsimps [length_append]; |
76 Addsimps [length_append]; |
78 |
77 |
79 Goal "length (map f l) = length l"; |
78 Goal "length (map f xs) = length xs"; |
80 by (induct_tac "l" 1); |
79 by (induct_tac "xs" 1); |
81 by (ALLGOALS Simp_tac); |
80 by (Auto_tac); |
82 qed "length_map"; |
81 qed "length_map"; |
83 Addsimps [length_map]; |
82 Addsimps [length_map]; |
84 |
83 |
85 Goal "length(rev xs) = length(xs)"; |
84 Goal "length(rev xs) = length(xs)"; |
86 by (induct_tac "xs" 1); |
85 by (induct_tac "xs" 1); |
87 by (ALLGOALS Asm_simp_tac); |
86 by (Auto_tac); |
88 qed "length_rev"; |
87 qed "length_rev"; |
89 Addsimps [length_rev]; |
88 Addsimps [length_rev]; |
90 |
89 |
91 Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1"; |
90 Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1"; |
92 by (exhaust_tac "xs" 1); |
91 by (exhaust_tac "xs" 1); |
93 by (ALLGOALS Asm_full_simp_tac); |
92 by (Auto_tac); |
94 qed "length_tl"; |
93 qed "length_tl"; |
95 Addsimps [length_tl]; |
94 Addsimps [length_tl]; |
96 |
95 |
97 Goal "(length xs = 0) = (xs = [])"; |
96 Goal "(length xs = 0) = (xs = [])"; |
98 by (induct_tac "xs" 1); |
97 by (induct_tac "xs" 1); |
99 by (ALLGOALS Asm_simp_tac); |
98 by (Auto_tac); |
100 qed "length_0_conv"; |
99 qed "length_0_conv"; |
101 AddIffs [length_0_conv]; |
100 AddIffs [length_0_conv]; |
102 |
101 |
103 Goal "(0 = length xs) = (xs = [])"; |
102 Goal "(0 = length xs) = (xs = [])"; |
104 by (induct_tac "xs" 1); |
103 by (induct_tac "xs" 1); |
105 by (ALLGOALS Asm_simp_tac); |
104 by (Auto_tac); |
106 qed "zero_length_conv"; |
105 qed "zero_length_conv"; |
107 AddIffs [zero_length_conv]; |
106 AddIffs [zero_length_conv]; |
108 |
107 |
109 Goal "(0 < length xs) = (xs ~= [])"; |
108 Goal "(0 < length xs) = (xs ~= [])"; |
110 by (induct_tac "xs" 1); |
109 by (induct_tac "xs" 1); |
111 by (ALLGOALS Asm_simp_tac); |
110 by (Auto_tac); |
112 qed "length_greater_0_conv"; |
111 qed "length_greater_0_conv"; |
113 AddIffs [length_greater_0_conv]; |
112 AddIffs [length_greater_0_conv]; |
114 |
113 |
115 (** @ - append **) |
114 (** @ - append **) |
116 |
115 |
117 section "@ - append"; |
116 section "@ - append"; |
118 |
117 |
119 Goal "(xs@ys)@zs = xs@(ys@zs)"; |
118 Goal "(xs@ys)@zs = xs@(ys@zs)"; |
120 by (induct_tac "xs" 1); |
119 by (induct_tac "xs" 1); |
121 by (ALLGOALS Asm_simp_tac); |
120 by (Auto_tac); |
122 qed "append_assoc"; |
121 qed "append_assoc"; |
123 Addsimps [append_assoc]; |
122 Addsimps [append_assoc]; |
124 |
123 |
125 Goal "xs @ [] = xs"; |
124 Goal "xs @ [] = xs"; |
126 by (induct_tac "xs" 1); |
125 by (induct_tac "xs" 1); |
127 by (ALLGOALS Asm_simp_tac); |
126 by (Auto_tac); |
128 qed "append_Nil2"; |
127 qed "append_Nil2"; |
129 Addsimps [append_Nil2]; |
128 Addsimps [append_Nil2]; |
130 |
129 |
131 Goal "(xs@ys = []) = (xs=[] & ys=[])"; |
130 Goal "(xs@ys = []) = (xs=[] & ys=[])"; |
132 by (induct_tac "xs" 1); |
131 by (induct_tac "xs" 1); |
133 by (ALLGOALS Asm_simp_tac); |
132 by (Auto_tac); |
134 qed "append_is_Nil_conv"; |
133 qed "append_is_Nil_conv"; |
135 AddIffs [append_is_Nil_conv]; |
134 AddIffs [append_is_Nil_conv]; |
136 |
135 |
137 Goal "([] = xs@ys) = (xs=[] & ys=[])"; |
136 Goal "([] = xs@ys) = (xs=[] & ys=[])"; |
138 by (induct_tac "xs" 1); |
137 by (induct_tac "xs" 1); |
139 by (ALLGOALS Asm_simp_tac); |
138 by (Auto_tac); |
140 by (Blast_tac 1); |
|
141 qed "Nil_is_append_conv"; |
139 qed "Nil_is_append_conv"; |
142 AddIffs [Nil_is_append_conv]; |
140 AddIffs [Nil_is_append_conv]; |
143 |
141 |
144 Goal "(xs @ ys = xs) = (ys=[])"; |
142 Goal "(xs @ ys = xs) = (ys=[])"; |
145 by (induct_tac "xs" 1); |
143 by (induct_tac "xs" 1); |
146 by (ALLGOALS Asm_simp_tac); |
144 by (Auto_tac); |
147 qed "append_self_conv"; |
145 qed "append_self_conv"; |
148 |
146 |
149 Goal "(xs = xs @ ys) = (ys=[])"; |
147 Goal "(xs = xs @ ys) = (ys=[])"; |
150 by (induct_tac "xs" 1); |
148 by (induct_tac "xs" 1); |
151 by (ALLGOALS Asm_simp_tac); |
149 by (Auto_tac); |
152 by (Blast_tac 1); |
|
153 qed "self_append_conv"; |
150 qed "self_append_conv"; |
154 AddIffs [append_self_conv,self_append_conv]; |
151 AddIffs [append_self_conv,self_append_conv]; |
155 |
152 |
156 Goal "!ys. length xs = length ys | length us = length vs \ |
153 Goal "!ys. length xs = length ys | length us = length vs \ |
157 \ --> (xs@us = ys@vs) = (xs=ys & us=vs)"; |
154 \ --> (xs@us = ys@vs) = (xs=ys & us=vs)"; |
231 section "map"; |
228 section "map"; |
232 |
229 |
233 Goal |
230 Goal |
234 "(!x. x : set xs --> f x = g x) --> map f xs = map g xs"; |
231 "(!x. x : set xs --> f x = g x) --> map f xs = map g xs"; |
235 by (induct_tac "xs" 1); |
232 by (induct_tac "xs" 1); |
236 by (ALLGOALS Asm_simp_tac); |
233 by (Auto_tac); |
237 bind_thm("map_ext", impI RS (allI RS (result() RS mp))); |
234 bind_thm("map_ext", impI RS (allI RS (result() RS mp))); |
238 |
235 |
239 Goal "map (%x. x) = (%xs. xs)"; |
236 Goal "map (%x. x) = (%xs. xs)"; |
240 by (rtac ext 1); |
237 by (rtac ext 1); |
241 by (induct_tac "xs" 1); |
238 by (induct_tac "xs" 1); |
242 by (ALLGOALS Asm_simp_tac); |
239 by (Auto_tac); |
243 qed "map_ident"; |
240 qed "map_ident"; |
244 Addsimps[map_ident]; |
241 Addsimps[map_ident]; |
245 |
242 |
246 Goal "map f (xs@ys) = map f xs @ map f ys"; |
243 Goal "map f (xs@ys) = map f xs @ map f ys"; |
247 by (induct_tac "xs" 1); |
244 by (induct_tac "xs" 1); |
248 by (ALLGOALS Asm_simp_tac); |
245 by (Auto_tac); |
249 qed "map_append"; |
246 qed "map_append"; |
250 Addsimps[map_append]; |
247 Addsimps[map_append]; |
251 |
248 |
252 Goalw [o_def] "map (f o g) xs = map f (map g xs)"; |
249 Goalw [o_def] "map (f o g) xs = map f (map g xs)"; |
253 by (induct_tac "xs" 1); |
250 by (induct_tac "xs" 1); |
254 by (ALLGOALS Asm_simp_tac); |
251 by (Auto_tac); |
255 qed "map_compose"; |
252 qed "map_compose"; |
256 Addsimps[map_compose]; |
253 Addsimps[map_compose]; |
257 |
254 |
258 Goal "rev(map f xs) = map f (rev xs)"; |
255 Goal "rev(map f xs) = map f (rev xs)"; |
259 by (induct_tac "xs" 1); |
256 by (induct_tac "xs" 1); |
260 by (ALLGOALS Asm_simp_tac); |
257 by (Auto_tac); |
261 qed "rev_map"; |
258 qed "rev_map"; |
262 |
259 |
263 (* a congruence rule for map: *) |
260 (* a congruence rule for map: *) |
264 Goal |
261 Goal |
265 "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys"; |
262 "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys"; |
266 by (rtac impI 1); |
263 by (rtac impI 1); |
267 by (hyp_subst_tac 1); |
264 by (hyp_subst_tac 1); |
268 by (induct_tac "ys" 1); |
265 by (induct_tac "ys" 1); |
269 by (ALLGOALS Asm_simp_tac); |
266 by (Auto_tac); |
270 val lemma = result(); |
267 val lemma = result(); |
271 bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp))); |
268 bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp))); |
272 |
269 |
273 Goal "(map f xs = []) = (xs = [])"; |
270 Goal "(map f xs = []) = (xs = [])"; |
274 by (induct_tac "xs" 1); |
271 by (induct_tac "xs" 1); |
275 by (ALLGOALS Asm_simp_tac); |
272 by (Auto_tac); |
276 qed "map_is_Nil_conv"; |
273 qed "map_is_Nil_conv"; |
277 AddIffs [map_is_Nil_conv]; |
274 AddIffs [map_is_Nil_conv]; |
278 |
275 |
279 Goal "([] = map f xs) = (xs = [])"; |
276 Goal "([] = map f xs) = (xs = [])"; |
280 by (induct_tac "xs" 1); |
277 by (induct_tac "xs" 1); |
281 by (ALLGOALS Asm_simp_tac); |
278 by (Auto_tac); |
282 qed "Nil_is_map_conv"; |
279 qed "Nil_is_map_conv"; |
283 AddIffs [Nil_is_map_conv]; |
280 AddIffs [Nil_is_map_conv]; |
284 |
281 |
285 |
282 |
286 (** rev **) |
283 (** rev **) |
287 |
284 |
288 section "rev"; |
285 section "rev"; |
289 |
286 |
290 Goal "rev(xs@ys) = rev(ys) @ rev(xs)"; |
287 Goal "rev(xs@ys) = rev(ys) @ rev(xs)"; |
291 by (induct_tac "xs" 1); |
288 by (induct_tac "xs" 1); |
292 by (ALLGOALS Asm_simp_tac); |
289 by (Auto_tac); |
293 qed "rev_append"; |
290 qed "rev_append"; |
294 Addsimps[rev_append]; |
291 Addsimps[rev_append]; |
295 |
292 |
296 Goal "rev(rev l) = l"; |
293 Goal "rev(rev l) = l"; |
297 by (induct_tac "l" 1); |
294 by (induct_tac "l" 1); |
298 by (ALLGOALS Asm_simp_tac); |
295 by (Auto_tac); |
299 qed "rev_rev_ident"; |
296 qed "rev_rev_ident"; |
300 Addsimps[rev_rev_ident]; |
297 Addsimps[rev_rev_ident]; |
301 |
298 |
302 Goal "(rev xs = []) = (xs = [])"; |
299 Goal "(rev xs = []) = (xs = [])"; |
303 by (induct_tac "xs" 1); |
300 by (induct_tac "xs" 1); |
304 by (ALLGOALS Asm_simp_tac); |
301 by (Auto_tac); |
305 qed "rev_is_Nil_conv"; |
302 qed "rev_is_Nil_conv"; |
306 AddIffs [rev_is_Nil_conv]; |
303 AddIffs [rev_is_Nil_conv]; |
307 |
304 |
308 Goal "([] = rev xs) = (xs = [])"; |
305 Goal "([] = rev xs) = (xs = [])"; |
309 by (induct_tac "xs" 1); |
306 by (induct_tac "xs" 1); |
310 by (ALLGOALS Asm_simp_tac); |
307 by (Auto_tac); |
311 qed "Nil_is_rev_conv"; |
308 qed "Nil_is_rev_conv"; |
312 AddIffs [Nil_is_rev_conv]; |
309 AddIffs [Nil_is_rev_conv]; |
313 |
310 |
314 val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs"; |
311 val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs"; |
315 by(stac (rev_rev_ident RS sym) 1); |
312 by(stac (rev_rev_ident RS sym) 1); |
319 bes prems 1; |
316 bes prems 1; |
320 qed "rev_induct"; |
317 qed "rev_induct"; |
321 |
318 |
322 Goal "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P"; |
319 Goal "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P"; |
323 by(res_inst_tac [("xs","xs")] rev_induct 1); |
320 by(res_inst_tac [("xs","xs")] rev_induct 1); |
324 by(ALLGOALS Asm_simp_tac); |
321 by(Auto_tac); |
325 bind_thm ("rev_exhaust", |
322 bind_thm ("rev_exhaust", |
326 impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp))))); |
323 impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp))))); |
327 |
324 |
328 |
325 |
329 (** mem **) |
326 (** mem **) |
330 |
327 |
331 section "mem"; |
328 section "mem"; |
332 |
329 |
333 Goal "x mem (xs@ys) = (x mem xs | x mem ys)"; |
330 Goal "x mem (xs@ys) = (x mem xs | x mem ys)"; |
334 by (induct_tac "xs" 1); |
331 by (induct_tac "xs" 1); |
335 by (ALLGOALS Asm_simp_tac); |
332 by (Auto_tac); |
336 qed "mem_append"; |
333 qed "mem_append"; |
337 Addsimps[mem_append]; |
334 Addsimps[mem_append]; |
338 |
335 |
339 Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))"; |
336 Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))"; |
340 by (induct_tac "xs" 1); |
337 by (induct_tac "xs" 1); |
341 by (ALLGOALS Asm_simp_tac); |
338 by (Auto_tac); |
342 qed "mem_filter"; |
339 qed "mem_filter"; |
343 Addsimps[mem_filter]; |
340 Addsimps[mem_filter]; |
344 |
341 |
345 (** set **) |
342 (** set **) |
346 |
343 |
347 section "set"; |
344 section "set"; |
348 |
345 |
349 Goal "set (xs@ys) = (set xs Un set ys)"; |
346 Goal "set (xs@ys) = (set xs Un set ys)"; |
350 by (induct_tac "xs" 1); |
347 by (induct_tac "xs" 1); |
351 by (ALLGOALS Asm_simp_tac); |
348 by (Auto_tac); |
352 qed "set_append"; |
349 qed "set_append"; |
353 Addsimps[set_append]; |
350 Addsimps[set_append]; |
354 |
351 |
355 Goal "(x mem xs) = (x: set xs)"; |
352 Goal "(x mem xs) = (x: set xs)"; |
356 by (induct_tac "xs" 1); |
353 by (induct_tac "xs" 1); |
357 by (ALLGOALS Asm_simp_tac); |
354 by (Auto_tac); |
358 by (Blast_tac 1); |
|
359 qed "set_mem_eq"; |
355 qed "set_mem_eq"; |
360 |
356 |
361 Goal "set l <= set (x#l)"; |
357 Goal "set l <= set (x#l)"; |
362 by (Simp_tac 1); |
358 by (Auto_tac); |
363 by (Blast_tac 1); |
|
364 qed "set_subset_Cons"; |
359 qed "set_subset_Cons"; |
365 |
360 |
366 Goal "(set xs = {}) = (xs = [])"; |
361 Goal "(set xs = {}) = (xs = [])"; |
367 by (induct_tac "xs" 1); |
362 by (induct_tac "xs" 1); |
368 by (ALLGOALS Asm_simp_tac); |
363 by (Auto_tac); |
369 qed "set_empty"; |
364 qed "set_empty"; |
370 Addsimps [set_empty]; |
365 Addsimps [set_empty]; |
371 |
366 |
372 Goal "set(rev xs) = set(xs)"; |
367 Goal "set(rev xs) = set(xs)"; |
373 by (induct_tac "xs" 1); |
368 by (induct_tac "xs" 1); |
374 by (ALLGOALS Asm_simp_tac); |
369 by (Auto_tac); |
375 qed "set_rev"; |
370 qed "set_rev"; |
376 Addsimps [set_rev]; |
371 Addsimps [set_rev]; |
377 |
372 |
378 Goal "set(map f xs) = f``(set xs)"; |
373 Goal "set(map f xs) = f``(set xs)"; |
379 by (induct_tac "xs" 1); |
374 by (induct_tac "xs" 1); |
380 by (ALLGOALS Asm_simp_tac); |
375 by (Auto_tac); |
381 qed "set_map"; |
376 qed "set_map"; |
382 Addsimps [set_map]; |
377 Addsimps [set_map]; |
383 |
378 |
384 Goal "(x : set(filter P xs)) = (x : set xs & P x)"; |
379 Goal "(x : set(filter P xs)) = (x : set xs & P x)"; |
385 by (induct_tac "xs" 1); |
380 by (induct_tac "xs" 1); |
386 by (ALLGOALS Asm_simp_tac); |
381 by (Auto_tac); |
387 by(Blast_tac 1); |
|
388 qed "in_set_filter"; |
382 qed "in_set_filter"; |
389 Addsimps [in_set_filter]; |
383 Addsimps [in_set_filter]; |
390 |
384 |
391 |
385 |
392 (** list_all **) |
386 (** list_all **) |
393 |
387 |
394 section "list_all"; |
388 section "list_all"; |
395 |
389 |
396 Goal "list_all (%x. True) xs = True"; |
390 Goal "list_all (%x. True) xs = True"; |
397 by (induct_tac "xs" 1); |
391 by (induct_tac "xs" 1); |
398 by (ALLGOALS Asm_simp_tac); |
392 by (Auto_tac); |
399 qed "list_all_True"; |
393 qed "list_all_True"; |
400 Addsimps [list_all_True]; |
394 Addsimps [list_all_True]; |
401 |
395 |
402 Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; |
396 Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; |
403 by (induct_tac "xs" 1); |
397 by (induct_tac "xs" 1); |
404 by (ALLGOALS Asm_simp_tac); |
398 by (Auto_tac); |
405 qed "list_all_append"; |
399 qed "list_all_append"; |
406 Addsimps [list_all_append]; |
400 Addsimps [list_all_append]; |
407 |
401 |
408 Goal "list_all P xs = (!x. x mem xs --> P(x))"; |
402 Goal "list_all P xs = (!x. x mem xs --> P(x))"; |
409 by (induct_tac "xs" 1); |
403 by (induct_tac "xs" 1); |
410 by (ALLGOALS Asm_simp_tac); |
404 by (Auto_tac); |
411 by (Blast_tac 1); |
|
412 qed "list_all_mem_conv"; |
405 qed "list_all_mem_conv"; |
413 |
406 |
414 |
407 |
415 (** filter **) |
408 (** filter **) |
416 |
409 |
417 section "filter"; |
410 section "filter"; |
418 |
411 |
419 Goal "filter P (xs@ys) = filter P xs @ filter P ys"; |
412 Goal "filter P (xs@ys) = filter P xs @ filter P ys"; |
420 by (induct_tac "xs" 1); |
413 by (induct_tac "xs" 1); |
421 by (ALLGOALS Asm_simp_tac); |
414 by (Auto_tac); |
422 qed "filter_append"; |
415 qed "filter_append"; |
423 Addsimps [filter_append]; |
416 Addsimps [filter_append]; |
424 |
417 |
425 Goal "filter (%x. True) xs = xs"; |
418 Goal "filter (%x. True) xs = xs"; |
426 by (induct_tac "xs" 1); |
419 by (induct_tac "xs" 1); |
427 by (ALLGOALS Asm_simp_tac); |
420 by (Auto_tac); |
428 qed "filter_True"; |
421 qed "filter_True"; |
429 Addsimps [filter_True]; |
422 Addsimps [filter_True]; |
430 |
423 |
431 Goal "filter (%x. False) xs = []"; |
424 Goal "filter (%x. False) xs = []"; |
432 by (induct_tac "xs" 1); |
425 by (induct_tac "xs" 1); |
433 by (ALLGOALS Asm_simp_tac); |
426 by (Auto_tac); |
434 qed "filter_False"; |
427 qed "filter_False"; |
435 Addsimps [filter_False]; |
428 Addsimps [filter_False]; |
436 |
429 |
437 Goal "length (filter P xs) <= length xs"; |
430 Goal "length (filter P xs) <= length xs"; |
438 by (induct_tac "xs" 1); |
431 by (induct_tac "xs" 1); |
439 by (ALLGOALS Asm_simp_tac); |
432 by (Auto_tac); |
440 qed "length_filter"; |
433 qed "length_filter"; |
441 |
434 |
442 |
435 |
443 (** concat **) |
436 (** concat **) |
444 |
437 |
445 section "concat"; |
438 section "concat"; |
446 |
439 |
447 Goal "concat(xs@ys) = concat(xs)@concat(ys)"; |
440 Goal "concat(xs@ys) = concat(xs)@concat(ys)"; |
448 by (induct_tac "xs" 1); |
441 by (induct_tac "xs" 1); |
449 by (ALLGOALS Asm_simp_tac); |
442 by (Auto_tac); |
450 qed"concat_append"; |
443 qed"concat_append"; |
451 Addsimps [concat_append]; |
444 Addsimps [concat_append]; |
452 |
445 |
453 Goal "(concat xss = []) = (!xs:set xss. xs=[])"; |
446 Goal "(concat xss = []) = (!xs:set xss. xs=[])"; |
454 by (induct_tac "xss" 1); |
447 by (induct_tac "xss" 1); |
455 by (ALLGOALS Asm_simp_tac); |
448 by (Auto_tac); |
456 qed "concat_eq_Nil_conv"; |
449 qed "concat_eq_Nil_conv"; |
457 AddIffs [concat_eq_Nil_conv]; |
450 AddIffs [concat_eq_Nil_conv]; |
458 |
451 |
459 Goal "([] = concat xss) = (!xs:set xss. xs=[])"; |
452 Goal "([] = concat xss) = (!xs:set xss. xs=[])"; |
460 by (induct_tac "xss" 1); |
453 by (induct_tac "xss" 1); |
461 by (ALLGOALS Asm_simp_tac); |
454 by (Auto_tac); |
462 qed "Nil_eq_concat_conv"; |
455 qed "Nil_eq_concat_conv"; |
463 AddIffs [Nil_eq_concat_conv]; |
456 AddIffs [Nil_eq_concat_conv]; |
464 |
457 |
465 Goal "set(concat xs) = Union(set `` set xs)"; |
458 Goal "set(concat xs) = Union(set `` set xs)"; |
466 by (induct_tac "xs" 1); |
459 by (induct_tac "xs" 1); |
467 by (ALLGOALS Asm_simp_tac); |
460 by (Auto_tac); |
468 qed"set_concat"; |
461 qed"set_concat"; |
469 Addsimps [set_concat]; |
462 Addsimps [set_concat]; |
470 |
463 |
471 Goal "map f (concat xs) = concat (map (map f) xs)"; |
464 Goal "map f (concat xs) = concat (map (map f) xs)"; |
472 by (induct_tac "xs" 1); |
465 by (induct_tac "xs" 1); |
473 by (ALLGOALS Asm_simp_tac); |
466 by (Auto_tac); |
474 qed "map_concat"; |
467 qed "map_concat"; |
475 |
468 |
476 Goal "filter p (concat xs) = concat (map (filter p) xs)"; |
469 Goal "filter p (concat xs) = concat (map (filter p) xs)"; |
477 by (induct_tac "xs" 1); |
470 by (induct_tac "xs" 1); |
478 by (ALLGOALS Asm_simp_tac); |
471 by (Auto_tac); |
479 qed"filter_concat"; |
472 qed"filter_concat"; |
480 |
473 |
481 Goal "rev(concat xs) = concat (map rev (rev xs))"; |
474 Goal "rev(concat xs) = concat (map rev (rev xs))"; |
482 by (induct_tac "xs" 1); |
475 by (induct_tac "xs" 1); |
483 by (ALLGOALS Asm_simp_tac); |
476 by (Auto_tac); |
484 qed "rev_concat"; |
477 qed "rev_concat"; |
485 |
478 |
486 (** nth **) |
479 (** nth **) |
487 |
480 |
488 section "nth"; |
481 section "nth"; |
545 |
538 |
546 (** last & butlast **) |
539 (** last & butlast **) |
547 |
540 |
548 Goal "last(xs@[x]) = x"; |
541 Goal "last(xs@[x]) = x"; |
549 by (induct_tac "xs" 1); |
542 by (induct_tac "xs" 1); |
550 by (ALLGOALS Asm_simp_tac); |
543 by (Auto_tac); |
551 qed "last_snoc"; |
544 qed "last_snoc"; |
552 Addsimps [last_snoc]; |
545 Addsimps [last_snoc]; |
553 |
546 |
554 Goal "butlast(xs@[x]) = xs"; |
547 Goal "butlast(xs@[x]) = xs"; |
555 by (induct_tac "xs" 1); |
548 by (induct_tac "xs" 1); |
556 by (ALLGOALS Asm_simp_tac); |
549 by (Auto_tac); |
557 qed "butlast_snoc"; |
550 qed "butlast_snoc"; |
558 Addsimps [butlast_snoc]; |
551 Addsimps [butlast_snoc]; |
559 |
552 |
560 Goal "length(butlast xs) = length xs - 1"; |
553 Goal "length(butlast xs) = length xs - 1"; |
561 by (res_inst_tac [("xs","xs")] rev_induct 1); |
554 by (res_inst_tac [("xs","xs")] rev_induct 1); |
562 by (ALLGOALS Asm_simp_tac); |
555 by (Auto_tac); |
563 qed "length_butlast"; |
556 qed "length_butlast"; |
564 Addsimps [length_butlast]; |
557 Addsimps [length_butlast]; |
565 |
558 |
566 Goal |
559 Goal |
567 "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)"; |
560 "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)"; |
568 by (induct_tac "xs" 1); |
561 by (induct_tac "xs" 1); |
569 by (ALLGOALS Asm_simp_tac); |
562 by (Auto_tac); |
570 qed_spec_mp "butlast_append"; |
563 qed_spec_mp "butlast_append"; |
571 |
564 |
572 Goal "x:set(butlast xs) --> x:set xs"; |
565 Goal "x:set(butlast xs) --> x:set xs"; |
573 by (induct_tac "xs" 1); |
566 by (induct_tac "xs" 1); |
574 by (ALLGOALS Asm_simp_tac); |
567 by (Auto_tac); |
575 qed_spec_mp "in_set_butlastD"; |
568 qed_spec_mp "in_set_butlastD"; |
576 |
569 |
577 Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))"; |
570 Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))"; |
578 by (asm_simp_tac (simpset() addsimps [butlast_append]) 1); |
571 by (asm_simp_tac (simpset() addsimps [butlast_append]) 1); |
579 by (blast_tac (claset() addDs [in_set_butlastD]) 1); |
572 by (blast_tac (claset() addDs [in_set_butlastD]) 1); |
609 Delsimps [take_Cons,drop_Cons]; |
602 Delsimps [take_Cons,drop_Cons]; |
610 Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons]; |
603 Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons]; |
611 |
604 |
612 Goal "!xs. length(take n xs) = min (length xs) n"; |
605 Goal "!xs. length(take n xs) = min (length xs) n"; |
613 by (nat_ind_tac "n" 1); |
606 by (nat_ind_tac "n" 1); |
614 by (ALLGOALS Asm_simp_tac); |
607 by (Auto_tac); |
615 by (rtac allI 1); |
608 by (exhaust_tac "xs" 1); |
616 by (exhaust_tac "xs" 1); |
609 by (Auto_tac); |
617 by (ALLGOALS Asm_simp_tac); |
|
618 qed_spec_mp "length_take"; |
610 qed_spec_mp "length_take"; |
619 Addsimps [length_take]; |
611 Addsimps [length_take]; |
620 |
612 |
621 Goal "!xs. length(drop n xs) = (length xs - n)"; |
613 Goal "!xs. length(drop n xs) = (length xs - n)"; |
622 by (nat_ind_tac "n" 1); |
614 by (nat_ind_tac "n" 1); |
623 by (ALLGOALS Asm_simp_tac); |
615 by (Auto_tac); |
624 by (rtac allI 1); |
616 by (exhaust_tac "xs" 1); |
625 by (exhaust_tac "xs" 1); |
617 by (Auto_tac); |
626 by (ALLGOALS Asm_simp_tac); |
|
627 qed_spec_mp "length_drop"; |
618 qed_spec_mp "length_drop"; |
628 Addsimps [length_drop]; |
619 Addsimps [length_drop]; |
629 |
620 |
630 Goal "!xs. length xs <= n --> take n xs = xs"; |
621 Goal "!xs. length xs <= n --> take n xs = xs"; |
631 by (nat_ind_tac "n" 1); |
622 by (nat_ind_tac "n" 1); |
632 by (ALLGOALS Asm_simp_tac); |
623 by (Auto_tac); |
633 by (rtac allI 1); |
624 by (exhaust_tac "xs" 1); |
634 by (exhaust_tac "xs" 1); |
625 by (Auto_tac); |
635 by (ALLGOALS Asm_simp_tac); |
|
636 qed_spec_mp "take_all"; |
626 qed_spec_mp "take_all"; |
637 |
627 |
638 Goal "!xs. length xs <= n --> drop n xs = []"; |
628 Goal "!xs. length xs <= n --> drop n xs = []"; |
639 by (nat_ind_tac "n" 1); |
629 by (nat_ind_tac "n" 1); |
640 by (ALLGOALS Asm_simp_tac); |
630 by (Auto_tac); |
641 by (rtac allI 1); |
631 by (exhaust_tac "xs" 1); |
642 by (exhaust_tac "xs" 1); |
632 by (Auto_tac); |
643 by (ALLGOALS Asm_simp_tac); |
|
644 qed_spec_mp "drop_all"; |
633 qed_spec_mp "drop_all"; |
645 |
634 |
646 Goal |
635 Goal |
647 "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"; |
636 "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"; |
648 by (nat_ind_tac "n" 1); |
637 by (nat_ind_tac "n" 1); |
649 by (ALLGOALS Asm_simp_tac); |
638 by (Auto_tac); |
650 by (rtac allI 1); |
639 by (exhaust_tac "xs" 1); |
651 by (exhaust_tac "xs" 1); |
640 by (Auto_tac); |
652 by (ALLGOALS Asm_simp_tac); |
|
653 qed_spec_mp "take_append"; |
641 qed_spec_mp "take_append"; |
654 Addsimps [take_append]; |
642 Addsimps [take_append]; |
655 |
643 |
656 Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; |
644 Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; |
657 by (nat_ind_tac "n" 1); |
645 by (nat_ind_tac "n" 1); |
658 by (ALLGOALS Asm_simp_tac); |
646 by (Auto_tac); |
659 by (rtac allI 1); |
647 by (exhaust_tac "xs" 1); |
660 by (exhaust_tac "xs" 1); |
648 by (Auto_tac); |
661 by (ALLGOALS Asm_simp_tac); |
|
662 qed_spec_mp "drop_append"; |
649 qed_spec_mp "drop_append"; |
663 Addsimps [drop_append]; |
650 Addsimps [drop_append]; |
664 |
651 |
665 Goal "!xs n. take n (take m xs) = take (min n m) xs"; |
652 Goal "!xs n. take n (take m xs) = take (min n m) xs"; |
666 by (nat_ind_tac "m" 1); |
653 by (nat_ind_tac "m" 1); |
667 by (ALLGOALS Asm_simp_tac); |
654 by (Auto_tac); |
668 by (rtac allI 1); |
655 by (exhaust_tac "xs" 1); |
669 by (exhaust_tac "xs" 1); |
656 by (Auto_tac); |
670 by (ALLGOALS Asm_simp_tac); |
|
671 by (rtac allI 1); |
|
672 by (exhaust_tac "n" 1); |
657 by (exhaust_tac "n" 1); |
673 by (ALLGOALS Asm_simp_tac); |
658 by (Auto_tac); |
674 qed_spec_mp "take_take"; |
659 qed_spec_mp "take_take"; |
675 |
660 |
676 Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; |
661 Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; |
677 by (nat_ind_tac "m" 1); |
662 by (nat_ind_tac "m" 1); |
678 by (ALLGOALS Asm_simp_tac); |
663 by (Auto_tac); |
679 by (rtac allI 1); |
664 by (exhaust_tac "xs" 1); |
680 by (exhaust_tac "xs" 1); |
665 by (Auto_tac); |
681 by (ALLGOALS Asm_simp_tac); |
|
682 qed_spec_mp "drop_drop"; |
666 qed_spec_mp "drop_drop"; |
683 |
667 |
684 Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; |
668 Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; |
685 by (nat_ind_tac "m" 1); |
669 by (nat_ind_tac "m" 1); |
686 by (ALLGOALS Asm_simp_tac); |
670 by (Auto_tac); |
687 by (rtac allI 1); |
671 by (exhaust_tac "xs" 1); |
688 by (exhaust_tac "xs" 1); |
672 by (Auto_tac); |
689 by (ALLGOALS Asm_simp_tac); |
|
690 qed_spec_mp "take_drop"; |
673 qed_spec_mp "take_drop"; |
691 |
674 |
692 Goal "!xs. take n (map f xs) = map f (take n xs)"; |
675 Goal "!xs. take n (map f xs) = map f (take n xs)"; |
693 by (nat_ind_tac "n" 1); |
676 by (nat_ind_tac "n" 1); |
694 by (ALLGOALS Asm_simp_tac); |
677 by (Auto_tac); |
695 by (rtac allI 1); |
678 by (exhaust_tac "xs" 1); |
696 by (exhaust_tac "xs" 1); |
679 by (Auto_tac); |
697 by (ALLGOALS Asm_simp_tac); |
|
698 qed_spec_mp "take_map"; |
680 qed_spec_mp "take_map"; |
699 |
681 |
700 Goal "!xs. drop n (map f xs) = map f (drop n xs)"; |
682 Goal "!xs. drop n (map f xs) = map f (drop n xs)"; |
701 by (nat_ind_tac "n" 1); |
683 by (nat_ind_tac "n" 1); |
702 by (ALLGOALS Asm_simp_tac); |
684 by (Auto_tac); |
703 by (rtac allI 1); |
685 by (exhaust_tac "xs" 1); |
704 by (exhaust_tac "xs" 1); |
686 by (Auto_tac); |
705 by (ALLGOALS Asm_simp_tac); |
|
706 qed_spec_mp "drop_map"; |
687 qed_spec_mp "drop_map"; |
707 |
688 |
708 Goal "!n i. i < n --> (take n xs)!i = xs!i"; |
689 Goal "!n i. i < n --> (take n xs)!i = xs!i"; |
709 by (induct_tac "xs" 1); |
690 by (induct_tac "xs" 1); |
710 by (ALLGOALS Asm_simp_tac); |
691 by (Auto_tac); |
711 by (Clarify_tac 1); |
|
712 by (exhaust_tac "n" 1); |
692 by (exhaust_tac "n" 1); |
713 by (Blast_tac 1); |
693 by (Blast_tac 1); |
714 by (exhaust_tac "i" 1); |
694 by (exhaust_tac "i" 1); |
715 by (ALLGOALS Asm_full_simp_tac); |
695 by (Auto_tac); |
716 qed_spec_mp "nth_take"; |
696 qed_spec_mp "nth_take"; |
717 Addsimps [nth_take]; |
697 Addsimps [nth_take]; |
718 |
698 |
719 Goal "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)"; |
699 Goal "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)"; |
720 by (nat_ind_tac "n" 1); |
700 by (nat_ind_tac "n" 1); |
721 by (ALLGOALS Asm_simp_tac); |
701 by (Auto_tac); |
722 by (rtac allI 1); |
702 by (exhaust_tac "xs" 1); |
723 by (exhaust_tac "xs" 1); |
703 by (Auto_tac); |
724 by (ALLGOALS Asm_simp_tac); |
|
725 qed_spec_mp "nth_drop"; |
704 qed_spec_mp "nth_drop"; |
726 Addsimps [nth_drop]; |
705 Addsimps [nth_drop]; |
727 |
706 |
728 (** takeWhile & dropWhile **) |
707 (** takeWhile & dropWhile **) |
729 |
708 |
730 section "takeWhile & dropWhile"; |
709 section "takeWhile & dropWhile"; |
731 |
710 |
732 Goal "takeWhile P xs @ dropWhile P xs = xs"; |
711 Goal "takeWhile P xs @ dropWhile P xs = xs"; |
733 by (induct_tac "xs" 1); |
712 by (induct_tac "xs" 1); |
734 by (ALLGOALS Asm_full_simp_tac); |
713 by (Auto_tac); |
735 qed "takeWhile_dropWhile_id"; |
714 qed "takeWhile_dropWhile_id"; |
736 Addsimps [takeWhile_dropWhile_id]; |
715 Addsimps [takeWhile_dropWhile_id]; |
737 |
716 |
738 Goal "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs"; |
717 Goal "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs"; |
739 by (induct_tac "xs" 1); |
718 by (induct_tac "xs" 1); |
740 by (ALLGOALS Asm_full_simp_tac); |
719 by (Auto_tac); |
741 by (Blast_tac 1); |
|
742 bind_thm("takeWhile_append1", conjI RS (result() RS mp)); |
720 bind_thm("takeWhile_append1", conjI RS (result() RS mp)); |
743 Addsimps [takeWhile_append1]; |
721 Addsimps [takeWhile_append1]; |
744 |
722 |
745 Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys"; |
723 Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys"; |
746 by (induct_tac "xs" 1); |
724 by (induct_tac "xs" 1); |
747 by (ALLGOALS Asm_full_simp_tac); |
725 by (Auto_tac); |
748 bind_thm("takeWhile_append2", ballI RS (result() RS mp)); |
726 bind_thm("takeWhile_append2", ballI RS (result() RS mp)); |
749 Addsimps [takeWhile_append2]; |
727 Addsimps [takeWhile_append2]; |
750 |
728 |
751 Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"; |
729 Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"; |
752 by (induct_tac "xs" 1); |
730 by (induct_tac "xs" 1); |
753 by (ALLGOALS Asm_full_simp_tac); |
731 by (Auto_tac); |
754 by (Blast_tac 1); |
|
755 bind_thm("dropWhile_append1", conjI RS (result() RS mp)); |
732 bind_thm("dropWhile_append1", conjI RS (result() RS mp)); |
756 Addsimps [dropWhile_append1]; |
733 Addsimps [dropWhile_append1]; |
757 |
734 |
758 Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys"; |
735 Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys"; |
759 by (induct_tac "xs" 1); |
736 by (induct_tac "xs" 1); |
760 by (ALLGOALS Asm_full_simp_tac); |
737 by (Auto_tac); |
761 bind_thm("dropWhile_append2", ballI RS (result() RS mp)); |
738 bind_thm("dropWhile_append2", ballI RS (result() RS mp)); |
762 Addsimps [dropWhile_append2]; |
739 Addsimps [dropWhile_append2]; |
763 |
740 |
764 Goal "x:set(takeWhile P xs) --> x:set xs & P x"; |
741 Goal "x:set(takeWhile P xs) --> x:set xs & P x"; |
765 by (induct_tac "xs" 1); |
742 by (induct_tac "xs" 1); |
766 by (ALLGOALS Asm_full_simp_tac); |
743 by (Auto_tac); |
767 qed_spec_mp"set_take_whileD"; |
744 qed_spec_mp"set_take_whileD"; |
768 |
745 |
769 qed_goal "zip_Nil_Nil" thy "zip [] [] = []" (K [Simp_tac 1]); |
746 qed_goal "zip_Nil_Nil" thy "zip [] [] = []" (K [Simp_tac 1]); |
770 qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" |
747 qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" |
771 (K [Simp_tac 1]); |
748 (K [Simp_tac 1]); |