# HG changeset patch
# User nipkow
# Date 1384677013 -3600
# Node ID 949a612097fb2a87ce437ebc6a92bcb43f6681fb
# Parent  96ccc8972fc7b225d80e991d8f400d8e4007fcc4# Parent  f43ae1afd08a11c957b12317421de059314e8864
merged

diff -r 96ccc8972fc7 -r 949a612097fb src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Sat Nov 16 22:17:45 2013 +0100
+++ b/src/HOL/Library/IArray.thy	Sun Nov 17 09:30:13 2013 +0100
@@ -31,6 +31,14 @@
 [simp]: "length as = List.length (IArray.list_of as)"
 hide_const (open) length
 
+fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+"all p (IArray as) = (ALL a : set as. p a)"
+hide_const (open) all
+
+fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+"exists p (IArray as) = (EX a : set as. p a)"
+hide_const (open) exists
+
 lemma list_of_code [code]:
 "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
 by (cases as) (simp add: map_nth)
@@ -43,6 +51,8 @@
 code_printing
   type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
 | constant IArray \<rightharpoonup> (SML) "Vector.fromList"
+| constant IArray.all \<rightharpoonup> (SML) "Vector.all"
+| constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
 
 lemma [code]:
 "size (as :: 'a iarray) = 0"
diff -r 96ccc8972fc7 -r 949a612097fb src/HOL/ex/IArray_Examples.thy
--- a/src/HOL/ex/IArray_Examples.thy	Sat Nov 16 22:17:45 2013 +0100
+++ b/src/HOL/ex/IArray_Examples.thy	Sun Nov 17 09:30:13 2013 +0100
@@ -14,6 +14,12 @@
 lemma "IArray.list_of (IArray.of_fun (%n. n*n) 5) = [0,1,4,9,16]"
 by eval
 
+lemma "\<not> IArray.all (\<lambda>x. x > 2) (IArray [1,3::int])"
+by eval
+
+lemma "IArray.exists (\<lambda>x. x > 2) (IArray [1,3::int])"
+by eval
+
 fun sum2 :: "'a::monoid_add iarray \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
 "sum2 A n s = (if n=0 then s else sum2 A (n - 1) (s + A!!(n - 1)))"