# HG changeset patch
# User nipkow
# Date 1540740673 -3600
# Node ID a5c0d61ce5dbfad0324005a2de22db9e67e8560d
# Parent  e0c32187916b9ffc4ded5745e76c431786d75ea4
added lemmas

diff -r e0c32187916b -r a5c0d61ce5db src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Oct 28 14:00:51 2018 +0100
+++ b/src/HOL/List.thy	Sun Oct 28 16:31:13 2018 +0100
@@ -4384,6 +4384,13 @@
 lemma nths_nil [simp]: "nths [] A = []"
 by (auto simp add: nths_def)
 
+lemma nths_all: "\<forall>i < length xs. i \<in> I \<Longrightarrow> nths xs I = xs"
+apply (simp add: nths_def)
+apply (subst filter_True)
+ apply (clarsimp simp: in_set_zip subset_iff)
+apply simp
+done
+
 lemma length_nths:
   "length (nths xs I) = card{i. i < length xs \<and> i \<in> I}"
 by(simp add: nths_def length_filter_conv_card cong:conj_cong)
@@ -4423,7 +4430,7 @@
 by(induction xs arbitrary: I) (simp_all add: nths_Cons)
 
 lemma set_nths: "set(nths xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
-  by (induct xs arbitrary: I) (auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
+by (induct xs arbitrary: I) (auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
 
 lemma set_nths_subset: "set(nths xs I) \<subseteq> set xs"
 by(auto simp add:set_nths)
@@ -4444,6 +4451,20 @@
 by (induct l rule: rev_induct)
    (simp_all split: nat_diff_split add: nths_append)
 
+lemma nths_nths: "nths (nths xs A) B = nths xs {i \<in> A. \<exists>j \<in> B. card {i' \<in> A. i' < i} = j}"
+apply(induction xs arbitrary: A B)
+apply(auto simp add: nths_Cons card_less_Suc card_less_Suc2)
+done
+
+lemma drop_eq_nths: "drop n xs = nths xs {i. i \<ge> n}"
+apply(induction xs arbitrary: n)
+apply (auto simp add: nths_Cons nths_all drop_Cons' intro: arg_cong2[where f=nths, OF refl])
+done
+
+lemma nths_drop: "nths (drop n xs) I = nths xs ((+) n ` I)"
+by(force simp: drop_eq_nths nths_nths simp flip: atLeastLessThan_iff
+         intro: arg_cong2[where f=nths, OF refl])
+
 lemma filter_eq_nths: "filter P xs = nths xs {i. i<length xs \<and> P(xs!i)}"
 by(induction xs) (auto simp: nths_Cons)