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
|