src/HOL/List.thy
changeset 24796 529e458f84d2
parent 24748 ee0a0eb6b738
child 24902 49f002c3964e
     1.1 --- a/src/HOL/List.thy	Mon Oct 01 15:14:57 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Oct 01 19:21:32 2007 +0200
     1.3 @@ -1177,6 +1177,24 @@
     1.4  lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
     1.5  by (induct xs arbitrary: n) (auto split:nat.splits)
     1.6  
     1.7 +lemma list_update_overwrite:
     1.8 +  "xs [i := x, i := y] = xs [i := y]"
     1.9 +apply (induct xs arbitrary: i)
    1.10 +apply simp
    1.11 +apply (case_tac i)
    1.12 +apply simp_all
    1.13 +done
    1.14 +
    1.15 +lemma list_update_swap:
    1.16 +  "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
    1.17 +apply (induct xs arbitrary: i i')
    1.18 +apply simp
    1.19 +apply (case_tac i, case_tac i')
    1.20 +apply auto
    1.21 +apply (case_tac i')
    1.22 +apply auto
    1.23 +done
    1.24 +
    1.25  
    1.26  subsubsection {* @{text last} and @{text butlast} *}
    1.27  
    1.28 @@ -1237,6 +1255,7 @@
    1.29  lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
    1.30  by(induct xs)(auto simp:neq_Nil_conv)
    1.31  
    1.32 +
    1.33  subsubsection {* @{text take} and @{text drop} *}
    1.34  
    1.35  lemma take_0 [simp]: "take 0 xs = []"
    1.36 @@ -1437,6 +1456,16 @@
    1.37    finally show ?thesis .
    1.38  qed
    1.39  
    1.40 +lemma nth_drop':
    1.41 +  "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
    1.42 +apply (induct i arbitrary: xs)
    1.43 +apply (simp add: neq_Nil_conv)
    1.44 +apply (erule exE)+
    1.45 +apply simp
    1.46 +apply (case_tac xs)
    1.47 +apply simp_all
    1.48 +done
    1.49 +
    1.50  
    1.51  subsubsection {* @{text takeWhile} and @{text dropWhile} *}
    1.52  
    1.53 @@ -1982,6 +2011,10 @@
    1.54  apply (simp_all add: take_all)
    1.55  done
    1.56  
    1.57 +lemma map_nth:
    1.58 +  "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
    1.59 +  by (rule nth_equalityI, auto)
    1.60 +
    1.61  (* needs nth_equalityI *)
    1.62  lemma list_all2_antisym:
    1.63    "\<lbrakk> (\<And>x y. \<lbrakk>P x y; Q y x\<rbrakk> \<Longrightarrow> x = y); list_all2 P xs ys; list_all2 Q ys xs \<rbrakk> 
    1.64 @@ -2269,6 +2302,14 @@
    1.65  lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
    1.66  by (simp add: set_replicate_conv_if split: split_if_asm)
    1.67  
    1.68 +lemma replicate_append_same:
    1.69 +  "replicate i x @ [x] = x # replicate i x"
    1.70 +  by (induct i) simp_all
    1.71 +
    1.72 +lemma map_replicate_trivial:
    1.73 +  "map (\<lambda>i. x) [0..<i] = replicate i x"
    1.74 +  by (induct i) (simp_all add: replicate_append_same)
    1.75 +
    1.76  
    1.77  subsubsection{*@{text rotate1} and @{text rotate}*}
    1.78