src/HOL/List.thy
changeset 46669 c1d2ab32174a
parent 46664 1f6c140f9c72
child 46698 f1dfcf8be88d
     1.1 --- a/src/HOL/List.thy	Fri Feb 24 22:46:44 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Feb 25 09:07:37 2012 +0100
     1.3 @@ -2342,12 +2342,8 @@
     1.4  by (simp add: list_all2_conv_all_nth)
     1.5  
     1.6  lemma list_all2_update_cong:
     1.7 -  "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
     1.8 -by (simp add: list_all2_conv_all_nth nth_list_update)
     1.9 -
    1.10 -lemma list_all2_update_cong2:
    1.11 -  "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
    1.12 -by (simp add: list_all2_lengthD list_all2_update_cong)
    1.13 +  "\<lbrakk> list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
    1.14 +by (cases "i < length ys") (auto simp add: list_all2_conv_all_nth nth_list_update)
    1.15  
    1.16  lemma list_all2_takeI [simp,intro?]:
    1.17    "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"