# HG changeset patch
# User nipkow
# Date 1266679238 -3600
# Node ID e649508742241e4191711684ee310121e91b8ab1
# Parent  0831bd85eee50d498befbfe9e09a21915a023f36
added lemma

diff -r 0831bd85eee5 -r e64950874224 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Feb 20 08:53:51 2010 +0100
+++ b/src/HOL/List.thy	Sat Feb 20 16:20:38 2010 +0100
@@ -1677,12 +1677,23 @@
 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
 by(simp add: hd_conv_nth)
 
+lemma set_take_subset_set_take:
+  "m <= n \<Longrightarrow> set(take m xs) <= set(take n xs)"
+by(induct xs arbitrary: m n)(auto simp:take_Cons split:nat.split)
+
 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
 
 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
 
+lemma set_drop_subset_set_drop:
+  "m >= n \<Longrightarrow> set(drop m xs) <= set(drop n xs)"
+apply(induct xs arbitrary: m n)
+apply(auto simp:drop_Cons split:nat.split)
+apply (metis set_drop_subset subset_iff)
+done
+
 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
 using set_take_subset by fast