Added a take/dropWhile lemma.
authornipkow
Mon Aug 04 11:50:35 1997 +0200 (1997-08-04)
changeset 35862ee1ed79c802
parent 3585 5b2dcdc1829c
child 3587 00ea30ea0734
Added a take/dropWhile lemma.
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Fri Aug 01 10:59:19 1997 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Aug 04 11:50:35 1997 +0200
     1.3 @@ -571,8 +571,14 @@
     1.4  
     1.5  section "takeWhile & dropWhile";
     1.6  
     1.7 -goal thy
     1.8 -  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
     1.9 +goal thy "takeWhile P xs @ dropWhile P xs = xs";
    1.10 +by (induct_tac "xs" 1);
    1.11 + by (Simp_tac 1);
    1.12 +by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    1.13 +qed "takeWhile_dropWhile_id";
    1.14 +Addsimps [takeWhile_dropWhile_id];
    1.15 +
    1.16 +goal thy  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
    1.17  by (induct_tac "xs" 1);
    1.18   by (Simp_tac 1);
    1.19  by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);