1.1 --- a/src/HOL/List.thy	Thu Jun 17 10:02:29 2010 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Jun 18 14:14:29 2010 +0200
     1.3 @@ -3190,6 +3190,14 @@
     1.4  lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
     1.5  by auto
     1.6  
     1.7 +lemma Ball_set_replicate[simp]:
     1.8 +  "(ALL x : set(replicate n a). P x) = (P a | n=0)"
     1.9 +by(simp add: set_replicate_conv_if)
    1.10 +
    1.11 +lemma Bex_set_replicate[simp]:
    1.12 +  "(EX x : set(replicate n a). P x) = (P a & n\<noteq>0)"
    1.13 +by(simp add: set_replicate_conv_if)
    1.14 +
    1.15  lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
    1.16  by (simp add: set_replicate_conv_if split: split_if_asm)
    1.17  
    1.18 @@ -4706,7 +4714,11 @@
    1.19  
    1.20  lemma list_all_length:
    1.21    "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
    1.22 -  unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
    1.23 +unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
    1.24 +
    1.25 +lemma list_all_cong[fundef_cong]:
    1.26 +  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
    1.27 +by (simp add: list_all_iff)
    1.28  
    1.29  lemma list_ex_iff [code_post]:
    1.30    "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
    1.31 @@ -4717,7 +4729,11 @@
    1.32  
    1.33  lemma list_ex_length:
    1.34    "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
    1.35 -  unfolding list_ex_iff set_conv_nth by auto
    1.36 +unfolding list_ex_iff set_conv_nth by auto
    1.37 +
    1.38 +lemma list_ex_cong[fundef_cong]:
    1.39 +  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
    1.40 +by (simp add: list_ex_iff)
    1.41  
    1.42  lemma filtermap_conv:
    1.43     "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"