src/HOL/List.ML
changeset 5077 71043526295f
parent 5043 3fdc881e8ff9
child 5122 229190f9f303
     1.1 --- a/src/HOL/List.ML	Wed Jun 24 11:24:52 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Wed Jun 24 13:59:45 1998 +0200
     1.3 @@ -537,6 +537,18 @@
     1.4  qed_spec_mp "nth_mem";
     1.5  Addsimps [nth_mem];
     1.6  
     1.7 +(** list update **)
     1.8 +
     1.9 +section "list update";
    1.10 +
    1.11 +Goal "!i. length(xs[i:=x]) = length xs";
    1.12 +by (induct_tac "xs" 1);
    1.13 +by (Simp_tac 1);
    1.14 +by (asm_full_simp_tac (simpset() addsplits [split_nat_case]) 1);
    1.15 +qed_spec_mp "length_list_update";
    1.16 +Addsimps [length_list_update];
    1.17 +
    1.18 +
    1.19  (** last & butlast **)
    1.20  
    1.21  Goal "last(xs@[x]) = x";