# HG changeset patch
# User kuncar
# Date 1323436602 -3600
# Node ID 2373d86cf2e85fd4afaa7e4891f9b44ac8390d6e
# Parent  977cf00fb8d3b748a120691ca4a7eddbdc0dbbfa# Parent  16e8e4d33c426d5753459e8ec9dbf3b448b87b5e
merged

diff -r 977cf00fb8d3 -r 2373d86cf2e8 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Dec 09 14:14:37 2011 +0100
+++ b/src/HOL/List.thy	Fri Dec 09 14:16:42 2011 +0100
@@ -2202,6 +2202,15 @@
 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
 by (cases xs) auto
 
+lemma list_all2_induct
+  [consumes 1, case_names Nil Cons, induct set: list_all2]:
+  assumes P: "list_all2 P xs ys"
+  assumes Nil: "R [] []"
+  assumes Cons: "\<And>x xs y ys. \<lbrakk>P x y; R xs ys\<rbrakk> \<Longrightarrow> R (x # xs) (y # ys)"
+  shows "R xs ys"
+using P
+by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons)
+
 lemma list_all2_rev [iff]:
 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
 by (simp add: list_all2_def zip_rev cong: conj_cong)