# HG changeset patch
# User nipkow
# Date 816190152 -3600
# Node ID 6c29cfab679c90140b68f9df63dfebb4cb2b740a
# Parent  1fbf9407757c3bd771ce752a22896c071997db19
added new arithmetic lemmas and the functions take and drop.

diff -r 1fbf9407757c -r 6c29cfab679c src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Sun Nov 12 13:14:13 1995 +0100
+++ b/src/HOL/Arith.ML	Sun Nov 12 16:29:12 1995 +0100
@@ -94,6 +94,21 @@
 by (Asm_simp_tac 1);
 qed "add_left_cancel_less";
 
+Addsimps [add_left_cancel, add_right_cancel,
+          add_left_cancel_le, add_left_cancel_less];
+
+goal Arith.thy "(m+n = 0) = (m=0 & n=0)";
+by (nat_ind_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_is_0";
+Addsimps [add_is_0];
+
+goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
+by (nat_ind_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_pred";
+Addsimps [add_pred];
+
 (*** Multiplication ***)
 
 (*right annihilation in product*)
@@ -156,8 +171,6 @@
 goal Arith.thy "!!m::nat. m - n <= m";
 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (etac le_trans 1);
-by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
 qed "diff_le_self";
 
 goal Arith.thy "!!n::nat. (n+m) - n = m";
diff -r 1fbf9407757c -r 6c29cfab679c src/HOL/List.ML
--- a/src/HOL/List.ML	Sun Nov 12 13:14:13 1995 +0100
+++ b/src/HOL/List.ML	Sun Nov 12 16:29:12 1995 +0100
@@ -50,6 +50,10 @@
 by (ALLGOALS Asm_simp_tac);
 qed "same_append_eq";
 
+goal List.thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
+by (list.induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "hd_append";
 
 (** rev **)
 
@@ -181,6 +185,39 @@
 bind_thm ("nth_mem",result() RS spec RS mp);
 Addsimps [nth_mem];
 
+(** drop **)
+
+goalw thy [drop_def] "drop 0 xs = xs";
+by(Simp_tac 1);
+qed "drop_0";
+
+goalw thy [drop_def] "drop (Suc n) (x#xs) = drop n xs";
+by(Simp_tac 1);
+qed "drop_Suc";
+
+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];
+
+(** take **)
+
+goalw thy [take_def] "take 0 xs = []";
+by(Simp_tac 1);
+qed "take_0";
+
+goalw thy [take_def] "take (Suc n) (x#xs) = x # take n xs";
+by(Simp_tac 1);
+qed "take_Suc";
+
+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];
 
 (** Additional mapping lemmas **)
 
diff -r 1fbf9407757c -r 6c29cfab679c src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Nov 12 13:14:13 1995 +0100
+++ b/src/HOL/List.thy	Sun Nov 12 16:29:12 1995 +0100
@@ -13,19 +13,20 @@
 
 consts
 
-  null      :: "'a list => bool"
+  "@"	    :: "['a list, 'a list] => 'a list"		(infixr 65)
+  drop      :: "[nat, 'a list] => 'a list"
+  filter    :: "['a => bool, 'a list] => 'a list"
+  flat      :: "'a list list => 'a list"
+  foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
   hd        :: "'a list => 'a"
-  tl,ttl    :: "'a list => 'a list"
-  mem       :: "['a, 'a list] => bool"			(infixl 55)
+  length    :: "'a list => nat"
   list_all  :: "('a => bool) => ('a list => bool)"
   map       :: "('a=>'b) => ('a list => 'b list)"
-  "@"	    :: "['a list, 'a list] => 'a list"		(infixr 65)
+  mem       :: "['a, 'a list] => bool"			(infixl 55)
+  nth       :: "[nat, 'a list] => 'a"
+  take      :: "[nat, 'a list] => 'a list"
+  tl,ttl    :: "'a list => 'a list"
   rev       :: "'a list => 'a list"
-  filter    :: "['a => bool, 'a list] => 'a list"
-  foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
-  length    :: "'a list => nat"
-  flat      :: "'a list list => 'a list"
-  nth       :: "[nat, 'a list] => 'a"
 
 syntax
   (* list Enumeration *)
@@ -42,9 +43,6 @@
   "[x:xs . P]"	== "filter (%x.P) xs"
   "Alls x:xs.P"	== "list_all (%x.P) xs"
 
-primrec null list
-  null_Nil "null([]) = True"
-  null_Cons "null(x#xs) = False"
 primrec hd list
   hd_Nil  "hd([]) = (@x.False)"
   hd_Cons "hd(x#xs) = x"
@@ -83,5 +81,9 @@
   flat_Nil  "flat([]) = []"
   flat_Cons "flat(x#xs) = x @ flat(xs)"
 defs
-  nth_def "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))"
+  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
diff -r 1fbf9407757c -r 6c29cfab679c src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Sun Nov 12 13:14:13 1995 +0100
+++ b/src/HOL/Nat.ML	Sun Nov 12 16:29:12 1995 +0100
@@ -412,6 +412,11 @@
 by(fast_tac HOL_cs 1);
 qed "Suc_leD";
 
+goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n";
+by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
+qed "le_SucI";
+Addsimps[le_SucI];
+
 goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)";
 by (fast_tac (HOL_cs addEs [less_asym]) 1);
 qed "less_imp_le";