# HG changeset patch
# User Andreas Lochbihler
# Date 1403615158 -7200
# Node ID e02fcb7e63c377e6842c529434f784b1a78060a1
# Parent  7e22d7b75e2af2d8db6d3a36837fa6ff6ef2623c
add lemma

diff -r 7e22d7b75e2a -r e02fcb7e63c3 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jun 24 12:36:45 2014 +0200
+++ b/src/HOL/List.thy	Tue Jun 24 15:05:58 2014 +0200
@@ -2708,6 +2708,8 @@
   "xs = ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x,y) \<in> set (zip xs ys). x = y)"
 by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
 
+lemma list_all2_same: "list_all2 P xs xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x x)"
+by(auto simp add: list_all2_conv_all_nth set_conv_nth)
 
 subsubsection {* @{const List.product} and @{const product_lists} *}