src/HOL/List.thy
 changeset 6408 5b443d6331ed parent 6306 81e7fbf61db2 child 7032 d6efb3b8e669
```     1.1 --- a/src/HOL/List.thy	Wed Mar 31 16:14:20 1999 +0200
1.2 +++ b/src/HOL/List.thy	Thu Apr 01 18:42:48 1999 +0200
1.3 @@ -122,12 +122,17 @@
1.4  primrec
1.5    drop_Nil  "drop n [] = []"
1.6    drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
1.7 +  (* Warning: simpset does not contain this definition but separate theorems
1.8 +     for n=0 / n=Suc k*)
1.9  primrec
1.10    take_Nil  "take n [] = []"
1.11    take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
1.12 -primrec
1.13 -  "xs!0 = hd xs"
1.14 -  "xs!(Suc n) = (tl xs)!n"
1.15 +  (* Warning: simpset does not contain this definition but separate theorems
1.16 +     for n=0 / n=Suc k*)
1.17 +primrec
1.18 +  nth_Cons  "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
1.19 +  (* Warning: simpset does not contain this definition but separate theorems
1.20 +     for n=0 / n=Suc k*)
1.21  primrec
1.22   "    [][i:=v] = []"
1.23   "(x#xs)[i:=v] = (case i of 0     => v # xs
1.24 @@ -141,6 +146,8 @@
1.25  primrec
1.26    "zip xs []     = []"
1.27    "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
1.28 +  (* Warning: simpset does not contain this definition but separate theorems
1.29 +     for xs=[] / xs=z#zs *)
1.30  primrec
1.31    "[i..0(] = []"
1.32    "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
1.33 @@ -154,7 +161,7 @@
1.34    replicate_0   "replicate  0      x = []"
1.35    replicate_Suc "replicate (Suc n) x = x # replicate n x"
1.36
1.37 -(** Lexcicographic orderings on lists **)
1.38 +(** Lexicographic orderings on lists **)
1.39
1.40  consts
1.41   lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
```