src/HOL/ex/IArray_Examples.thy
changeset 50138 ca989d793b34
child 51094 84b03c49c223
equal deleted inserted replaced
50137:0226d408058b 50138:ca989d793b34
       
     1 theory IArray_Examples
       
     2 imports "~~/src/HOL/Library/IArray"
       
     3 begin
       
     4 
       
     5 lemma "IArray [True,False] !! 1 = False"
       
     6 by eval
       
     7 
       
     8 lemma "IArray.length (IArray [[],[]]) = 2"
       
     9 by eval
       
    10 
       
    11 lemma "IArray.list_of (IArray [1,3::int]) = [1,3]"
       
    12 by eval
       
    13 
       
    14 lemma "IArray.list_of (IArray.of_fun (%n. n*n) 5) = [0,1,4,9,16]"
       
    15 by eval
       
    16 
       
    17 fun sum2 :: "'a::monoid_add iarray \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
       
    18 "sum2 A n s = (if n=0 then s else sum2 A (n - 1) (s + A!!(n - 1)))"
       
    19 
       
    20 definition sum :: "'a::monoid_add iarray \<Rightarrow> 'a" where
       
    21 "sum A = sum2 A (IArray.length A) 0"
       
    22 
       
    23 lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45"
       
    24 by eval
       
    25 
       
    26 end