equal
deleted
inserted
replaced
348 by (induct_tac "xs" 1); |
348 by (induct_tac "xs" 1); |
349 by (ALLGOALS Asm_simp_tac); |
349 by (ALLGOALS Asm_simp_tac); |
350 qed "set_map"; |
350 qed "set_map"; |
351 Addsimps [set_map]; |
351 Addsimps [set_map]; |
352 |
352 |
|
353 goal thy "set(map f xs) = f``(set xs)"; |
|
354 by (induct_tac "xs" 1); |
|
355 by (ALLGOALS Asm_simp_tac); |
|
356 qed "set_map"; |
|
357 Addsimps [set_map]; |
|
358 |
|
359 goal thy "(x : set(filter P xs)) = (x : set xs & P x)"; |
|
360 by (induct_tac "xs" 1); |
|
361 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
|
362 by(Blast_tac 1); |
|
363 qed "in_set_filter"; |
|
364 Addsimps [in_set_filter]; |
|
365 |
353 |
366 |
354 (** list_all **) |
367 (** list_all **) |
355 |
368 |
356 section "list_all"; |
369 section "list_all"; |
357 |
370 |
382 by (induct_tac "xs" 1); |
395 by (induct_tac "xs" 1); |
383 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
396 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
384 qed "filter_append"; |
397 qed "filter_append"; |
385 Addsimps [filter_append]; |
398 Addsimps [filter_append]; |
386 |
399 |
387 goal thy "size (filter P xs) <= size xs"; |
400 goal thy "filter (%x. True) xs = xs"; |
|
401 by (induct_tac "xs" 1); |
|
402 by (ALLGOALS Asm_simp_tac); |
|
403 qed "filter_True"; |
|
404 Addsimps [filter_True]; |
|
405 |
|
406 goal thy "filter (%x. False) xs = []"; |
|
407 by (induct_tac "xs" 1); |
|
408 by (ALLGOALS Asm_simp_tac); |
|
409 qed "filter_False"; |
|
410 Addsimps [filter_False]; |
|
411 |
|
412 goal thy "length (filter P xs) <= length xs"; |
388 by (induct_tac "xs" 1); |
413 by (induct_tac "xs" 1); |
389 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
414 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
390 qed "filter_size"; |
415 qed "length_filter"; |
391 |
416 |
392 |
417 |
393 (** concat **) |
418 (** concat **) |
394 |
419 |
395 section "concat"; |
420 section "concat"; |
713 qed_spec_mp"set_take_whileD"; |
738 qed_spec_mp"set_take_whileD"; |
714 |
739 |
715 qed_goal "zip_Nil_Nil" thy "zip [] [] = []" (K [Simp_tac 1]); |
740 qed_goal "zip_Nil_Nil" thy "zip [] [] = []" (K [Simp_tac 1]); |
716 qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" |
741 qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" |
717 (K [Simp_tac 1]); |
742 (K [Simp_tac 1]); |
|
743 |
|
744 (** nodups & remdups **) |
|
745 section "nodups & remdups"; |
|
746 |
|
747 goal thy "set(remdups xs) = set xs"; |
|
748 by (induct_tac "xs" 1); |
|
749 by (Simp_tac 1); |
|
750 by (asm_full_simp_tac (simpset() addsimps [insert_absorb] |
|
751 addsplits [expand_if]) 1); |
|
752 qed "set_remdups"; |
|
753 Addsimps [set_remdups]; |
|
754 |
|
755 goal thy "nodups(remdups xs)"; |
|
756 by (induct_tac "xs" 1); |
|
757 by (Simp_tac 1); |
|
758 by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1); |
|
759 qed "nodups_remdups"; |
|
760 |
|
761 goal thy "nodups xs --> nodups (filter P xs)"; |
|
762 by (induct_tac "xs" 1); |
|
763 by (Simp_tac 1); |
|
764 by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1); |
|
765 qed_spec_mp "nodups_filter"; |
|
766 |
718 (** replicate **) |
767 (** replicate **) |
719 section "replicate"; |
768 section "replicate"; |
720 |
769 |
721 goal thy "set(replicate (Suc n) x) = {x}"; |
770 goal thy "set(replicate (Suc n) x) = {x}"; |
722 by (induct_tac "n" 1); |
771 by (induct_tac "n" 1); |