--- a/src/HOL/List.thy Fri Mar 23 09:40:47 2007 +0100
+++ b/src/HOL/List.thy Fri Mar 23 09:40:49 2007 +0100
@@ -2832,6 +2832,10 @@
"list_all P (rev xs) \<longleftrightarrow> list_all P xs"
by (simp add: list_all_iff)
+lemma list_all_length:
+ "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
+ unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
+
lemma list_ex_iff [normal post]:
"list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
by (induct xs) simp_all
@@ -2839,6 +2843,10 @@
lemmas list_bex_code [code unfold] =
list_ex_iff [symmetric, THEN eq_reflection]
+lemma list_ex_length:
+ "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
+ unfolding list_ex_iff set_conv_nth by auto
+
lemma itrev [simp]:
"itrev xs ys = rev xs @ ys"
by (induct xs arbitrary: ys) simp_all