src/HOL/ex/IArray_Examples.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 54459 f43ae1afd08a
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
bundle lifting_syntax;
nipkow@50138
     1
theory IArray_Examples
haftmann@51143
     2
imports "~~/src/HOL/Library/IArray" "~~/src/HOL/Library/Code_Target_Numeral"
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@54459
    17
lemma "\<not> IArray.all (\<lambda>x. x > 2) (IArray [1,3::int])"
nipkow@54459
    18
by eval
nipkow@54459
    19
nipkow@54459
    20
lemma "IArray.exists (\<lambda>x. x > 2) (IArray [1,3::int])"
nipkow@54459
    21
by eval
nipkow@54459
    22
nipkow@50138
    23
fun sum2 :: "'a::monoid_add iarray \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
nipkow@50138
    24
"sum2 A n s = (if n=0 then s else sum2 A (n - 1) (s + A!!(n - 1)))"
nipkow@50138
    25
nipkow@50138
    26
definition sum :: "'a::monoid_add iarray \<Rightarrow> 'a" where
nipkow@50138
    27
"sum A = sum2 A (IArray.length A) 0"
nipkow@50138
    28
nipkow@50138
    29
lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45"
nipkow@50138
    30
by eval
nipkow@50138
    31
nipkow@50138
    32
end
haftmann@51094
    33