diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Library/IArray.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -46,6 +46,26 @@
 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