140 |
140 |
141 Addsimps [list_rec_Nil, list_rec_Cons]; |
141 Addsimps [list_rec_Nil, list_rec_Cons]; |
142 |
142 |
143 |
143 |
144 (*Type checking -- proved by induction, as usual*) |
144 (*Type checking -- proved by induction, as usual*) |
145 val prems = goal List.thy |
145 val prems = Goal |
146 "[| l: list(A); \ |
146 "[| l: list(A); \ |
147 \ c: C(Nil); \ |
147 \ c: C(Nil); \ |
148 \ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \ |
148 \ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \ |
149 \ |] ==> list_rec(l,c,h) : C(l)"; |
149 \ |] ==> list_rec(l,c,h) : C(l)"; |
150 by (list_ind_tac "l" prems 1); |
150 by (list_ind_tac "l" prems 1); |
151 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
151 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
152 qed "list_rec_type"; |
152 qed "list_rec_type"; |
153 |
153 |
154 (** Versions for use with definitions **) |
154 (** Versions for use with definitions **) |
155 |
155 |
156 val [rew] = goal List.thy |
156 val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c"; |
157 "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c"; |
|
158 by (rewtac rew); |
157 by (rewtac rew); |
159 by (rtac list_rec_Nil 1); |
158 by (rtac list_rec_Nil 1); |
160 qed "def_list_rec_Nil"; |
159 qed "def_list_rec_Nil"; |
161 |
160 |
162 val [rew] = goal List.thy |
161 val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))"; |
163 "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))"; |
|
164 by (rewtac rew); |
162 by (rewtac rew); |
165 by (rtac list_rec_Cons 1); |
163 by (rtac list_rec_Cons 1); |
166 qed "def_list_rec_Cons"; |
164 qed "def_list_rec_Cons"; |
167 |
165 |
168 fun list_recs def = map standard |
166 fun list_recs def = map standard |
261 simpset_ref() := simpset() setSolver (type_auto_tac list_typechecks); |
259 simpset_ref() := simpset() setSolver (type_auto_tac list_typechecks); |
262 |
260 |
263 |
261 |
264 (*** theorems about map ***) |
262 (*** theorems about map ***) |
265 |
263 |
266 val prems = goal List.thy |
264 Goal "l: list(A) ==> map(%u. u, l) = l"; |
267 "l: list(A) ==> map(%u. u, l) = l"; |
265 by (list_ind_tac "l" [] 1); |
268 by (list_ind_tac "l" prems 1); |
|
269 by (ALLGOALS Asm_simp_tac); |
266 by (ALLGOALS Asm_simp_tac); |
270 qed "map_ident"; |
267 qed "map_ident"; |
271 |
268 |
272 val prems = goal List.thy |
269 Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"; |
273 "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"; |
270 by (list_ind_tac "l" [] 1); |
274 by (list_ind_tac "l" prems 1); |
|
275 by (ALLGOALS Asm_simp_tac); |
271 by (ALLGOALS Asm_simp_tac); |
276 qed "map_compose"; |
272 qed "map_compose"; |
277 |
273 |
278 val prems = goal List.thy |
274 Goal "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"; |
279 "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"; |
275 by (list_ind_tac "xs" [] 1); |
280 by (list_ind_tac "xs" prems 1); |
|
281 by (ALLGOALS Asm_simp_tac); |
276 by (ALLGOALS Asm_simp_tac); |
282 qed "map_app_distrib"; |
277 qed "map_app_distrib"; |
283 |
278 |
284 val prems = goal List.thy |
279 Goal "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"; |
285 "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"; |
280 by (list_ind_tac "ls" [] 1); |
286 by (list_ind_tac "ls" prems 1); |
|
287 by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib]))); |
281 by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib]))); |
288 qed "map_flat"; |
282 qed "map_flat"; |
289 |
283 |
290 val prems = goal List.thy |
284 Goal "l: list(A) ==> \ |
291 "l: list(A) ==> \ |
|
292 \ list_rec(map(h,l), c, d) = \ |
285 \ list_rec(map(h,l), c, d) = \ |
293 \ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))"; |
286 \ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))"; |
294 by (list_ind_tac "l" prems 1); |
287 by (list_ind_tac "l" [] 1); |
295 by (ALLGOALS Asm_simp_tac); |
288 by (ALLGOALS Asm_simp_tac); |
296 qed "list_rec_map"; |
289 qed "list_rec_map"; |
297 |
290 |
298 (** theorems about list(Collect(A,P)) -- used in ex/term.ML **) |
291 (** theorems about list(Collect(A,P)) -- used in ex/term.ML **) |
299 |
292 |
300 (* c : list(Collect(B,P)) ==> c : list(B) *) |
293 (* c : list(Collect(B,P)) ==> c : list(B) *) |
301 bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD)); |
294 bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD)); |
302 |
295 |
303 val prems = goal List.thy |
296 Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"; |
304 "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"; |
297 by (list_ind_tac "l" [] 1); |
305 by (list_ind_tac "l" prems 1); |
|
306 by (ALLGOALS Asm_simp_tac); |
298 by (ALLGOALS Asm_simp_tac); |
307 qed "map_list_Collect"; |
299 qed "map_list_Collect"; |
308 |
300 |
309 (*** theorems about length ***) |
301 (*** theorems about length ***) |
310 |
302 |
311 val prems = goal List.thy |
303 Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)"; |
312 "xs: list(A) ==> length(map(h,xs)) = length(xs)"; |
304 by (list_ind_tac "xs" [] 1); |
313 by (list_ind_tac "xs" prems 1); |
|
314 by (ALLGOALS Asm_simp_tac); |
305 by (ALLGOALS Asm_simp_tac); |
315 qed "length_map"; |
306 qed "length_map"; |
316 |
307 |
317 val prems = goal List.thy |
308 Goal "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)"; |
318 "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)"; |
309 by (list_ind_tac "xs" [] 1); |
319 by (list_ind_tac "xs" prems 1); |
|
320 by (ALLGOALS Asm_simp_tac); |
310 by (ALLGOALS Asm_simp_tac); |
321 qed "length_app"; |
311 qed "length_app"; |
322 |
312 |
323 (* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m |
313 (* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m |
324 Used for rewriting below*) |
314 Used for rewriting below*) |
325 val add_commute_succ = nat_succI RSN (2,add_commute); |
315 val add_commute_succ = nat_succI RSN (2,add_commute); |
326 |
316 |
327 val prems = goal List.thy |
317 Goal "xs: list(A) ==> length(rev(xs)) = length(xs)"; |
328 "xs: list(A) ==> length(rev(xs)) = length(xs)"; |
318 by (list_ind_tac "xs" [] 1); |
329 by (list_ind_tac "xs" prems 1); |
|
330 by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app, add_commute_succ]))); |
319 by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app, add_commute_succ]))); |
331 qed "length_rev"; |
320 qed "length_rev"; |
332 |
321 |
333 val prems = goal List.thy |
322 Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"; |
334 "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"; |
323 by (list_ind_tac "ls" [] 1); |
335 by (list_ind_tac "ls" prems 1); |
|
336 by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app]))); |
324 by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app]))); |
337 qed "length_flat"; |
325 qed "length_flat"; |
338 |
326 |
339 (** Length and drop **) |
327 (** Length and drop **) |
340 |
328 |
362 bind_thm ("drop_length", (drop_length_lemma RS bspec)); |
350 bind_thm ("drop_length", (drop_length_lemma RS bspec)); |
363 |
351 |
364 |
352 |
365 (*** theorems about app ***) |
353 (*** theorems about app ***) |
366 |
354 |
367 val [major] = goal List.thy "xs: list(A) ==> xs@Nil=xs"; |
355 Goal "xs: list(A) ==> xs@Nil=xs"; |
368 by (rtac (major RS list.induct) 1); |
356 by (etac list.induct 1); |
369 by (ALLGOALS Asm_simp_tac); |
357 by (ALLGOALS Asm_simp_tac); |
370 qed "app_right_Nil"; |
358 qed "app_right_Nil"; |
371 |
359 |
372 val prems = goal List.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"; |
360 Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"; |
373 by (list_ind_tac "xs" prems 1); |
361 by (list_ind_tac "xs" [] 1); |
374 by (ALLGOALS Asm_simp_tac); |
362 by (ALLGOALS Asm_simp_tac); |
375 qed "app_assoc"; |
363 qed "app_assoc"; |
376 |
364 |
377 val prems = goal List.thy |
365 Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"; |
378 "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"; |
366 by (list_ind_tac "ls" [] 1); |
379 by (list_ind_tac "ls" prems 1); |
|
380 by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc]))); |
367 by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc]))); |
381 qed "flat_app_distrib"; |
368 qed "flat_app_distrib"; |
382 |
369 |
383 (*** theorems about rev ***) |
370 (*** theorems about rev ***) |
384 |
371 |
385 val prems = goal List.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"; |
372 Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"; |
386 by (list_ind_tac "l" prems 1); |
373 by (list_ind_tac "l" [] 1); |
387 by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib]))); |
374 by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib]))); |
388 qed "rev_map_distrib"; |
375 qed "rev_map_distrib"; |
389 |
376 |
390 (*Simplifier needs the premises as assumptions because rewriting will not |
377 (*Simplifier needs the premises as assumptions because rewriting will not |
391 instantiate the variable ?A in the rules' typing conditions; note that |
378 instantiate the variable ?A in the rules' typing conditions; note that |
394 Goal "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"; |
381 Goal "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"; |
395 by (etac list.induct 1); |
382 by (etac list.induct 1); |
396 by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_right_Nil,app_assoc]))); |
383 by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_right_Nil,app_assoc]))); |
397 qed "rev_app_distrib"; |
384 qed "rev_app_distrib"; |
398 |
385 |
399 val prems = goal List.thy "l: list(A) ==> rev(rev(l))=l"; |
386 Goal "l: list(A) ==> rev(rev(l))=l"; |
400 by (list_ind_tac "l" prems 1); |
387 by (list_ind_tac "l" [] 1); |
401 by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib]))); |
388 by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib]))); |
402 qed "rev_rev_ident"; |
389 qed "rev_rev_ident"; |
403 |
390 |
404 val prems = goal List.thy |
391 Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"; |
405 "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"; |
392 by (list_ind_tac "ls" [] 1); |
406 by (list_ind_tac "ls" prems 1); |
|
407 by (ALLGOALS (asm_simp_tac (simpset() addsimps |
393 by (ALLGOALS (asm_simp_tac (simpset() addsimps |
408 [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil]))); |
394 [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil]))); |
409 qed "rev_flat"; |
395 qed "rev_flat"; |
410 |
396 |
411 |
397 |
412 (*** theorems about list_add ***) |
398 (*** theorems about list_add ***) |
413 |
399 |
414 val prems = goal List.thy |
400 Goal "[| xs: list(nat); ys: list(nat) |] ==> \ |
415 "[| xs: list(nat); ys: list(nat) |] ==> \ |
|
416 \ list_add(xs@ys) = list_add(ys) #+ list_add(xs)"; |
401 \ list_add(xs@ys) = list_add(ys) #+ list_add(xs)"; |
417 by (cut_facts_tac prems 1); |
402 by (list_ind_tac "xs" [] 1); |
418 by (list_ind_tac "xs" prems 1); |
|
419 by (ALLGOALS |
403 by (ALLGOALS |
420 (asm_simp_tac (simpset() addsimps [add_0_right, add_assoc RS sym]))); |
404 (asm_simp_tac (simpset() addsimps [add_0_right, add_assoc RS sym]))); |
421 by (rtac (add_commute RS subst_context) 1); |
405 by (rtac (add_commute RS subst_context) 1); |
422 by (REPEAT (ares_tac [refl, list_add_type] 1)); |
406 by (REPEAT (ares_tac [refl, list_add_type] 1)); |
423 qed "list_add_app"; |
407 qed "list_add_app"; |
424 |
408 |
425 val prems = goal List.thy |
409 Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)"; |
426 "l: list(nat) ==> list_add(rev(l)) = list_add(l)"; |
410 by (list_ind_tac "l" [] 1); |
427 by (list_ind_tac "l" prems 1); |
|
428 by (ALLGOALS |
411 by (ALLGOALS |
429 (asm_simp_tac (simpset() addsimps [list_add_app, add_0_right]))); |
412 (asm_simp_tac (simpset() addsimps [list_add_app, add_0_right]))); |
430 qed "list_add_rev"; |
413 qed "list_add_rev"; |
431 |
414 |
432 val prems = goal List.thy |
415 Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"; |
433 "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"; |
416 by (list_ind_tac "ls" [] 1); |
434 by (list_ind_tac "ls" prems 1); |
|
435 by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app]))); |
417 by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app]))); |
436 by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1)); |
418 by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1)); |
437 qed "list_add_flat"; |
419 qed "list_add_flat"; |
438 |
420 |
439 (** New induction rule **) |
421 (** New induction rule **) |
440 |
422 |
441 val major::prems = goal List.thy |
423 val major::prems = Goal |
442 "[| l: list(A); \ |
424 "[| l: list(A); \ |
443 \ P(Nil); \ |
425 \ P(Nil); \ |
444 \ !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) \ |
426 \ !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) \ |
445 \ |] ==> P(l)"; |
427 \ |] ==> P(l)"; |
446 by (rtac (major RS rev_rev_ident RS subst) 1); |
428 by (rtac (major RS rev_rev_ident RS subst) 1); |