# HG changeset patch
# User nipkow
# Date 819631520 -3600
# Node ID a6a034a47a71ed0c947e8225c8791ed8b116331a
# Parent  f5f97ee67cbb7d41c24ebaade9143a30f3c599ea
defined take/drop by induction over list rather than nat.

diff -r f5f97ee67cbb -r a6a034a47a71 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Dec 22 11:09:28 1995 +0100
+++ b/src/HOL/List.ML	Fri Dec 22 12:25:20 1995 +0100
@@ -187,37 +187,31 @@
 
 (** drop **)
 
-goalw thy [drop_def] "drop 0 xs = xs";
-by(Simp_tac 1);
+goal thy "drop 0 xs = xs";
+by (list.induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "drop_0";
 
-goalw thy [drop_def] "drop (Suc n) (x#xs) = drop n xs";
+goal thy "drop (Suc n) (x#xs) = drop n xs";
 by(Simp_tac 1);
-qed "drop_Suc";
+qed "drop_Suc_Cons";
 
-goalw thy [drop_def] "drop n [] = []";
-by (nat_ind_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "drop_Nil";
-
-Addsimps [drop_0,drop_Suc,drop_Nil];
+Delsimps [drop_Cons];
+Addsimps [drop_0,drop_Suc_Cons];
 
 (** take **)
 
-goalw thy [take_def] "take 0 xs = []";
-by(Simp_tac 1);
+goal thy "take 0 xs = []";
+by (list.induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "take_0";
 
-goalw thy [take_def] "take (Suc n) (x#xs) = x # take n xs";
+goal thy "take (Suc n) (x#xs) = x # take n xs";
 by(Simp_tac 1);
-qed "take_Suc";
+qed "take_Suc_Cons";
 
-goalw thy [take_def] "take n [] = []";
-by (nat_ind_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "take_Nil";
-
-Addsimps [take_0,take_Suc,take_Nil];
+Delsimps [take_Cons];
+Addsimps [take_0,take_Suc_Cons];
 
 (** Additional mapping lemmas **)
 
diff -r f5f97ee67cbb -r a6a034a47a71 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Dec 22 11:09:28 1995 +0100
+++ b/src/HOL/List.thy	Fri Dec 22 12:25:20 1995 +0100
@@ -80,10 +80,12 @@
 primrec flat list
   flat_Nil  "flat([]) = []"
   flat_Cons "flat(x#xs) = x @ flat(xs)"
+primrec drop list
+  drop_Nil  "drop n [] = []"
+  drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
+primrec take list
+  take_Nil  "take n [] = []"
+  take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
 defs
-  drop_def "drop n == nat_rec n (%xs.xs)   \
-\	                (%m r xs. case xs of [] => [] | y#ys => r ys)"
-  take_def "take n == nat_rec n (%xs.[])   \
-\	                (%m r xs. case xs of [] => [] | y#ys => y # r ys)"
   nth_def  "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))"
 end