# HG changeset patch
# User nipkow
# Date 870688235 -7200
# Node ID 2ee1ed79c802c3535c0b8b5ce1c4e4894c479630
# Parent  5b2dcdc1829c974fc150471b2932d249a93cc6aa
Added a take/dropWhile lemma.

diff -r 5b2dcdc1829c -r 2ee1ed79c802 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Aug 01 10:59:19 1997 +0200
+++ b/src/HOL/List.ML	Mon Aug 04 11:50:35 1997 +0200
@@ -571,8 +571,14 @@
 
 section "takeWhile & dropWhile";
 
-goal thy
-  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
+goal thy "takeWhile P xs @ dropWhile P xs = xs";
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+qed "takeWhile_dropWhile_id";
+Addsimps [takeWhile_dropWhile_id];
+
+goal thy  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);