src/HOL/ex/IArray_Examples.thy
 author wenzelm Mon Aug 31 21:28:08 2015 +0200 (2015-08-31) changeset 61070 b72a990adfe2 parent 54459 f43ae1afd08a child 66453 cc19f7ca2ed6 permissions -rw-r--r--
prefer symbols;
```     1 theory IArray_Examples
```
```     2 imports "~~/src/HOL/Library/IArray" "~~/src/HOL/Library/Code_Target_Numeral"
```
```     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 lemma "\<not> IArray.all (\<lambda>x. x > 2) (IArray [1,3::int])"
```
```    18 by eval
```
```    19
```
```    20 lemma "IArray.exists (\<lambda>x. x > 2) (IArray [1,3::int])"
```
```    21 by eval
```
```    22
```
```    23 fun sum2 :: "'a::monoid_add iarray \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
```
```    24 "sum2 A n s = (if n=0 then s else sum2 A (n - 1) (s + A!!(n - 1)))"
```
```    25
```
```    26 definition sum :: "'a::monoid_add iarray \<Rightarrow> 'a" where
```
```    27 "sum A = sum2 A (IArray.length A) 0"
```
```    28
```
```    29 lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45"
```
```    30 by eval
```
```    31
```
```    32 end
```
```    33
```