# 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 \ bool) \ 'a iarray \ bool" where +"all p (IArray as) = (ALL a : set as. p a)" +hide_const (open) all + +fun exists :: "('a \ bool) \ 'a iarray \ 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 (\n. as !! n) [0 ..< IArray.length as]" by (cases as) (simp add: map_nth) @@ -43,6 +51,8 @@ code_printing type_constructor iarray \ (SML) "_ Vector.vector" | constant IArray \ (SML) "Vector.fromList" +| constant IArray.all \ (SML) "Vector.all" +| constant IArray.exists \ (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 "\ IArray.all (\x. x > 2) (IArray [1,3::int])" +by eval + +lemma "IArray.exists (\x. x > 2) (IArray [1,3::int])" +by eval + fun sum2 :: "'a::monoid_add iarray \ nat \ 'a \ 'a" where "sum2 A n s = (if n=0 then s else sum2 A (n - 1) (s + A!!(n - 1)))"