# HG changeset patch
# User pusch
# Date 922984968 -7200
# Node ID 5b443d6331ed2ec5d37c0f28ebeaab2f257a4384
# Parent  ec60d821f3f6194406caad3b31714d2811a982e9
new definition for nth.
added warnings, if primrec definition is deleted from simpset.

diff -r ec60d821f3f6 -r 5b443d6331ed src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Mar 31 16:14:20 1999 +0200
+++ b/src/HOL/List.ML	Thu Apr 01 18:42:48 1999 +0200
@@ -570,15 +570,23 @@
 
 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 "(x#xs)!0 = x";
+by Auto_tac;
+qed "nth_Cons_0";
+Addsimps [nth_Cons_0];
 
-Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
-by (induct_tac "n" 1);
+Goal "(x#xs)!(Suc n) = xs!n";
+by Auto_tac;
+qed "nth_Cons_Suc";
+Addsimps [nth_Cons_Suc];
+
+Delsimps (thms "nth.simps");
+
+Goal "!n. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
+by (induct_tac "xs" 1);
  by (Asm_simp_tac 1);
  by (rtac allI 1);
- by (exhaust_tac "xs" 1);
+ by (exhaust_tac "n" 1);
   by Auto_tac;
 qed_spec_mp "nth_append";
 
diff -r ec60d821f3f6 -r 5b443d6331ed src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Mar 31 16:14:20 1999 +0200
+++ b/src/HOL/List.thy	Thu Apr 01 18:42:48 1999 +0200
@@ -122,12 +122,17 @@
 primrec
   drop_Nil  "drop n [] = []"
   drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
+  (* Warning: simpset does not contain this definition but separate theorems 
+     for n=0 / n=Suc k*)
 primrec
   take_Nil  "take n [] = []"
   take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
-primrec
-  "xs!0 = hd xs"
-  "xs!(Suc n) = (tl xs)!n"
+  (* Warning: simpset does not contain this definition but separate theorems 
+     for n=0 / n=Suc k*)
+primrec 
+  nth_Cons  "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
+  (* Warning: simpset does not contain this definition but separate theorems 
+     for n=0 / n=Suc k*)
 primrec
  "    [][i:=v] = []"
  "(x#xs)[i:=v] = (case i of 0     => v # xs 
@@ -141,6 +146,8 @@
 primrec
   "zip xs []     = []"
   "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
+  (* Warning: simpset does not contain this definition but separate theorems 
+     for xs=[] / xs=z#zs *)
 primrec
   "[i..0(] = []"
   "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
@@ -154,7 +161,7 @@
   replicate_0   "replicate  0      x = []"
   replicate_Suc "replicate (Suc n) x = x # replicate n x"
 
-(** Lexcicographic orderings on lists **)
+(** Lexicographic orderings on lists **)
 
 consts
  lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"