added lemma length_alloc

--- a/src/HOL/Imperative_HOL/Array.thy	Thu Nov 04 13:42:36 2010 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy	Thu Nov 04 17:27:37 2010 +0100
@@ -134,9 +134,13 @@
   by (auto simp add: update_def set_set_swap list_update_swap)
 
 lemma get_alloc:
-  "get (snd (alloc ls' h)) (fst (alloc ls h)) = ls'"
+  "get (snd (alloc xs h)) (fst (alloc ys h)) = xs"
   by (simp add: Let_def split_def alloc_def)
 
+lemma length_alloc:
+  "length (snd (alloc (xs :: 'a::heap list) h)) (fst (alloc (ys :: 'a list) h)) = List.length xs"
+  by (simp add: Array.length_def get_alloc)
+
 lemma set:
   "set (fst (alloc ls h))
      new_ls (snd (alloc ls h))