equal
deleted
inserted
replaced
4382 by (auto simp add: nths_def) 
4382 by (auto simp add: nths_def) 
4383 
4383 
4384 lemma nths_nil [simp]: "nths [] A = []" 
4384 lemma nths_nil [simp]: "nths [] A = []" 
4385 by (auto simp add: nths_def) 
4385 by (auto simp add: nths_def) 
4386 
4386 

4387 lemma nths_all: "\<forall>i < length xs. i \<in> I \<Longrightarrow> nths xs I = xs" 

4388 apply (simp add: nths_def) 

4389 apply (subst filter_True) 

4390 apply (clarsimp simp: in_set_zip subset_iff) 

4391 apply simp 

4392 done 

4393 
4387 lemma length_nths: 
4394 lemma length_nths: 
4388 "length (nths xs I) = card{i. i < length xs \<and> i \<in> I}" 
4395 "length (nths xs I) = card{i. i < length xs \<and> i \<in> I}" 
4389 by(simp add: nths_def length_filter_conv_card cong:conj_cong) 
4396 by(simp add: nths_def length_filter_conv_card cong:conj_cong) 
4390 
4397 
4391 lemma nths_shift_lemma_Suc: 
4398 lemma nths_shift_lemma_Suc: 
4421 
4428 
4422 lemma nths_map: "nths (map f xs) I = map f (nths xs I)" 
4429 lemma nths_map: "nths (map f xs) I = map f (nths xs I)" 
4423 by(induction xs arbitrary: I) (simp_all add: nths_Cons) 
4430 by(induction xs arbitrary: I) (simp_all add: nths_Cons) 
4424 
4431 
4425 lemma set_nths: "set(nths xs I) = {xs!ii. i<size xs \<and> i \<in> I}" 
4432 lemma set_nths: "set(nths xs I) = {xs!ii. i<size xs \<and> i \<in> I}" 
4426 by (induct xs arbitrary: I) (auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc) 
4433 by (induct xs arbitrary: I) (auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc) 
4427 
4434 
4428 lemma set_nths_subset: "set(nths xs I) \<subseteq> set xs" 
4435 lemma set_nths_subset: "set(nths xs I) \<subseteq> set xs" 
4429 by(auto simp add:set_nths) 
4436 by(auto simp add:set_nths) 
4430 
4437 
4431 lemma notin_set_nthsI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(nths xs I)" 
4438 lemma notin_set_nthsI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(nths xs I)" 
4441 by (induct xs arbitrary: I) (auto simp: nths_Cons) 
4448 by (induct xs arbitrary: I) (auto simp: nths_Cons) 
4442 
4449 
4443 lemma nths_upt_eq_take [simp]: "nths l {..<n} = take n l" 
4450 lemma nths_upt_eq_take [simp]: "nths l {..<n} = take n l" 
4444 by (induct l rule: rev_induct) 
4451 by (induct l rule: rev_induct) 
4445 (simp_all split: nat_diff_split add: nths_append) 
4452 (simp_all split: nat_diff_split add: nths_append) 

4453 

4454 lemma nths_nths: "nths (nths xs A) B = nths xs {i \<in> A. \<exists>j \<in> B. card {i' \<in> A. i' < i} = j}" 

4455 apply(induction xs arbitrary: A B) 

4456 apply(auto simp add: nths_Cons card_less_Suc card_less_Suc2) 

4457 done 

4458 

4459 lemma drop_eq_nths: "drop n xs = nths xs {i. i \<ge> n}" 

4460 apply(induction xs arbitrary: n) 

4461 apply (auto simp add: nths_Cons nths_all drop_Cons' intro: arg_cong2[where f=nths, OF refl]) 

4462 done 

4463 

4464 lemma nths_drop: "nths (drop n xs) I = nths xs ((+) n ` I)" 

4465 by(force simp: drop_eq_nths nths_nths simp flip: atLeastLessThan_iff 

4466 intro: arg_cong2[where f=nths, OF refl]) 
4446 
4467 
4447 lemma filter_eq_nths: "filter P xs = nths xs {i. i<length xs \<and> P(xs!i)}" 
4468 lemma filter_eq_nths: "filter P xs = nths xs {i. i<length xs \<and> P(xs!i)}" 
4448 by(induction xs) (auto simp: nths_Cons) 
4469 by(induction xs) (auto simp: nths_Cons) 
4449 
4470 
4450 lemma filter_in_nths: 
4471 lemma filter_in_nths: 