# HG changeset patch
# User haftmann
# Date 1174639249 -3600
# Node ID c78f1d924bfea2c9ba68cacd3e9776a9cd8bb102
# Parent  e2d378a97905d56d2115fe520de7dc5418d378af
two further properties about lists

diff -r e2d378a97905 -r c78f1d924bfe src/HOL/List.thy
--- 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