# 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 **)