Added "nth" and some lemmas.

--- a/List.ML	Wed Dec 14 11:17:18 1994 +0100
+++ b/List.ML	Thu Jan 26 10:41:21 1995 +0100
@@ -50,6 +50,11 @@
 by(ALLGOALS(asm_simp_tac list_ss));
 qed "append_Nil2";
 
+goal List.thy "(xs@ys = []) = (xs=[] & ys=[])";
+by (list.induct_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac list_ss));
+qed "append_is_Nil";
+
 (** mem **)
 
 goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
@@ -91,6 +96,11 @@
 by(fast_tac HOL_cs 1);
 qed "expand_list_case";
 
+(** nth **)
+
+val [nth_0,nth_Suc] = nat_recs nth_def; 
+store_thm("nth_0",nth_0);
+store_thm("nth_Suc",nth_Suc);
 
 (** Additional mapping lemmas **)
 
@@ -110,7 +120,8 @@
 qed "map_compose";
 
 val list_ss = list_ss addsimps
-  [not_Cons_self, append_assoc, append_Nil2, mem_append, mem_filter,
+  [not_Cons_self, append_assoc, append_Nil2, append_is_Nil,
+   mem_append, mem_filter,
    map_ident, map_append, map_compose,
-   list_all_True, list_all_conj];
+   list_all_True, list_all_conj, nth_0, nth_Suc];
 

--- a/List.thy	Wed Dec 14 11:17:18 1994 +0100
+++ b/List.thy	Thu Jan 26 10:41:21 1995 +0100
@@ -23,6 +23,7 @@
   filter    :: "['a => bool, 'a list] => 'a list"
   foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
   length    :: "'a list => nat"
+  nth       :: "[nat, 'a list] => 'a"
 
 syntax
   (* list Enumeration *)
@@ -73,4 +74,6 @@
 primrec length list
   length_Nil  "length([]) = 0"
   length_Cons "length(x#xs) = Suc(length(xs))"
+defs
+  nth_def "nth(n) == nat_rec(n, hd, %m r xs. r(tl(xs)))"
 end