src/HOL/ex/IArray_Examples.thy
 changeset 50138 ca989d793b34 child 51094 84b03c49c223
equal 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`