# HG changeset patch
# User haftmann
# Date 1360759132 -3600
# Node ID 84b03c49c2232cde27e3407fe9727e9a7f49e70d
# Parent  9d7aa2bb097b85ce6eb5abde1733c034d5cdfcf5
IArray ignorant of particular representation of nat

diff -r 9d7aa2bb097b -r 84b03c49c223 src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/Library/IArray.thy	Wed Feb 13 13:38:52 2013 +0100
@@ -1,7 +1,7 @@
 header "Immutable Arrays with Code Generation"
 
 theory IArray
-imports "~~/src/HOL/Library/Efficient_Nat"
+imports Main
 begin
 
 text{* Immutable arrays are lists wrapped up in an additional constructor.
@@ -15,39 +15,69 @@
 
 datatype 'a iarray = IArray "'a list"
 
-fun of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
-"of_fun f n = IArray (map f [0..<n])"
-hide_const (open) of_fun
-
-fun length :: "'a iarray \<Rightarrow> nat" where
-"length (IArray xs) = List.length xs"
-hide_const (open) length
-
-fun sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
-"(IArray as) !! n = as!n"
-hide_const (open) sub
-
-fun list_of :: "'a iarray \<Rightarrow> 'a list" where
+primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
 "list_of (IArray xs) = xs"
 hide_const (open) list_of
 
+definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
+[simp]: "of_fun f n = IArray (map f [0..<n])"
+hide_const (open) of_fun
+
+definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+[simp]: "as !! n = IArray.list_of as ! n"
+hide_const (open) sub
+
+definition length :: "'a iarray \<Rightarrow> nat" where
+[simp]: "length as = List.length (IArray.list_of as)"
+hide_const (open) length
+
+lemma list_of_code [code]:
+"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
+by (cases as) (simp add: map_nth)
+
 
 subsection "Code Generation"
 
+code_reserved SML Vector
+
 code_type iarray
   (SML "_ Vector.vector")
 
 code_const IArray
   (SML "Vector.fromList")
-code_const IArray.sub
-  (SML "Vector.sub(_,_)")
-code_const IArray.length
+
+primrec tabulate :: "code_numeral \<times> (code_numeral \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
+"tabulate (n, f) = IArray (map (f \<circ> Code_Numeral.of_nat) [0..<Code_Numeral.nat_of n])"
+hide_const (open) tabulate
+
+lemma [code]:
+"IArray.of_fun f n = IArray.tabulate (Code_Numeral.of_nat n, f \<circ> Code_Numeral.nat_of)"
+by simp 
+
+code_const IArray.tabulate
+  (SML "Vector.tabulate")
+
+primrec sub' :: "'a iarray \<times> code_numeral \<Rightarrow> 'a" where
+"sub' (as, n) = IArray.list_of as ! Code_Numeral.nat_of n"
+hide_const (open) sub'
+
+lemma [code]:
+"as !! n = IArray.sub' (as, Code_Numeral.of_nat n)"
+by simp
+
+code_const IArray.sub'
+  (SML "Vector.sub")
+
+definition length' :: "'a iarray \<Rightarrow> code_numeral" where
+[simp]: "length' as = Code_Numeral.of_nat (List.length (IArray.list_of as))"
+hide_const (open) length'
+
+lemma [code]:
+"IArray.length as = Code_Numeral.nat_of (IArray.length' as)"
+by simp
+
+code_const IArray.length'
   (SML "Vector.length")
-code_const IArray.of_fun
-  (SML "!(fn f => fn n => Vector.tabulate(n,f))")
-
-lemma list_of_code[code]:
-  "IArray.list_of A = map (%n. A!!n) [0..< IArray.length A]"
-by (cases A) (simp add: map_nth)
 
 end
+
diff -r 9d7aa2bb097b -r 84b03c49c223 src/HOL/ex/IArray_Examples.thy
--- a/src/HOL/ex/IArray_Examples.thy	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/ex/IArray_Examples.thy	Wed Feb 13 13:38:52 2013 +0100
@@ -1,5 +1,5 @@
 theory IArray_Examples
-imports "~~/src/HOL/Library/IArray"
+imports "~~/src/HOL/Library/IArray" "~~/src/HOL/Library/Efficient_Nat"
 begin
 
 lemma "IArray [True,False] !! 1 = False"
@@ -24,3 +24,4 @@
 by eval
 
 end
+