# HG changeset patch
# User nipkow
# Date 948881078 -3600
# Node ID c4b5cbfb90dd1852878295d21c596b3cadf60686
# Parent  b0e44ab7363152f8d90fadc8b54616e5b879aff0
optimized xs[i:=x]!j lemmas.

diff -r b0e44ab73631 -r c4b5cbfb90dd src/HOL/List.ML
--- a/src/HOL/List.ML	Tue Jan 25 22:31:53 2000 +0100
+++ b/src/HOL/List.ML	Wed Jan 26 11:04:38 2000 +0100
@@ -705,6 +705,18 @@
 by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
 qed_spec_mp "nth_list_update";
 
+Goal "i < length xs  ==> (xs[i:=x])!i = x";
+by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
+qed "nth_list_update_eq";
+Addsimps [nth_list_update_eq];
+
+Goal "!i j. i ~= j --> xs[i:=x]!j = xs!j";
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
+qed_spec_mp "nth_list_update_neq";
+Addsimps [nth_list_update_neq];
+
 Goal "!i. i < size xs --> xs[i:=x, i:=y] = xs[i:=y]";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);