src/HOL/ex/IArray_Examples.thy
changeset 54459 f43ae1afd08a
parent 51143 0a2371e7ced3
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/ex/IArray_Examples.thy	Fri Nov 15 22:02:05 2013 +0100
     1.2 +++ b/src/HOL/ex/IArray_Examples.thy	Sat Nov 16 18:26:57 2013 +0100
     1.3 @@ -14,6 +14,12 @@
     1.4  lemma "IArray.list_of (IArray.of_fun (%n. n*n) 5) = [0,1,4,9,16]"
     1.5  by eval
     1.6  
     1.7 +lemma "\<not> IArray.all (\<lambda>x. x > 2) (IArray [1,3::int])"
     1.8 +by eval
     1.9 +
    1.10 +lemma "IArray.exists (\<lambda>x. x > 2) (IArray [1,3::int])"
    1.11 +by eval
    1.12 +
    1.13  fun sum2 :: "'a::monoid_add iarray \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.14  "sum2 A n s = (if n=0 then s else sum2 A (n - 1) (s + A!!(n - 1)))"
    1.15