# HG changeset patch
# User nipkow
# Date 908358648 -7200
# Node ID 85fd64148873c329ddc7a13853283904ca1354c9
# Parent  983ce142121178f740d71bfc9f290d00927bce85
Nat: added zero_neq_conv
List: added nth/update lemmas.

diff -r 983ce1421211 -r 85fd64148873 src/HOL/List.ML
--- a/src/HOL/List.ML	Tue Oct 13 14:25:01 1998 +0200
+++ b/src/HOL/List.ML	Wed Oct 14 11:50:48 1998 +0200
@@ -570,6 +570,10 @@
 
 section "nth";
 
+Goal "(x#xs)!n = (case n of 0 => x | Suc m => xs!m)";
+by(simp_tac (simpset() addsplits [nat.split]) 1);
+qed "nth_Cons";
+
 Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
 by (induct_tac "n" 1);
  by (Asm_simp_tac 1);
@@ -625,9 +629,17 @@
 qed_spec_mp "length_list_update";
 Addsimps [length_list_update];
 
+Goal "!i j. i < length xs  --> (xs[i:=x])!j = (if i=j then x else 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";
+
 
 (** last & butlast **)
 
+section "last / butlast";
+
 Goal "last(xs@[x]) = x";
 by (induct_tac "xs" 1);
 by Auto_tac;
diff -r 983ce1421211 -r 85fd64148873 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Tue Oct 13 14:25:01 1998 +0200
+++ b/src/HOL/Nat.ML	Wed Oct 14 11:50:48 1998 +0200
@@ -38,6 +38,12 @@
 qed "neq0_conv";
 AddIffs [neq0_conv];
 
+Goal "(0 ~= n) = (0 < n)";
+by(exhaust_tac "n" 1);
+by(Auto_tac);
+qed "zero_neq_conv";
+AddIffs [zero_neq_conv];
+
 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);