src/HOL/List.ML
changeset 4502 337c073de95e
parent 4423 a129b817b58a
child 4605 579e0ef2df6b
     1.1 --- a/src/HOL/List.ML	Mon Dec 29 21:39:22 1997 +0100
     1.2 +++ b/src/HOL/List.ML	Tue Dec 30 11:14:09 1997 +0100
     1.3 @@ -438,8 +438,7 @@
     1.4  section "nth";
     1.5  
     1.6  goal thy
     1.7 -  "!xs. nth n (xs@ys) = \
     1.8 -\          (if n < length xs then nth n xs else nth (n - length xs) ys)";
     1.9 +  "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
    1.10  by (nat_ind_tac "n" 1);
    1.11   by (Asm_simp_tac 1);
    1.12   by (rtac allI 1);
    1.13 @@ -450,7 +449,7 @@
    1.14   by (ALLGOALS Asm_simp_tac);
    1.15  qed_spec_mp "nth_append";
    1.16  
    1.17 -goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
    1.18 +goal thy "!n. n < length xs --> (map f xs)!n = f(xs!n)";
    1.19  by (induct_tac "xs" 1);
    1.20  (* case [] *)
    1.21  by (Asm_full_simp_tac 1);
    1.22 @@ -461,7 +460,7 @@
    1.23  qed_spec_mp "nth_map";
    1.24  Addsimps [nth_map];
    1.25  
    1.26 -goal thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
    1.27 +goal thy "!n. n < length xs --> list_all P xs --> P(xs!n)";
    1.28  by (induct_tac "xs" 1);
    1.29  (* case [] *)
    1.30  by (Simp_tac 1);
    1.31 @@ -471,7 +470,7 @@
    1.32  by (ALLGOALS Asm_full_simp_tac);
    1.33  qed_spec_mp "list_all_nth";
    1.34  
    1.35 -goal thy "!n. n < length xs --> (nth n xs) mem xs";
    1.36 +goal thy "!n. n < length xs --> xs!n mem xs";
    1.37  by (induct_tac "xs" 1);
    1.38  (* case [] *)
    1.39  by (Simp_tac 1);
    1.40 @@ -643,7 +642,7 @@
    1.41  by (ALLGOALS Asm_simp_tac);
    1.42  qed_spec_mp "drop_map";
    1.43  
    1.44 -goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
    1.45 +goal thy "!n i. i < n --> (take n xs)!i = xs!i";
    1.46  by (induct_tac "xs" 1);
    1.47   by (ALLGOALS Asm_simp_tac);
    1.48  by (Clarify_tac 1);
    1.49 @@ -654,7 +653,7 @@
    1.50  qed_spec_mp "nth_take";
    1.51  Addsimps [nth_take];
    1.52  
    1.53 -goal thy  "!xs i. n + i <= length xs --> nth i (drop n xs) = nth (n + i) xs";
    1.54 +goal thy  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
    1.55  by (nat_ind_tac "n" 1);
    1.56   by (ALLGOALS Asm_simp_tac);
    1.57  by (rtac allI 1);