added lemma length_alloc
authorhaftmann
Thu Nov 04 17:27:37 2010 +0100 (2010-11-04)
changeset 403601a73b5b90a3c
parent 40359 84388bba911d
child 40361 c409827db57d
added lemma length_alloc
src/HOL/Imperative_HOL/Array.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Thu Nov 04 13:42:36 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Thu Nov 04 17:27:37 2010 +0100
     1.3 @@ -134,9 +134,13 @@
     1.4    by (auto simp add: update_def set_set_swap list_update_swap)
     1.5  
     1.6  lemma get_alloc:
     1.7 -  "get (snd (alloc ls' h)) (fst (alloc ls h)) = ls'"
     1.8 +  "get (snd (alloc xs h)) (fst (alloc ys h)) = xs"
     1.9    by (simp add: Let_def split_def alloc_def)
    1.10  
    1.11 +lemma length_alloc:
    1.12 +  "length (snd (alloc (xs :: 'a::heap list) h)) (fst (alloc (ys :: 'a list) h)) = List.length xs"
    1.13 +  by (simp add: Array.length_def get_alloc)
    1.14 +
    1.15  lemma set:
    1.16    "set (fst (alloc ls h))
    1.17       new_ls (snd (alloc ls h))