new definition for nth.
authorpusch
Thu Apr 01 18:42:48 1999 +0200 (1999-04-01)
changeset 64085b443d6331ed
parent 6407 ec60d821f3f6
child 6409 41643761bef2
new definition for nth.
added warnings, if primrec definition is deleted from simpset.
src/HOL/List.ML
src/HOL/List.thy
     1.1 --- a/src/HOL/List.ML	Wed Mar 31 16:14:20 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Apr 01 18:42:48 1999 +0200
     1.3 @@ -570,15 +570,23 @@
     1.4  
     1.5  section "nth";
     1.6  
     1.7 -Goal "(x#xs)!n = (case n of 0 => x | Suc m => xs!m)";
     1.8 -by (simp_tac (simpset() addsplits [nat.split]) 1);
     1.9 -qed "nth_Cons";
    1.10 +Goal "(x#xs)!0 = x";
    1.11 +by Auto_tac;
    1.12 +qed "nth_Cons_0";
    1.13 +Addsimps [nth_Cons_0];
    1.14  
    1.15 -Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
    1.16 -by (induct_tac "n" 1);
    1.17 +Goal "(x#xs)!(Suc n) = xs!n";
    1.18 +by Auto_tac;
    1.19 +qed "nth_Cons_Suc";
    1.20 +Addsimps [nth_Cons_Suc];
    1.21 +
    1.22 +Delsimps (thms "nth.simps");
    1.23 +
    1.24 +Goal "!n. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
    1.25 +by (induct_tac "xs" 1);
    1.26   by (Asm_simp_tac 1);
    1.27   by (rtac allI 1);
    1.28 - by (exhaust_tac "xs" 1);
    1.29 + by (exhaust_tac "n" 1);
    1.30    by Auto_tac;
    1.31  qed_spec_mp "nth_append";
    1.32  
     2.1 --- a/src/HOL/List.thy	Wed Mar 31 16:14:20 1999 +0200
     2.2 +++ b/src/HOL/List.thy	Thu Apr 01 18:42:48 1999 +0200
     2.3 @@ -122,12 +122,17 @@
     2.4  primrec
     2.5    drop_Nil  "drop n [] = []"
     2.6    drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
     2.7 +  (* Warning: simpset does not contain this definition but separate theorems 
     2.8 +     for n=0 / n=Suc k*)
     2.9  primrec
    2.10    take_Nil  "take n [] = []"
    2.11    take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
    2.12 -primrec
    2.13 -  "xs!0 = hd xs"
    2.14 -  "xs!(Suc n) = (tl xs)!n"
    2.15 +  (* Warning: simpset does not contain this definition but separate theorems 
    2.16 +     for n=0 / n=Suc k*)
    2.17 +primrec 
    2.18 +  nth_Cons  "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
    2.19 +  (* Warning: simpset does not contain this definition but separate theorems 
    2.20 +     for n=0 / n=Suc k*)
    2.21  primrec
    2.22   "    [][i:=v] = []"
    2.23   "(x#xs)[i:=v] = (case i of 0     => v # xs 
    2.24 @@ -141,6 +146,8 @@
    2.25  primrec
    2.26    "zip xs []     = []"
    2.27    "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
    2.28 +  (* Warning: simpset does not contain this definition but separate theorems 
    2.29 +     for xs=[] / xs=z#zs *)
    2.30  primrec
    2.31    "[i..0(] = []"
    2.32    "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
    2.33 @@ -154,7 +161,7 @@
    2.34    replicate_0   "replicate  0      x = []"
    2.35    replicate_Suc "replicate (Suc n) x = x # replicate n x"
    2.36  
    2.37 -(** Lexcicographic orderings on lists **)
    2.38 +(** Lexicographic orderings on lists **)
    2.39  
    2.40  consts
    2.41   lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"