move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
header "Immutable Arrays with Code Generation"
theory IArray
imports Main
begin
text{* Immutable arrays are lists wrapped up in an additional constructor.
There are no update operations. Hence code generation can safely implement
this type by efficient target language arrays. Currently only SML is
provided. Should be extended to other target languages and more operations.
Note that arrays cannot be printed directly but only by turning them into
lists first. Arrays could be converted back into lists for printing if they
were wrapped up in an additional constructor. *}
datatype 'a iarray = IArray "'a list"
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")
lemma [code]:
"size (as :: 'a iarray) = 0"
by (cases as) simp
lemma [code]:
"iarray_size f as = Suc (list_size f (IArray.list_of as))"
by (cases as) simp
lemma [code]:
"iarray_rec f as = f (IArray.list_of as)"
by (cases as) simp
lemma [code]:
"iarray_case f as = f (IArray.list_of as)"
by (cases as) simp
lemma [code]:
"HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
by (cases as, cases bs) (simp add: equal)
primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
"tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
hide_const (open) tabulate
lemma [code]:
"IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
by simp
code_const IArray.tabulate
(SML "Vector.tabulate")
primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
"sub' (as, n) = IArray.list_of as ! nat_of_integer n"
hide_const (open) sub'
lemma [code]:
"as !! n = IArray.sub' (as, integer_of_nat n)"
by simp
code_const IArray.sub'
(SML "Vector.sub")
definition length' :: "'a iarray \<Rightarrow> integer" where
[simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
hide_const (open) length'
lemma [code]:
"IArray.length as = nat_of_integer (IArray.length' as)"
by simp
code_const IArray.length'
(SML "Vector.length")
end