src/HOL/ex/IArray_Examples.thy
author haftmann
Thu Mar 14 09:46:04 2019 +0100 (5 weeks ago)
changeset 69908 1bd74a0944b3
parent 66453 cc19f7ca2ed6
permissions -rw-r--r--
slightly more complete check of code generation for immutable arrays
     1 theory IArray_Examples
     2 imports "HOL-Library.IArray" "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 definition partial_geometric_sum :: "'a::comm_ring_1 list \<Rightarrow> 'a"
    33   where "partial_geometric_sum xs = (let
    34     values = IArray xs;
    35     coefficients = IArray.of_fun of_nat (length xs)
    36   in sum_list (map (\<lambda>i. values !! i * coefficients !! i) [0..<IArray.length values]))"
    37 
    38 export_code partial_geometric_sum checking SML OCaml? Haskell? Scala
    39 
    40 end
    41