new theory of immutable arrays
authornipkow
Wed Nov 21 09:07:41 2012 +0100 (2012-11-21)
changeset 50138ca989d793b34
parent 50137 0226d408058b
child 50139 7eb626617bbe
new theory of immutable arrays
NEWS
src/HOL/Library/IArray.thy
src/HOL/ROOT
src/HOL/ex/IArray_Examples.thy
     1.1 --- a/NEWS	Tue Nov 20 22:53:59 2012 +0100
     1.2 +++ b/NEWS	Wed Nov 21 09:07:41 2012 +0100
     1.3 @@ -212,6 +212,8 @@
     1.4  from sorted associative lists. Merging two trees with rbt_union may
     1.5  return a structurally different tree than before. MINOR INCOMPATIBILITY.
     1.6  
     1.7 +* Library/IArray.thy: immutable arrays with code generation.
     1.8 +
     1.9  * Simproc "finite_Collect" rewrites set comprehensions into pointfree
    1.10  expressions.
    1.11  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/IArray.thy	Wed Nov 21 09:07:41 2012 +0100
     2.3 @@ -0,0 +1,53 @@
     2.4 +header "Immutable Arrays with Code Generation"
     2.5 +
     2.6 +theory IArray
     2.7 +imports "~~/src/HOL/Library/Efficient_Nat"
     2.8 +begin
     2.9 +
    2.10 +text{* Immutable arrays are lists wrapped up in an additional constructor.
    2.11 +There are no update operations. Hence code generation can safely implement
    2.12 +this type by efficient target language arrays.  Currently only SML is
    2.13 +provided. Should be extended to other target languages and more operations.
    2.14 +
    2.15 +Note that arrays cannot be printed directly but only by turning them into
    2.16 +lists first. Arrays could be converted back into lists for printing if they
    2.17 +were wrapped up in an additional constructor. *}
    2.18 +
    2.19 +datatype 'a iarray = IArray "'a list"
    2.20 +
    2.21 +fun of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
    2.22 +"of_fun f n = IArray (map f [0..<n])"
    2.23 +hide_const (open) of_fun
    2.24 +
    2.25 +fun length :: "'a iarray \<Rightarrow> nat" where
    2.26 +"length (IArray xs) = List.length xs"
    2.27 +hide_const (open) length
    2.28 +
    2.29 +fun sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
    2.30 +"(IArray as) !! n = as!n"
    2.31 +hide_const (open) sub
    2.32 +
    2.33 +fun list_of :: "'a iarray \<Rightarrow> 'a list" where
    2.34 +"list_of (IArray xs) = xs"
    2.35 +hide_const (open) list_of
    2.36 +
    2.37 +
    2.38 +subsection "Code Generation"
    2.39 +
    2.40 +code_type iarray
    2.41 +  (SML "_ Vector.vector")
    2.42 +
    2.43 +code_const IArray
    2.44 +  (SML "Vector.fromList")
    2.45 +code_const IArray.sub
    2.46 +  (SML "Vector.sub(_,_)")
    2.47 +code_const IArray.length
    2.48 +  (SML "Vector.length")
    2.49 +code_const IArray.of_fun
    2.50 +  (SML "!(fn f => fn n => Vector.tabulate(n,f))")
    2.51 +
    2.52 +lemma list_of_code[code]:
    2.53 +  "IArray.list_of A = map (%n. A!!n) [0..< IArray.length A]"
    2.54 +by (cases A) (simp add: map_nth)
    2.55 +
    2.56 +end
     3.1 --- a/src/HOL/ROOT	Tue Nov 20 22:53:59 2012 +0100
     3.2 +++ b/src/HOL/ROOT	Wed Nov 21 09:07:41 2012 +0100
     3.3 @@ -49,6 +49,7 @@
     3.4      (* Code_Prolog  FIXME cf. 76965c356d2a *)
     3.5      Code_Real_Approx_By_Float
     3.6      Code_Target_Numeral
     3.7 +    IArray
     3.8      Refute
     3.9    theories [condition = ISABELLE_FULL_TEST]
    3.10      Sum_of_Squares_Remote
    3.11 @@ -484,6 +485,7 @@
    3.12      FinFunPred
    3.13      Set_Comprehension_Pointfree_Tests
    3.14      Parallel_Example
    3.15 +    IArray_Examples
    3.16    theories SVC_Oracle
    3.17    theories [condition = SVC_HOME]
    3.18      svc_test
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ex/IArray_Examples.thy	Wed Nov 21 09:07:41 2012 +0100
     4.3 @@ -0,0 +1,26 @@
     4.4 +theory IArray_Examples
     4.5 +imports "~~/src/HOL/Library/IArray"
     4.6 +begin
     4.7 +
     4.8 +lemma "IArray [True,False] !! 1 = False"
     4.9 +by eval
    4.10 +
    4.11 +lemma "IArray.length (IArray [[],[]]) = 2"
    4.12 +by eval
    4.13 +
    4.14 +lemma "IArray.list_of (IArray [1,3::int]) = [1,3]"
    4.15 +by eval
    4.16 +
    4.17 +lemma "IArray.list_of (IArray.of_fun (%n. n*n) 5) = [0,1,4,9,16]"
    4.18 +by eval
    4.19 +
    4.20 +fun sum2 :: "'a::monoid_add iarray \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    4.21 +"sum2 A n s = (if n=0 then s else sum2 A (n - 1) (s + A!!(n - 1)))"
    4.22 +
    4.23 +definition sum :: "'a::monoid_add iarray \<Rightarrow> 'a" where
    4.24 +"sum A = sum2 A (IArray.length A) 0"
    4.25 +
    4.26 +lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45"
    4.27 +by eval
    4.28 +
    4.29 +end