author | haftmann |
Wed, 13 Feb 2013 13:38:52 +0100 | |
changeset 51094 | 84b03c49c223 |
parent 50138 | ca989d793b34 |
child 51143 | 0a2371e7ced3 |
permissions | -rw-r--r-- |
50138 | 1 |
theory IArray_Examples |
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
2 |
imports "~~/src/HOL/Library/IArray" "~~/src/HOL/Library/Efficient_Nat" |
50138 | 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 |
|
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
27 |