added rev_take and rev_drop
authornipkow
Mon Apr 29 11:29:34 2002 +0200 (2002-04-29)
changeset 1309604f8cbd1b500
parent 13095 8ed413a57bdc
child 13097 c9c7f23d0ceb
added rev_take and rev_drop
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Fri Apr 26 11:47:01 2002 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Apr 29 11:29:34 2002 +0200
     1.3 @@ -896,6 +896,20 @@
     1.4   by Auto_tac;
     1.5  qed_spec_mp "drop_map";
     1.6  
     1.7 +Goal "!i. rev (take i xs) = drop (length xs - i) (rev xs)";
     1.8 +by(induct_tac "xs" 1);
     1.9 + by Auto_tac;
    1.10 +by (case_tac "i" 1);
    1.11 + by Auto_tac;
    1.12 +qed_spec_mp "rev_take";
    1.13 +
    1.14 +Goal "!i. rev (drop i xs) = take (length xs - i) (rev xs)";
    1.15 +by(induct_tac "xs" 1);
    1.16 + by Auto_tac;
    1.17 +by (case_tac "i" 1);
    1.18 + by Auto_tac;
    1.19 +qed_spec_mp "rev_drop";
    1.20 +
    1.21  Goal "!n i. i < n --> (take n xs)!i = xs!i";
    1.22  by (induct_tac "xs" 1);
    1.23   by Auto_tac;