src/HOL/List.ML
changeset 6433 228237ec56e5
parent 6408 5b443d6331ed
child 6451 bc943acc5fda
     1.1 --- a/src/HOL/List.ML	Wed Apr 14 19:07:39 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Apr 15 18:10:37 1999 +0200
     1.3 @@ -436,11 +436,31 @@
     1.4  qed "set_map";
     1.5  Addsimps [set_map];
     1.6  
     1.7 +Goal "set(filter P xs) = {x. x : set xs & P x}";
     1.8 +by(induct_tac "xs" 1);
     1.9 +by(Auto_tac);
    1.10 +qed "set_filter";
    1.11 +Addsimps [set_filter];
    1.12 +(*
    1.13  Goal "(x : set (filter P xs)) = (x : set xs & P x)";
    1.14  by (induct_tac "xs" 1);
    1.15  by Auto_tac;
    1.16  qed "in_set_filter";
    1.17  Addsimps [in_set_filter];
    1.18 +*)
    1.19 +Goal "set[i..j(] = {k. i <= k & k < j}";
    1.20 +by(induct_tac "j" 1);
    1.21 +by(Auto_tac);
    1.22 +by(arith_tac 1);
    1.23 +qed "set_upt";
    1.24 +Addsimps [set_upt];
    1.25 +
    1.26 +Goal "!i < size xs. set(xs[i := x]) <= insert x (set xs)";
    1.27 +by(induct_tac "xs" 1);
    1.28 + by(Simp_tac 1);
    1.29 +by(asm_simp_tac (simpset() addsplits [nat.split]) 1);
    1.30 +by(Blast_tac 1);
    1.31 +qed_spec_mp "set_list_update_subset";
    1.32  
    1.33  Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";
    1.34  by (induct_tac "xs" 1);
    1.35 @@ -643,6 +663,20 @@
    1.36  by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
    1.37  qed_spec_mp "nth_list_update";
    1.38  
    1.39 +Goal "!i. i < size xs --> xs[i:=x, i:=y] = xs[i:=y]";
    1.40 +by(induct_tac "xs" 1);
    1.41 + by(Simp_tac 1);
    1.42 +by(asm_simp_tac (simpset() addsplits [nat.split]) 1);
    1.43 +qed_spec_mp "list_update_overwrite";
    1.44 +Addsimps [list_update_overwrite];
    1.45 +
    1.46 +Goal "!i < length xs. (xs[i := x] = xs) = (xs!i = x)";
    1.47 +by(induct_tac "xs" 1);
    1.48 + by(Simp_tac 1);
    1.49 +by(simp_tac (simpset() addsplits [nat.split]) 1);
    1.50 +by(Blast_tac 1);
    1.51 +qed_spec_mp "list_update_same_conv";
    1.52 +
    1.53  
    1.54  (** last & butlast **)
    1.55  
    1.56 @@ -933,6 +967,43 @@
    1.57  qed_spec_mp "nth_upt";
    1.58  Addsimps [nth_upt];
    1.59  
    1.60 +Goal "!i. i+m <= n --> take m [i..n(] = [i..i+m(]";
    1.61 +by(induct_tac "m" 1);
    1.62 + by(Simp_tac 1);
    1.63 +by(Clarify_tac 1);
    1.64 +by(stac upt_rec 1);
    1.65 +br sym 1;
    1.66 +by(stac upt_rec 1);
    1.67 +by(asm_simp_tac (simpset() delsimps (thms"upt.simps")) 1);
    1.68 +qed_spec_mp "take_upt";
    1.69 +Addsimps [take_upt];
    1.70 +
    1.71 +Goal "!m i. i < n-m --> (map f [m..n(]) ! i = f(m+i)";
    1.72 +by(induct_tac "n" 1);
    1.73 + by(Simp_tac 1);
    1.74 +by(Clarify_tac 1);
    1.75 +by(subgoal_tac "m < Suc n" 1);
    1.76 + by(arith_tac 2);
    1.77 +by(stac upt_rec 1);
    1.78 +by(asm_simp_tac (simpset() delsplits [split_if]) 1);
    1.79 +by(split_tac [split_if] 1);
    1.80 +br conjI 1;
    1.81 + by(simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
    1.82 + by(simp_tac (simpset() addsimps [nth_append] addsplits [nat.split]) 1);
    1.83 + by(Clarify_tac 1);
    1.84 + br conjI 1;
    1.85 +  by(Clarify_tac 1);
    1.86 +  by(subgoal_tac "Suc(m+nat) < n" 1);
    1.87 +   by(arith_tac 2);
    1.88 +  by(Asm_simp_tac 1);
    1.89 + by(Clarify_tac 1);
    1.90 + by(subgoal_tac "n = Suc(m+nat)" 1);
    1.91 +  by(arith_tac 2);
    1.92 + by(Asm_simp_tac 1);
    1.93 +by(simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
    1.94 +by(arith_tac 1);
    1.95 +qed_spec_mp "nth_map_upt";
    1.96 +
    1.97  
    1.98  (** nodups & remdups **)
    1.99  section "nodups & remdups";