src/HOL/List.thy
changeset 14302 6c24235e8d5d
parent 14300 bf8b8c9425c3
child 14316 91b897b9a2dc
     1.1 --- a/src/HOL/List.thy	Thu Dec 18 15:06:24 2003 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Dec 19 04:28:45 2003 +0100
     1.3 @@ -758,6 +758,23 @@
     1.4  lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
     1.5  by (induct xs) auto
     1.6  
     1.7 +lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
     1.8 +by(simp add:last.simps)
     1.9 +
    1.10 +lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
    1.11 +by(simp add:last.simps)
    1.12 +
    1.13 +lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
    1.14 +by (induct xs) (auto)
    1.15 +
    1.16 +lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
    1.17 +by(simp add:last_append)
    1.18 +
    1.19 +lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
    1.20 +by(simp add:last_append)
    1.21 +
    1.22 +
    1.23 +
    1.24  lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
    1.25  by (induct xs rule: rev_induct) auto
    1.26  
    1.27 @@ -1111,6 +1128,10 @@
    1.28    "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
    1.29    by (simp add: list_all2_conv_all_nth)
    1.30  
    1.31 +lemma list_all2_nthD2:
    1.32 +  "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
    1.33 +  by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
    1.34 +
    1.35  lemma list_all2_map1: 
    1.36    "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
    1.37    by (simp add: list_all2_conv_all_nth)
    1.38 @@ -1131,7 +1152,16 @@
    1.39    "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
    1.40    by (simp add: list_all2_lengthD list_all2_update_cong)
    1.41  
    1.42 -lemma list_all2_dropI [intro?]:
    1.43 +lemma list_all2_takeI [simp,intro?]:
    1.44 +  "\<And>n ys. list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
    1.45 +  apply (induct xs)
    1.46 +   apply simp
    1.47 +  apply (clarsimp simp add: list_all2_Cons1)
    1.48 +  apply (case_tac n)
    1.49 +  apply auto
    1.50 +  done
    1.51 +
    1.52 +lemma list_all2_dropI [simp,intro?]:
    1.53    "\<And>n bs. list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
    1.54    apply (induct as, simp)
    1.55    apply (clarsimp simp add: list_all2_Cons1)