src/HOL/List.thy
changeset 14187 26dfcd0ac436
parent 14111 993471c762b8
child 14208 144f45277d5a
     1.1 --- a/src/HOL/List.thy	Thu Sep 11 22:33:12 2003 +0200
     1.2 +++ b/src/HOL/List.thy	Sun Sep 14 17:53:27 2003 +0200
     1.3 @@ -737,10 +737,23 @@
     1.4  "!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
     1.5  by (induct xs) (auto split: nat.split)
     1.6  
     1.7 +lemma list_update_id[simp]: "!!i. i < length xs \<Longrightarrow> xs[i := xs!i] = xs"
     1.8 +apply(induct xs)
     1.9 + apply simp
    1.10 +apply(simp split:nat.splits)
    1.11 +done
    1.12 +
    1.13  lemma list_update_same_conv:
    1.14  "!!i. i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
    1.15  by (induct xs) (auto split: nat.split)
    1.16  
    1.17 +lemma list_update_append1:
    1.18 + "!!i. i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
    1.19 +apply(induct xs)
    1.20 + apply simp
    1.21 +apply(simp split:nat.split)
    1.22 +done
    1.23 +
    1.24  lemma update_zip:
    1.25  "!!i xy xs. length xs = length ys ==>
    1.26  (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
    1.27 @@ -796,6 +809,18 @@
    1.28  
    1.29  declare take_Cons [simp del] and drop_Cons [simp del]
    1.30  
    1.31 +lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
    1.32 +by(cases xs, simp_all)
    1.33 +
    1.34 +lemma drop_tl: "!!n. drop n (tl xs) = tl(drop n xs)"
    1.35 +by(induct xs, simp_all add:drop_Cons drop_Suc split:nat.split)
    1.36 +
    1.37 +lemma nth_via_drop: "!!n. drop n xs = y#ys \<Longrightarrow> xs!n = y"
    1.38 +apply(induct xs)
    1.39 + apply simp
    1.40 +apply(simp add:drop_Cons nth_Cons split:nat.splits)
    1.41 +done
    1.42 +
    1.43  lemma take_Suc_conv_app_nth:
    1.44   "!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
    1.45  apply(induct xs)
    1.46 @@ -905,6 +930,12 @@
    1.47  lemma set_drop_subset: "\<And>n. set(drop n xs) \<subseteq> set xs"
    1.48  by(induct xs)(auto simp:drop_Cons split:nat.split)
    1.49  
    1.50 +lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
    1.51 +using set_take_subset by fast
    1.52 +
    1.53 +lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
    1.54 +using set_drop_subset by fast
    1.55 +
    1.56  lemma append_eq_conv_conj:
    1.57  "!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
    1.58  apply(induct xs)