src/HOL/ex/IArray_Examples.thy
 author hoelzl Thu Jan 31 11:31:27 2013 +0100 (2013-01-31) changeset 50999 3de230ed0547 parent 50138 ca989d793b34 child 51094 84b03c49c223 permissions -rw-r--r--
introduce order topology
 nipkow@50138 ` 1` ```theory IArray_Examples ``` nipkow@50138 ` 2` ```imports "~~/src/HOL/Library/IArray" ``` nipkow@50138 ` 3` ```begin ``` nipkow@50138 ` 4` nipkow@50138 ` 5` ```lemma "IArray [True,False] !! 1 = False" ``` nipkow@50138 ` 6` ```by eval ``` nipkow@50138 ` 7` nipkow@50138 ` 8` ```lemma "IArray.length (IArray [[],[]]) = 2" ``` nipkow@50138 ` 9` ```by eval ``` nipkow@50138 ` 10` nipkow@50138 ` 11` ```lemma "IArray.list_of (IArray [1,3::int]) = [1,3]" ``` nipkow@50138 ` 12` ```by eval ``` nipkow@50138 ` 13` nipkow@50138 ` 14` ```lemma "IArray.list_of (IArray.of_fun (%n. n*n) 5) = [0,1,4,9,16]" ``` nipkow@50138 ` 15` ```by eval ``` nipkow@50138 ` 16` nipkow@50138 ` 17` ```fun sum2 :: "'a::monoid_add iarray \ nat \ 'a \ 'a" where ``` nipkow@50138 ` 18` ```"sum2 A n s = (if n=0 then s else sum2 A (n - 1) (s + A!!(n - 1)))" ``` nipkow@50138 ` 19` nipkow@50138 ` 20` ```definition sum :: "'a::monoid_add iarray \ 'a" where ``` nipkow@50138 ` 21` ```"sum A = sum2 A (IArray.length A) 0" ``` nipkow@50138 ` 22` nipkow@50138 ` 23` ```lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45" ``` nipkow@50138 ` 24` ```by eval ``` nipkow@50138 ` 25` nipkow@50138 ` 26` ```end ```