50138

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
