# HG changeset patch
# User kleing
# Date 1072157741 -3600
# Node ID 91b897b9a2dc06655e7c17e0443d0345edfeb8d5
# Parent  d3e98d53533c3259fd56757f7a01a85b7b6f34e5
added some [intro?] and [trans] for list_all2 lemmas

diff -r d3e98d53533c -r 91b897b9a2dc src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Dec 22 22:52:38 2003 +0100
+++ b/src/HOL/List.thy	Tue Dec 23 06:35:41 2003 +0100
@@ -1039,7 +1039,8 @@
 
 subsection {* @{text list_all2} *}
 
-lemma list_all2_lengthD: "list_all2 P xs ys ==> length xs = length ys"
+lemma list_all2_lengthD [intro?]: 
+  "list_all2 P xs ys ==> length xs = length ys"
 by (simp add: list_all2_def)
 
 lemma list_all2_Nil [iff]: "list_all2 P [] ys = (ys = [])"
@@ -1124,7 +1125,7 @@
   "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
   by (simp add: list_all2_conv_all_nth)
 
-lemma list_all2_nthD [dest?]:
+lemma list_all2_nthD [intro?]:
   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   by (simp add: list_all2_conv_all_nth)
 
@@ -1140,7 +1141,7 @@
   "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
   by (auto simp add: list_all2_conv_all_nth)
 
-lemma list_all2_refl:
+lemma list_all2_refl [intro?]:
   "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
   by (simp add: list_all2_conv_all_nth)
 
@@ -1168,7 +1169,7 @@
   apply (case_tac n, simp, simp)
   done
 
-lemma list_all2_mono [intro?]:
+lemma list_all2_mono [trans, intro?]:
   "\<And>y. list_all2 P x y \<Longrightarrow> (\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> list_all2 Q x y"
   apply (induct x, simp)
   apply (case_tac y, auto)