--- a/src/HOL/Library/IArray.thy Thu May 29 22:46:21 2014 +0200
+++ b/src/HOL/Library/IArray.thy Fri May 30 08:23:07 2014 +0200
@@ -86,10 +86,14 @@
constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
-"sub' (as, n) = IArray.list_of as ! nat_of_integer n"
+[code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
hide_const (open) sub'
lemma [code]:
+ "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
+ by simp
+
+lemma [code]:
"as !! n = IArray.sub' (as, integer_of_nat n)"
by simp
@@ -97,10 +101,14 @@
constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
definition length' :: "'a iarray \<Rightarrow> integer" where
-[simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
+[code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
hide_const (open) length'
lemma [code]:
+ "IArray.length' (IArray as) = integer_of_nat (List.length as)"
+ by simp
+
+lemma [code]:
"IArray.length as = nat_of_integer (IArray.length' as)"
by simp