# HG changeset patch
# User haftmann
# Date 1278341183 -7200
# Node ID 271ecd4fb9f9a3a460874fb960dbf20a452eb6ab
# Parent  3046ebbb43c097b638e94d195679ae6e067e7d16
moved "open" operations from Heap.thy to Array.thy and Ref.thy

diff -r 3046ebbb43c0 -r 271ecd4fb9f9 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 16:46:23 2010 +0200
@@ -8,24 +8,132 @@
 imports Heap_Monad
 begin
 
+subsection {* Primitive layer *}
+
+definition 
+  array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
+  "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
+
+definition
+  get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
+  "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
+
+definition
+  set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
+  "set_array a x = 
+  arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
+
+definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
+  "array xs h = (let
+     l = lim h;
+     r = Array l;
+     h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
+   in (r, h''))"
+
+definition length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
+  "length a h = List.length (get_array a h)"
+  
+definition change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
+  "change a i x h = set_array a ((get_array a h)[i:=x]) h"
+
+text {* Properties of imperative arrays *}
+
+text {* FIXME: Does there exist a "canonical" array axiomatisation in
+the literature?  *}
+
+definition noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70) where
+  "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
+
+lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
+  and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
+  unfolding noteq_arrs_def by auto
+
+lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False"
+  unfolding noteq_arrs_def by auto
+
+lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
+  by (simp add: array_present_def noteq_arrs_def array_def Let_def)
+
+lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
+  by (simp add: get_array_def set_array_def o_def)
+
+lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
+  by (simp add: noteq_arrs_def get_array_def set_array_def)
+
+lemma set_array_same [simp]:
+  "set_array r x (set_array r y h) = set_array r x h"
+  by (simp add: set_array_def)
+
+lemma array_set_set_swap:
+  "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
+  by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
+
+lemma get_array_change_eq [simp]:
+  "get_array a (change a i v h) = (get_array a h) [i := v]"
+  by (simp add: change_def)
+
+lemma nth_change_array_neq_array [simp]:
+  "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i"
+  by (simp add: change_def noteq_arrs_def)
+
+lemma get_arry_array_change_elem_neqIndex [simp]:
+  "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i"
+  by simp
+
+lemma length_change [simp]: 
+  "length a (change b i v h) = length a h"
+  by (simp add: change_def length_def set_array_def get_array_def)
+
+lemma change_swap_neqArray:
+  "a =!!= a' \<Longrightarrow> 
+  change a i v (change a' i' v' h) 
+  = change a' i' v' (change a i v h)"
+apply (unfold change_def)
+apply simp
+apply (subst array_set_set_swap, assumption)
+apply (subst array_get_set_neq)
+apply (erule noteq_arrs_sym)
+apply (simp)
+done
+
+lemma change_swap_neqIndex:
+  "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)"
+  by (auto simp add: change_def array_set_set_swap list_update_swap)
+
+lemma get_array_init_array_list:
+  "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
+  by (simp add: Let_def split_def array_def)
+
+lemma set_array:
+  "set_array (fst (array ls h))
+     new_ls (snd (array ls h))
+       = snd (array new_ls h)"
+  by (simp add: Let_def split_def array_def)
+
+lemma array_present_change [simp]: 
+  "array_present a (change b i v h) = array_present a h"
+  by (simp add: change_def array_present_def set_array_def get_array_def)
+
+
+
 subsection {* Primitives *}
 
 definition
   new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
-  [code del]: "new n x = Heap_Monad.heap (Heap.array (replicate n x))"
+  [code del]: "new n x = Heap_Monad.heap (Array.array (replicate n x))"
 
 definition
   of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
-  [code del]: "of_list xs = Heap_Monad.heap (Heap.array xs)"
+  [code del]: "of_list xs = Heap_Monad.heap (Array.array xs)"
 
 definition
-  length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
-  [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))"
+  len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
+  [code del]: "len arr = Heap_Monad.heap (\<lambda>h. (Array.length arr h, h))"
 
 definition
   nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap"
 where
-  [code del]: "nth a i = (do len \<leftarrow> length a;
+  [code del]: "nth a i = (do len \<leftarrow> len a;
                  (if i < len
                      then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
                      else raise ''array lookup: index out of range'')
@@ -34,9 +142,9 @@
 definition
   upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
 where
-  [code del]: "upd i x a = (do len \<leftarrow> length a;
+  [code del]: "upd i x a = (do len \<leftarrow> len a;
                       (if i < len
-                           then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
+                           then Heap_Monad.heap (\<lambda>h. (a, change a i x h))
                            else raise ''array update: index out of range'')
                    done)" 
 
@@ -73,7 +181,7 @@
   freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap"
 where
   "freeze a = (do
-     n \<leftarrow> length a;
+     n \<leftarrow> len a;
      mapM (nth a) [0..<n]
    done)"
 
@@ -81,12 +189,11 @@
    map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
 where
   "map f a = (do
-     n \<leftarrow> length a;
+     n \<leftarrow> len a;
      mapM (\<lambda>n. map_entry n f a) [0..<n];
      return a
    done)"
 
-hide_const (open) new map -- {* avoid clashed with some popular names *}
 
 
 subsection {* Properties *}
@@ -125,12 +232,12 @@
   "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
   by (simp add: make'_def o_def)
 
-definition length' where
-  [code del]: "length' a = Array.length a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
-hide_const (open) length'
+definition len' where
+  [code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
+hide_const (open) len'
 lemma [code]:
-  "Array.length a = Array.length' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
-  by (simp add: length'_def)
+  "Array.len a = Array.len' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
+  by (simp add: len'_def)
 
 definition nth' where
   [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
@@ -154,7 +261,7 @@
 code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
 code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)")
 code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
-code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
+code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
 code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
 code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
 
@@ -167,7 +274,7 @@
 code_const Array (OCaml "failwith/ \"bare Array\"")
 code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
 code_const Array.of_list' (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
-code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
+code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
 code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
 code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
 
@@ -180,8 +287,10 @@
 code_const Array (Haskell "error/ \"bare Array\"")
 code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
 code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
-code_const Array.length' (Haskell "Heap.lengthArray")
+code_const Array.len' (Haskell "Heap.lengthArray")
 code_const Array.nth' (Haskell "Heap.readArray")
 code_const Array.upd' (Haskell "Heap.writeArray")
 
+hide_const (open) new map -- {* avoid clashed with some popular names *}
+
 end
diff -r 3046ebbb43c0 -r 271ecd4fb9f9 src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 16:46:23 2010 +0200
@@ -37,7 +37,10 @@
 
 subsection {* A polymorphic heap with dynamic arrays and references *}
 
-subsubsection {* Type definitions *}
+text {*
+  References and arrays are developed in parallel,
+  but keeping them separate makes some later proofs simpler.
+*}
 
 types addr = nat -- "untyped heap references"
 types heap_rep = nat -- "representable values"
@@ -82,283 +85,4 @@
   #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})
 *}
 
-
-subsection {* Imperative references and arrays *}
-
-text {*
-  References and arrays are developed in parallel,
-  but keeping them separate makes some later proofs simpler.
-*}
-
-subsubsection {* Primitive operations *}
-
-definition
-  ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where
-  "ref_present r h \<longleftrightarrow> addr_of_ref r < lim h"
-
-definition 
-  array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
-  "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
-
-definition
-  get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> 'a" where
-  "get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))"
-
-definition
-  get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
-  "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
-
-definition
-  set_ref :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
-  "set_ref r x = 
-  refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))"
-
-definition
-  set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
-  "set_array a x = 
-  arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
-
-definition ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
-  "ref x h = (let
-     l = lim h;
-     r = Ref l;
-     h'' = set_ref r x (h\<lparr>lim := l + 1\<rparr>)
-   in (r, h''))"
-
-definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
-  "array xs h = (let
-     l = lim h;
-     r = Array l;
-     h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
-   in (r, h''))"
-  
-definition
-  upd :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
-  "upd a i x h = set_array a ((get_array a h)[i:=x]) h"
-
-definition
-  length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
-  "length a h = size (get_array a h)"
-
-
-subsubsection {* Reference equality *}
-
-text {* 
-  The following relations are useful for comparing arrays and references.
-*}
-
-definition
-  noteq_refs :: "('a\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70)
-where
-  "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
-
-definition
-  noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70)
-where
-  "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
-
-lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r"
-  and noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
-  and unequal_refs [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
-  and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
-unfolding noteq_refs_def noteq_arrs_def by auto
-
-lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
-  unfolding noteq_refs_def by auto
-
-lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
-  by (simp add: ref_present_def ref_def Let_def noteq_refs_def)
-
-lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
-  by (simp add: array_present_def noteq_arrs_def array_def Let_def)
-
-
-subsubsection {* Properties of heap containers *}
-
-text {* Properties of imperative arrays *}
-
-text {* FIXME: Does there exist a "canonical" array axiomatisation in
-the literature?  *}
-
-lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
-  by (simp add: get_array_def set_array_def o_def)
-
-lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
-  by (simp add: noteq_arrs_def get_array_def set_array_def)
-
-lemma set_array_same [simp]:
-  "set_array r x (set_array r y h) = set_array r x h"
-  by (simp add: set_array_def)
-
-lemma array_set_set_swap:
-  "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
-  by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
-
-lemma array_ref_set_set_swap:
-  "set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)"
-  by (simp add: Let_def expand_fun_eq set_array_def set_ref_def)
-
-lemma get_array_upd_eq [simp]:
-  "get_array a (upd a i v h) = (get_array a h) [i := v]"
-  by (simp add: upd_def)
-
-lemma nth_upd_array_neq_array [simp]:
-  "a =!!= b \<Longrightarrow> get_array a (upd b j v h) ! i = get_array a h ! i"
-  by (simp add: upd_def noteq_arrs_def)
-
-lemma get_arry_array_upd_elem_neqIndex [simp]:
-  "i \<noteq> j \<Longrightarrow> get_array a (upd a j v h) ! i = get_array a h ! i"
-  by simp
-
-lemma length_upd_eq [simp]: 
-  "length a (upd a i v h) = length a h" 
-  by (simp add: length_def upd_def)
-
-lemma length_upd_neq [simp]: 
-  "length a (upd b i v h) = length a h"
-  by (simp add: upd_def length_def set_array_def get_array_def)
-
-lemma upd_swap_neqArray:
-  "a =!!= a' \<Longrightarrow> 
-  upd a i v (upd a' i' v' h) 
-  = upd a' i' v' (upd a i v h)"
-apply (unfold upd_def)
-apply simp
-apply (subst array_set_set_swap, assumption)
-apply (subst array_get_set_neq)
-apply (erule noteq_arrs_sym)
-apply (simp)
-done
-
-lemma upd_swap_neqIndex:
-  "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> upd a i v (upd a i' v' h) = upd a i' v' (upd a i v h)"
-by (auto simp add: upd_def array_set_set_swap list_update_swap)
-
-lemma get_array_init_array_list:
-  "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
-  by (simp add: Let_def split_def array_def)
-
-lemma set_array:
-  "set_array (fst (array ls h))
-     new_ls (snd (array ls h))
-       = snd (array new_ls h)"
-  by (simp add: Let_def split_def array_def)
-
-lemma array_present_upd [simp]: 
-  "array_present a (upd b i v h) = array_present a h"
-  by (simp add: upd_def array_present_def set_array_def get_array_def)
-
-(*lemma array_of_list_replicate:
-  "array_of_list (replicate n x) = array n x"
-  by (simp add: expand_fun_eq array_of_list_def array_def)*)
-
-text {* Properties of imperative references *}
-
-lemma next_ref_fresh [simp]:
-  assumes "(r, h') = ref x h"
-  shows "\<not> ref_present r h"
-  using assms by (cases h) (auto simp add: ref_def ref_present_def Let_def)
-
-lemma next_ref_present [simp]:
-  assumes "(r, h') = ref x h"
-  shows "ref_present r h'"
-  using assms by (cases h) (auto simp add: ref_def set_ref_def ref_present_def Let_def)
-
-lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x"
-  by (simp add: get_ref_def set_ref_def)
-
-lemma ref_get_set_neq [simp]: "r =!= s \<Longrightarrow> get_ref r (set_ref s x h) = get_ref r h"
-  by (simp add: noteq_refs_def get_ref_def set_ref_def)
-
-(* FIXME: We need some infrastructure to infer that locally generated
-  new refs (by new_ref(_no_init), new_array(')) are distinct
-  from all existing refs.
-*)
-
-lemma ref_set_get: "set_ref r (get_ref r h) h = h"
-apply (simp add: set_ref_def get_ref_def)
-oops
-
-lemma set_ref_same[simp]:
-  "set_ref r x (set_ref r y h) = set_ref r x h"
-  by (simp add: set_ref_def)
-
-lemma ref_set_set_swap:
-  "r =!= r' \<Longrightarrow> set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)"
-  by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def)
-
-lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)"
-  by (simp add: ref_def set_ref_def Let_def)
-
-lemma ref_get_new [simp]:
-  "get_ref (fst (ref v h)) (snd (ref v' h)) = v'"
-  by (simp add: ref_def Let_def split_def)
-
-lemma ref_set_new [simp]:
-  "set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)"
-  by (simp add: ref_def Let_def split_def)
-
-lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow> 
-  get_ref r (snd (ref v h)) = get_ref r h"
-  by (simp add: get_ref_def set_ref_def ref_def Let_def noteq_refs_def)
-
-lemma lim_set_ref [simp]:
-  "lim (set_ref r v h) = lim h"
-  by (simp add: set_ref_def)
-
-lemma ref_present_new_ref [simp]: 
-  "ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))"
-  by (simp add: ref_present_def ref_def Let_def)
-
-lemma ref_present_set_ref [simp]:
-  "ref_present r (set_ref r' v h) = ref_present r h"
-  by (simp add: set_ref_def ref_present_def)
-
-lemma noteq_refsI: "\<lbrakk> ref_present r h; \<not>ref_present r' h \<rbrakk>  \<Longrightarrow> r =!= r'"
-  unfolding noteq_refs_def ref_present_def
-  by auto
-
-text {* Non-interaction between imperative array and imperative references *}
-
-lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h"
-  by (simp add: get_array_def set_ref_def)
-
-lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i"
-  by simp
-
-lemma get_ref_upd [simp]: "get_ref r (upd a i v h) = get_ref r h"
-  by (simp add: get_ref_def set_array_def upd_def)
-
-lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)"
-  by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def)
-
-text {*not actually true ???*}
-lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)"
-apply (case_tac a)
-apply (simp add: Let_def upd_def)
-apply auto
-oops
-
-lemma length_new_ref[simp]: 
-  "length a (snd (ref v h)) = length a h"
-  by (simp add: get_array_def set_ref_def length_def  ref_def Let_def)
-
-lemma get_array_new_ref [simp]: 
-  "get_array a (snd (ref v h)) = get_array a h"
-  by (simp add: ref_def set_ref_def get_array_def Let_def)
-
-lemma ref_present_upd [simp]: 
-  "ref_present r (upd a i v h) = ref_present r h"
-  by (simp add: upd_def ref_present_def set_array_def get_array_def)
-
-lemma array_present_set_ref [simp]:
-  "array_present a (set_ref r v h) = array_present a h"
-  by (simp add: array_present_def set_ref_def)
-
-lemma array_present_new_ref [simp]:
-  "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
-  by (simp add: array_present_def ref_def Let_def)
-
-hide_const (open) empty upd length array ref
-
 end
diff -r 3046ebbb43c0 -r 271ecd4fb9f9 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 05 16:46:23 2010 +0200
@@ -5,7 +5,7 @@
 header {* Monadic references *}
 
 theory Ref
-imports Heap_Monad
+imports Array
 begin
 
 text {*
@@ -14,11 +14,111 @@
   and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
 *}
 
+subsection {* Primitive layer *}
+
+definition
+  ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where
+  "ref_present r h \<longleftrightarrow> addr_of_ref r < lim h"
+
+definition
+  get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> 'a" where
+  "get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))"
+
+definition
+  set_ref :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
+  "set_ref r x = 
+  refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))"
+
+definition ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
+  "ref x h = (let
+     l = lim h;
+     r = Ref l;
+     h'' = set_ref r x (h\<lparr>lim := l + 1\<rparr>)
+   in (r, h''))"
+
+definition noteq_refs :: "('a\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70) where
+  "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
+
+lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r"
+  and unequal_refs [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
+  unfolding noteq_refs_def by auto
+
+lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
+  unfolding noteq_refs_def by auto
+
+lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
+  by (simp add: ref_present_def ref_def Let_def noteq_refs_def)
+
+lemma next_ref_fresh [simp]:
+  assumes "(r, h') = ref x h"
+  shows "\<not> ref_present r h"
+  using assms by (cases h) (auto simp add: ref_def ref_present_def Let_def)
+
+lemma next_ref_present [simp]:
+  assumes "(r, h') = ref x h"
+  shows "ref_present r h'"
+  using assms by (cases h) (auto simp add: ref_def set_ref_def ref_present_def Let_def)
+
+lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x"
+  by (simp add: get_ref_def set_ref_def)
+
+lemma ref_get_set_neq [simp]: "r =!= s \<Longrightarrow> get_ref r (set_ref s x h) = get_ref r h"
+  by (simp add: noteq_refs_def get_ref_def set_ref_def)
+
+(* FIXME: We need some infrastructure to infer that locally generated
+  new refs (by new_ref(_no_init), new_array(')) are distinct
+  from all existing refs.
+*)
+
+lemma ref_set_get: "set_ref r (get_ref r h) h = h"
+apply (simp add: set_ref_def get_ref_def)
+oops
+
+lemma set_ref_same[simp]:
+  "set_ref r x (set_ref r y h) = set_ref r x h"
+  by (simp add: set_ref_def)
+
+lemma ref_set_set_swap:
+  "r =!= r' \<Longrightarrow> set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)"
+  by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def)
+
+lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)"
+  by (simp add: ref_def set_ref_def Let_def)
+
+lemma ref_get_new [simp]:
+  "get_ref (fst (ref v h)) (snd (ref v' h)) = v'"
+  by (simp add: ref_def Let_def split_def)
+
+lemma ref_set_new [simp]:
+  "set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)"
+  by (simp add: ref_def Let_def split_def)
+
+lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow> 
+  get_ref r (snd (ref v h)) = get_ref r h"
+  by (simp add: get_ref_def set_ref_def ref_def Let_def noteq_refs_def)
+
+lemma lim_set_ref [simp]:
+  "lim (set_ref r v h) = lim h"
+  by (simp add: set_ref_def)
+
+lemma ref_present_new_ref [simp]: 
+  "ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))"
+  by (simp add: ref_present_def ref_def Let_def)
+
+lemma ref_present_set_ref [simp]:
+  "ref_present r (set_ref r' v h) = ref_present r h"
+  by (simp add: set_ref_def ref_present_def)
+
+lemma noteq_refsI: "\<lbrakk> ref_present r h; \<not>ref_present r' h \<rbrakk>  \<Longrightarrow> r =!= r'"
+  unfolding noteq_refs_def ref_present_def
+  by auto
+
+
 subsection {* Primitives *}
 
 definition
   new :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where
-  [code del]: "new v = Heap_Monad.heap (Heap.ref v)"
+  [code del]: "new v = Heap_Monad.heap (Ref.ref v)"
 
 definition
   lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
@@ -55,6 +155,48 @@
   by (auto simp add: change_def lookup_chain)
 
 
+text {* Non-interaction between imperative array and imperative references *}
+
+lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h"
+  by (simp add: get_array_def set_ref_def)
+
+lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i"
+  by simp
+
+lemma get_ref_upd [simp]: "get_ref r (Array.change a i v h) = get_ref r h"
+  by (simp add: get_ref_def set_array_def Array.change_def)
+
+lemma new_ref_upd: "fst (ref v (Array.change a i v' h)) = fst (ref v h)"
+  by (simp add: set_array_def get_array_def Let_def ref_new_set Array.change_def ref_def)
+
+lemma upd_set_ref_swap: "Array.change a i v (set_ref r v' h) = set_ref r v' (Array.change a i v h)"
+  by (simp add: set_ref_def Array.change_def get_array_def set_array_def)
+
+lemma length_new_ref[simp]: 
+  "length a (snd (ref v h)) = length a h"
+  by (simp add: get_array_def set_ref_def length_def  ref_def Let_def)
+
+lemma get_array_new_ref [simp]: 
+  "get_array a (snd (ref v h)) = get_array a h"
+  by (simp add: ref_def set_ref_def get_array_def Let_def)
+
+lemma ref_present_upd [simp]: 
+  "ref_present r (Array.change a i v h) = ref_present r h"
+  by (simp add: Array.change_def ref_present_def set_array_def get_array_def)
+
+lemma array_present_set_ref [simp]:
+  "array_present a (set_ref r v h) = array_present a h"
+  by (simp add: array_present_def set_ref_def)
+
+lemma array_present_new_ref [simp]:
+  "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
+  by (simp add: array_present_def ref_def Let_def)
+
+lemma array_ref_set_set_swap:
+  "set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)"
+  by (simp add: Let_def expand_fun_eq set_array_def set_ref_def)
+
+
 subsection {* Code generator setup *}
 
 subsubsection {* SML *}
diff -r 3046ebbb43c0 -r 271ecd4fb9f9 src/HOL/Imperative_HOL/Relational.thy
--- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 05 16:46:23 2010 +0200
@@ -91,10 +91,10 @@
 subsection {* Elimination rules for array commands *}
 
 lemma crel_length:
-  assumes "crel (length a) h h' r"
-  obtains "h = h'" "r = Heap.length a h'"
+  assumes "crel (len a) h h' r"
+  obtains "h = h'" "r = Array.length a h'"
   using assms
-  unfolding length_def
+  unfolding Array.len_def
   by (elim crel_heap) simp
 
 (* Strong version of the lemma for this operation is missing *) 
@@ -106,14 +106,14 @@
 
 lemma crel_nth[consumes 1]:
   assumes "crel (nth a i) h h' r"
-  obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
+  obtains "r = (get_array a h) ! i" "h = h'" "i < Array.length a h"
   using assms
   unfolding nth_def
   by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
 
 lemma crel_upd[consumes 1]:
   assumes "crel (upd i v a) h h' r"
-  obtains "r = a" "h' = Heap.upd a i v h"
+  obtains "r = a" "h' = Array.change a i v h"
   using assms
   unfolding upd_def
   by (elim crelE crel_if crel_return crel_raise
@@ -129,14 +129,14 @@
 
 lemma crel_map_entry:
   assumes "crel (Array.map_entry i f a) h h' r"
-  obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
+  obtains "r = a" "h' = Array.change a i (f (get_array a h ! i)) h"
   using assms
   unfolding Array.map_entry_def
   by (elim crelE crel_upd crel_nth) auto
 
 lemma crel_swap:
   assumes "crel (Array.swap i x a) h h' r"
-  obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
+  obtains "r = get_array a h ! i" "h' = Array.change a i x h"
   using assms
   unfolding Array.swap_def
   by (elim crelE crel_upd crel_nth crel_return) auto
@@ -160,25 +160,25 @@
 
 lemma crel_mapM_nth:
   assumes
-  "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' xs"
-  assumes "n \<le> Heap.length a h"
-  shows "h = h' \<and> xs = drop (Heap.length a h - n) (get_array a h)"
+  "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' xs"
+  assumes "n \<le> Array.length a h"
+  shows "h = h' \<and> xs = drop (Array.length a h - n) (get_array a h)"
 using assms
 proof (induct n arbitrary: xs h h')
   case 0 thus ?case
-    by (auto elim!: crel_return simp add: Heap.length_def)
+    by (auto elim!: crel_return simp add: Array.length_def)
 next
   case (Suc n)
-  from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
+  from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
     by (simp add: upt_conv_Cons')
   with Suc(2) obtain r where
-    crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
-    and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
+    crel_mapM: "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
+    and xs_def: "xs = get_array a h ! (Array.length a h - Suc n) # r"
     by (auto elim!: crelE crel_nth crel_return)
-  from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)" 
+  from Suc(3) have "Array.length a h - n = Suc (Array.length a h - Suc n)" 
     by arith
   with Suc.hyps[OF crel_mapM] xs_def show ?case
-    unfolding Heap.length_def
+    unfolding Array.length_def
     by (auto simp add: nth_drop')
 qed
 
@@ -186,17 +186,17 @@
   assumes "crel (Array.freeze a) h h' xs"
   obtains "h = h'" "xs = get_array a h"
 proof 
-  from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
+  from assms have "crel (mapM (Array.nth a) [0..<Array.length a h]) h h' xs"
     unfolding freeze_def
     by (auto elim: crelE crel_length)
-  hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
+  hence "crel (mapM (Array.nth a) [(Array.length a h - Array.length a h)..<Array.length a h]) h h' xs"
     by simp
   from crel_mapM_nth[OF this] show "h = h'" and "xs = get_array a h" by auto
 qed
 
 lemma crel_mapM_map_entry_remains:
-  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
-  assumes "i < Heap.length a h - n"
+  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+  assumes "i < Array.length a h - n"
   shows "get_array a h ! i = get_array a h' ! i"
 using assms
 proof (induct n arbitrary: h h' r)
@@ -205,23 +205,23 @@
     by (auto elim: crel_return)
 next
   case (Suc n)
-  let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
-  from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
+  let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
+  from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where
-    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
+    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
     by (auto simp add: elim!: crelE crel_map_entry crel_return)
-  have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
-  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
+  have length_remains: "Array.length a ?h1 = Array.length a h" by simp
+  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
     by simp
   from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
 qed
 
 lemma crel_mapM_map_entry_changes:
-  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
-  assumes "n \<le> Heap.length a h"  
-  assumes "i \<ge> Heap.length a h - n"
-  assumes "i < Heap.length a h"
+  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+  assumes "n \<le> Array.length a h"  
+  assumes "i \<ge> Array.length a h - n"
+  assumes "i < Array.length a h"
   shows "get_array a h' ! i = f (get_array a h ! i)"
 using assms
 proof (induct n arbitrary: h h' r)
@@ -230,54 +230,54 @@
     by (auto elim!: crel_return)
 next
   case (Suc n)
-  let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
-  from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
+  let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
+  from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where
-    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
+    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
     by (auto simp add: elim!: crelE crel_map_entry crel_return)
-  have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
-  from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
-  from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
-  from Suc(4) length_remains have cases: "i = Heap.length a ?h1 - Suc n \<or> i \<ge> Heap.length a ?h1 - n" by arith
-  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
+  have length_remains: "Array.length a ?h1 = Array.length a h" by simp
+  from Suc(3) have less: "Array.length a h - Suc n < Array.length a h - n" by arith
+  from Suc(3) have less2: "Array.length a h - Suc n < Array.length a h" by arith
+  from Suc(4) length_remains have cases: "i = Array.length a ?h1 - Suc n \<or> i \<ge> Array.length a ?h1 - n" by arith
+  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
     by simp
   from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
-    crel_mapM_map_entry_remains[OF this, of "Heap.length a h - Suc n", symmetric] less less2
+    crel_mapM_map_entry_remains[OF this, of "Array.length a h - Suc n", symmetric] less less2
   show ?case
-    by (auto simp add: nth_list_update_eq Heap.length_def)
+    by (auto simp add: nth_list_update_eq Array.length_def)
 qed
 
 lemma crel_mapM_map_entry_length:
-  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
-  assumes "n \<le> Heap.length a h"
-  shows "Heap.length a h' = Heap.length a h"
+  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+  assumes "n \<le> Array.length a h"
+  shows "Array.length a h' = Array.length a h"
 using assms
 proof (induct n arbitrary: h h' r)
   case 0
   thus ?case by (auto elim!: crel_return)
 next
   case (Suc n)
-  let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
-  from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
+  let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
+  from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where 
-    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
+    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
     by (auto elim!: crelE crel_map_entry crel_return)
-  have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
-  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
+  have length_remains: "Array.length a ?h1 = Array.length a h" by simp
+  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
     by simp
   from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
 qed
 
 lemma crel_mapM_map_entry:
-assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Heap.length a h]) h h' r"
+assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Array.length a h]) h h' r"
   shows "get_array a h' = List.map f (get_array a h)"
 proof -
-  from assms have "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - Heap.length a h..<Heap.length a h]) h h' r" by simp
+  from assms have "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - Array.length a h..<Array.length a h]) h h' r" by simp
   from crel_mapM_map_entry_length[OF this]
   crel_mapM_map_entry_changes[OF this] show ?thesis
-    unfolding Heap.length_def
+    unfolding Array.length_def
     by (auto intro: nth_equalityI)
 qed
 
@@ -322,7 +322,7 @@
   using assms
   unfolding Ref.new_def
   apply (elim crel_heap)
-  unfolding Heap.ref_def
+  unfolding Ref.ref_def
   apply (simp add: Let_def)
   unfolding ref_present_def
   apply auto
@@ -331,22 +331,22 @@
   done
 
 lemma crel_lookup:
-  assumes "crel (!ref) h h' r"
-  obtains "h = h'" "r = get_ref ref h"
+  assumes "crel (!r') h h' r"
+  obtains "h = h'" "r = get_ref r' h"
 using assms
 unfolding Ref.lookup_def
 by (auto elim: crel_heap)
 
 lemma crel_update:
-  assumes "crel (ref := v) h h' r"
-  obtains "h' = set_ref ref v h" "r = ()"
+  assumes "crel (r' := v) h h' r"
+  obtains "h' = set_ref r' v h" "r = ()"
 using assms
 unfolding Ref.update_def
 by (auto elim: crel_heap)
 
 lemma crel_change:
-  assumes "crel (Ref.change f ref) h h' r"
-  obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
+  assumes "crel (Ref.change f r') h h' r"
+  obtains "h' = set_ref r' (f (get_ref r' h)) h" "r = f (get_ref r' h)"
 using assms
 unfolding Ref.change_def Let_def
 by (auto elim!: crelE crel_lookup crel_update crel_return)
@@ -431,22 +431,22 @@
 subsection {* Introduction rules for array commands *}
 
 lemma crel_lengthI:
-  shows "crel (length a) h h (Heap.length a h)"
-  unfolding length_def
+  shows "crel (Array.len a) h h (Array.length a h)"
+  unfolding len_def
   by (rule crel_heapI') auto
 
 (* thm crel_newI for Array.new is missing *)
 
 lemma crel_nthI:
-  assumes "i < Heap.length a h"
+  assumes "i < Array.length a h"
   shows "crel (nth a i) h h ((get_array a h) ! i)"
   using assms
   unfolding nth_def
   by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
 
 lemma crel_updI:
-  assumes "i < Heap.length a h"
-  shows "crel (upd i v a) h (Heap.upd a i v h) a"
+  assumes "i < Array.length a h"
+  shows "crel (upd i v a) h (Array.change a i v h) a"
   using assms
   unfolding upd_def
   by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
@@ -467,15 +467,15 @@
 subsubsection {* Introduction rules for reference commands *}
 
 lemma crel_lookupI:
-  shows "crel (!ref) h h (get_ref ref h)"
+  shows "crel (!r) h h (get_ref r h)"
   unfolding lookup_def by (auto intro!: crel_heapI')
 
 lemma crel_updateI:
-  shows "crel (ref := v) h (set_ref ref v h) ()"
+  shows "crel (r := v) h (set_ref r v h) ()"
   unfolding update_def by (auto intro!: crel_heapI')
 
 lemma crel_changeI: 
-  shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
+  shows "crel (Ref.change f r) h (set_ref r (f (get_ref r h)) h) (f (get_ref r h))"
 unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
 
 subsubsection {* Introduction rules for the assert command *}
@@ -587,8 +587,8 @@
 subsection {* Introduction rules for array commands *}
 
 lemma noError_length:
-  shows "noError (Array.length a) h"
-  unfolding length_def
+  shows "noError (Array.len a) h"
+  unfolding len_def
   by (intro noError_heap)
 
 lemma noError_new:
@@ -596,14 +596,14 @@
 unfolding Array.new_def by (intro noError_heap)
 
 lemma noError_upd:
-  assumes "i < Heap.length a h"
+  assumes "i < Array.length a h"
   shows "noError (Array.upd i v a) h"
   using assms
   unfolding upd_def
   by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
 
 lemma noError_nth:
-assumes "i < Heap.length a h"
+assumes "i < Array.length a h"
   shows "noError (Array.nth a i) h"
   using assms
   unfolding nth_def
@@ -614,14 +614,14 @@
   unfolding of_list_def by (rule noError_heap)
 
 lemma noError_map_entry:
-  assumes "i < Heap.length a h"
+  assumes "i < Array.length a h"
   shows "noError (map_entry i f a) h"
   using assms
   unfolding map_entry_def
   by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
 
 lemma noError_swap:
-  assumes "i < Heap.length a h"
+  assumes "i < Array.length a h"
   shows "noError (swap i x a) h"
   using assms
   unfolding swap_def
@@ -644,23 +644,23 @@
   noError_nth crel_nthI elim: crel_length)
 
 lemma noError_mapM_map_entry:
-  assumes "n \<le> Heap.length a h"
-  shows "noError (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h"
+  assumes "n \<le> Array.length a h"
+  shows "noError (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
 using assms
 proof (induct n arbitrary: h)
   case 0
   thus ?case by (auto intro: noError_return)
 next
   case (Suc n)
-  from Suc.prems have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
+  from Suc.prems have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
     by (simp add: upt_conv_Cons')
-  with Suc.hyps[of "(Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h)"] Suc.prems show ?case
+  with Suc.hyps[of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case
     by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
 qed
 
 lemma noError_map:
   shows "noError (Array.map f a) h"
-using noError_mapM_map_entry[of "Heap.length a h" a h]
+using noError_mapM_map_entry[of "Array.length a h" a h]
 unfolding Array.map_def
 by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
 
@@ -671,15 +671,15 @@
 unfolding Ref.new_def by (intro noError_heap)
 
 lemma noError_lookup:
-  shows "noError (!ref) h"
+  shows "noError (!r) h"
   unfolding lookup_def by (intro noError_heap)
 
 lemma noError_update:
-  shows "noError (ref := v) h"
+  shows "noError (r := v) h"
   unfolding update_def by (intro noError_heap)
 
 lemma noError_change:
-  shows "noError (Ref.change f ref) h"
+  shows "noError (Ref.change f r) h"
   unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
 
 subsection {* Introduction rules for the assert command *}
diff -r 3046ebbb43c0 -r 271ecd4fb9f9 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Jul 05 16:46:23 2010 +0200
@@ -27,7 +27,7 @@
   = multiset_of (get_array a h)"
   using assms
   unfolding swap_def
-  by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
+  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
 
 function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
 where
@@ -101,7 +101,7 @@
 
 lemma part_length_remains:
   assumes "crel (part1 a l r p) h h' rs"
-  shows "Heap.length a h = Heap.length a h'"
+  shows "Array.length a h = Array.length a h'"
 using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
@@ -207,7 +207,7 @@
         by (elim crelE crel_nth crel_if crel_return) auto
       from swp False have "get_array a h1 ! r \<ge> p"
         unfolding swap_def
-        by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
+        by (auto simp add: Array.length_def elim!: crelE crel_nth crel_upd crel_return)
       with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
         by fastsimp
       have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
@@ -243,7 +243,7 @@
 
 lemma partition_length_remains:
   assumes "crel (partition a l r) h h' rs"
-  shows "Heap.length a h = Heap.length a h'"
+  shows "Array.length a h = Array.length a h'"
 proof -
   from assms part_length_remains show ?thesis
     unfolding partition.simps swap_def
@@ -287,14 +287,14 @@
          else middle)"
     unfolding partition.simps
     by (elim crelE crel_return crel_nth crel_if crel_upd) simp
-  from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
-    (Heap.upd a rs (get_array a h1 ! r) h1)"
+  from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
+    (Array.change a rs (get_array a h1 ! r) h1)"
     unfolding swap_def
     by (elim crelE crel_return crel_nth crel_upd) simp
-  from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
+  from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
     unfolding swap_def
     by (elim crelE crel_return crel_nth crel_upd) simp
-  from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
+  from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
     unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
   from `l < r` have "l \<le> r - 1" by simp 
   note middle_in_bounds = part_returns_index_in_bounds[OF part this]
@@ -304,7 +304,7 @@
   with swap
   have right_remains: "get_array a h ! r = get_array a h' ! rs"
     unfolding swap_def
-    by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
+    by (auto simp add: Array.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
   from part_partitions [OF part]
   show ?thesis
   proof (cases "get_array a h1 ! middle \<le> ?pivot")
@@ -314,12 +314,12 @@
       fix i
       assume i_is_left: "l \<le> i \<and> i < rs"
       with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
-      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+      have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
       from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
       with part_partitions[OF part] right_remains True
       have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
       with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
-        unfolding Heap.upd_def Heap.length_def by simp
+        unfolding Array.change_def Array.length_def by simp
     }
     moreover
     {
@@ -331,7 +331,7 @@
       proof
         assume i_is: "rs < i \<and> i \<le> r - 1"
         with swap_length_remains in_bounds middle_in_bounds rs_equals
-        have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+        have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
         from part_partitions[OF part] rs_equals right_remains i_is
         have "get_array a h' ! rs \<le> get_array a h1 ! i"
           by fastsimp
@@ -345,7 +345,7 @@
           by fastsimp
         with i_is True rs_equals right_remains h'_def
         show ?thesis using in_bounds
-          unfolding Heap.upd_def Heap.length_def
+          unfolding Array.change_def Array.length_def
           by auto
       qed
     }
@@ -357,11 +357,11 @@
       fix i
       assume i_is_left: "l \<le> i \<and> i < rs"
       with swap_length_remains in_bounds middle_in_bounds rs_equals
-      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+      have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
       from part_partitions[OF part] rs_equals right_remains i_is_left
       have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
       with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
-        unfolding Heap.upd_def by simp
+        unfolding Array.change_def by simp
     }
     moreover
     {
@@ -372,7 +372,7 @@
       proof
         assume i_is: "rs < i \<and> i \<le> r - 1"
         with swap_length_remains in_bounds middle_in_bounds rs_equals
-        have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+        have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
         from part_partitions[OF part] rs_equals right_remains i_is
         have "get_array a h' ! rs \<le> get_array a h1 ! i"
           by fastsimp
@@ -381,7 +381,7 @@
         assume i_is: "i = r"
         from i_is False rs_equals right_remains h'_def
         show ?thesis using in_bounds
-          unfolding Heap.upd_def Heap.length_def
+          unfolding Array.change_def Array.length_def
           by auto
       qed
     }
@@ -425,7 +425,7 @@
 
 lemma length_remains:
   assumes "crel (quicksort a l r) h h' rs"
-  shows "Heap.length a h = Heap.length a h'"
+  shows "Array.length a h = Array.length a h'"
 using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
@@ -482,7 +482,7 @@
  
 lemma quicksort_sorts:
   assumes "crel (quicksort a l r) h h' rs"
-  assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h" 
+  assumes l_r_length: "l < Array.length a h" "r < Array.length a h" 
   shows "sorted (subarray l (r + 1) a h')"
   using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
@@ -524,7 +524,7 @@
       from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
         length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
       have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
-        unfolding Heap.length_def subarray_def by (cases p, auto)
+        unfolding Array.length_def subarray_def by (cases p, auto)
       with left_subarray_remains part_conds1 pivot_unchanged
       have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
         by (simp, subst set_of_multiset_of[symmetric], simp)
@@ -535,7 +535,7 @@
       from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
         length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
       have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
-        unfolding Heap.length_def subarray_def by auto
+        unfolding Array.length_def subarray_def by auto
       with right_subarray_remains part_conds2 pivot_unchanged
       have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
         by (simp, subst set_of_multiset_of[symmetric], simp)
@@ -556,18 +556,18 @@
 
 
 lemma quicksort_is_sort:
-  assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
+  assumes crel: "crel (quicksort a 0 (Array.length a h - 1)) h h' rs"
   shows "get_array a h' = sort (get_array a h)"
 proof (cases "get_array a h = []")
   case True
   with quicksort_is_skip[OF crel] show ?thesis
-  unfolding Heap.length_def by simp
+  unfolding Array.length_def by simp
 next
   case False
   from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
-    unfolding Heap.length_def subarray_def by auto
+    unfolding Array.length_def subarray_def by auto
   with length_remains[OF crel] have "sorted (get_array a h')"
-    unfolding Heap.length_def by simp
+    unfolding Array.length_def by simp
   with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
 qed
 
@@ -576,7 +576,7 @@
 We will now show that exceptions do not occur. *}
 
 lemma noError_part1: 
-  assumes "l < Heap.length a h" "r < Heap.length a h"
+  assumes "l < Array.length a h" "r < Array.length a h"
   shows "noError (part1 a l r p) h"
   using assms
 proof (induct a l r p arbitrary: h rule: part1.induct)
@@ -587,7 +587,7 @@
 qed
 
 lemma noError_partition:
-  assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
+  assumes "l < r" "l < Array.length a h" "r < Array.length a h"
   shows "noError (partition a l r) h"
 using assms
 unfolding partition.simps swap_def
@@ -603,7 +603,7 @@
 done
 
 lemma noError_quicksort:
-  assumes "l < Heap.length a h" "r < Heap.length a h"
+  assumes "l < Array.length a h" "r < Array.length a h"
   shows "noError (quicksort a l r) h"
 using assms
 proof (induct a l r arbitrary: h rule: quicksort.induct)
@@ -628,7 +628,7 @@
 subsection {* Example *}
 
 definition "qsort a = do
-    k \<leftarrow> length a;
+    k \<leftarrow> len a;
     quicksort a 0 (k - 1);
     return a
   done"
diff -r 3046ebbb43c0 -r 271ecd4fb9f9 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 05 16:46:23 2010 +0200
@@ -37,7 +37,7 @@
       else get_array a h ! k)"
 using assms unfolding swap.simps
 by (elim crel_elim_all)
- (auto simp: Heap.length_def)
+ (auto simp: length_def)
 
 lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
   shows "get_array a h' ! k = (if k < i then get_array a h ! k
@@ -69,7 +69,7 @@
 
 lemma rev_length:
   assumes "crel (rev a i j) h h' r"
-  shows "Heap.length a h = Heap.length a h'"
+  shows "Array.length a h = Array.length a h'"
 using assms
 proof (induct a i j arbitrary: h h' rule: rev.induct)
   case (1 a i j h h'')
@@ -93,7 +93,7 @@
 qed
 
 lemma rev2_rev': assumes "crel (rev a i j) h h' u"
-  assumes "j < Heap.length a h"
+  assumes "j < Array.length a h"
   shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
 proof - 
   {
@@ -103,15 +103,15 @@
       by auto
   } 
   with assms(2) rev_length[OF assms(1)] show ?thesis
-  unfolding subarray_def Heap.length_def
+  unfolding subarray_def Array.length_def
   by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
 qed
 
 lemma rev2_rev: 
-  assumes "crel (rev a 0 (Heap.length a h - 1)) h h' u"
+  assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
   shows "get_array a h' = List.rev (get_array a h)"
   using rev2_rev'[OF assms] rev_length[OF assms] assms
-    by (cases "Heap.length a h = 0", auto simp add: Heap.length_def
+    by (cases "Array.length a h = 0", auto simp add: Array.length_def
       subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elim_all)
   (drule sym[of "List.length (get_array a h)"], simp)
 
diff -r 3046ebbb43c0 -r 271ecd4fb9f9 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 05 16:46:23 2010 +0200
@@ -123,25 +123,25 @@
   "array_ran a h = {e. Some e \<in> set (get_array a h)}"
     -- {*FIXME*}
 
-lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Heap.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
-unfolding array_ran_def Heap.length_def by simp
+lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Array.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
+unfolding array_ran_def Array.length_def by simp
 
 lemma array_ran_upd_array_Some:
-  assumes "cl \<in> array_ran a (Heap.upd a i (Some b) h)"
+  assumes "cl \<in> array_ran a (Array.change a i (Some b) h)"
   shows "cl \<in> array_ran a h \<or> cl = b"
 proof -
   have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
   with assms show ?thesis 
-    unfolding array_ran_def Heap.upd_def by fastsimp
+    unfolding array_ran_def Array.change_def by fastsimp
 qed
 
 lemma array_ran_upd_array_None:
-  assumes "cl \<in> array_ran a (Heap.upd a i None h)"
+  assumes "cl \<in> array_ran a (Array.change a i None h)"
   shows "cl \<in> array_ran a h"
 proof -
   have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
   with assms show ?thesis
-    unfolding array_ran_def Heap.upd_def by auto
+    unfolding array_ran_def Array.change_def by auto
 qed
 
 definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool"
@@ -152,7 +152,7 @@
 lemma correctArray_update:
   assumes "correctArray rcs a h"
   assumes "correctClause rcs c" "sorted c" "distinct c"
-  shows "correctArray rcs a (Heap.upd a i (Some c) h)"
+  shows "correctArray rcs a (Array.change a i (Some c) h)"
   using assms
   unfolding correctArray_def
   by (auto dest:array_ran_upd_array_Some)
@@ -471,7 +471,7 @@
     fix clj
     let ?rs = "merge (remove l cli) (remove (compl l) clj)"
     let ?rs' = "merge (remove (compl l) cli) (remove l clj)"
-    assume "h = h'" "Some clj = get_array a h' ! j" "j < Heap.length a h'"
+    assume "h = h'" "Some clj = get_array a h' ! j" "j < Array.length a h'"
     with correct_a have clj: "correctClause r clj" "sorted clj" "distinct clj"
       unfolding correctArray_def by (auto intro: array_ranI)
     with clj l_not_zero correct_cli
@@ -485,7 +485,7 @@
   }
   {
     fix v clj
-    assume "Some clj = get_array a h ! j" "j < Heap.length a h"
+    assume "Some clj = get_array a h ! j" "j < Array.length a h"
     with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj"
       unfolding correctArray_def by (auto intro: array_ranI)
     assume "crel (res_thm' l cli clj) h h' rs"
diff -r 3046ebbb43c0 -r 271ecd4fb9f9 src/HOL/Imperative_HOL/ex/Subarray.thy
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Mon Jul 05 16:46:23 2010 +0200
@@ -8,65 +8,64 @@
 imports Array Sublist
 begin
 
-definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
-where
+definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
   "subarray n m a h \<equiv> sublist' n m (get_array a h)"
 
-lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
-apply (simp add: subarray_def Heap.upd_def)
+lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
+apply (simp add: subarray_def Array.change_def)
 apply (simp add: sublist'_update1)
 done
 
-lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
-apply (simp add: subarray_def Heap.upd_def)
+lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
+apply (simp add: subarray_def Array.change_def)
 apply (subst sublist'_update2)
 apply fastsimp
 apply simp
 done
 
-lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h[i - n := v]"
-unfolding subarray_def Heap.upd_def
+lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h[i - n := v]"
+unfolding subarray_def Array.change_def
 by (simp add: sublist'_update3)
 
 lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
 by (simp add: subarray_def sublist'_Nil')
 
-lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
-by (simp add: subarray_def Heap.length_def sublist'_single)
+lemma subarray_single: "\<lbrakk> n < Array.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
+by (simp add: subarray_def length_def sublist'_single)
 
-lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
-by (simp add: subarray_def Heap.length_def length_sublist')
+lemma length_subarray: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
+by (simp add: subarray_def length_def length_sublist')
 
-lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
+lemma length_subarray_0: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
 by (simp add: length_subarray)
 
-lemma subarray_nth_array_Cons: "\<lbrakk> i < Heap.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
-unfolding Heap.length_def subarray_def
+lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
+unfolding Array.length_def subarray_def
 by (simp add: sublist'_front)
 
-lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Heap.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
-unfolding Heap.length_def subarray_def
+lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Array.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
+unfolding Array.length_def subarray_def
 by (simp add: sublist'_back)
 
 lemma subarray_append: "\<lbrakk> i < j; j < k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h"
 unfolding subarray_def
 by (simp add: sublist'_append)
 
-lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
-unfolding Heap.length_def subarray_def
+lemma subarray_all: "subarray 0 (Array.length a h) a h = get_array a h"
+unfolding Array.length_def subarray_def
 by (simp add: sublist'_all)
 
-lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Heap.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
-unfolding Heap.length_def subarray_def
+lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
+unfolding Array.length_def subarray_def
 by (simp add: nth_sublist')
 
-lemma subarray_eq_samelength_iff: "Heap.length a h = Heap.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
-unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
+lemma subarray_eq_samelength_iff: "Array.length a h = Array.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
+unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
 
-lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
-unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
+lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length a h \<longrightarrow> P (get_array a h ! k))"
+unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
 
-lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
-unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
+lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length a h \<longrightarrow> P (get_array a h ! k))"
+unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
 
 end
\ No newline at end of file