# HG changeset patch
# User haftmann
# Date 1288888057 -3600
# Node ID 1a73b5b90a3cd380b643707fdba1158471c961cc
# Parent  84388bba911d20d30e22b13d2f4e644d7c43f8e2
added lemma length_alloc

diff -r 84388bba911d -r 1a73b5b90a3c src/HOL/Imperative_HOL/Array.thy
--- 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))