src/HOL/List.ML
changeset 8287 42911a6bb13f
parent 8254 84a5fe44520f
child 8423 3c19160b6432
     1.1 --- a/src/HOL/List.ML	Wed Feb 23 10:45:08 2000 +0100
     1.2 +++ b/src/HOL/List.ML	Thu Feb 24 08:55:37 2000 +0100
     1.3 @@ -485,13 +485,6 @@
     1.4  qed "set_upt";
     1.5  Addsimps [set_upt];
     1.6  
     1.7 -Goal "!i < size xs. set(xs[i := x]) <= insert x (set xs)";
     1.8 -by (induct_tac "xs" 1);
     1.9 - by (Simp_tac 1);
    1.10 -by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
    1.11 -by (Blast_tac 1);
    1.12 -qed_spec_mp "set_list_update_subset";
    1.13 -
    1.14  Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";
    1.15  by (induct_tac "xs" 1);
    1.16   by (Simp_tac 1);
    1.17 @@ -744,8 +737,11 @@
    1.18   by (asm_full_simp_tac (simpset() addsimps []) 1);
    1.19  by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);
    1.20  by (Fast_tac  1);
    1.21 -qed_spec_mp "set_update_subset";
    1.22 +qed_spec_mp "set_update_subset_insert";
    1.23  
    1.24 +Goal "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A";
    1.25 +by(fast_tac (claset() addSDs [set_update_subset_insert RS subsetD]) 1);
    1.26 +qed "set_update_subsetI";
    1.27  
    1.28  (** last & butlast **)
    1.29