equal
deleted
inserted
replaced
558 Addsimps [filter_False]; |
558 Addsimps [filter_False]; |
559 |
559 |
560 Goal "length (filter P xs) <= length xs"; |
560 Goal "length (filter P xs) <= length xs"; |
561 by (induct_tac "xs" 1); |
561 by (induct_tac "xs" 1); |
562 by Auto_tac; |
562 by Auto_tac; |
|
563 by (asm_simp_tac (simpset() addsimps [le_SucI]) 1); |
563 qed "length_filter"; |
564 qed "length_filter"; |
564 Addsimps[length_filter]; |
565 Addsimps[length_filter]; |
565 |
566 |
566 Goal "set (filter P xs) <= set xs"; |
567 Goal "set (filter P xs) <= set xs"; |
567 by Auto_tac; |
568 by Auto_tac; |