optimized xs[i:=x]!j lemmas.
authornipkow
Wed Jan 26 11:04:38 2000 +0100 (2000-01-26)
changeset 8144c4b5cbfb90dd
parent 8143 b0e44ab73631
child 8145 cdd5386eb6fe
optimized xs[i:=x]!j lemmas.
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Tue Jan 25 22:31:53 2000 +0100
     1.2 +++ b/src/HOL/List.ML	Wed Jan 26 11:04:38 2000 +0100
     1.3 @@ -705,6 +705,18 @@
     1.4  by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
     1.5  qed_spec_mp "nth_list_update";
     1.6  
     1.7 +Goal "i < length xs  ==> (xs[i:=x])!i = x";
     1.8 +by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
     1.9 +qed "nth_list_update_eq";
    1.10 +Addsimps [nth_list_update_eq];
    1.11 +
    1.12 +Goal "!i j. i ~= j --> xs[i:=x]!j = xs!j";
    1.13 +by (induct_tac "xs" 1);
    1.14 + by (Simp_tac 1);
    1.15 +by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
    1.16 +qed_spec_mp "nth_list_update_neq";
    1.17 +Addsimps [nth_list_update_neq];
    1.18 +
    1.19  Goal "!i. i < size xs --> xs[i:=x, i:=y] = xs[i:=y]";
    1.20  by (induct_tac "xs" 1);
    1.21   by (Simp_tac 1);