src/HOL/ex/IArray_Examples.thy
author nipkow
Wed, 21 Nov 2012 09:07:41 +0100
changeset 50138 ca989d793b34
child 51094 84b03c49c223
permissions -rw-r--r--
new theory of immutable arrays
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50138
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     1
theory IArray_Examples
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     2
imports "~~/src/HOL/Library/IArray"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     3
begin
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     4
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     5
lemma "IArray [True,False] !! 1 = False"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     6
by eval
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     7
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     8
lemma "IArray.length (IArray [[],[]]) = 2"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     9
by eval
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    10
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    11
lemma "IArray.list_of (IArray [1,3::int]) = [1,3]"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    12
by eval
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    13
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    14
lemma "IArray.list_of (IArray.of_fun (%n. n*n) 5) = [0,1,4,9,16]"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    15
by eval
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    16
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    17
fun sum2 :: "'a::monoid_add iarray \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    18
"sum2 A n s = (if n=0 then s else sum2 A (n - 1) (s + A!!(n - 1)))"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    19
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    20
definition sum :: "'a::monoid_add iarray \<Rightarrow> 'a" where
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    21
"sum A = sum2 A (IArray.length A) 0"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    22
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    23
lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    24
by eval
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    25
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    26
end