src/HOL/List.ML
changeset 4605 579e0ef2df6b
parent 4502 337c073de95e
child 4628 0c7e97836e3c
     1.1 --- a/src/HOL/List.ML	Fri Feb 06 11:18:29 1998 +0100
     1.2 +++ b/src/HOL/List.ML	Fri Feb 06 18:55:18 1998 +0100
     1.3 @@ -350,6 +350,19 @@
     1.4  qed "set_map";
     1.5  Addsimps [set_map];
     1.6  
     1.7 +goal thy "set(map f xs) = f``(set xs)";
     1.8 +by (induct_tac "xs" 1);
     1.9 +by (ALLGOALS Asm_simp_tac);
    1.10 +qed "set_map";
    1.11 +Addsimps [set_map];
    1.12 +
    1.13 +goal thy "(x : set(filter P xs)) = (x : set xs & P x)";
    1.14 +by (induct_tac "xs" 1);
    1.15 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.16 +by(Blast_tac 1);
    1.17 +qed "in_set_filter";
    1.18 +Addsimps [in_set_filter];
    1.19 +
    1.20  
    1.21  (** list_all **)
    1.22  
    1.23 @@ -384,10 +397,22 @@
    1.24  qed "filter_append";
    1.25  Addsimps [filter_append];
    1.26  
    1.27 -goal thy "size (filter P xs) <= size xs";
    1.28 +goal thy "filter (%x. True) xs = xs";
    1.29 +by (induct_tac "xs" 1);
    1.30 +by (ALLGOALS Asm_simp_tac);
    1.31 +qed "filter_True";
    1.32 +Addsimps [filter_True];
    1.33 +
    1.34 +goal thy "filter (%x. False) xs = []";
    1.35 +by (induct_tac "xs" 1);
    1.36 +by (ALLGOALS Asm_simp_tac);
    1.37 +qed "filter_False";
    1.38 +Addsimps [filter_False];
    1.39 +
    1.40 +goal thy "length (filter P xs) <= length xs";
    1.41  by (induct_tac "xs" 1);
    1.42   by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.43 -qed "filter_size";
    1.44 +qed "length_filter";
    1.45  
    1.46  
    1.47  (** concat **)
    1.48 @@ -715,6 +740,30 @@
    1.49  qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
    1.50  qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" 
    1.51  						      (K [Simp_tac 1]);
    1.52 +
    1.53 +(** nodups & remdups **)
    1.54 +section "nodups & remdups";
    1.55 +
    1.56 +goal thy "set(remdups xs) = set xs";
    1.57 +by (induct_tac "xs" 1);
    1.58 + by (Simp_tac 1);
    1.59 +by (asm_full_simp_tac (simpset() addsimps [insert_absorb]
    1.60 +                                 addsplits [expand_if]) 1);
    1.61 +qed "set_remdups";
    1.62 +Addsimps [set_remdups];
    1.63 +
    1.64 +goal thy "nodups(remdups xs)";
    1.65 +by (induct_tac "xs" 1);
    1.66 + by (Simp_tac 1);
    1.67 +by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
    1.68 +qed "nodups_remdups";
    1.69 +
    1.70 +goal thy "nodups xs --> nodups (filter P xs)";
    1.71 +by (induct_tac "xs" 1);
    1.72 + by (Simp_tac 1);
    1.73 +by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
    1.74 +qed_spec_mp "nodups_filter";
    1.75 +
    1.76  (** replicate **)
    1.77  section "replicate";
    1.78