src/HOL/List.thy
changeset 69206 a5c0d61ce5db
parent 69140 f2d233f6356c
child 69220 ab94035ba6ea
equal deleted inserted replaced
69205:e0c32187916b 69206:a5c0d61ce5db
  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!i|i. i<size xs \<and> i \<in> I}"
  4432 lemma set_nths: "set(nths xs I) = {xs!i|i. 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: