src/HOL/List.ML
changeset 6408 5b443d6331ed
parent 6394 3d9fd50fcc43
child 6433 228237ec56e5
     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