added some [intro?] and [trans] for list_all2 lemmas
authorkleing
Tue Dec 23 06:35:41 2003 +0100 (2003-12-23)
changeset 1431691b897b9a2dc
parent 14315 d3e98d53533c
child 14317 85125b18d38a
added some [intro?] and [trans] for list_all2 lemmas
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Mon Dec 22 22:52:38 2003 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Dec 23 06:35:41 2003 +0100
     1.3 @@ -1039,7 +1039,8 @@
     1.4  
     1.5  subsection {* @{text list_all2} *}
     1.6  
     1.7 -lemma list_all2_lengthD: "list_all2 P xs ys ==> length xs = length ys"
     1.8 +lemma list_all2_lengthD [intro?]: 
     1.9 +  "list_all2 P xs ys ==> length xs = length ys"
    1.10  by (simp add: list_all2_def)
    1.11  
    1.12  lemma list_all2_Nil [iff]: "list_all2 P [] ys = (ys = [])"
    1.13 @@ -1124,7 +1125,7 @@
    1.14    "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
    1.15    by (simp add: list_all2_conv_all_nth)
    1.16  
    1.17 -lemma list_all2_nthD [dest?]:
    1.18 +lemma list_all2_nthD [intro?]:
    1.19    "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
    1.20    by (simp add: list_all2_conv_all_nth)
    1.21  
    1.22 @@ -1140,7 +1141,7 @@
    1.23    "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
    1.24    by (auto simp add: list_all2_conv_all_nth)
    1.25  
    1.26 -lemma list_all2_refl:
    1.27 +lemma list_all2_refl [intro?]:
    1.28    "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
    1.29    by (simp add: list_all2_conv_all_nth)
    1.30  
    1.31 @@ -1168,7 +1169,7 @@
    1.32    apply (case_tac n, simp, simp)
    1.33    done
    1.34  
    1.35 -lemma list_all2_mono [intro?]:
    1.36 +lemma list_all2_mono [trans, intro?]:
    1.37    "\<And>y. list_all2 P x y \<Longrightarrow> (\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> list_all2 Q x y"
    1.38    apply (induct x, simp)
    1.39    apply (case_tac y, auto)