# HG changeset patch # User nipkow # Date 1384622817 -3600 # Node ID f43ae1afd08a11c957b12317421de059314e8864 # Parent 82ef58dba83b0d60d23762bb45fab94722fcbf2e added functions all and exists to IArray diff -r 82ef58dba83b -r f43ae1afd08a src/HOL/Library/IArray.thy --- a/src/HOL/Library/IArray.thy Fri Nov 15 22:02:05 2013 +0100 +++ b/src/HOL/Library/IArray.thy Sat Nov 16 18:26:57 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 82ef58dba83b -r f43ae1afd08a src/HOL/ex/IArray_Examples.thy --- a/src/HOL/ex/IArray_Examples.thy Fri Nov 15 22:02:05 2013 +0100 +++ b/src/HOL/ex/IArray_Examples.thy Sat Nov 16 18:26:57 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)))"