# HG changeset patch
# User bulwahn
# Date 1330157257 -3600
# Node ID c1d2ab32174abb6ed05e8aba587fce2d564cbe96
# Parent  1f6c140f9c72e0a0047064255e92e6a19c34a710
one general list_all2_update_cong instead of two special ones

diff -r 1f6c140f9c72 -r c1d2ab32174a src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 24 22:46:44 2012 +0100
+++ b/src/HOL/List.thy	Sat Feb 25 09:07:37 2012 +0100
@@ -2342,12 +2342,8 @@
 by (simp add: list_all2_conv_all_nth)
 
 lemma list_all2_update_cong:
-  "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
-by (simp add: list_all2_conv_all_nth nth_list_update)
-
-lemma list_all2_update_cong2:
-  "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
-by (simp add: list_all2_lengthD list_all2_update_cong)
+  "\<lbrakk> list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
+by (cases "i < length ys") (auto simp add: list_all2_conv_all_nth nth_list_update)
 
 lemma list_all2_takeI [simp,intro?]:
   "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"