--- 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
+
--- 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
+