# HG changeset patch
# User paulson
# Date 865246422 -7200
# Node ID 7707cb7a50546ddebddab7c1ca14ea381bab1a54
# Parent  8db8fc8607d917259d21bf9984f50198253277d6
Corrected statement of filter_append;  added filter_size

diff -r 8db8fc8607d9 -r 7707cb7a5054 src/HOL/List.ML
--- a/src/HOL/List.ML	Mon Jun 02 12:12:57 1997 +0200
+++ b/src/HOL/List.ML	Mon Jun 02 12:13:42 1997 +0200
@@ -175,7 +175,6 @@
 goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
 qed "set_of_list_append";
 Addsimps[set_of_list_append];
 
@@ -199,7 +198,6 @@
 goal thy "set_of_list(rev xs) = set_of_list(xs)";
 by(induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
-by(Blast_tac 1);
 qed "set_of_list_rev";
 Addsimps [set_of_list_rev];
 
@@ -233,12 +231,17 @@
 
 (** filter **)
 
-goal thy "[x:xs@ys . P] = [x:xs . P] @ [y:ys . P]";
+goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
 by(induct_tac "xs" 1);
  by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "filter_append";
 Addsimps [filter_append];
 
+goal thy "size (filter P xs) <= size xs";
+by(induct_tac "xs" 1);
+ by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+qed "filter_size";
+
 
 (** concat **)